Update Basic.lean

Aristotle/Basic.lean

@@ -5,18 +5,17 @@ import Mathlib.Analysis.Calculus.Deriv.Shift
 
 open MeromorphicOn Real Set Classical Topology
 
-set_option checkBinderAnnotations false
-
-theorem eventually_eventually_nhdsWithin₁
+@[simp]
+theorem eventually_nhdsNE_eventually_nhds_iff_eventually_nhdsNE
     {α : Type*} [TopologicalSpace α] [T1Space α] {a : α} {p : α → Prop} :
-    (∀ᶠ (y : α) in 𝓝[≠] a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝[≠] a, p x := by
+    (∀ᶠ 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
+    filter_upwards [h] with _ hy
     exact eventually_nhdsWithin_of_eventually_nhds hy
   · intro h
-    filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with y h₁y h₂y
+    filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _
     simp_all [IsOpen.nhdsWithin_eq]
 
 theorem Filter.EventuallyEq.nhdsNE_deriv
@@ -24,42 +23,38 @@ theorem Filter.EventuallyEq.nhdsNE_deriv
     {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]
+  rw [Filter.EventuallyEq, ← eventually_nhdsNE_eventually_nhds_iff_eventually_nhdsNE] at *
+  filter_upwards [h] with y hy
+  apply Filter.EventuallyEq.deriv hy
 
 variable
   {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
   {U : Set 𝕜} {f g : 𝕜 → E} {a : WithTop E} {a₀ : E}
 
+@[fun_prop]
+theorem AnalyticAt.deriv₁
+    {𝕜 : Type u} [NontriviallyNormedField 𝕜]
+    {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
+    {f : 𝕜 → F} {x : 𝕜}
+    (h : AnalyticAt 𝕜 f x) :
+    AnalyticAt 𝕜 (deriv f) x := by
+  obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd
+  exact h.deriv x (by simp [hr])
 
 /-- Derivatives of meromorphic functions are meromorphic. -/
 @[fun_prop]
 theorem meromorphicAt_deriv {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
     MeromorphicAt (deriv f) x := by
-
   rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h
   obtain ⟨n, g, h₁g, h₂g⟩ := h
-
   have : deriv (fun z ↦ (z - x) ^ n • g z)
-      =ᶠ[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
+      =ᶠ[𝓝[≠] x] fun z ↦ (n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z := by
     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)]
+      add_comm, deriv_comp_sub_const (f := (· ^ n))]
     aesop
-
-  have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] deriv (fun z ↦ (z - x) ^ n • g z) := by
-    sorry
-
-  apply MeromorphicAt.congr _ this.symm
+  rw [MeromorphicAt.meromorphicAt_congr (Filter.EventuallyEq.nhdsNE_deriv h₂g),
+    MeromorphicAt.meromorphicAt_congr this]
   fun_prop