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

---
 Nevanlinna/meromorphicOn_decompose.lean | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index a13c472..7df34e3 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -38,8 +38,15 @@ theorem MeromorphicOn.decompose
     · intro z hz
       rw [← (h₄g z hz).order_eq_zero_iff]
 
-      let A := (h₄g z hz).meromorphicAt_order
-      let B := h₂g ⟨z, hz⟩
+      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
     · intro z hz