diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index c72691a..eb05efd 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@@ -367,26 +367,25 @@ theorem MeromorphicOn.decompose₃'
   have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U
 
   let d := - h₁f.meromorphicOn.divisor.toFun
+  have h₁d : d.support = (Function.support h₁f.meromorphicOn.divisor) := by
+    ext x
+    unfold d
+    simp
   let h₁ := ∏ᶠ u, fun z ↦ (z - u) ^ (d u)
   have h₁h₁ : StronglyMeromorphicOn h₁ U := by
     intro z hz
     exact stronglyMeromorphicOn_ratlPolynomial₃ d z trivial
+  have h₂h₁ : h₁h₁.meromorphicOn.divisor = d := by
+    sorry
+  have h₃h₁ : ∀ (z : ℂ) (hz : z ∈ U), (h₁h₁ z hz).meromorphicAt.order ≠ ⊤ := by
+    sorry
   let g' := f * h₁
   have h₁g' : MeromorphicOn g' U := h₁f.meromorphicOn.mul h₁h₁.meromorphicOn
   have h₂g' : h₁g'.divisor.toFun = 0 := by
-    rw [MeromorphicOn.divisor_mul h₁f.meromorphicOn (fun z hz ↦ h₃f ⟨z, hz⟩) h₁h₁.meromorphicOn _]
-    unfold MeromorphicOn.divisor
+    rw [MeromorphicOn.divisor_mul h₁f.meromorphicOn (fun z hz ↦ h₃f ⟨z, hz⟩) h₁h₁.meromorphicOn h₃h₁]
+    rw [h₂h₁]
+    unfold d
     simp
-    funext z
-    by_cases hz : z ∈ U
-    · simp [hz]
-      have : (Function.support d).Finite := by
-        sorry
-      rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d this]
-      simp
-      sorry
-    · simp [hz]
-    sorry
 
   let g := h₁g'.makeStronglyMeromorphicOn
   have h₁g : StronglyMeromorphicOn g U := by