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