-- 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)
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
let d n := v n - x

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
⊢ 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‖
⊢ Tendsto (fun n => ‖c n‖⁻¹⁻¹) atTop atTop

Tactic:
apply tendsto_inv_nhdsGT_zero.comp

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 (𝓝[>] 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‖
n : ℕ
⊢ 0 ≤ (u n)⁻¹

Tactic:
simp [(u_pos n).le]

Result:
no goals

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‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
n : ℕ
⊢ x + d n ∈ s

Tactic:
simpa [d] using (hv n).1.1

Result:
no goals

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‖
this : Tendsto (fun n => ‖c n‖⁻¹⁻¹) atTop atTop
⊢ Tendsto (fun n => ‖c n‖) atTop atTop

Tactic:
simpa

Result:
no goals

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‖
n : ℕ
⊢ ‖r‖ * (u n * u n) = ‖r‖ * u n * u n

Tactic:
ring

Result:
no goals

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)
A : ∀ (n : ℕ), (s \ {x} ∩ Metric.ball x (u n * u n)).Nonempty
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
choose v hv using A

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)
⊢ 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‖
n : ℕ
⊢ d n ≠ 0

Tactic:
simpa using (M n).2

Result:
no goals

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 ∧ ¬v n = x) ∧ ‖v n - x‖ < u n * u n
⊢ ‖d n‖ ≤ u n * u n

Tactic:
simpa using hv.2.le

Result:
no goals