Update stronglyMeromorphicOn_eliminate.lean

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -537,15 +537,53 @@ theorem MeromorphicOn.decompose_log
     congr
     ext u
     rw [log_zpow]
+    --
     intro x hx
     simp at hx
-    simp
+    have h₁x : x ∈ U := by
+      exact h₁f.meromorphicOn.divisor.supportInU hx
+
     apply zpow_ne_zero
     simp
+
+    by_contra hCon
+    rw [← hCon] at hx
+    unfold MeromorphicOn.divisor at hx
+    rw [hCon] at hz
     simp at hz
-    contrapose
+    let A := (h₁f x h₁x).order_eq_zero_iff
+    let B := A.2 hz
+    simp [B] at hx
+    obtain ⟨a, b⟩ := hx
+    let c := b.1
+    simp_rw [hCon] at c
+    tauto
+    --
+    simp at hz
+    by_contra hCon
+    simp at hCon
+    rw [h₄g] at hz
+    simp at hz
+    tauto
+    --
+    rw [Finset.prod_ne_zero_iff]
+    intro x hx
+    simp at hx
+    have h₁x : x ∈ U := by
+      exact h₁f.meromorphicOn.divisor.supportInU hx
+
+    apply zpow_ne_zero
     simp
 
-
+    by_contra hCon
-    repeat
+    rw [← hCon] at hx
-      sorry
+    unfold MeromorphicOn.divisor at hx
+    rw [hCon] at hz
+    simp at hz
+    let A := (h₁f x h₁x).order_eq_zero_iff
+    let B := A.2 hz
+    simp [B] at hx
+    obtain ⟨a, b⟩ := hx
+    let c := b.1
+    simp_rw [hCon] at c
+    tauto