awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
⊢ 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)
have 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)
Tactic: rcases eq_or_ne y 0 with rfl | hy₀
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne y 0 with rfl | hy₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
⊢ 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)
have 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)
Tactic: rw [zero_mem_tangentConeAt_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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 : ℕ → 𝕜) (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)
have 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)
Tactic: obtain ⟨c, hc⟩ := NormedField.exists_lt_norm 𝕜 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
have rw : ∀ (hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε) (c : 𝕜) (hc : 1 < ‖c‖) (n : ℕ), ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n
Tactic: rw [Metric.mem_closure_iff] at hx
Cleared hypotheses: hx, c, hc, n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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 : ℕ
⊢ ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n
have rcases : ∀ (v : E) (hvs : v ∈ s) (hv : dist x v < (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⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
⊢ ∃ (d : E), x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n
have h : x + (v - x) ∈ s ∧ ‖v - x‖ < (1 / (2 * ‖c‖)) ^ n
Tactic: use v - x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
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‖
⊢ ∃ (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)
have this : ∀ (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']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
⊢ ∃ (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)
have 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)
Tactic: choose d hds hd using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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)
have refine : Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm.{u_1} (E := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x)) atTop atTop
Tactic: refine ⟨(c ^ ·), d, ?tendsto_c, .of_forall hds, ?tendsto_cd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
⊢ ∃ (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)
have 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)
Tactic: refine ⟨(c ^ ·), d, ?tendsto_c, .of_forall hds, ?tendsto_cd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
have simp : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c‖ ^ x) atTop atTop
Tactic: simp only [norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have 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))
Tactic: rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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))
have 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))
Tactic: refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
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
⊢ 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))
have hn₁ : N ≤ n
Tactic: rw [Set.mem_Ici] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
⊢ 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))
have suffices : ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
Tactic: suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
⊢ ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
have rw : ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
Tactic: rw [← lt_div_iff₀' (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
have refine : (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
Tactic: refine (hd n).trans_le ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
⊢ (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
have grw : (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 n / ‖c‖ ^ n
Tactic: grw [hn]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
grw : (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 n / ‖c‖ ^ n
⊢ (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
have h₂ : LE.le (α := ℝ) 1 2
Tactic: grw [hn]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have case : ∀ (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: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
case case₁ case₂ :
  ∀ (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)
have case₃ : ∀ (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))
Tactic: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
case case₁ case₂ :
  ∀ (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))
case₃ :
  ∀ (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))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have case₄ : ∀ (N : ℕ),
  True →
    ∀ (n : ℕ) (hn : N ≤ 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: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
case case₁ case₂ :
  ∀ (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))
case₃ :
  ∀ (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))
case₄ :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : N ≤ 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))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have case₅ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
Tactic: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
case case₁ case₂ :
  ∀ (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))
case₃ :
  ∀ (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))
case₄ :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : N ≤ 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))
case₅ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have case₆ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
Tactic: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
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
case case₁ case₂ :
  ∀ (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))
case₃ :
  ∀ (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))
case₄ :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : N ≤ 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))
case₅ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
case₆ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have case₇ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
Tactic: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1