From e80aebfe3853df121dfe7e6c99bcb218c74254f0 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 13 Dec 2024 16:24:24 +0100
Subject: [PATCH] Update stronglyMeromorphicOn_eliminate.lean

---
 .../stronglyMeromorphicOn_eliminate.lean      | 48 +++++++++++++++++--
 1 file changed, 43 insertions(+), 5 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index c45bbcb..cb895e3 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/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
 
-
-    repeat
-      sorry
+    by_contra hCon
+    rw [← hCon] at hx
+    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