awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
| (r' ^ k) ^ n
have rw : (r' ^ n) ^ k
Tactic: rw [← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ (r' ^ k) ^ n
have conv : IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ (r' ^ n) ^ k
Tactic: conv in (r' ^ _) ^ _ => rw [← pow_mul, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ (r' ^ n) ^ k
have suffices : ∀ (n : ℕ), norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * norm.{u_2} (E := R) 1 * ‖r' ^ n‖
Tactic: suffices ∀ n : ℕ, ‖(n : R)‖ ≤ (r' - 1)⁻¹ * ‖(1 : R)‖ * ‖r' ^ n‖ from
    (isBigO_of_le' _ this).pow _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * norm.{u_2} (E := R) 1 * ‖r' ^ n‖
have rw : norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * norm.{u_2} (E := R) 1
Tactic: rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * norm.{u_2} (E := R) 1
have refine : (↑n : ℝ) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖
Tactic: refine n.norm_cast_le.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
have pos : ∀ (h0 : r₁ = 0),
  IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
Tactic: by_cases h0 : r₁ = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
pos :
  ∀ (h0 : r₁ = 0),
    IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
      r₂ ^ n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
have neg : ∀ (h0 : ¬r₁ = 0),
  IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
Tactic: by_cases h0 : r₁ = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
have pos : ∀ (n : ℕ) (hn : n ≥ 1),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      (fun (x : ℕ) ↦
          Eq.{u_2 + 1} (α := R) ((fun (_x : ℕ) ↦ (0 : R)) x) ((fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) x))
        x}
    n
Tactic: refine (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
have h0₁ : 0 < ‖r₁‖
Tactic: rw [← Ne, ← norm_pos_iff] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
have A : IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦
  (r₂ / ‖r₁‖) ^ n
Tactic: have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
    isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A :
  IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦
    (r₂ / ‖r₁‖) ^ n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n
have neg : IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ ‖r₁‖ ^ n
Tactic: suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
    simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
have pos : ∀ (h0 : r = 0), Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
Tactic: by_cases h0 : r = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
pos : ∀ (h0 : r = 0), Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
have neg : ∀ (h0 : ¬r = 0), Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
Tactic: by_cases h0 : r = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
have hr' : 1 < |r|⁻¹
Tactic: have hr' : 1 < |r|⁻¹ := (one_lt_inv₀ (abs_pos.2 h0)).2 hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
have neg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖HPow.hPow (α := ℝ) (↑x : ℝ) k * r ^ x‖) atTop (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : SeminormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0)
have apply : Tendsto (α := ℕ) (HPow.hPow ‖x‖) atTop (𝓝 0)
Tactic: apply squeeze_zero_norm' (eventually_norm_pow_le x)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
⊢ Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0) ↔ ‖x‖ < 1
have refine : Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0) → ‖x‖ < 1
Tactic: refine ⟨?_, tendsto_pow_atTop_nhds_zero_of_norm_lt_one⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
⊢ Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0) → ‖x‖ < 1
have rw : Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) atTop (𝓝 0) → Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖x‖ ^ n) atTop (𝓝 0)
Tactic: rw [← abs_of_nonneg (norm_nonneg _), ← tendsto_pow_atTop_nhds_zero_iff,
    tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
⊢ Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) atTop (𝓝 0) → Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖x‖ ^ n) atTop (𝓝 0)
have hl : EventuallyEq (β := ℝ) atTop (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) fun (n : ℕ) ↦ ‖x‖ ^ n
Tactic: apply Tendsto.congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
⊢ EventuallyEq (β := ℝ) atTop (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) fun (n : ℕ) ↦ ‖x‖ ^ n
have h : ∀ (n : ℕ) (hn : 1 ≤ n), ‖x ^ n‖ = ‖x‖ ^ n
Tactic: filter_upwards [eventually_ge_atTop 1] with n hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
n : ℕ
hn : 1 ≤ n
⊢ ‖x ^ n‖ = ‖x‖ ^ n
have h : ‖HPow.hPow (β := ℕ) x 1‖ = HPow.hPow (β := ℕ) ‖x‖ 1
Tactic: induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hn IH => simp [pow_succ, IH]
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
n : ℕ
hn : 1 ≤ n
h : ‖HPow.hPow (β := ℕ) x 1‖ = HPow.hPow (β := ℕ) ‖x‖ 1
⊢ ‖x ^ n‖ = ‖x‖ ^ n
have h₁ : ∀ (n : ℕ) (hn : 1 ≤ n) (IH : ‖x ^ n‖ = ‖x‖ ^ n), ‖x ^ (n + 1)‖ = ‖x‖ ^ (n + 1)
Tactic: induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hn IH => simp [pow_succ, IH]
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 / (1 + a ^ n))) atTop (𝓝 1)
have simp_rw : Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ HDiv.hDiv (α := S) (β := S) (1 : S) ((v : (a : R) → S) (1 + a ^ n) : S)) atTop
  (𝓝 1)
Tactic: simp_rw [map_div₀ v, v.map_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ HDiv.hDiv (α := S) (β := S) (1 : S) ((v : (a : R) → S) (1 + a ^ n) : S))
    atTop (𝓝 1)
have apply : Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 + a ^ n)) atTop (𝓝 1)
Tactic: apply one_div_one (G := S) ▸ Tendsto.div tendsto_const_nhds _ one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 + a ^ n)) atTop (𝓝 1)
have h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
Tactic: have h_add := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_add 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 + a ^ n)) atTop (𝓝 1)
have h_sub : Tendsto (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HSub.hSub (α := S) 1 0))
Tactic: have h_sub := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_sub 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 / (1 + a ^ n))) atTop (𝓝 0)
have simp_rw : Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ ((v : (a : R) → S) (a ^ n + 1))⁻¹) atTop (𝓝 0)
Tactic: simp_rw [div_eq_mul_inv, one_mul, map_inv₀, fun n ↦ add_comm 1 (a ^ n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ ((v : (a : R) → S) (a ^ n + 1))⁻¹) atTop (𝓝 0)
have refine : Tendsto.{0, u_3} (β := S)
  (fun (n : ℕ) ↦ HSub.hSub (α := S) (β := S) ((v : (a : R) → S) (a ^ n) : S) ((v : (a : R) → S) 1 : S)) atTop atTop
Tactic: refine (tendsto_atTop_mono (fun n ↦ v.le_add _ _) ?_).inv_tendsto_atTop
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Field R_1
inst_1 : Field S
inst_2 : LinearOrder S
v w : AbsoluteValue R_1 S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
R : Type u_4
inst_6 : NormedRing R
inst_7 : CompleteSpace R
⊢ HasSummableGeomSeries R
have summable_geometric_of_norm_lt_one : ∀ (ξ : R), ‖ξ‖ < 1 → Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ ξ ^ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Field R_1
inst_1 : Field S
inst_2 : LinearOrder S
v w : AbsoluteValue R_1 S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
R : Type u_4
inst_6 : NormedRing R
inst_7 : CompleteSpace R
x : R
hx : ‖x‖ < 1
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
have h1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ ^ n
Tactic: have h1 : Summable fun n : ℕ ↦ ‖x‖ ^ n := summable_geometric_of_lt_one (norm_nonneg _) hx
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
⊢ norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have pos : ∀ (hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n),
  norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
Tactic: by_cases hx : Summable (fun n ↦ x ^ n)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
pos :
  ∀ (hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n),
    norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
⊢ norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have neg : ∀ (hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n),
  norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
Tactic: by_cases hx : Summable (fun n ↦ x ^ n)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have pos : ‖HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
Tactic: rw [hx.tsum_eq_zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ ‖HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have pos : ‖HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
Tactic: simp only [_root_.pow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ ‖HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have pos : norm.{u_4} (E := R) 1 + norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
Tactic: refine le_trans (norm_add_le _ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ norm.{u_4} (E := R) (∑' (b : ℕ), (fun (n : ℕ) ↦ x ^ (n + 1)) b) ≤ (1 - ‖x‖)⁻¹ - 1
have refine : HasSum (fun (b : ℕ) ↦ ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)
Tactic: refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ HasSum (fun (b : ℕ) ↦ ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)
have h₁ : Eq (α := ℝ) 1 (∑ i ∈ Finset.range 1, ‖x‖ ^ i)
Tactic: convert! (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ norm.{u_4} (E := R) 1 + norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have this : norm.{u_4} (E := R) (∑' (b : ℕ), (fun (n : ℕ) ↦ x ^ (n + 1)) b) ≤ (1 - ‖x‖)⁻¹ - 1
Tactic: have : ‖∑' b : ℕ, (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 := by
      refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
      convert! (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)
      simp
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
this : norm.{u_4} (E := R) (∑' (b : ℕ), (fun (n : ℕ) ↦ x ^ (n + 1)) b) ≤ (1 - ‖x‖)⁻¹ - 1
⊢ norm.{u_4} (E := R) 1 + norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have linarith : norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹ < norm.{u_4} (E := R) 1 + norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) →
  1 * norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) - (1 * (1 - ‖x‖)⁻¹ - HMul.hMul (α := ℝ) 1 1) +
      (1 * norm.{u_4} (E := R) 1 - HMul.hMul (α := ℝ) 1 1 + 1 * (1 - ‖x‖)⁻¹ -
        (1 * norm.{u_4} (E := R) 1 + 1 * norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)))) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have neg : 0 ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
Tactic: simp only [tsum_eq_zero_of_not_summable hx, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ 0 ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
⊢ 0 ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have this : 1 ≤ norm.{u_4} (E := R) 1
Tactic: have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
this : 1 ≤ norm.{u_4} (E := R) 1
⊢ 0 ≤ 1 - ‖x‖
have linarith : 1 - ‖x‖ < 0 → ‖x‖ - 1 + (1 - ‖x‖ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
this : 1 ≤ norm.{u_4} (E := R) 1
⊢ 0 ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have this₁ : 0 ≤ (1 - ‖x‖)⁻¹
Tactic: have : 0 ≤ (1 - ‖x‖)⁻¹ := inv_nonneg.2 (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
this_1 : 1 ≤ norm.{u_4} (E := R) 1
this : 0 ≤ (1 - ‖x‖)⁻¹
⊢ 0 ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
have linarith : norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹ < 0 →
  1 - norm.{u_4} (E := R) 1 + (HMul.hMul (α := ℝ) 1 0 - 1 * (1 - ‖x‖)⁻¹) +
      (1 * norm.{u_4} (E := R) 1 - HMul.hMul (α := ℝ) 1 1 + 1 * (1 - ‖x‖)⁻¹ - HMul.hMul (α := ℝ) 1 0) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ (i + 1) = HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1
have rw : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = ∑' (i : ℕ), x ^ i
Tactic: rw [eq_sub_iff_add_eq, (summable_geometric_of_norm_lt_one h).tsum_eq_zero_add,
    pow_zero, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
rw : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = ∑' (i : ℕ), x ^ i
⊢ ∑' (i : ℕ), x ^ (i + 1) = HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1
have rw₁ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)
Tactic: rw [eq_sub_iff_add_eq, (summable_geometric_of_norm_lt_one h).tsum_eq_zero_add,
    pow_zero, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
rw : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = ∑' (i : ℕ), x ^ i
rw₁ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)
⊢ ∑' (i : ℕ), x ^ (i + 1) = HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1
have rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))
Tactic: rw [eq_sub_iff_add_eq, (summable_geometric_of_norm_lt_one h).tsum_eq_zero_add,
    pow_zero, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
rw : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = ∑' (i : ℕ), x ^ i
rw₁ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)
rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))
⊢ ∑' (i : ℕ), x ^ (i + 1) = HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1
have rw₃ : HAdd.hAdd (α := R) 1 (∑' (i : ℕ), x ^ (i + 1)) = HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))
Tactic: rw [eq_sub_iff_add_eq, (summable_geometric_of_norm_lt_one h).tsum_eq_zero_add,
    pow_zero, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)
have simp_rw : Eq.{u_4 + 1} (α := R) (∑' (i : ℕ), x * x ^ i) (∑' (i : ℕ), x ^ (i + 1))
Tactic: simp_rw [← (summable_geometric_of_norm_lt_one h).tsum_mul_left, ← _root_.pow_succ']