From 5bf670231fb4df8d689c765df5063b08f51d772b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 24 Oct 2024 16:05:44 +0200
Subject: [PATCH] Update stronglyMeromorphicAt.lean

---
 Nevanlinna/stronglyMeromorphicAt.lean | 31 +++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean
index 344b499..9e5eadb 100644
--- a/Nevanlinna/stronglyMeromorphicAt.lean
+++ b/Nevanlinna/stronglyMeromorphicAt.lean
@@ -211,3 +211,34 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
             apply zero_zpow n
             dsimp [n]
             rwa [WithTop.untop_eq_iff h₂f]
+
+
+theorem makeStronglyMeromorphic_id
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀) :
+  f = hf.meromorphicAt.makeStronglyMeromorphicAt := by
+
+  funext z
+  by_cases hz : z = z₀
+  · rw [hz]
+    unfold MeromorphicAt.makeStronglyMeromorphicAt
+    simp
+    let h₀f := hf
+    rcases hf with h₁f|h₁f
+    · have A : f =ᶠ[𝓝[≠] z₀] 0 := by
+        apply Filter.EventuallyEq.filter_mono h₁f
+        exact nhdsWithin_le_nhds
+      let B := (MeromorphicAt.order_eq_top_iff h₀f.meromorphicAt).2 A
+      simp [B]
+      exact Filter.EventuallyEq.eq_of_nhds h₁f
+    · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f
+
+      by_cases h₃f : h₀f.meromorphicAt.order = 0
+      · simp [h₃f]
+        sorry
+      · simp [h₃f]
+
+        sorry
+
+  · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz