Update Basic.lean

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 𝕜]
+  {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
-  {U : Set 𝕜} {f g : 𝕜 → E} {a : WithTop E} {a₀ : E}
 
 /-- 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. -/
+  obtain ⟨g, h₁g, h₂g, h₃⟩ := h.order_ne_top_iff.1 h₁
-@[fun_prop]
+  lift h.order to ℤ using h₁ with n hn
-theorem MeromorphicAt.logDeriv {f : 𝕜 → 𝕜} {x : 𝕜} (h : MeromorphicAt f x) :
+
-    MeromorphicAt (f⁻¹ * deriv f) x := by
+  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