awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
cd : ℕ → R × E
hcd :
  Tendsto ((fun (p : R × E) ↦ p.1 • p.2) ∘ cd) atTop (𝓝 y) ∧
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ (cd n).1) atTop ⊤ ∧
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ (cd n).2) atTop (𝓝 0) ∧
        ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) (cd n).2
⊢ ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)

Tactic:
⟨Prod.fst ∘ cd, Prod.snd ∘ cd, hcd.2.2.1, hcd.2.2.2, hcd.1⟩

Premises used: Function.comp, Prod.fst, And.right, And.left, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
cd : ℕ → R × E
hcd :
  Tendsto ((fun (p : R × E) ↦ p.1 • p.2) ∘ cd) atTop (𝓝 y) ∧
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ (cd n).1) atTop ⊤ ∧
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ (cd n).2) atTop (𝓝 0) ∧
        ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) (cd n).2
⊢ ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)

Tactic:
exact ⟨Prod.fst ∘ cd, Prod.snd ∘ cd, hcd.2.2.1, hcd.2.2.2, hcd.1⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
c : ℕ → R
d : ℕ → E
hd₀ : Tendsto d atTop (𝓝 0)
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt R s x

Tactic:
mem_tangentConeAt_of_seq atTop c d hd₀ hds hcd

Premises used: Filter.atTop, mem_tangentConeAt_of_seq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
c : ℕ → R
d : ℕ → E
hd₀ : Tendsto d atTop (𝓝 0)
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt R s x

Tactic:
exact mem_tangentConeAt_of_seq atTop c d hd₀ hds hcd

Premises used: Filter.atTop, mem_tangentConeAt_of_seq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
α : Type u_3
l : Filter α
c : α → 𝕜
d : α → E
y : E
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
hd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n

Tactic:
have : ∀ᶠ n in l, (c n)⁻¹ • c n • d n = d n :=
    (eventually_ne_of_tendsto_norm_atTop hc 0).mono fun n hn ↦ inv_smul_smul₀ hn (d n)
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
α : Type u_3
l : Filter α
c : α → 𝕜
d : α → E
y : E
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
hd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
this : ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n
⊢ Tendsto c l (Bornology.cobounded 𝕜)

Tactic:
rw [tendsto_norm_atTop_iff_cobounded] at hc

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
α : Type u_3
l : Filter α
c : α → 𝕜
d : α → E
y : E
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
hd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
this : ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n
hc₁ : Tendsto c l (Bornology.cobounded 𝕜)
⊢ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)

Tactic:
rw [tendsto_norm_atTop_iff_cobounded] at hc

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
α : Type u_3
l : Filter α
c : α → 𝕜
d : α → E
y : E
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
hd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
this : ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n
hc₁ : Tendsto c l (Bornology.cobounded 𝕜)
hd₁ : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n

Tactic:
rw [tendsto_norm_atTop_iff_cobounded] at hc

Premises used: tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
α : Type u_3
l : Filter α
c : α → 𝕜
d : α → E
y : E
hc : Tendsto c l (Bornology.cobounded 𝕜)
hd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
this : ∀ᶠ (n : α) in l, (c n)⁻¹ • c n • d n = d n
⊢ Tendsto d l (𝓝 0)

Tactic:
simpa using Tendsto.congr' this <| (tendsto_inv₀_cobounded.comp hc).smul hd

Premises used: Filter.tendsto_inv₀_cobounded, Filter.Tendsto.smul, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
x y : E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
mem_tangentConeAt_of_add_smul_mem
    (tendsto_nhdsWithin_iff.mpr ⟨tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr, ?_⟩) hs

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.intro, mem_tangentConeAt_of_add_smul_mem, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
x y : E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
refine : ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set 𝕜) {0}ᶜ (r ^ n)
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
refine mem_tangentConeAt_of_add_smul_mem
    (tendsto_nhdsWithin_iff.mpr ⟨tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr, ?_⟩) hs

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.intro, mem_tangentConeAt_of_add_smul_mem, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
s : Set E
x y : E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set 𝕜) {0}ᶜ (r ^ n)

Tactic:
simp [hr₀]
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
mp :
  y ∈ tangentConeAt 𝕜 s x →
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
mpr :
  (∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)) →
    y ∈ tangentConeAt 𝕜 s x
⊢ y ∈ tangentConeAt 𝕜 s x ↔
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
mp :
  0 ∈ tangentConeAt 𝕜 s x →
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)
mp₁ :
  ∀ (hy₀ : y ≠ 0),
    y ∈ tangentConeAt 𝕜 s x →
      ∃ (c : ℕ → 𝕜) (d : ℕ → E),
        Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
          (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 s x →
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)

Tactic:
rcases eq_or_ne y 0 with rfl | hy₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
mp :
  x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)
⊢ 0 ∈ tangentConeAt 𝕜 s x →
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)

