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

Tactic:
apply tendsto_inv_nhdsGT_zero.comp

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 (𝓝[>] 0)

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 : ℕ → 𝕜
d : ℕ → 𝕜 := fun n => v n - x
n : ℕ
hv : ∀ (n : ℕ), (v n ∈ s ∧ ¬v n = x) ∧ dist (v n) x < u n
⊢ d n ≠ 0

Tactic:
simpa [d, sub_ne_zero] using (hv n).1.2

Result:
no goals

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
d_ne : ∀ (n : ℕ), d n ≠ 0
⊢ 0 < ‖y‖

Tactic:
simpa using hy

Result:
no goals

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
d_ne : ∀ (n : ℕ), d n ≠ 0
B : ∀ (n : ℕ), ‖d n‖ ≤ u n
n : ℕ
hn : 0 ≤ n
⊢ ¬d n = 0

Tactic:
simpa using d_ne n

Result:
no goals

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 x => ‖d x‖) atTop (𝓝[>] 0)

Tactic:
simp only [nhdsWithin, tendsto_inf, tendsto_principal, mem_Ioi, norm_pos_iff, ne_eq,
  eventually_atTop, ge_iff_le]

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 (𝓝 0) ∧ ∃ a, ∀ (b : ℕ), a ≤ b → ¬d b = 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
d_ne : ∀ (n : ℕ), d n ≠ 0
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
refine ⟨fun n ↦ y * (d n)⁻¹, d, ?_, ?_, ?_⟩

Result:
case inr.intro.intro.intro.refine_1
𝕜 : 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
⊢ ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s

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 => ‖(fun n => y * (d n)⁻¹) n‖) atTop atTop

case inr.intro.intro.intro.refine_3
𝕜 : 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 => (fun n => y * (d n)⁻¹) n • d n) atTop (𝓝 y)

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

Tactic:
exact zero_mem_tangentCone hx

Result:
no goals

Proof state:
case inr.intro.intro.intro.refine_3
𝕜 : 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 => (fun n => y * (d n)⁻¹) n • d n) atTop (𝓝 y)

Tactic:
convert tendsto_const_nhds (α := ℕ) (x := y) with n

Result:
case h.e'_3.h
𝕜 : 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
n : ℕ
⊢ (fun n => y * (d n)⁻¹) n • d n = y

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
d_ne : ∀ (n : ℕ), d n ≠ 0
n : ℕ
⊢ x + d n ∈ s

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

Result:
no goals

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)

Tactic:
exact squeeze_zero (fun n ↦ by positivity) B u_lim

Result:
no goals

Proof state:
case inr.intro.intro.intro.refine_1
𝕜 : 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
⊢ ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s

Tactic:
exact Eventually.of_forall (fun n ↦ by simpa [d] using (hv n).1.1)

Result:
no goals

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
d_ne : ∀ (n : ℕ), d n ≠ 0
B : ∀ (n : ℕ), ‖d n‖ ≤ u n
n : ℕ
⊢ 0 ≤ ‖d n‖

Tactic:
positivity

Result:
no goals