From d80894ea6f2daa5b7e1b92522a14f1a5dc7ea7aa Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 23 Oct 2024 13:03:41 +0200
Subject: [PATCH] Update stronglyMeromorphic.lean

---
 Nevanlinna/stronglyMeromorphic.lean | 97 ++++++++++++++---------------
 1 file changed, 47 insertions(+), 50 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index 4140e50..3223e64 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -3,6 +3,9 @@ import Nevanlinna.analyticAt
 import Nevanlinna.mathlibAddOn
 
 
+open Topology
+
+
 /- Strongly MeromorphicAt -/
 def StronglyMeromorphicAt
   (f : ℂ → ℂ)
@@ -108,22 +111,28 @@ lemma m₂
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
-  ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = hf.makeStronglyMeromorphicAt z := by
+  f =ᶠ[𝓝[≠] z₀] hf.makeStronglyMeromorphicAt := by
   apply eventually_nhdsWithin_of_forall
   exact fun x a => m₁ hf x a
 
 
-open Topology
-
 lemma Mnhds
   {f g : ℂ → ℂ}
   {z₀ : ℂ}
-  (h₁ : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = g z)
+  (h₁ : f =ᶠ[𝓝[≠] z₀] g)
   (h₂ : f z₀ = g z₀) :
-  ∀ᶠ (z : ℂ) in nhds z₀, f z = g z := by
-  rw [eventually_nhds_iff]
-  rw [eventually_nhdsWithin_iff] at h₁
-  sorry
+  f =ᶠ[𝓝 z₀] g := by
+  apply eventually_nhds_iff.2
+  obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁)
+  use t
+  constructor
+  · intro y hy
+    by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ)
+    · exact h₁t y hy h₂y
+    · simp at h₂y
+      rwa [h₂y]
+  · exact h₂t
+
 
 theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
   {f : ℂ → ℂ}
@@ -132,51 +141,39 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
   StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by
 
   by_cases h₂f : hf.order = ⊤
-  · rw [MeromorphicAt.order_eq_top_iff] at h₂f
-    let Z : ℂ → ℂ := fun z ↦ 0
-    have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
-      --unfold Filter.EventuallyEq
+  · have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
       apply Mnhds
-      · apply eventually_nhdsWithin_of_forall
-        intro x hx
-
-        sorry
-
-
-      sorry
-
-
+      · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
+        exact (MeromorphicAt.order_eq_top_iff hf).1 h₂f
+      · unfold MeromorphicAt.makeStronglyMeromorphicAt
+        simp [h₂f]
 
     apply AnalyticAt.stronglyMeromorphicAt
     rw [analyticAt_congr this]
     apply analyticAt_const
+  · let n := hf.order.untop h₂f
+    have : hf.order = n := by
+      exact Eq.symm (WithTop.coe_untop hf.order h₂f)
+    rw [hf.order_eq_int_iff] at this
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
+    right
+    use n
+    use g
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · apply Mnhds
+        · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
+          exact h₃g
+        · unfold MeromorphicAt.makeStronglyMeromorphicAt
+          simp
+          by_cases h₃f : hf.order = 0
+          · simp [h₃f]
 
-
-
-  by_cases h₂f : hf.order = 0
-  · apply AnalyticAt.stronglyMeromorphicAt
-
-    let A := h₂f
-    rw [(by rfl : (0 : WithTop ℤ) = (0 : ℤ)), hf.order_eq_int_iff] at A
-    simp at A
-    have : hf.makeStronglyMeromorphicAt = Classical.choose A := by
-      simp [MeromorphicAt.makeStronglyMeromorphicAt, h₂f]
-    let B := Classical.choose_spec A
-
-    rw [this]
-    tauto
-  · by_cases h₃f : hf.order = ⊤
-    · rw [MeromorphicAt.order_eq_top_iff] at h₃f
-      left
-
-      sorry
-    · sorry
-
-
-
-theorem makeStronglyMeromorphic_eventuallyEq
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = hf.makeStronglyMeromorphicAt z := by
-  sorry
+            sorry
+          · simp [h₃f]
+            left
+            apply zero_zpow n
+            dsimp [n]
+            rwa [WithTop.untop_eq_iff h₂f]