Update

Nevanlinna/mathlibAddOn.lean

@@ -1,3 +1,4 @@
+import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Add
 
@@ -33,3 +34,20 @@ theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
   have : c • f = fun x ↦ c • f x := rfl
   rw [this]
   exact ContDiff.const_smul c hf
+
+
+-- Mathlib.Analysis.Analytic.Meromorphic
+
+theorem meromorphicAt_congr
+  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
+  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
+  (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
+  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
+
+theorem meromorphicAt_congr'
+  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
+  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
+  (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
+  meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)

Nevanlinna/stronglyMeromorphic.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
+import Nevanlinna.mathlibAddOn
 
 
 /- Strongly MeromorphicAt -/
@@ -20,27 +21,46 @@ theorem StronglyMeromorphicAt.meromorphicAt
   · use 0; simp
     rw [analyticAt_congr h]
     exact analyticAt_const
-  · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
-    have : MeromorphicAt (fun z ↦ (z - z₀) ^ n • g z) z₀ := by
-      simp
-      apply MeromorphicAt.mul
-      apply MeromorphicAt.zpow
-      apply MeromorphicAt.sub
-
-      sorry
-    apply MeromorphicAt.congr this
-    rw [Filter.eventuallyEq_comm]
-    exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
+  · obtain ⟨n, g, h₁g, _, h₃g⟩ := h
+    rw [meromorphicAt_congr' h₃g]
+    apply MeromorphicAt.smul
+    apply MeromorphicAt.zpow
+    apply MeromorphicAt.sub
+    apply MeromorphicAt.id
+    apply MeromorphicAt.const
+    exact AnalyticAt.meromorphicAt h₁g
 
 
-/- Strongly MeromorphicAt of positive order is analytic -/
+/- Strongly MeromorphicAt of non-negative order is analytic -/
 theorem StronglyMeromorphicAt.analytic
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (h₁f : StronglyMeromorphicAt f z₀)
   (h₂f : 0 ≤ h₁f.meromorphicAt.order):
   AnalyticAt ℂ f z₀ := by
-  sorry
+  let h₁f' := h₁f
+  rcases h₁f' with h|h
+  · rw [analyticAt_congr h]
+    exact analyticAt_const
+  · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
+    rw [analyticAt_congr h₃g]
+
+    have : h₁f.meromorphicAt.order = n := by
+      rw [MeromorphicAt.order_eq_int_iff]
+      use g
+      constructor
+      · exact h₁g
+      · constructor
+        · exact h₂g
+        · exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
+    rw [this] at h₂f
+    apply AnalyticAt.smul
+    nth_rw 1 [← Int.toNat_of_nonneg (WithTop.coe_nonneg.mp h₂f)]
+    apply AnalyticAt.pow
+    apply AnalyticAt.sub
+    apply analyticAt_id -- Warning: want apply AnalyticAt.id
+    apply analyticAt_const -- Warning: want AnalyticAt.const
+    exact h₁g
 
 
 
@@ -51,7 +71,20 @@ def MeromorphicAt.makeStronglyMeromorphicAt
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
   ℂ → ℂ := by
-  exact 0
+  by_cases h₂f : hf.order = ⊤
+  · 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