Update stronglyMeromorphic.lean

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 : ℂ → ℂ}