From 306ed1b0832ceaa8208c1ab29d98dbe892dafbd7 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 24 Oct 2024 14:37:27 +0200
Subject: [PATCH] Update stronglyMeromorphicOn.lean

---
 Nevanlinna/stronglyMeromorphicOn.lean | 132 +++-----------------------
 1 file changed, 11 insertions(+), 121 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphicOn.lean b/Nevanlinna/stronglyMeromorphicOn.lean
index fee12b5..82cb06e 100644
--- a/Nevanlinna/stronglyMeromorphicOn.lean
+++ b/Nevanlinna/stronglyMeromorphicOn.lean
@@ -38,138 +38,28 @@ theorem StronglyMeromorphicOn.analytic
 theorem AnalyticOn.stronglyMeromorphicOn
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (h₁f : AnalyticOn ℂ f U) :
+  (h₁f : AnalyticOnNhd ℂ f U) :
   StronglyMeromorphicOn f U := by
   intro z hz
   apply AnalyticAt.stronglyMeromorphicAt
-  let A := h₁f z hz
   exact h₁f z hz
 
 
 /- Make strongly MeromorphicAt -/
-noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
+noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
   ℂ → ℂ := by
   intro z
-  by_cases z = z₀
-  · by_cases h₁f : hf.order = (0 : ℤ)
-    · rw [hf.order_eq_int_iff] at h₁f
-      exact (Classical.choose h₁f) z₀
-    · exact 0
+  by_cases hz : z ∈ U
+  · exact (hf z hz).makeStronglyMeromorphicAt z
   · exact f z
 
 
-lemma m₁
+theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  ∀ z ≠ z₀, f z = hf.makeStronglyMeromorphicAt z := by
-  intro z hz
-  unfold MeromorphicAt.makeStronglyMeromorphicAt
-  simp [hz]
-
-
-lemma m₂
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  f =ᶠ[𝓝[≠] z₀] hf.makeStronglyMeromorphicAt := by
-  apply eventually_nhdsWithin_of_forall
-  exact fun x a => m₁ hf x a
-
-
-lemma Mnhds
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (h₁ : f =ᶠ[𝓝[≠] z₀] g)
-  (h₂ : f z₀ = g z₀) :
-  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 localIdentity
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f z₀)
-  (hg : AnalyticAt ℂ g z₀) :
-  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
-  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
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by
-
-  by_cases h₂f : hf.order = ⊤
-  · have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
-      apply Mnhds
-      · 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 : ℤ)
-          · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
-            simp [h₃f]
-            obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
-            simp at h₃G
-            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₀] (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]
-          · have : hf.order ≠ 0 := h₃f
-            simp [this]
-            left
-            apply zero_zpow n
-            dsimp [n]
-            rwa [WithTop.untop_eq_iff h₂f]
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
+  sorry