From c6396e002dea8a814cc05b1fa61f33e30669c335 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 19 Nov 2025 14:43:14 +0100
Subject: [PATCH] Update Basic.lean

---
 Aristotle/Basic.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean
index 90f861f..d7e6563 100644
--- a/Aristotle/Basic.lean
+++ b/Aristotle/Basic.lean
@@ -8,6 +8,13 @@ variable
 
 /-- Derivatives of meromorphic functions are meromorphic. -/
 theorem meromorphicAt_deriv_of_order_eq_top {f : 𝕜 → 𝕜} {x : 𝕜}
-    (h : MeromorphicAt f x) (h₁ : h.order = ⊤) :
+    (h : MeromorphicAt f x) (h₁ : h.order ≠ ⊤) :
     MeromorphicAt (deriv f) x := by
+
+  have := h.eventually_analyticAt
+  obtain ⟨n, hn⟩ := h
+
+  let g : 𝕜 → 𝕜 := sorry
+  rw [MeromorphicAt.meromorphicAt_congr]
+
   sorry