From 405b68924d4d00c257cd494fc060f8b3b7e7bb52 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 14 Oct 2024 13:25:49 +0200
Subject: [PATCH] Update stronglyMeromorphic.lean

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

diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index 5c84145..6f9ca10 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -63,28 +63,17 @@ theorem StronglyMeromorphicAt.analytic
     exact h₁g
 
 
-
 /- Make strongly MeromorphicAt -/
-
-def MeromorphicAt.makeStronglyMeromorphicAt
+noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
   ℂ → ℂ := by
-  by_cases h₂f : hf.order = ⊤
+  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
   · exact 0
-  · have : ∃ n : ℤ, hf.order = n := by
-      exact Option.ne_none_iff_exists'.mp h₂f
-
-    let o := hf.order.untop h₂f
-    have : hf.order = o := by
-      exact Eq.symm (WithTop.coe_untop hf.order h₂f)
-    rw [MeromorphicAt.order_eq_int_iff] at this
-    obtain ⟨g, hg⟩ := this
-    exact fun z ↦ (z - z₀) ^ o • g z
-    sorry
-
-
 
 
 theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
@@ -92,6 +81,7 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
   StronglyMeromorphicAt hf.makeStronglyMeromorphic z₀ := by
+
   sorry