awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t
this :
  ∀ ⦃x_1 : E × F⦄,
    Membership.mem (γ := Submodule 𝕜 (E × F))
        (Submodule.prod (Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) (Submodule.span 𝕜 (tangentConeAt 𝕜 t y))) x_1 →
      Membership.mem (γ := Submodule 𝕜 (E × F)) (Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) x_1
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F))

Tactic:
(hs.1.prod ht.1).mono this

Premises used: Dense.mono, And.left, Dense.prod
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
ht : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) : Set F) ∧ y ∈ closure[inst_8] t
this :
  ∀ ⦃x_1 : E × F⦄,
    Membership.mem (γ := Submodule 𝕜 (E × F))
        (Submodule.prod (Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) (Submodule.span 𝕜 (tangentConeAt 𝕜 t y))) x_1 →
      Membership.mem (γ := Submodule 𝕜 (E × F)) (Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) x_1
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) : Set (E × F))

Tactic:
exact (hs.1.prod ht.1).mono this

Premises used: Dense.mono, And.left, Dense.prod
-- Module: Mathlib.Analysis.Calculus.TangentCone.Prod
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
s : Set E
t : Set F
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
⊢ UniqueDiffOn 𝕜 (s ×ˢ t)

Tactic:
fun ⟨x, y⟩ h => UniqueDiffWithinAt.prod (hs x h.1) (ht y h.2)

Premises used: UniqueDiffOn, SProd.sprod, UniqueDiffWithinAt, _private.0.UniqueDiffOn.prod.match_1, And.right, And.left, UniqueDiffWithinAt.prod
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
⊢ ∃ (u : ℕ → ℝ), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
obtain :
  ∀ (u : ℕ → ℝ) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ :
      ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ (n : ℕ), ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x

Tactic:
have A n : ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x :=
    accPt_iff_nhds.mp hx _ (closedBall_mem_nhds _ (u_pos n))
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
A : ∀ (n : ℕ), ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x
choose :
  ∀ (v : (n : ℕ) → E) (hv : ∀ (n : ℕ), v n ∈ closedBall x (u n) ∩ s) (hvx : ∀ (n : ℕ), v n ≠ x),
    (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
choose v hv hvx using A
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hv : ∀ (n : ℕ), v n ∈ closedBall x (u n) ∩ s
hvx : ∀ (n : ℕ), v n ≠ x
⊢ ∀ (n : ℕ), v n ∈ closedBall x (u n)

Tactic:
choose hvu hvs using hv
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hv : ∀ (n : ℕ), v n ∈ closedBall x (u n) ∩ s
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
⊢ ∀ (n : ℕ), v n ∈ s

Tactic:
choose hvu hvs using hv
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
n : ℕ
⊢ x + d n ∈ s \ {x}

Tactic:
simp [d, hvs, hvx]
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
⊢ ∀ (n : ℕ), x + d n ∈ s \ {x}

Tactic:
have M n : x + d n ∈ s \ {x} := by simp [d, hvs, hvx]
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
let : ∀ (r : 𝕜) (hr : 1 < ‖r‖), (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
let ⟨r, hr⟩ := exists_one_lt_norm 𝕜
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → 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

Premises used: And.right
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
⊢ ∀ (n : ℕ), ∃ (d_1 : 𝕜), d_1 ≠ 0 ∧ ‖d_1 • d n‖ < 1 ∧ 1 / ‖r‖ ≤ ‖d_1 • d n‖ ∧ ‖d_1‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖

Tactic:
have W n := rescale_to_shell hr zero_lt_one (x := d n) (by simpa using (M n).2)
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
W : ∀ (n : ℕ), ∃ (d_1 : 𝕜), d_1 ≠ 0 ∧ ‖d_1 • d n‖ < 1 ∧ 1 / ‖r‖ ≤ ‖d_1 • d n‖ ∧ ‖d_1‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
choose :
  ∀ (c : (n : ℕ) → 𝕜) (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‖),
    (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
choose c c_ne c_le le_c hc using W
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
apply : IsCompact.{u_2} (X := E) (closedBall 0 1 \ ball 0 (1 / ‖r‖))
apply₁ : ∀ (n : ℕ), Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) (c n • d n)
⊢ ∃ (l : E),
    Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l ∧
      ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)

Tactic:
apply IsCompact.tendsto_subseq _ (fun n ↦ ?_)

Premises used: IsCompact.tendsto_subseq
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
⊢ IsCompact.{u_2} (X := E) (closedBall 0 1 \ ball 0 (1 / ‖r‖))

Tactic:
(isCompact_closedBall 0 1).diff Metric.isOpen_ball

Premises used: Metric.isOpen_ball, IsCompact.diff, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
⊢ IsCompact.{u_2} (X := E) (closedBall 0 1 \ ball 0 (1 / ‖r‖))

Tactic:
exact (isCompact_closedBall 0 1).diff Metric.isOpen_ball

Premises used: Metric.isOpen_ball, IsCompact.diff, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
n : ℕ
⊢ Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) (c n • d n)