Tactic:
rw [zero_mem_tangentConeAt_iff]

Premises used: zero_mem_tangentConeAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
mp :
  ∀ (c : 𝕜) (hc : 1 < ‖c‖),
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)
⊢ ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)

Tactic:
obtain ⟨c, hc⟩ := NormedField.exists_lt_norm 𝕜 1

Premises used: NormedField.exists_lt_norm, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
rw :
  ∀ (hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε) (c : 𝕜) (hc : 1 < ‖c‖) (n : ℕ),
    ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n
⊢ ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n

Tactic:
rw [Metric.mem_closure_iff] at hx

Premises used: Metric.mem_closure_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ (1 / (2 * ‖c‖)) ^ n > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
rcases : ∀ (v : E) (hvs : v ∈ s) (hv : dist x v < (1 / (2 * ‖c‖)) ^ n), ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n
⊢ ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n

Tactic:
rcases hx ((1 / (2 * ‖c‖)) ^ n) (by positivity) with ⟨v, hvs, hv⟩

Premises used: Norm.norm, HMul.hMul, HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
v : E
hvs : v ∈ s
hv : dist x v < (1 / (2 * ‖c‖)) ^ n
h : x + (v - x) ∈ s ∧ ‖v - x‖ < (1 / (2 * ‖c‖)) ^ n
⊢ ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n

Tactic:
use v - x
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
v : E
hvs : v ∈ s
hv : dist x v < (1 / (2 * ‖c‖)) ^ n
⊢ x + (v - x) ∈ s ∧ ‖v - x‖ < (1 / (2 * ‖c‖)) ^ n

Tactic:
simp_all [dist_eq_norm_sub']

Premises used: dist_eq_norm_sub'
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ (n : ℕ), ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n

Tactic:
have (n : ℕ) : ∃ d : E, x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n := by
        rw [Metric.mem_closure_iff] at hx
        rcases hx ((1 / (2 * ‖c‖)) ^ n) (by positivity) with ⟨v, hvs, hv⟩
        use v - x
        simp_all [dist_eq_norm_sub']
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
this : ∀ (n : ℕ), ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n
mp :
  ∀ (d : (n : ℕ) → E) (hds : ∀ (n : ℕ), x + d n ∈ s) (hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n),
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)
⊢ ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)

Tactic:
choose d hds hd using this
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)

Tactic:
⟨(c ^ ·), d, ?tendsto_c, .of_forall hds, ?tendsto_cd⟩

Premises used: Filter.Eventually.of_forall, HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
refine : Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm.{u_1} (E := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x)) atTop atTop
refine₁ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
⊢ ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 0)

Tactic:
refine ⟨(c ^ ·), d, ?tendsto_c, .of_forall hds, ?tendsto_cd⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
simp : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c‖ ^ x) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm.{u_1} (E := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x)) atTop atTop

Tactic:
simp only [norm_pow]

Premises used: norm_pow
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c‖ ^ x) atTop atTop

Tactic:
tendsto_pow_atTop_atTop_of_one_lt hc

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c‖ ^ x) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt hc

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm.{u_1} (E := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x)) atTop atTop

Tactic:
case tendsto_c =>
        simp only [norm_pow]
        exact tendsto_pow_atTop_atTop_of_one_lt hc

Premises used: norm_pow, tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
rw :
  ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ Set.Ici ia,
            Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ ib))
              (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x) (d x))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)

Tactic:
rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]

Premises used: Filter.atTop_basis, Filter.HasBasis.tendsto_iff, one_half_lt_one, one_half_pos, Metric.nhds_basis_ball_pow
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ Set.Ici ia,
            Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ ib))
              (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x) (d x))

Tactic:
fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩

Premises used: trivial, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
refine :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : n ∈ Set.Ici N),
        Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ N))
          (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n))
⊢ ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ Set.Ici ia,
            Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ ib))
              (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x) (d x))

Tactic:
refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
h : True
n : ℕ
hn : n ∈ Set.Ici N
⊢ N ≤ n

Tactic:
rw [Set.mem_Ici] at hn

Premises used: Set.mem_Ici
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
h : True
n : ℕ
hn : N ≤ n
this : ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
⊢ Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ N))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n))

Tactic:
simpa [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
h : True
n : ℕ
hn : N ≤ n
suffices : ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
⊢ Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ N))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n))

Tactic:
suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
h : True
n : ℕ
hn : N ≤ n
⊢ 0 < ‖c‖ ^ n

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
h : True
n : ℕ
hn : N ≤ n
rw : ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
⊢ ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N

Tactic:
rw [← lt_div_iff₀' (by positivity)]

Premises used: lt_div_iff₀'
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
h : True
n : ℕ
hn : N ≤ n
⊢ ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n

Tactic:
(hd n).trans_le ?_

Premises used: LT.lt.trans_le