-- 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 δ
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:
intros

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
u✝ v✝ : E
⊢ f v✝ - f u✝ - (f' v✝ - f' u✝) = f v✝ - f' v✝ - (f u✝ - f' u✝)

Proof state:
case neg.intro.intro
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 δ
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖

Tactic:
suffices ∀ y ∈ B ∩ closure s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖ from
  mem_nhdsWithin_iff.2 ⟨δ, δ_pos, fun y hy => by simpa using this y hy⟩

Result:
case neg.intro.intro
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 δ
⊢ ∀ y ∈ B ∩ closure s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖

Proof state:
case neg.intro.intro
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'‖ < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖

Tactic:
set B := ball x δ

Result:
case neg.intro.intro
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 δ
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure s] x, ‖f x_1 - f x - f' (x_1 - x)‖ ≤ ε * ‖x_1 - 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 δ
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))
y : E
y_in : y ∈ closure s
⊢ ContinuousWithinAt (f - ⇑f') s y

Tactic:
exact Tendsto.sub (f_cont y y_in) f'.cont.continuousWithinAt

Result:
no goals

Proof state:
case pos
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
⊢ HasFDerivWithinAt f f' (closure s) x

Tactic:
rw [← closure_closure] at hx

Result:
case pos
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 (closure s)
⊢ 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 δ
this : ∀ y ∈ B ∩ closure s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖
y : E
hy : y ∈ ball x δ ∩ closure s
⊢ y ∈ {x_1 | (fun x_2 => ‖f x_2 - f x - f' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}

Tactic:
simpa using this y hy

Result:
no goals

Proof state:
case neg
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
⊢ HasFDerivWithinAt f f' (closure s) x

Tactic:
push_neg at hx

Result:
case neg
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
⊢ HasFDerivWithinAt f f' (closure s) x