feat: weaken assumptions in lemmas about fderivWithin (#4330)

This is a partial forward-port of leanprover-community/mathlib#19045.

I only forward-ported 1 file that was already merged into
`master`. I'll do some git history rewrites in pending PRs instead.

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.calculus.fderiv.basic
-! leanprover-community/mathlib commit e3fb84046afd187b710170887195d50bada934ee
+! leanprover-community/mathlib commit 3a69562db5a458db8322b190ec8d9a8bbd8a5b14
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -391,25 +391,30 @@ theorem hasFDerivWithinAt_univ : HasFDerivWithinAt f f' univ x ↔ HasFDerivAt f
 alias hasFDerivWithinAt_univ ↔ HasFDerivWithinAt.hasFDerivAt_of_univ _
 #align has_fderiv_within_at.has_fderiv_at_of_univ HasFDerivWithinAt.hasFDerivAt_of_univ
 
-theorem hasFDerivWithinAt_insert {y : E} {g' : E →L[𝕜] F} :
-    HasFDerivWithinAt g g' (insert y s) x ↔ HasFDerivWithinAt g g' s x := by
+theorem hasFDerivWithinAt_insert {y : E} :
+    HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x := by
   rcases eq_or_ne x y with (rfl | h)
   · simp_rw [HasFDerivWithinAt, HasFDerivAtFilter]
     apply Asymptotics.isLittleO_insert
-    simp only [sub_self, g'.map_zero]
-  refine' ⟨fun h => h.mono <| subset_insert y s, fun hg => hg.mono_of_mem _⟩
+    simp only [sub_self, map_zero]
+  refine' ⟨fun h => h.mono <| subset_insert y s, fun hf => hf.mono_of_mem _⟩
   simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin]
 #align has_fderiv_within_at_insert hasFDerivWithinAt_insert
 
 alias hasFDerivWithinAt_insert ↔ HasFDerivWithinAt.of_insert HasFDerivWithinAt.insert'
 #align has_fderiv_within_at.of_insert HasFDerivWithinAt.of_insert
 #align has_fderiv_within_at.insert' HasFDerivWithinAt.insert'
 
-theorem HasFDerivWithinAt.insert {g' : E →L[𝕜] F} (h : HasFDerivWithinAt g g' s x) :
+theorem HasFDerivWithinAt.insert (h : HasFDerivWithinAt g g' s x) :
     HasFDerivWithinAt g g' (insert x s) x :=
   h.insert'
 #align has_fderiv_within_at.insert HasFDerivWithinAt.insert
 
+theorem hasFDerivWithinAt_diff_singleton (y : E) :
+    HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x := by
+  rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert]
+#align has_fderiv_within_at_diff_singleton hasFDerivWithinAt_diff_singleton
+
 theorem HasStrictFDerivAt.isBigO_sub (hf : HasStrictFDerivAt f f' x) :
     (fun p : E × E => f p.1 - f p.2) =O[𝓝 (x, x)] fun p : E × E => p.1 - p.2 :=
   hf.isBigO.congr_of_sub.2 (f'.isBigO_comp _ _)
@@ -568,7 +573,7 @@ theorem DifferentiableWithinAt.mono (h : DifferentiableWithinAt 𝕜 f t x) (st
 #align differentiable_within_at.mono DifferentiableWithinAt.mono
 
 theorem DifferentiableWithinAt.mono_of_mem (h : DifferentiableWithinAt 𝕜 f s x) {t : Set E}
-    (hst : s ∈ nhdsWithin x t) : DifferentiableWithinAt 𝕜 f t x :=
+    (hst : s ∈ 𝓝[t] x) : DifferentiableWithinAt 𝕜 f t x :=
   (h.hasFDerivWithinAt.mono_of_mem hst).differentiableWithinAt
 #align differentiable_within_at.mono_of_mem DifferentiableWithinAt.mono_of_mem
 
@@ -578,28 +583,14 @@ theorem differentiableWithinAt_univ : DifferentiableWithinAt 𝕜 f univ x ↔ D
 
 theorem differentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
     DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x := by
-  simp only [DifferentiableWithinAt, HasFDerivWithinAt, HasFDerivAtFilter,
-    nhdsWithin_restrict' s ht]
+  simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter ht]
 #align differentiable_within_at_inter differentiableWithinAt_inter
 
 theorem differentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
     DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x := by
-  simp only [DifferentiableWithinAt, HasFDerivWithinAt, HasFDerivAtFilter,
-    nhdsWithin_restrict'' s ht]
+  simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter' ht]
 #align differentiable_within_at_inter' differentiableWithinAt_inter'
 
-theorem DifferentiableWithinAt.antimono (h : DifferentiableWithinAt 𝕜 f s x) (hst : s ⊆ t)
-    (hx : s ∈ 𝓝[t] x) : DifferentiableWithinAt 𝕜 f t x := by
-  rwa [← differentiableWithinAt_inter' hx, inter_eq_self_of_subset_right hst]
-#align differentiable_within_at.antimono DifferentiableWithinAt.antimono
-
-theorem HasFDerivWithinAt.antimono (h : HasFDerivWithinAt f f' s x) (hst : s ⊆ t)
-    (hs : UniqueDiffWithinAt 𝕜 s x) (hx : s ∈ 𝓝[t] x) : HasFDerivWithinAt f f' t x := by
-  have h' : HasFDerivWithinAt f _ t x :=
-    (h.differentiableWithinAt.antimono hst hx).hasFDerivWithinAt
-  rwa [hs.eq h (h'.mono hst)]
-#align has_fderiv_within_at.antimono HasFDerivWithinAt.antimono
-
 theorem DifferentiableAt.differentiableWithinAt (h : DifferentiableAt 𝕜 f x) :
     DifferentiableWithinAt 𝕜 f s x :=
   (differentiableWithinAt_univ.2 h).mono (subset_univ _)
@@ -635,45 +626,31 @@ theorem differentiableOn_of_locally_differentiableOn
   exact (differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩)
 #align differentiable_on_of_locally_differentiable_on differentiableOn_of_locally_differentiableOn
 
+theorem fderivWithin_of_mem (st : t ∈ 𝓝[s] x) (ht : UniqueDiffWithinAt 𝕜 s x)
+    (h : DifferentiableWithinAt 𝕜 f t x) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x :=
+  ((DifferentiableWithinAt.hasFDerivWithinAt h).mono_of_mem st).fderivWithin ht
+#align fderiv_within_of_mem fderivWithin_of_mem
+
 theorem fderivWithin_subset (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x)
     (h : DifferentiableWithinAt 𝕜 f t x) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x :=
-  ((DifferentiableWithinAt.hasFDerivWithinAt h).mono st).fderivWithin ht
+  fderivWithin_of_mem (nhdsWithin_mono _ st self_mem_nhdsWithin) ht h
 #align fderiv_within_subset fderivWithin_subset
 
-theorem fderivWithin_subset' (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (hx : s ∈ 𝓝[t] x)
-    (h : DifferentiableWithinAt 𝕜 f s x) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x :=
-  fderivWithin_subset st ht (h.antimono st hx)
-#align fderiv_within_subset' fderivWithin_subset'
-
-@[simp]
-theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f := by
-  ext x : 1
-  by_cases h : DifferentiableAt 𝕜 f x
-  · apply HasFDerivWithinAt.fderivWithin _ uniqueDiffWithinAt_univ
-    rw [hasFDerivWithinAt_univ]
-    apply h.hasFDerivAt
-  · have : ¬DifferentiableWithinAt 𝕜 f univ x := by rwa [differentiableWithinAt_univ]
-    rw [fderiv_zero_of_not_differentiableAt h, fderivWithin_zero_of_not_differentiableWithinAt this]
-#align fderiv_within_univ fderivWithin_univ
-
-theorem fderivWithin_inter (ht : t ∈ 𝓝 x) (hs : UniqueDiffWithinAt 𝕜 s x) :
-    fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x := by
-  by_cases h : DifferentiableWithinAt 𝕜 f (s ∩ t) x
-  · apply fderivWithin_subset (inter_subset_left _ _) _ ((differentiableWithinAt_inter ht).1 h)
-    apply hs.inter ht
-  · have : ¬DifferentiableWithinAt 𝕜 f s x := by rwa [← differentiableWithinAt_inter ht]
-    rw [fderivWithin_zero_of_not_differentiableWithinAt h,
-      fderivWithin_zero_of_not_differentiableWithinAt this]
+theorem fderivWithin_inter (ht : t ∈ 𝓝 x) : fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x := by
+  simp only [fderivWithin, hasFDerivWithinAt_inter ht]
 #align fderiv_within_inter fderivWithin_inter
 
 theorem fderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x := by
-  have : s = univ ∩ s := by simp only [univ_inter]
-  rw [this, ← fderivWithin_univ]
-  exact fderivWithin_inter h (uniqueDiffOn_univ _ (mem_univ _))
+  simp only [fderiv, fderivWithin, HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.2 h]
 #align fderiv_within_of_mem_nhds fderivWithin_of_mem_nhds
 
+@[simp]
+theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f :=
+  funext fun _ => fderivWithin_of_mem_nhds univ_mem
+#align fderiv_within_univ fderivWithin_univ
+
 theorem fderivWithin_of_open (hs : IsOpen s) (hx : x ∈ s) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x :=
-  fderivWithin_of_mem_nhds (IsOpen.mem_nhds hs hx)
+  fderivWithin_of_mem_nhds (hs.mem_nhds hx)
 #align fderiv_within_of_open fderivWithin_of_open
 
 theorem fderivWithin_eq_fderiv (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableAt 𝕜 f x) :
@@ -798,7 +775,51 @@ end Continuous
 section congr
 
 /-! ### congr properties of the derivative -/
-
+theorem hasFDerivWithinAt_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
+    HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x :=
+  calc
+    HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' (s \ {y}) x :=
+      (hasFDerivWithinAt_diff_singleton _).symm
+    _ ↔ HasFDerivWithinAt f f' (t \ {y}) x := by
+      suffices 𝓝[s \ {y}] x = 𝓝[t \ {y}] x by simp only [HasFDerivWithinAt, this]
+      simpa only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter', diff_eq,
+        inter_comm] using h
+    _ ↔ HasFDerivWithinAt f f' t x := hasFDerivWithinAt_diff_singleton _
+#align has_fderiv_within_at_congr_set' hasFDerivWithinAt_congr_set'
+
+theorem hasFDerivWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
+    HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x :=
+  hasFDerivWithinAt_congr_set' x <| h.filter_mono inf_le_left
+#align has_fderiv_within_at_congr_set hasFDerivWithinAt_congr_set
+
+theorem differentiableWithinAt_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
+    DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x :=
+  exists_congr fun _ => hasFDerivWithinAt_congr_set' _ h
+#align differentiable_within_at_congr_set' differentiableWithinAt_congr_set'
+
+theorem differentiableWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
+    DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x :=
+  exists_congr fun _ => hasFDerivWithinAt_congr_set h
+#align differentiable_within_at_congr_set differentiableWithinAt_congr_set
+
+theorem fderivWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
+    fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := by
+  simp only [fderivWithin, hasFDerivWithinAt_congr_set' y h]
+#align fderiv_within_congr_set' fderivWithin_congr_set'
+
+theorem fderivWithin_congr_set (h : s =ᶠ[𝓝 x] t) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x :=
+  fderivWithin_congr_set' x <| h.filter_mono inf_le_left
+#align fderiv_within_congr_set fderivWithin_congr_set
+
+theorem fderivWithin_eventually_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
+    fderivWithin 𝕜 f s =ᶠ[𝓝 x] fderivWithin 𝕜 f t :=
+  (eventually_nhds_nhdsWithin.2 h).mono fun _ => fderivWithin_congr_set' y
+#align fderiv_within_eventually_congr_set' fderivWithin_eventually_congr_set'
+
+theorem fderivWithin_eventually_congr_set (h : s =ᶠ[𝓝 x] t) :
+    fderivWithin 𝕜 f s =ᶠ[𝓝 x] fderivWithin 𝕜 f t :=
+  fderivWithin_eventually_congr_set' x <| h.filter_mono inf_le_left
+#align fderiv_within_eventually_congr_set fderivWithin_eventually_congr_set
 
 theorem Filter.EventuallyEq.hasStrictFDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) (h' : ∀ y, f₀' y = f₁' y) :
     HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x := by
@@ -853,19 +874,19 @@ theorem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem (h : f₀ =ᶠ[
   h.differentiableWithinAt_iff (h.eq_of_nhdsWithin hx)
 #align filter.eventually_eq.differentiable_within_at_iff_of_mem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem
 
-theorem HasFDerivWithinAt.congr_mono (h : HasFDerivWithinAt f f' s x) (ht : ∀ x ∈ t, f₁ x = f x)
+theorem HasFDerivWithinAt.congr_mono (h : HasFDerivWithinAt f f' s x) (ht : EqOn f₁ f t)
     (hx : f₁ x = f x) (h₁ : t ⊆ s) : HasFDerivWithinAt f₁ f' t x :=
   HasFDerivAtFilter.congr_of_eventuallyEq (h.mono h₁) (Filter.mem_inf_of_right ht) hx
 #align has_fderiv_within_at.congr_mono HasFDerivWithinAt.congr_mono
 
-theorem HasFDerivWithinAt.congr (h : HasFDerivWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x)
+theorem HasFDerivWithinAt.congr (h : HasFDerivWithinAt f f' s x) (hs : EqOn f₁ f s)
     (hx : f₁ x = f x) : HasFDerivWithinAt f₁ f' s x :=
   h.congr_mono hs hx (Subset.refl _)
 #align has_fderiv_within_at.congr HasFDerivWithinAt.congr
 
-theorem HasFDerivWithinAt.congr' (h : HasFDerivWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x)
-    (hx : x ∈ s) : HasFDerivWithinAt f₁ f' s x :=
-  h.congr hs (hs x hx)
+theorem HasFDerivWithinAt.congr' (h : HasFDerivWithinAt f f' s x) (hs : EqOn f₁ f s) (hx : x ∈ s) :
+    HasFDerivWithinAt f₁ f' s x :=
+  h.congr hs (hs hx)
 #align has_fderiv_within_at.congr' HasFDerivWithinAt.congr'
 
 theorem HasFDerivWithinAt.congr_of_eventuallyEq (h : HasFDerivWithinAt f f' s x)
@@ -878,8 +899,8 @@ theorem HasFDerivAt.congr_of_eventuallyEq (h : HasFDerivAt f f' x) (h₁ : f₁
   HasFDerivAtFilter.congr_of_eventuallyEq h h₁ (mem_of_mem_nhds h₁ : _)
 #align has_fderiv_at.congr_of_eventually_eq HasFDerivAt.congr_of_eventuallyEq
 
-theorem DifferentiableWithinAt.congr_mono (h : DifferentiableWithinAt 𝕜 f s x)
-    (ht : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) : DifferentiableWithinAt 𝕜 f₁ t x :=
+theorem DifferentiableWithinAt.congr_mono (h : DifferentiableWithinAt 𝕜 f s x) (ht : EqOn f₁ f t)
+    (hx : f₁ x = f x) (h₁ : t ⊆ s) : DifferentiableWithinAt 𝕜 f₁ t x :=
   (HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt ht hx h₁).differentiableWithinAt
 #align differentiable_within_at.congr_mono DifferentiableWithinAt.congr_mono
 
@@ -913,44 +934,46 @@ theorem DifferentiableAt.congr_of_eventuallyEq (h : DifferentiableAt 𝕜 f x) (
 #align differentiable_at.congr_of_eventually_eq DifferentiableAt.congr_of_eventuallyEq
 
 theorem DifferentiableWithinAt.fderivWithin_congr_mono (h : DifferentiableWithinAt 𝕜 f s x)
-    (hs : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) :
+    (hs : EqOn f₁ f t) (hx : f₁ x = f x) (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) :
     fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x :=
   (HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt hs hx h₁).fderivWithin hxt
 #align differentiable_within_at.fderiv_within_congr_mono DifferentiableWithinAt.fderivWithin_congr_mono
 
-theorem Filter.EventuallyEq.fderivWithin_eq (hs : UniqueDiffWithinAt 𝕜 s x) (hL : f₁ =ᶠ[𝓝[s] x] f)
-    (hx : f₁ x = f x) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
-  if h : DifferentiableWithinAt 𝕜 f s x then
-    HasFDerivWithinAt.fderivWithin (h.hasFDerivWithinAt.congr_of_eventuallyEq hL hx) hs
-  else by
-    have h' : ¬DifferentiableWithinAt 𝕜 f₁ s x :=
-      mt (fun h => h.congr_of_eventuallyEq (hL.mono fun x => Eq.symm) hx.symm) h
-    rw [fderivWithin_zero_of_not_differentiableWithinAt h,
-      fderivWithin_zero_of_not_differentiableWithinAt h']
+theorem Filter.EventuallyEq.fderivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
+    fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := by
+  simp only [fderivWithin, hs.hasFDerivWithinAt_iff hx]
 #align filter.eventually_eq.fderiv_within_eq Filter.EventuallyEq.fderivWithin_eq
 
-theorem Filter.EventuallyEq.fderivWithin_eq_nhds (hs : UniqueDiffWithinAt 𝕜 s x)
-    (hL : f₁ =ᶠ[𝓝 x] f) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
-  (show f₁ =ᶠ[𝓝[s] x] f from nhdsWithin_le_nhds hL).fderivWithin_eq hs (mem_of_mem_nhds hL : _)
+theorem Filter.EventuallyEq.fderiv_within' (hs : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) :
+    fderivWithin 𝕜 f₁ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 f t :=
+  (eventually_nhdsWithin_nhdsWithin.2 hs).mp <|
+    eventually_mem_nhdsWithin.mono fun _y hys hs =>
+      EventuallyEq.fderivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht)
+        (hs.self_of_nhdsWithin hys)
+#align filter.eventually_eq.fderiv_within' Filter.EventuallyEq.fderiv_within'
+
+protected theorem Filter.EventuallyEq.fderivWithin (hs : f₁ =ᶠ[𝓝[s] x] f) :
+    fderivWithin 𝕜 f₁ s =ᶠ[𝓝[s] x] fderivWithin 𝕜 f s :=
+  hs.fderiv_within' Subset.rfl
+#align filter.eventually_eq.fderiv_within Filter.EventuallyEq.fderivWithin
+
+theorem Filter.EventuallyEq.fderivWithin_eq_nhds (h : f₁ =ᶠ[𝓝 x] f) :
+    fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
+  (h.filter_mono nhdsWithin_le_nhds).fderivWithin_eq h.self_of_nhds
 #align filter.eventually_eq.fderiv_within_eq_nhds Filter.EventuallyEq.fderivWithin_eq_nhds
 
-theorem fderivWithin_congr (hs : UniqueDiffWithinAt 𝕜 s x) (hL : ∀ y ∈ s, f₁ y = f y)
-    (hx : f₁ x = f x) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := by
-  apply Filter.EventuallyEq.fderivWithin_eq hs _ hx
-  apply mem_of_superset self_mem_nhdsWithin
-  exact hL
+theorem fderivWithin_congr (hs : EqOn f₁ f s) (hx : f₁ x = f x) :
+    fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
+  (hs.eventuallyEq.filter_mono inf_le_right).fderivWithin_eq hx
 #align fderiv_within_congr fderivWithin_congr
 
-theorem fderivWithin_congr' (hs : UniqueDiffWithinAt 𝕜 s x) (hL : ∀ y ∈ s, f₁ y = f y)
-    (hx : x ∈ s) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
-  fderivWithin_congr hs hL (hL x hx)
+theorem fderivWithin_congr' (hs : EqOn f₁ f s) (hx : x ∈ s) :
+    fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
+  fderivWithin_congr hs (hs hx)
 #align fderiv_within_congr' fderivWithin_congr'
 
-theorem Filter.EventuallyEq.fderiv_eq (hL : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ x = fderiv 𝕜 f x := by
-  have A : f₁ x = f x := hL.eq_of_nhds
-  rw [← fderivWithin_univ, ← fderivWithin_univ]
-  rw [← nhdsWithin_univ] at hL
-  exact hL.fderivWithin_eq uniqueDiffWithinAt_univ A
+theorem Filter.EventuallyEq.fderiv_eq (h : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ x = fderiv 𝕜 f x := by
+  rw [← fderivWithin_univ, ← fderivWithin_univ, h.fderivWithin_eq_nhds]
 #align filter.eventually_eq.fderiv_eq Filter.EventuallyEq.fderiv_eq
 
 protected theorem Filter.EventuallyEq.fderiv (h : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ =ᶠ[𝓝 x] fderiv 𝕜 f :=
@@ -1128,14 +1151,15 @@ open Function
 variable (𝕜 : Type _) {E F : Type _} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F}
 
-theorem support_fderiv_subset : support (fderiv 𝕜 f) ⊆ tsupport f := by
-  intro x
-  rw [← not_imp_not]
-  intro h2x
-  rw [not_mem_tsupport_iff_eventuallyEq] at h2x
-  exact nmem_support.mpr (h2x.fderiv_eq.trans <| fderiv_const_apply 0)
+theorem support_fderiv_subset : support (fderiv 𝕜 f) ⊆ tsupport f := fun x ↦ by
+  rw [← not_imp_not, not_mem_tsupport_iff_eventuallyEq, nmem_support]
+  exact fun hx => hx.fderiv_eq.trans <| fderiv_const_apply 0
 #align support_fderiv_subset support_fderiv_subset
 
+theorem tsupport_fderiv_subset : tsupport (fderiv 𝕜 f) ⊆ tsupport f :=
+  closure_minimal (support_fderiv_subset 𝕜) isClosed_closure
+#align tsupport_fderiv_subset tsupport_fderiv_subset
+
 protected theorem HasCompactSupport.fderiv (hf : HasCompactSupport f) :
     HasCompactSupport (fderiv 𝕜 f) :=
   hf.mono' <| support_fderiv_subset 𝕜