diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index a3248df..40194f9 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@@ -337,9 +337,32 @@ theorem MeromorphicOn.decompose₃
 
   obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := MeromorphicOn.decompose₂ h₁f (P := P) hP
   let h := ∏ p ∈ P, fun z => (z - p.1) ^ h₁f.meromorphicOn.divisor p.1
-  have h₁h : MeromorphicOn h U := by
-    sorry
   have h₂h : StronglyMeromorphicOn h U := by
+    -- WARNING: This is a general lemma we should add!
+    intro u hu
+    right
+    by_cases h₁u : ⟨u, hu⟩ ∈ P
+    · sorry
+    · use 0
+      use h
+      simp only [zpow_zero, smul_eq_mul, one_mul, eventually_true, and_true]
+      constructor
+      ·
+        sorry
+      · unfold h
+        simp only [Finset.prod_apply]
+        rw [Finset.prod_ne_zero_iff]
+        intro p hp
+        apply zpow_ne_zero
+        rw [sub_ne_zero]
+        by_contra hCon
+        have : ⟨u, hu⟩ = p := by
+          exact SetCoe.ext hCon
+        rw [← this] at hp
+        tauto
+
+
+  have h₁h : MeromorphicOn h U := by
     sorry
   have h₃h : h₁h.divisor = h₁f.meromorphicOn.divisor := by
     sorry