diff --git a/Nevanlinna/mathlibAddOn.lean b/Nevanlinna/mathlibAddOn.lean
index d039589..f25169c 100644
--- a/Nevanlinna/mathlibAddOn.lean
+++ b/Nevanlinna/mathlibAddOn.lean
@@ -74,3 +74,23 @@ lemma WithTopCoe
       exact Int.ofNat_eq_zero.mp this
     rw [this]
     rfl
+
+
+
+
+lemma rwx
+  {a b : WithTop ℤ}
+  (ha : a ≠ ⊤)
+  (hb : b ≠ ⊤) :
+  a + b ≠ ⊤ := by
+  simp; tauto
+
+lemma untop_add
+  {a b : WithTop ℤ}
+  (ha : a ≠ ⊤)
+  (hb : b ≠ ⊤) :
+  (a + b).untop (rwx ha hb) = a.untop ha + (b.untop hb) := by
+  rw [WithTop.untop_eq_iff]
+  rw [WithTop.coe_add]
+  rw [WithTop.coe_untop]
+  rw [WithTop.coe_untop]
diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean
index bc4be60..6bbf2a7 100644
--- a/Nevanlinna/meromorphicOn_divisor.lean
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@@ -102,6 +102,29 @@ theorem MeromorphicOn.divisor_def₂
   exact Eq.symm (WithTop.coe_untop (hf z hz).order h₂f)
 
 
+theorem MeromorphicOn.divisor_mul₀
+  {f₁ f₂ : ℂ → ℂ}
+  {U : Set ℂ}
+  {z : ℂ}
+  (hz : z ∈ U)
+  (h₁f₁ : MeromorphicOn f₁ U)
+  (h₂f₁ : (h₁f₁ z hz).order ≠ ⊤)
+  (h₁f₂ : MeromorphicOn f₂ U)
+  (h₂f₂ : (h₁f₂ z hz).order ≠ ⊤) :
+  (h₁f₁.mul h₁f₂).divisor.toFun z = h₁f₁.divisor.toFun z + h₁f₂.divisor.toFun z := by
+  by_cases h₁z : z ∈ U
+  · rw [MeromorphicOn.divisor_def₂ h₁f₁ hz h₂f₁]
+    rw [MeromorphicOn.divisor_def₂ h₁f₂ hz h₂f₂]
+    have B : ((h₁f₁.mul h₁f₂) z hz).order ≠ ⊤ := by
+      rw [MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)]
+      simp; tauto
+    rw [MeromorphicOn.divisor_def₂ (h₁f₁.mul h₁f₂) hz B]
+    simp_rw [MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)]
+    rw [untop_add]
+  · unfold MeromorphicOn.divisor
+    simp [h₁z]
+
+
 theorem MeromorphicOn.divisor_mul
   {f₁ f₂ : ℂ → ℂ}
   {U : Set ℂ}
@@ -111,12 +134,11 @@ theorem MeromorphicOn.divisor_mul
   (h₂f₂ : ∀ z, (hz : z ∈ U) → (h₁f₂ z hz).order ≠ ⊤) :
   (h₁f₁.mul h₁f₂).divisor.toFun = h₁f₁.divisor.toFun + h₁f₂.divisor.toFun := by
   funext z
-
   by_cases hz : z ∈ U
-  · simp [hz]
-    rw [MeromorphicOn.divisor_def₂ h₁f₁ hz (h₂f₁ z hz)]
-    rw [MeromorphicOn.divisor_def₂ h₁f₂ hz (h₂f₂ z hz)]
-    let A := MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)
-    sorry
-  · unfold MeromorphicOn.divisor
-    simp [hz]
+  · rw [MeromorphicOn.divisor_mul₀ hz h₁f₁ (h₂f₁ z hz) h₁f₂ (h₂f₂ z hz)]
+    simp
+  · simp
+    rw [Function.nmem_support.mp (fun a => hz (h₁f₁.divisor.supportInU a))]
+    rw [Function.nmem_support.mp (fun a => hz (h₁f₂.divisor.supportInU a))]
+    rw [Function.nmem_support.mp (fun a => hz ((h₁f₁.mul h₁f₂).divisor.supportInU a))]
+    simp