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

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

diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index c0aca67..d82645d 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -140,7 +140,20 @@ theorem localIdentity
   (hf : AnalyticAt ℂ f z₀)
   (hg : AnalyticAt ℂ g z₀) :
   f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
-  sorry
+  intro h
+  let Δ := f - g
+  have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg
+  have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by
+    exact Filter.eventuallyEq_iff_sub.mp h
+
+  have : Δ =ᶠ[𝓝 z₀] 0 := by
+    rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h
+    · exact h
+    · have := Filter.EventuallyEq.eventually t₁
+      let A := Filter.eventually_and.2 ⟨this, h⟩
+      let _ := Filter.Eventually.exists A
+      tauto
+  exact Filter.eventuallyEq_iff_sub.mpr this
 
 
 theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
@@ -179,7 +192,6 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
           simp
           by_cases h₃f : hf.order = (0 : ℤ)
           · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
-            let G := Classical.choose h₄f
             simp [h₃f]
             obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
             simp at h₃G
@@ -187,7 +199,7 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
             rw [hn]
             rw [hn] at h₃g; simp at h₃g
             simp
-            have : g =ᶠ[𝓝 z₀] G := by
+            have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
               apply localIdentity h₁g h₁G
               exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
             rw [Filter.EventuallyEq.eq_of_nhds this]