-- 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 (𝓝 0) ∧ ∃ a, ∀ (b : ℕ), a ≤ b → ¬d b = 0

Tactic:
have B (n : ℕ) : ‖d n‖ ≤ u n := by
  specialize hv n
  simp only [mem_inter_iff, mem_diff, mem_singleton_iff, Metric.mem_ball, dist_eq_norm] at hv
  simpa using hv.2.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
B : ∀ (n : ℕ), ‖d n‖ ≤ u n
⊢ Tendsto (fun x => ‖d x‖) atTop (𝓝 0) ∧ ∃ a, ∀ (b : ℕ), a ≤ b → ¬d b = 0

Proof state:
case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 0
⊢ y ∈ 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 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)
⊢ y ∈ tangentConeAt 𝕜 s x

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

Tactic:
rcases eq_or_ne y 0 with rfl | hy

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

case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
hx : (𝓝[s \ {x}] x).NeBot
y : 𝕜
hy : y ≠ 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 : ℕ → 𝕜
d : ℕ → 𝕜 := fun n => v n - x
d_ne : ∀ (n : ℕ), d n ≠ 0
n : ℕ
hv : (v n ∈ s ∧ ¬v n = x) ∧ ‖v n - x‖ < u n
⊢ ‖d n‖ ≤ u n

Tactic:
simpa using hv.2.le

Result:
no goals

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

Tactic:
choose v hv using A

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)
⊢ 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 : ℕ → 𝕜
d : ℕ → 𝕜 := fun n => v n - x
d_ne : ∀ (n : ℕ), d n ≠ 0
n : ℕ
hv : v n ∈ s \ {x} ∩ Metric.ball x (u n)
⊢ ‖d n‖ ≤ u n

Tactic:
simp only [mem_inter_iff, mem_diff, mem_singleton_iff, Metric.mem_ball, dist_eq_norm] 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
d_ne : ∀ (n : ℕ), d n ≠ 0
n : ℕ
hv : (v n ∈ s ∧ ¬v n = x) ∧ ‖v n - x‖ < u n
⊢ ‖d n‖ ≤ u n

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

Tactic:
simp only [norm_mul, norm_inv]

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

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 : ℕ
⊢ ‖d n‖ ≤ u n

Tactic:
specialize hv n

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
d_ne : ∀ (n : ℕ), d n ≠ 0
n : ℕ
hv : v n ∈ s \ {x} ∩ Metric.ball x (u n)
⊢ ‖d n‖ ≤ u n

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

Tactic:
let d := fun n ↦ v n - x

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

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

Tactic:
have A n : ((s \ {x}) ∩ Metric.ball x (u n)).Nonempty := by
  apply NeBot.nonempty_of_mem hx (inter_mem_nhdsWithin _ (Metric.ball_mem_nhds _ (u_pos n)))

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

Tactic:
apply NeBot.nonempty_of_mem hx (inter_mem_nhdsWithin _ (Metric.ball_mem_nhds _ (u_pos n)))

Result:
no goals

Proof state:
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

Tactic:
simp [mul_assoc, inv_mul_cancel₀ (d_ne n)]

Result:
no goals