Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case neg.refine_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
⊢ ContinuousWithinAt (fun y ↦ ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)

pp: case neg.refine_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
⊢ ContinuousWithinAt (fun y ↦ ε * ‖y.2 - y.1‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)

Tactic:
all_goals
    -- common start for both continuity proofs
    have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by grw [inter_subset_right]
    obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by
      simpa [closure_prod_eq] using closure_mono this uv_in
    apply ContinuousWithinAt.mono _ this
    simp only [ContinuousWithinAt]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 ‖f v - f u - (f' v - f' u)‖)

E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ε * ‖y.2 - y.1‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 (ε * ‖v - u‖))