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

Tactic:
apply Submodule.closure_subset_topologicalClosure_span

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

Tactic:
have A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x}) :=
  closure_mono (diff_subset_diff_left 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
A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x})
⊢ x ∈ closure ((s ∩ t) \ {x})

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

Tactic:
apply mem_closure_of_tendsto this

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))
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x, slope f x x_1 ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure

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

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

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

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

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

Tactic:
exact subset_closure (zero_mem _)

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

Tactic:
have : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x)) := by
  apply Tendsto.mono_left (hasDerivWithinAt_iff_tendsto_slope.1 H'.hasDerivWithinAt)
  rw [inter_comm, inter_diff_assoc]
  exact nhdsWithin_mono _ inter_subset_right

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

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
⊢ Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))

Tactic:
apply Tendsto.mono_left (hasDerivWithinAt_iff_tendsto_slope.1 H'.hasDerivWithinAt)

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

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

Tactic:
simpa [derivWithin_zero_of_isolated H] using subset_closure (zero_mem _)

Result:
no goals

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}
⊢ (y - x)⁻¹ • (f y - f x) ∈ (Submodule.span 𝕜 (f '' t)).topologicalClosure

Tactic:
refine Submodule.smul_mem _ _ (Submodule.sub_mem _ ?_ ?_)

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

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