-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem range_derivWithin_subset_closure_span_image
    (f : 𝕜 → F) {s t : Set 𝕜} (h : s ⊆ closure (s ∩ t)) :
    range (derivWithin f s) ⊆ closure (Submodule.span 𝕜 (f '' t))

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
⊢ (𝓝[(s ∩ t) \ {x}] x).NeBot

Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot] at H ⊢

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : x ∈ closure (s \ {x})
H' : DifferentiableWithinAt 𝕜 f s x
⊢ x ∈ closure ((s ∩ t) \ {x})

Proof state:
case h.refine_2.a.hx
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ x ∈ closure (s ∩ t)

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot]

Result:
case h.refine_2.a.hx
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ (𝓝[s ∩ t] x).NeBot

Proof state:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ slope f x y ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure

Tactic:
simp only [slope, vsub_eq_sub, SetLike.mem_coe]

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ (y - x)⁻¹ • (f y - f x) ∈ (Submodule.span 𝕜 (f '' t)).topologicalClosure

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
⊢ range (derivWithin f s) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))

Tactic:
rintro - ⟨x, rfl⟩

Result:
case intro
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : x ∈ closure (s \ {x})
H' : DifferentiableWithinAt 𝕜 f s x
A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x})
B : closure (s ∩ t) \ {x} ⊆ closure ((s ∩ t) \ {x})
⊢ x ∈ closure ((s ∩ t) \ {x})

Tactic:
simpa using A.trans (closure_mono B) H

Result:
no goals

Proof state:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Tactic:
have I : (𝓝[(s ∩ t) \ {x}] x).NeBot := by
  rw [← mem_closure_iff_nhdsWithin_neBot] at H ⊢
  have A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x}) :=
    closure_mono (diff_subset_diff_left h)
  have B : closure (s ∩ t) \ {x} ⊆ closure ((s ∩ t) \ {x}) := by
    convert closure_diff; exact closure_singleton.symm
  simpa using A.trans (closure_mono B) H

Result:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Proof state:
case h.refine_1.a.a
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ f y ∈ f '' t

Tactic:
exact mem_image_of_mem _ hy.1.2

Result:
no goals

Proof state:
case intro
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Tactic:
rcases eq_or_neBot (𝓝[s \ {x}] x) with H|H

Result:
case intro.inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

case intro.inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Proof state:
case h.e'_3.h.e'_4
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : x ∈ closure (s \ {x})
H' : DifferentiableWithinAt 𝕜 f s x
A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x})
⊢ {x} = closure {x}

Tactic:
exact closure_singleton.symm

Result:
no goals

Proof state:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Tactic:
rw [derivWithin_zero_of_not_differentiableWithinAt H']

Result:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Proof state:
case h.refine_2.a
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ f x ∈ closure (f '' t)

Tactic:
suffices A : f x ∈ closure (f '' (s ∩ t)) from
  closure_mono (image_subset _ inter_subset_right) A

Result:
case h.refine_2.a
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ f x ∈ closure (f '' (s ∩ t))