Tactic:
simp only [mem_diff, Metric.mem_closedBall, dist_zero_right, (c_le n).le,
      Metric.mem_ball, not_lt, true_and, le_c n]

Premises used: LT.lt.le, Metric.mem_ball, not_lt, Set.mem_diff, Metric.mem_closedBall, dist_zero_right, true_and
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
obtain :
  ∀ (l : E) (l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l) (φ : ℕ → ℕ)
    (φ_strict : StrictMono φ) (hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)),
    (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
obtain ⟨l, l_mem, φ, φ_strict, hφ⟩ :
      ∃ l ∈ Metric.closedBall (0 : E) 1 \ Metric.ball (0 : E) (1 / ‖r‖),
      ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l) := by
    apply IsCompact.tendsto_subseq _ (fun n ↦ ?_)
    · exact (isCompact_closedBall 0 1).diff Metric.isOpen_ball
    simp only [mem_diff, Metric.mem_closedBall, dist_zero_right, (c_le n).le,
      Metric.mem_ball, not_lt, true_and, le_c n]

Premises used: Norm.norm, HDiv.hDiv, Metric.ball, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
⟨l, ?_, ?_⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
refine_1 : l ∈ tangentConeAt 𝕜 s x
refine_2 : Membership.mem (γ := Set E) {0}ᶜ l
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
refine ⟨l, ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
refine_2 : ∀ (l_mem : l = 0), l ∉ closedBall 0 1 \ ball 0 (1 / ‖r‖)
⊢ ¬l = 0

Tactic:
contrapose l_mem
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
l_mem : l = 0
refine_2 : ¬r = 0
⊢ l ∉ closedBall 0 1 \ ball 0 (1 / ‖r‖)

Tactic:
simp only [one_div, l_mem, mem_diff, Metric.mem_closedBall, dist_self, zero_le_one,
      Metric.mem_ball, inv_pos, norm_pos_iff, ne_eq, not_not, true_and]

Premises used: norm_pos_iff, Classical.not_not, inv_pos, ne_eq, Metric.mem_ball, zero_le_one, dist_self, Set.mem_diff, one_div, Metric.mem_closedBall, true_and
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
l_mem : l = 0
refine_2 : ∀ (hr : r = 0), ‖r‖ ≤ 1
⊢ ¬r = 0

Tactic:
contrapose! hr
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
c : (n : ℕ) → 𝕜
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‖
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]
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
refine_1 : Tendsto (d ∘ φ) atTop (𝓝 0)
refine_1₁ : ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s
refine_1₂ : Tendsto (fun (n : ℕ) ↦ (c ∘ φ) n • (d ∘ φ) n) atTop (𝓝 l)
⊢ l ∈ tangentConeAt 𝕜 s x

Tactic:
apply mem_tangentConeAt_of_seq atTop (c ∘ φ) (d ∘ φ)

Premises used: Function.comp, Filter.atTop, mem_tangentConeAt_of_seq
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (d ∘ φ) atTop (𝓝 0)

Tactic:
Tendsto.comp ?_ φ_strict.tendsto_atTop

Premises used: StrictMono.tendsto_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
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‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
refine_1 : Tendsto d atTop (𝓝 0)
⊢ Tendsto (d ∘ φ) atTop (𝓝 0)

Tactic:
refine Tendsto.comp ?_ φ_strict.tendsto_atTop

Premises used: StrictMono.tendsto_atTop, Filter.Tendsto.comp