From 4145a9ebc98ff638d06a1ee7c7e941f102704afb Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 8 Nov 2024 12:00:37 +0100
Subject: [PATCH] Update meromorphicOn_decompose.lean

---
 Nevanlinna/meromorphicOn_decompose.lean | 33 +++++++++++++++++++------
 1 file changed, 26 insertions(+), 7 deletions(-)

diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index 7df34e3..b0bba43 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -9,6 +9,20 @@ import Nevanlinna.stronglyMeromorphicOn
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
+lemma WithTopCoe
+  {n : WithTop ℕ} :
+  WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
+  rcases n with h|h
+  · intro h
+    contradiction
+  · intro h₁
+    simp only [WithTop.map, Option.map] at h₁
+    have : (h : ℤ) = 0 := by
+      exact WithTop.coe_eq_zero.mp h₁
+    have : h = 0 := by
+      exact Int.ofNat_eq_zero.mp this
+    rw [this]
+    rfl
 
 theorem MeromorphicOn.decompose
   {f : ℂ → ℂ}
@@ -41,13 +55,18 @@ theorem MeromorphicOn.decompose
       have A := (h₄g z hz).meromorphicAt_order
       rw [h₂g ⟨z, hz⟩] at A
 
-      have t₀ : (0 : WithTop ℤ) = WithTop.map Nat.cast (0 : WithTop ℕ) := by
-        sorry
-      --rw [← this] at A
-
-      rw [WithTop.map_coe] at A
-
-      sorry
+      have t₀ : (h₄g z hz).order ≠ ⊤ := by
+        by_contra hC
+        rw [hC] at A
+        tauto
+      have t₁ : ∃ n : ℕ, (h₄g z hz).order = n := by
+        exact Option.ne_none_iff_exists'.mp t₀
+      obtain ⟨n, hn⟩ := t₁
+      rw [hn] at A
+      apply WithTopCoe
+      rw [eq_comm]
+      rw [hn]
+      exact A
     · intro z hz
 
       sorry