From c699823ad8cf6c41a16ea8e5cfb75529f90431bc Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 26 Nov 2025 16:54:46 +0100
Subject: [PATCH] Update Basic.lean

---
 Aristotle/Basic.lean | 42 +++++++++++++++++++++++++++++++++---------
 1 file changed, 33 insertions(+), 9 deletions(-)

diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean
index d7e6563..13bd18f 100644
--- a/Aristotle/Basic.lean
+++ b/Aristotle/Basic.lean
@@ -1,20 +1,44 @@
 import Mathlib.Analysis.Meromorphic.Basic
-import Mathlib.Analysis.Meromorphic.Order
+import Mathlib.Analysis.Calculus.Deriv.Mul
+import Mathlib.Analysis.Calculus.Deriv.ZPow
+import Mathlib.Analysis.Calculus.Deriv.Shift
 
 open MeromorphicOn Metric Real Set Classical
 
 variable
-  {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
+  {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
+  {U : Set 𝕜} {f g : 𝕜 → E} {a : WithTop E} {a₀ : E}
+
 
 /-- Derivatives of meromorphic functions are meromorphic. -/
-theorem meromorphicAt_deriv_of_order_eq_top {f : 𝕜 → 𝕜} {x : 𝕜}
-    (h : MeromorphicAt f x) (h₁ : h.order ≠ ⊤) :
+@[fun_prop]
+theorem meromorphicAt_deriv {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
     MeromorphicAt (deriv f) x := by
 
-  have := h.eventually_analyticAt
-  obtain ⟨n, hn⟩ := h
+  rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h
+  obtain ⟨n, g, h₁g, h₂g⟩ := h
 
-  let g : 𝕜 → 𝕜 := sorry
-  rw [MeromorphicAt.meromorphicAt_congr]
+  have : deriv (fun z ↦ (z - x) ^ n • g z)
+      =ᶠ[nhdsWithin x {x}ᶜ] fun z₀ ↦ (n * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀ := by
+    have τ₀ : ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, AnalyticAt 𝕜 g y := by
+      exact eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt
+    have τ₁ : ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, y ≠ x := by
+      exact eventually_nhdsWithin_of_forall fun x_1 a ↦ a
+    filter_upwards [τ₀, τ₁] with z₀ h₁ h₂
+    rw [deriv_smul]
+    rw [add_comm]
+    congr
+    rw [deriv_comp_sub_const (f := fun z ↦ z ^ n)]
+    aesop
+    refine DifferentiableAt.zpow ?_ ?_
+    fun_prop
+    left
+    exact sub_ne_zero_of_ne h₂
+    fun_prop
 
-  sorry
+  have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] (fun z ↦ (z - x) ^ n • g z) := by
+    sorry
+
+  apply MeromorphicAt.congr _ this.symm
+  fun_prop