From 6aa5bc3b1c6b06ea71990428534370b46c626886 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 24 Oct 2024 13:12:03 +0200
Subject: [PATCH] Update stronglyMeromorphic.lean

---
 Nevanlinna/stronglyMeromorphic.lean | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index b386dcb..c0aca67 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -134,6 +134,15 @@ lemma Mnhds
   · exact h₂t
 
 
+theorem localIdentity
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀)
+  (hg : AnalyticAt ℂ g z₀) :
+  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
+  sorry
+
+
 theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
   {f : ℂ → ℂ}
   {z₀ : ℂ}
@@ -174,12 +183,13 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
             simp [h₃f]
             obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
             simp at h₃G
-            have hn : n = 0 := by
-              sorry
+            have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
             rw [hn]
+            rw [hn] at h₃g; simp at h₃g
             simp
             have : g =ᶠ[𝓝 z₀] G := by
-              sorry
+              apply localIdentity h₁g h₁G
+              exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
             rw [Filter.EventuallyEq.eq_of_nhds this]
           · have : hf.order ≠ 0 := h₃f
             simp [this]