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

---
 Nevanlinna/stronglyMeromorphic.lean | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index 6f9ca10..c1a4a90 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -4,7 +4,6 @@ import Nevanlinna.mathlibAddOn
 
 
 /- Strongly MeromorphicAt -/
-
 def StronglyMeromorphicAt
   (f : ℂ → ℂ)
   (z₀ : ℂ) :=
@@ -63,6 +62,25 @@ theorem StronglyMeromorphicAt.analytic
     exact h₁g
 
 
+/- Analytic functions are strongly meromorphic -/
+theorem AnalyticAt.stronglyMeromorphicAt
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁f : AnalyticAt ℂ f z₀) :
+  StronglyMeromorphicAt f z₀ := by
+  by_cases h₂f : h₁f.order = ⊤
+  · rw [AnalyticAt.order_eq_top_iff] at h₂f
+    tauto
+  · have : h₁f.order ≠ ⊤ := h₂f
+    rw [← ENat.coe_toNat_eq_self] at this
+    rw [eq_comm, AnalyticAt.order_eq_nat_iff] at this
+    right
+    use h₁f.order.toNat
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
+    use g
+    tauto
+
+
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}