From 2bb8762a4fda69034dc74f86bd75c63c933472dc Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 4 Nov 2025 16:30:01 +0100
Subject: [PATCH] Update Basic.lean

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

diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean
index 7e921cf..90f861f 100644
--- a/Aristotle/Basic.lean
+++ b/Aristotle/Basic.lean
@@ -7,20 +7,7 @@ variable
   {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
 
 /-- Derivatives of meromorphic functions are meromorphic. -/
-@[fun_prop]
-theorem meromorphicAt_deriv {f : 𝕜 → 𝕜} {x : 𝕜}
-    (h : MeromorphicAt f x) (h₁ : h.order ≠ ⊤) :
+theorem meromorphicAt_deriv_of_order_eq_top {f : 𝕜 → 𝕜} {x : 𝕜}
+    (h : MeromorphicAt f x) (h₁ : h.order = ⊤) :
     MeromorphicAt (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