From 9ebb1c5215a8594fd87656e3c9c256da2ae10e4b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 14 Nov 2024 15:32:19 +0100
Subject: [PATCH] Update stronglyMeromorphicAt.lean

---
 Nevanlinna/stronglyMeromorphicAt.lean | 44 +++++++++++++++++++++++++--
 1 file changed, 41 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean
index 2b644d5..7c82a9d 100644
--- a/Nevanlinna/stronglyMeromorphicAt.lean
+++ b/Nevanlinna/stronglyMeromorphicAt.lean
@@ -399,6 +399,44 @@ theorem StronglyMeromorphicAt.decompose
     · rw [h₂g]
     · exact h₁g
   · constructor
-    · exact (order_eq_zero_iff h₁g).mp h₂g
-    ·
-      sorry
+    · rwa [← h₁g.order_eq_zero_iff]
+    · funext z
+      by_cases hz : z = z₀
+      · by_cases hOrd : h₁f.meromorphicAt.order.untop h₂f = 0
+        · simp [hOrd]
+          have : StronglyMeromorphicAt g₁ z₀ := by
+            unfold g₁
+            simp [hOrd]
+            have : (fun z => 1) * f = f := by
+              funext z
+              simp
+            rwa [this]
+          rw [hz]
+          unfold g
+          let A := makeStronglyMeromorphic_id this
+          rw [← A]
+          unfold g₁
+          rw [hOrd]
+          simp
+        · have : h₁f.meromorphicAt.order ≠ 0 := by
+            by_contra hC
+            simp_rw [hC] at hOrd
+            tauto
+          let A := h₁f.order_eq_zero_iff.not.1 this
+          simp at A
+          rw [hz, A]
+          simp
+          left
+          rw [zpow_eq_zero_iff]
+          assumption
+      · simp
+        have : g z = g₁ z := by
+          exact Eq.symm (m₁ h₁g₁ z hz)
+        rw [this]
+        unfold g₁
+        simp [hz]
+        rw [← mul_assoc]
+        rw [mul_inv_cancel₀]
+        simp
+        apply zpow_ne_zero
+        exact sub_ne_zero_of_ne hz