-- 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:
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))

Tactic:
apply ContinuousWithinAt.mem_closure_image

Result:
case h.refine_2.a.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}
⊢ ContinuousWithinAt f (s ∩ t) x

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)

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}
⊢ (𝓝[s ∩ t] x).NeBot

Tactic:
exact I.mono (nhdsWithin_mono _ diff_subset)

Result:
no goals

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
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ 𝓝[t ∩ (s \ {x})] x ≤ 𝓝[s \ {x}] x

Tactic:
exact nhdsWithin_mono _ inter_subset_right

Result:
no goals

Proof state:
case h.refine_2.a.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}
⊢ ContinuousWithinAt f (s ∩ t) x

Tactic:
apply H'.continuousWithinAt.mono inter_subset_left

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
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

Tactic:
rw [← closure_closure, ← Submodule.topologicalClosure_coe]

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
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure

Proof state:
case h.refine_1.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 ∈ Submodule.span 𝕜 (f '' t)

Tactic:
apply Submodule.subset_span

Result:
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

Proof state:
case h.refine_1
𝕜 : 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 ∈ (Submodule.span 𝕜 (f '' t)).topologicalClosure

Tactic:
apply Submodule.le_topologicalClosure

Result:
case h.refine_1.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 ∈ 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
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ 𝓝[(s ∩ t) \ {x}] x ≤ 𝓝[s \ {x}] x

Tactic:
rw [inter_comm, inter_diff_assoc]

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 : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ 𝓝[t ∩ (s \ {x})] x ≤ 𝓝[s \ {x}] x

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})
⊢ x ∈ closure ((s ∩ t) \ {x})

Tactic:
have B : closure (s ∩ t) \ {x} ⊆ closure ((s ∩ t) \ {x}) := by
  convert closure_diff; exact closure_singleton.symm

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
A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x})
B : closure (s ∩ t) \ {x} ⊆ closure ((s ∩ t) \ {x})
⊢ x ∈ closure ((s ∩ t) \ {x})

Proof state:
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))

Tactic:
by_cases H' : DifferentiableWithinAt 𝕜 f s x

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
⊢ derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))

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))