From b3f99c37f2d3aa6da4165e9d3ef507bb0e211434 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 27 Oct 2025 15:27:06 +0100
Subject: [PATCH] Update Basic.lean

---
 Aristotle/Basic.lean | 28 +++++++++++++++-------------
 1 file changed, 15 insertions(+), 13 deletions(-)

diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean
index 4781412..7e921cf 100644
--- a/Aristotle/Basic.lean
+++ b/Aristotle/Basic.lean
@@ -1,24 +1,26 @@
 import Mathlib.Analysis.Meromorphic.Basic
+import Mathlib.Analysis.Meromorphic.Order
 
 open MeromorphicOn Metric Real Set Classical
 
 variable
-  {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
-  {U : Set 𝕜} {f g : 𝕜 → E} {a : WithTop E} {a₀ : E}
+  {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
 
 /-- Derivatives of meromorphic functions are meromorphic. -/
 @[fun_prop]
-theorem meromorphicAt_deriv {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
+theorem meromorphicAt_deriv {f : 𝕜 → 𝕜} {x : 𝕜}
+    (h : MeromorphicAt f x) (h₁ : h.order ≠ ⊤) :
     MeromorphicAt (deriv f) x := by
-  unfold MeromorphicAt at *
-  obtain ⟨n, hn⟩ := h
-  use n + 1
-  have := hn.deriv
-  sorry
 
-/-- Logarithmic derivatives of meromorphic functions are meromorphic. -/
-@[fun_prop]
-theorem MeromorphicAt.logDeriv {f : 𝕜 → 𝕜} {x : 𝕜} (h : MeromorphicAt f x) :
-    MeromorphicAt (f⁻¹ * deriv f) x := by
+  obtain ⟨g, h₁g, h₂g, h₃⟩ := h.order_ne_top_iff.1 h₁
+  lift h.order to ℤ using h₁ with n hn
+
+  have : (n : WithTop ℤ).untop₀ = n := by
+    sorry
+  simp_all [this]
+  have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] deriv (fun z ↦ (z - x) ^ n * g z) := by
+    sorry
+  have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] fun z ↦ n * (z - x) ^ (n - 1) * g z + (z - x) ^ n * deriv g z := by
+    sorry
+  apply MeromorphicAt.congr _ this.symm
   sorry