-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem zero_mem_tangentCone {s : Set E} {x : E} (hx : (𝓝[s \ {x}] x).NeBot) :
    0 ∈ tangentConeAt 𝕜 s x

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
have W n := rescale_to_shell hr (u_pos n) (x := d n) (by simpa using (M n).2)

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
W : ∀ (n : ℕ), ∃ d_1, d_1 ≠ 0 ∧ ‖d_1 • d n‖ < u n ∧ u n / ‖r‖ ≤ ‖d_1 • d n‖ ∧ ‖d_1‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
⊢ 0 ∈ tangentConeAt 𝕜 s x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
n : ℕ
hv : v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
⊢ ‖d n‖ ≤ u n * u n

Tactic:
simp only [mem_inter_iff, mem_diff, mem_singleton_iff, Metric.mem_ball, dist_eq_norm]
  at hv

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
n : ℕ
hv : (v n ∈ s ∧ ¬v n = x) ∧ ‖v n - x‖ < u n * u n
⊢ ‖d n‖ ≤ u n * u n

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
refine ⟨c, d, Eventually.of_forall (fun n ↦ by simpa [d] using (hv n).1.1), c_lim, ?_⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
⊢ Tendsto (fun n => ‖c n‖) atTop atTop

Tactic:
suffices Tendsto (fun n ↦ ‖c n‖⁻¹ ⁻¹) atTop atTop by simpa

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
⊢ Tendsto (fun n => ‖c n‖⁻¹⁻¹) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ :
    ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
  exists_seq_strictAnti_tendsto (0 : ℝ)

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ 0 ∈ tangentConeAt 𝕜 s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
B : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ ‖r‖ * u n
⊢ Tendsto (fun n => ‖c n‖⁻¹) atTop (𝓝 0)

Tactic:
apply squeeze_zero (fun n ↦ by positivity) B

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
B : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ ‖r‖ * u n
⊢ Tendsto (fun t => ‖r‖ * u t) atTop (𝓝 0)