From 5ef74df5e417f4c5830ecf7f3e69a800274c3b4e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 9 Dec 2023 12:32:15 +0000
Subject: [PATCH] chore(*Deriv*): golf (#8899)

Assorted golf I did while working on a refactor. Submitting as a separate PR.

- Move `not_differentiableAt_abs_zero` to `Calculus.Deriv.Add`, golf.
- Rename `HasFDerivWithinAt_of_nhdsWithin_eq_bot` to `HasFDerivWithinAt.of_nhdsWithin_eq_bot`, golf.
- Protect `Filter.EventuallyEq.rfl`.
- Golf here and there.
---
 Mathlib/Analysis/Calculus/Deriv/Add.lean      | 10 +++++
 Mathlib/Analysis/Calculus/FDeriv/Basic.lean   | 43 +++++++------------
 Mathlib/Analysis/Calculus/FDeriv/Equiv.lean   |  6 +--
 .../Analysis/Calculus/FDeriv/Measurable.lean  | 18 ++------
 .../Analysis/InnerProductSpace/Calculus.lean  | 22 ----------
 Mathlib/Order/Filter/Basic.lean               |  2 +-
 Mathlib/Topology/ContinuousOn.lean            |  7 ++-
 7 files changed, 34 insertions(+), 74 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/Deriv/Add.lean b/Mathlib/Analysis/Calculus/Deriv/Add.lean
index 77c1939ebd126..381e693167852 100644
--- a/Mathlib/Analysis/Calculus/Deriv/Add.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/Add.lean
@@ -282,6 +282,16 @@ theorem differentiableOn_neg : DifferentiableOn 𝕜 (Neg.neg : 𝕜 → 𝕜) s
   DifferentiableOn.neg differentiableOn_id
 #align differentiable_on_neg differentiableOn_neg
 
+theorem not_differentiableAt_abs_zero : ¬ DifferentiableAt ℝ (abs : ℝ → ℝ) 0 := by
+  intro h
+  have h₁ : deriv abs (0 : ℝ) = 1 :=
+    (uniqueDiffOn_Ici _ _ Set.left_mem_Ici).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
+      (hasDerivWithinAt_id _ _).congr_of_mem (fun _ h ↦ abs_of_nonneg h) Set.left_mem_Ici
+  have h₂ : deriv abs (0 : ℝ) = -1 :=
+    (uniqueDiffOn_Iic _ _ Set.right_mem_Iic).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
+      (hasDerivWithinAt_neg _ _).congr_of_mem (fun _ h ↦ abs_of_nonpos h) Set.right_mem_Iic
+  linarith
+
 end Neg2
 
 section Sub
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
index 4011043d4f0c3..8a546f66dd6d1 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
@@ -528,32 +528,24 @@ theorem DifferentiableWithinAt.differentiableAt (h : DifferentiableWithinAt 𝕜
 
 /-- If `x` is isolated in `s`, then `f` has any derivative at `x` within `s`,
 as this statement is empty. -/
-theorem HasFDerivWithinAt_of_nhdsWithin_eq_bot (h : 𝓝[s\{x}] x = ⊥) :
+theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot (h : 𝓝[s\{x}] x = ⊥) :
     HasFDerivWithinAt f f' s x := by
-  by_cases hx : x ∈ s
-  · have : s = s\{x} ∪ {x} := by simpa using (insert_eq_self.2 hx).symm
-    have A : 𝓝[s] x = 𝓝[s\{x}] x ⊔ 𝓟 {x} := by
-      conv_lhs => rw [this]
-      simp only [union_singleton, nhdsWithin_insert, sup_comm, principal_singleton]
-    simp [HasFDerivWithinAt, HasFDerivAtFilter, A, h]
-  · rw [diff_singleton_eq_self hx] at h
-    simp [HasFDerivWithinAt, HasFDerivAtFilter, h]
+  rw [← hasFDerivWithinAt_diff_singleton x, HasFDerivWithinAt, h]
+  apply isLittleO_bot
 
 /-- If `x` is not in the closure of `s`, then `f` has any derivative at `x` within `s`,
 as this statement is empty. -/
-theorem hasFDerivWithinAt_of_nmem_closure (h : x ∉ closure s) : HasFDerivWithinAt f f' s x := by
-  simp only [mem_closure_iff_nhdsWithin_neBot, neBot_iff, Ne.def, Classical.not_not] at h
-  simp [HasFDerivWithinAt, HasFDerivAtFilter, h, IsLittleO, IsBigOWith]
+theorem hasFDerivWithinAt_of_nmem_closure (h : x ∉ closure s) : HasFDerivWithinAt f f' s x :=
+  .of_nhdsWithin_eq_bot <| eq_bot_mono (nhdsWithin_mono _ (diff_subset _ _)) <| by
+    rwa [mem_closure_iff_nhdsWithin_neBot, not_neBot] at h
 #align has_fderiv_within_at_of_not_mem_closure hasFDerivWithinAt_of_nmem_closure
 
 theorem DifferentiableWithinAt.hasFDerivWithinAt (h : DifferentiableWithinAt 𝕜 f s x) :
     HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x := by
   by_cases H : 𝓝[s \ {x}] x = ⊥
-  · exact HasFDerivWithinAt_of_nhdsWithin_eq_bot H
-  · simp only [fderivWithin]
-    rw [if_neg H]
-    dsimp only [DifferentiableWithinAt] at h
-    rw [dif_pos h]
+  · exact .of_nhdsWithin_eq_bot H
+  · unfold DifferentiableWithinAt at h
+    rw [fderivWithin, if_neg H, dif_pos h]
     exact Classical.choose_spec h
 #align differentiable_within_at.has_fderiv_within_at DifferentiableWithinAt.hasFDerivWithinAt
 
@@ -705,15 +697,11 @@ theorem fderivWithin_inter (ht : t ∈ 𝓝 x) : fderivWithin 𝕜 f (s ∩ t) x
 @[simp]
 theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f := by
   ext1 x
-  by_cases H : 𝓝[univ \ {x}] x = ⊥
-  · have : Subsingleton E := by
-      apply not_nontrivial_iff_subsingleton.1
-      contrapose! H
-      have : (𝓝[{x}ᶜ] x).NeBot := Module.punctured_nhds_neBot 𝕜 E x
-      rw [compl_eq_univ_diff] at this
-      exact NeBot.ne this
-    exact Subsingleton.elim _ _
-  · simp [fderivWithin, fderiv, H]
+  nontriviality E
+  have H : 𝓝[univ \ {x}] x ≠ ⊥
+  · rw [← compl_eq_univ_diff, ← neBot_iff]
+    exact Module.punctured_nhds_neBot 𝕜 E x
+  simp [fderivWithin, fderiv, H]
 #align fderiv_within_univ fderivWithin_univ
 
 theorem fderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x := by
@@ -905,7 +893,7 @@ theorem fderivWithin_eventually_congr_set (h : s =ᶠ[𝓝 x] t) :
 
 theorem Filter.EventuallyEq.hasStrictFDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) (h' : ∀ y, f₀' y = f₁' y) :
     HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x := by
-  refine' isLittleO_congr ((h.prod_mk_nhds h).mono _) (eventually_of_forall fun _ => _root_.rfl)
+  refine' isLittleO_congr ((h.prod_mk_nhds h).mono _) .rfl
   rintro p ⟨hp₁, hp₂⟩
   simp only [*]
 #align filter.eventually_eq.has_strict_fderiv_at_iff Filter.EventuallyEq.hasStrictFDerivAt_iff
@@ -1148,7 +1136,6 @@ section Const
 
 /-! ### Derivative of a constant function -/
 
-
 theorem hasStrictFDerivAt_const (c : F) (x : E) :
     HasStrictFDerivAt (fun _ => c) (0 : E →L[𝕜] F) x :=
   (isLittleO_zero _ _).congr_left fun _ => by simp only [zero_apply, sub_self]
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean b/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
index 8586ebf76348d..14255476d5640 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
@@ -395,10 +395,8 @@ theorem HasFDerivAt.of_local_left_inverse {f : E → F} {f' : E ≃L[𝕜] F} {g
     simp
   refine' this.trans_isLittleO _
   clear this
-  refine'
-    ((hf.comp_tendsto hg).symm.congr' (hfg.mono _) (eventually_of_forall fun _ => rfl)).trans_isBigO
-      _
-  · rintro p hp
+  refine ((hf.comp_tendsto hg).symm.congr' (hfg.mono ?_) .rfl).trans_isBigO ?_
+  · intro p hp
     simp [hp, hfg.self_of_nhds]
   · refine' ((hf.isBigO_sub_rev f'.antilipschitz).comp_tendsto hg).congr'
       (eventually_of_forall fun _ => rfl) (hfg.mono _)
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
index bdffbade52316..21b0746eb5faf 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
@@ -115,9 +115,7 @@ namespace FDerivMeasurableAux
 at scale `r` by the linear map `L`, up to an error `ε`. We tweak the definition to make sure that
 this is an open set.-/
 def A (f : E → F) (L : E →L[𝕜] F) (r ε : ℝ) : Set E :=
-  { x |
-    ∃ r' ∈ Ioc (r / 2) r,
-      ∀ (y) (_ : y ∈ ball x r') (z) (_ : z ∈ ball x r'), ‖f z - f y - L (z - y)‖ < ε * r }
+  { x | ∃ r' ∈ Ioc (r / 2) r, ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r }
 #align fderiv_measurable_aux.A FDerivMeasurableAux.A
 
 /-- The set `B f K r s ε` is the set of points `x` around which there exists a continuous linear map
@@ -386,12 +384,7 @@ theorem measurableSet_of_differentiableAt_of_isComplete {K : Set (E →L[𝕜] F
   -- simp [differentiable_set_eq_D K hK, D, isOpen_B.measurableSet, MeasurableSet.iInter,
   --   MeasurableSet.iUnion]
   simp only [D, differentiable_set_eq_D K hK]
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iUnion fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
+  repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro
   exact isOpen_B.measurableSet
 #align measurable_set_of_differentiable_at_of_is_complete measurableSet_of_differentiableAt_of_isComplete
 
@@ -753,12 +746,7 @@ theorem measurableSet_of_differentiableWithinAt_Ici_of_isComplete {K : Set F} (h
   -- simp [differentiable_set_eq_d K hK, D, measurableSet_b, MeasurableSet.iInter,
   --   MeasurableSet.iUnion]
   simp only [differentiable_set_eq_D K hK, D]
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iUnion fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
-  refine MeasurableSet.iInter fun _ => ?_
+  repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro
   exact measurableSet_B
 #align measurable_set_of_differentiable_within_at_Ici_of_is_complete measurableSet_of_differentiableWithinAt_Ici_of_isComplete
 
diff --git a/Mathlib/Analysis/InnerProductSpace/Calculus.lean b/Mathlib/Analysis/InnerProductSpace/Calculus.lean
index 4531a3ea020cf..6aac288bcb92f 100644
--- a/Mathlib/Analysis/InnerProductSpace/Calculus.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Calculus.lean
@@ -252,28 +252,6 @@ theorem DifferentiableAt.norm (hf : DifferentiableAt ℝ f x) (h0 : f x ≠ 0) :
   ((contDiffAt_norm 𝕜 h0).differentiableAt le_rfl).comp x hf
 #align differentiable_at.norm DifferentiableAt.norm
 
-theorem not_differentiableAt_abs_zero : ¬ DifferentiableAt ℝ (abs : ℝ → ℝ) 0 := by
-  rw [DifferentiableAt]
-  push_neg
-  intro f
-  simp only [HasFDerivAt, HasFDerivAtFilter, abs_zero, sub_zero,
-    Asymptotics.isLittleO_iff, norm_eq_abs, not_forall, not_eventually, not_le, exists_prop]
-  use (1 / 2), by norm_num
-  rw [Filter.HasBasis.frequently_iff Metric.nhds_basis_ball]
-  intro δ hδ
-  obtain ⟨x, hx⟩ : ∃ x ∈ Metric.ball 0 δ, x ≠ 0 ∧ f x ≤ 0 := by
-    by_cases h : f (δ / 2) ≤ 0
-    · use (δ / 2)
-      simp [h, abs_of_nonneg hδ.le, hδ, hδ.ne']
-    · use -(δ / 2)
-      push_neg at h
-      simp [h.le, abs_of_nonneg hδ.le, hδ, hδ.ne']
-  use x, hx.left
-  rw [lt_abs]
-  left
-  cancel_denoms
-  linarith [abs_pos.mpr hx.right.left]
-
 theorem DifferentiableAt.dist (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x)
     (hne : f x ≠ g x) : DifferentiableAt ℝ (fun y => dist (f y) (g y)) x := by
   simp only [dist_eq_norm]; exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
index 491e825df6cff..37576cd2dd276 100644
--- a/Mathlib/Order/Filter/Basic.lean
+++ b/Mathlib/Order/Filter/Basic.lean
@@ -1492,7 +1492,7 @@ theorem EventuallyEq.refl (l : Filter α) (f : α → β) : f =ᶠ[l] f :=
   eventually_of_forall fun _ => rfl
 #align filter.eventually_eq.refl Filter.EventuallyEq.refl
 
-theorem EventuallyEq.rfl {l : Filter α} {f : α → β} : f =ᶠ[l] f :=
+protected theorem EventuallyEq.rfl {l : Filter α} {f : α → β} : f =ᶠ[l] f :=
   EventuallyEq.refl l f
 #align filter.eventually_eq.rfl Filter.EventuallyEq.rfl
 
diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean
index 04c4429245eed..16845e5ea41af 100644
--- a/Mathlib/Topology/ContinuousOn.lean
+++ b/Mathlib/Topology/ContinuousOn.lean
@@ -1157,10 +1157,9 @@ theorem OpenEmbedding.map_nhdsWithin_preimage_eq {f : α → β} (hf : OpenEmbed
   rw [inter_assoc, inter_self]
 #align open_embedding.map_nhds_within_preimage_eq OpenEmbedding.map_nhdsWithin_preimage_eq
 
-theorem continuousWithinAt_of_not_mem_closure {f : α → β} {s : Set α} {x : α} :
-    x ∉ closure s → ContinuousWithinAt f s x := by
-  intro hx
-  rw [mem_closure_iff_nhdsWithin_neBot, neBot_iff, not_not] at hx
+theorem continuousWithinAt_of_not_mem_closure {f : α → β} {s : Set α} {x : α} (hx : x ∉ closure s) :
+    ContinuousWithinAt f s x := by
+  rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
   rw [ContinuousWithinAt, hx]
   exact tendsto_bot
 #align continuous_within_at_of_not_mem_closure continuousWithinAt_of_not_mem_closure