Update Basic.lean

Aristotle/Basic.lean

@@ -3,25 +3,36 @@ import Mathlib.Analysis.Calculus.Deriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.ZPow
 import Mathlib.Analysis.Calculus.Deriv.Shift
 
-open MeromorphicOn Metric Real Set Classical
+open MeromorphicOn Real Set Classical Topology
+
+set_option checkBinderAnnotations false
 
 theorem eventually_eventually_nhdsWithin₁
-    {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} [IsClosed s] :
-    (∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhds y, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x := by
+    {α : Type*} [TopologicalSpace α] [T1Space α] {a : α} {p : α → Prop} :
+    (∀ᶠ (y : α) in 𝓝[≠] a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝[≠] a, p x := by
   nth_rw 2 [← eventually_eventually_nhdsWithin]
   constructor
   · intro h
     filter_upwards [h] with y hy
     exact eventually_nhdsWithin_of_eventually_nhds hy
   · intro h
-    filter_upwards [h] with y hy
-    have : y ∉ s := by sorry
-    rw [eventually_nhdsWithin_iff] at hy
-    rw [Filter.Eventually] at *
-    apply Filter.mem_of_superset hy
-    intro x hx
-    simp_all
-    sorry
+    filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with y h₁y h₂y
+    simp_all [IsOpen.nhdsWithin_eq]
+
+theorem Filter.EventuallyEq.nhdsNE_deriv
+    {𝕜 : Type u} [NontriviallyNormedField 𝕜]
+    {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜}
+    (h : f₁ =ᶠ[𝓝[≠] x] f) :
+    deriv f₁ =ᶠ[𝓝[≠] x] deriv f := by
+  rw [eventuallyEq_nhdsWithin_iff, eventually_nhds_iff] at *
+  obtain ⟨t, h₁t, h₂t, h₃t⟩ := h
+  use t
+  simp_all only [mem_compl_iff, mem_singleton_iff, and_self, and_true]
+  intro y h₁y h₂y
+  rw [Filter.EventuallyEq.deriv_eq]
+  apply eventually_nhds_iff.2
+  use t \ {x}
+  simp_all [IsOpen.sdiff h₂t isClosed_singleton]
 
 variable
   {𝕜 : Type*} [NontriviallyNormedField 𝕜]
@@ -41,21 +52,13 @@ theorem meromorphicAt_deriv {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x)
       =ᶠ[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)]
+    filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
+      eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂
+    rw [deriv_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂])) (by fun_prop),
+      add_comm, 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
 
-  have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] (fun z ↦ (z - x) ^ n • g z) := by
+  have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] deriv (fun z ↦ (z - x) ^ n • g z) := by
     sorry
 
   apply MeromorphicAt.congr _ this.symm