-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem tangentCone_nonempty_of_properSpace [ProperSpace E]
    {s : Set E} {x : E} (hx : (𝓝[s \ {x}] x).NeBot) :
    (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
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‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
B : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * u n
⊢ Tendsto (fun t => 1⁻¹ * ‖r‖ * u t) atTop (𝓝 0)

Tactic:
simpa using u_lim.const_mul _

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
d : ℕ → E := fun n => v n - x
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
have M n : x + d n ∈ s \ {x} := by simpa [d] using (hv n).1

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
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‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
l : E
l_mem : l ∈ Metric.closedBall 0 1 \ Metric.ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n => c n • d n) ∘ φ) atTop (𝓝 l)
⊢ l ∈ tangentConeAt 𝕜 s x

Tactic:
refine ⟨c ∘ φ, d ∘ φ, ?_, ?_, hφ⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.refine_1.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
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‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
l : E
l_mem : l ∈ Metric.closedBall 0 1 \ Metric.ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n => c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s

case intro.intro.intro.intro.intro.intro.intro.refine_1.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
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‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
l : E
l_mem : l ∈ Metric.closedBall 0 1 \ Metric.ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n => c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (fun n => ‖(c ∘ φ) n‖) atTop atTop

Proof state:
case intro.intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
l : E
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n => c n • d n) ∘ φ) atTop (𝓝 l)
l_mem : l = 0
hr : r = 0
⊢ ‖r‖ ≤ 1

Tactic:
simp [hr]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
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‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
l : E
l_mem : l ∈ Metric.closedBall 0 1 \ Metric.ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n => c n • d n) ∘ φ) atTop (𝓝 l)
⊢ l ∈ {0}ᶜ

Tactic:
simp only [mem_compl_iff, mem_singleton_iff]

Result:
case intro.intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace 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)
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‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
c_lim : Tendsto (fun n => ‖c n‖) atTop atTop
l : E
l_mem : l ∈ Metric.closedBall 0 1 \ Metric.ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n => c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ¬l = 0