diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index a67a66d..33fef88 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@@ -304,11 +304,8 @@ theorem MeromorphicOn.decompose₃
     ∧ (∀ u : U, g u ≠ 0)
     ∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by
 
-  have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
-    apply MeromorphicOn.order_ne_top h₂U h₁f h₂f
-
-  have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
-    exact h₁f.meromorphicOn.divisor.finiteSupport h₁U
+  have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := MeromorphicOn.order_ne_top h₂U h₁f h₂f
+  have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U
 
   let P' : Set U := Subtype.val ⁻¹' Function.support h₁f.meromorphicOn.divisor
   let P := (h₄f.preimage Set.injOn_subtype_val : Set.Finite P').toFinset