-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem tangentCone_eq_univ {s : Set 𝕜} {x : 𝕜} (hx : (𝓝[s \ {x}] x).NeBot) :
    tangentConeAt 𝕜 s x = univ

Proof state:
case inr.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → 𝕜 := fun n => v n - x
d_ne : ∀ (n : ℕ), d n ≠ 0
B : ∀ (n : ℕ), ‖d n‖ ≤ u n
⊢ Tendsto (fun x => ‖d x‖) atTop (𝓝 0) ∧ ∃ a, ∀ (b : ℕ), a ≤ b → ¬d b = 0

Tactic:
refine ⟨?_, 0, fun n hn ↦ by simpa using d_ne n⟩

Result:
case inr.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → 𝕜 := fun n => v n - x
d_ne : ∀ (n : ℕ), d n ≠ 0
B : ∀ (n : ℕ), ‖d n‖ ≤ u n
⊢ Tendsto (fun x => ‖d x‖) atTop (𝓝 0)

Proof state:
case inr.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → 𝕜 := fun n => v n - x
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
have d_ne n : d n ≠ 0 := by
  simp only [mem_inter_iff, mem_diff, mem_singleton_iff, Metric.mem_ball, d] at hv
  simpa [d, sub_ne_zero] using (hv n).1.2

Result:
case inr.intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → 𝕜 := fun n => v n - x
d_ne : ∀ (n : ℕ), d n ≠ 0
⊢ y ∈ tangentConeAt 𝕜 s x

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → 𝕜 := fun n => v n - x
n : ℕ
⊢ d n ≠ 0

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

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
d : ℕ → 𝕜 := fun n => v n - x
n : ℕ
hv : ∀ (n : ℕ), (v n ∈ s ∧ ¬v n = x) ∧ dist (v n) x < u n
⊢ d n ≠ 0

Proof state:
case inr.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → 𝕜 := fun n => v n - x
d_ne : ∀ (n : ℕ), d n ≠ 0
⊢ Tendsto (fun n => ‖y‖ * ‖d n‖⁻¹) atTop atTop

Tactic:
apply (tendsto_const_mul_atTop_of_pos (by simpa using hy)).2

Result:
case inr.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → 𝕜
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → 𝕜 := fun n => v n - x
d_ne : ∀ (n : ℕ), d n ≠ 0
⊢ Tendsto (fun x => ‖d x‖⁻¹) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
⊢ tangentConeAt 𝕜 s x = univ

Tactic:
apply eq_univ_iff_forall.2 (fun y ↦ ?_)

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
⊢ y ∈ tangentConeAt 𝕜 s x