From 25b0ffd899639d83b128cb3c825418c321bc31b3 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 21 Oct 2024 10:36:48 +0200
Subject: [PATCH] Update stronglyMeromorphic.lean

---
 Nevanlinna/stronglyMeromorphic.lean | 55 +++++++++++++++++++++++++----
 1 file changed, 49 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index c1a4a90..8d0f6b7 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -81,26 +81,69 @@ theorem AnalyticAt.stronglyMeromorphicAt
     tauto
 
 
+theorem MeromorphicAt.order_neq_top_iff
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = (z - z₀) ^ (hf.order.untop' 0) • g z := by
+
+  rw [← hf.order_eq_int_iff (hf.order.untop' 0)]
+  constructor
+  · intro h₁f
+    apply?
+    exact Eq.symm (ENat.coe_toNat h₁f)
+  · intro h₁f
+    exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))
+
+
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
   ℂ → ℂ := by
-  by_cases h₂f : hf.order = 0
-  · have : (0 : WithTop ℤ) = (0 : ℤ) := rfl
-    rw [this, hf.order_eq_int_iff] at h₂f
-    exact Classical.choose h₂f
+
+  by_cases h₁f : hf.order = ⊤
   · exact 0
+  ·
+
+  intro z
+  by_cases z = z₀
+  · by_cases h₂f : hf.order = 0
+    · have : (0 : WithTop ℤ) = (0 : ℤ) := rfl
+      rw [this, hf.order_eq_int_iff] at h₂f
+      exact (Classical.choose h₂f) z₀
+    · exact 0
+  · exact f z
 
 
 theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
-  StronglyMeromorphicAt hf.makeStronglyMeromorphic z₀ := by
+  StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by
+
+
+
+  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
 
-  sorry
 
 
 theorem makeStronglyMeromorphic_eventuallyEq