Working.

Nevanlinna/mathlibAddOn.lean

@@ -75,9 +75,6 @@ lemma WithTopCoe
     rw [this]
     rfl
 
-
-
-
 lemma rwx
   {a b : WithTop ℤ}
   (ha : a ≠ ⊤)
@@ -94,3 +91,12 @@ lemma untop_add
   rw [WithTop.coe_add]
   rw [WithTop.coe_untop]
   rw [WithTop.coe_untop]
+
+lemma untop'_of_ne_top
+  {a : WithTop ℤ}
+  {d : ℤ}
+  (ha : a ≠ ⊤) :
+  WithTop.untop' d a = a := by
+  obtain ⟨b, hb⟩ := WithTop.ne_top_iff_exists.1 ha
+  rw [← hb]
+  simp

Nevanlinna/stronglyMeromorphicOn.lean

@@ -102,3 +102,14 @@ theorem stronglyMeromorphicOn_of_makeStronglyMeromorphicOn
   let A := makeStronglyMeromorphicOn_changeDiscrete' hf hz
   rw [stronglyMeromorphicAt_congr A]
   exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z hz)
+
+
+theorem makeStronglyMeromorphicOn_changeOrder
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicOn f U)
+  (hz₀ : z₀ ∈ U) :
+  (stronglyMeromorphicOn_of_makeStronglyMeromorphicOn hf z₀ hz₀).meromorphicAt.order = (hf z₀ hz₀).order := by
+  apply MeromorphicAt.order_congr
+  exact makeStronglyMeromorphicOn_changeDiscrete hf hz₀

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -383,6 +383,10 @@ theorem MeromorphicOn.decompose₃'
   have h₃h₁ : ∀ (z : ℂ) (hz : z ∈ U), (h₁h₁ z hz).meromorphicAt.order ≠ ⊤ := by
     intro z hz
     apply stronglyMeromorphicOn_ratlPolynomial₃order
+  have h₄h₁ : ∀ (z : ℂ) (hz : z ∈ U), (h₁h₁ z hz).meromorphicAt.order = d z := by
+    intro z hz
+    rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁]
+    rwa [h₁d]
 
   let g' := f * h₁
   have h₁g' : MeromorphicOn g' U := h₁f.meromorphicOn.mul h₁h₁.meromorphicOn
@@ -391,6 +395,23 @@ theorem MeromorphicOn.decompose₃'
     rw [h₂h₁]
     unfold d
     simp
+  have h₃g' : ∀ u : U, (h₁g' u.1 u.2).order = 0 := by
+    intro u
+    rw [(h₁f u.1 u.2).meromorphicAt.order_mul (h₁h₁ u.1 u.2).meromorphicAt]
+    rw [h₄h₁]
+    unfold d
+    unfold MeromorphicOn.divisor
+    simp
+    have : (h₁f u.1 u.2).meromorphicAt.order = WithTop.untop' 0 (h₁f u.1 u.2).meromorphicAt.order := by
+      rw [eq_comm]
+      let A := h₃f u
+      exact untop'_of_ne_top A
+    rw [this]
+    simp
+    rw [← WithTop.LinearOrderedAddCommGroup.coe_neg]
+    rw [← WithTop.coe_add]
+    simp
+    exact u.2
 
   let g := h₁g'.makeStronglyMeromorphicOn
   have h₁g : StronglyMeromorphicOn g U := stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁g'
@@ -405,8 +426,10 @@ theorem MeromorphicOn.decompose₃'
   have h₄g : ∀ u : U, g u ≠ 0 := by
     intro u
     rw [← (h₁g u.1 u.2).order_eq_zero_iff]
-
-    sorry
+    rw [makeStronglyMeromorphicOn_changeOrder]
+    let A := h₃g' u
+    exact A
+    exact u.2
 
   use g
   constructor