-- Mathlib/Analysis/Calculus/FDeriv/Extend.lean
theorem hasFDerivWithinAt_closure_of_tendsto_fderiv {f : E → F} {s : Set E} {x : E} {f' : E →L[ℝ] F}
    (f_diff : DifferentiableOn ℝ f s) (s_conv : Convex ℝ s) (s_open : IsOpen s)
    (f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y)
    (h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')) :
    HasFDerivWithinAt f f' (closure s) x

Proof state:
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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
⊢ fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z

Tactic:
have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open

Result:
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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderiv ℝ f z - f'‖ < ε
op : IsOpen (B ∩ s)
⊢ fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z

Proof state:
case neg.intro.intro.mk
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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure 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 ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y
⊢ ‖f (u, v).2 - f (u, v).1 - (f' (u, v).2 - f' (u, v).1)‖ ≤ ε * ‖(u, v).2 - (u, v).1‖

Tactic:
refine ContinuousWithinAt.closure_le uv_in ?_ ?_ key

Result:
case neg.intro.intro.mk.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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure 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 ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure 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)

case neg.intro.intro.mk.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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure 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 ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y
⊢ ContinuousWithinAt (fun y => ε * ‖y.2 - y.1‖) ((B ∩ s) ×ˢ (B ∩ s)) (u, v)

Proof state:
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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure 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 ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
⊢ Tendsto (fun y => ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) (𝓝[s] u ×ˢ 𝓝[s] v) (𝓝 ‖f v - f u - (f' v - f' u)‖)

Tactic:
have : ∀ u v, f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by intros; abel

Result:
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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure 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 ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y
this✝ : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
this : ∀ (u v : E), f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u)
⊢ Tendsto (fun y => ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) (𝓝[s] u ×ˢ 𝓝[s] v) (𝓝 ‖f v - f u - (f' v - f' u)‖)

Proof state:
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 s
f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y
h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure 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 ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure s
v_in : v ∈ closure s
u✝ v✝ : E
⊢ f v✝ - f u✝ - (f' v✝ - f' u✝) = f v✝ - f' v✝ - (f u✝ - f' u✝)

Tactic:
abel

Result:
no goals