awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
have rw : HMul.hMul (α := R) 1 (∑' (i : ℕ), x ^ i) + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
Tactic: rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]
-- 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 : HMul.hMul (α := R) 1 (∑' (i : ℕ), x ^ i) + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
have rw₁ : ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
Tactic: rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]
-- 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 : HMul.hMul (α := R) 1 (∑' (i : ℕ), x ^ i) + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₁ : ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
have rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ (i + 1)) = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
Tactic: rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]
-- 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 : HMul.hMul (α := R) 1 (∑' (i : ℕ), x ^ i) + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₁ : ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ (i + 1)) = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
have rw₃ : ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
Tactic: rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]
-- 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 : HMul.hMul (α := R) 1 (∑' (i : ℕ), x ^ i) + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₁ : ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ (i + 1)) = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₃ : ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
have rw₄ : ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 =
  HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ i) - 1
Tactic: rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]
-- 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 : HMul.hMul (α := R) 1 (∑' (i : ℕ), x ^ i) + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₁ : ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ (i + 1)) = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₃ : ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₄ :
  ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 =
    HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ i) - 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
have rw₅ : ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 =
  ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1
Tactic: rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]
-- 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 - x)⁻¹ʳ
have change : (↑(Units.oneSub x h)⁻¹ : R) = (1 - x)⁻¹ʳ
Tactic: change (Units.oneSub x h)⁻¹ = (1 - x)⁻¹ʳ
-- 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
⊢ (↑(Units.oneSub x h)⁻¹ : R) = (1 - x)⁻¹ʳ
have rw : (↑(Units.oneSub x h) : R)⁻¹ʳ = (1 - x)⁻¹ʳ
Tactic: rw [← Ring.inverse_unit]
-- 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
⊢ HasSum (fun (i : ℕ) ↦ x ^ i) (1 - x)⁻¹ʳ
have h₁ : (1 - x)⁻¹ʳ = ∑' (b : ℕ), x ^ b
Tactic: convert! (summable_geometric_of_norm_lt_one h).hasSum
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ ξ ≠ 1
have contrapose! : ∀ (h : ξ = 1), 1 ≤ ‖ξ‖
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ ξ ^ n) (1 - ξ)⁻¹
have xi_ne_one : ξ ≠ 1
Tactic: have xi_ne_one : ξ ≠ 1 := by
    contrapose! h
    simp [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ HasSum (fun (n : ℕ) ↦ ξ ^ n) (1 - ξ)⁻¹
have A : Tendsto (fun (n : ℕ) ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := K) 0 1 * (ξ - 1)⁻¹))
Tactic: have A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) :=
    ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one h).sub tendsto_const_nhds).mul tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun (n : ℕ) ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := K) 0 1 * (ξ - 1)⁻¹))
⊢ HasSum (fun (n : ℕ) ↦ ξ ^ n) (1 - ξ)⁻¹
have rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)
Tactic: rw [hasSum_iff_tendsto_nat_of_summable_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun (n : ℕ) ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := K) 0 1 * (ξ - 1)⁻¹))
rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)
⊢ HasSum (fun (n : ℕ) ↦ ξ ^ n) (1 - ξ)⁻¹
have rw₁ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖ξ ^ i‖
Tactic: rw [hasSum_iff_tendsto_nat_of_summable_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
⊢ (Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n) ↔ ‖ξ‖ < 1
have refine : ∀ (h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n), ‖ξ‖ < 1
Tactic: refine ⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
⊢ ‖ξ‖ < 1
have obtain : ∀ (k : ℕ) (hk : dist (ξ ^ k) 0 < 1), ‖ξ‖ < 1
Tactic: obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
    (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1
have hk₁ : ‖ξ‖ ^ k < 1
Tactic: simp only [norm_pow, dist_zero_right] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1
have hk₁ : ‖ξ‖ ^ k < HPow.hPow (α := ℝ) 1 k
Tactic: rw [← one_pow k] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖
have rcases : ∀ (r' : ℝ) (hrr' : ‖r‖ < r') (h : r' < 1), Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖
Tactic: rcases exists_between hr with ⟨r', hrr', h⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖
have hrr'₁ : ‖‖r‖‖ < r'
Tactic: rw [← norm_norm] at hrr'
Cleared hypotheses: hrr', h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖
have apply : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ r' ^ n
Tactic: apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ (↑(u n) : ℝ) * ‖r‖ ^ n
have apply : ∀ᶠ (x : ℕ) in atTop, ‖‖(↑(u x) : R) * r ^ x‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u x) : ℝ) * ‖r‖ ^ x‖
Tactic: apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ ∀ᶠ (x : ℕ) in atTop, ‖‖(↑(u x) : R) * r ^ x‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u x) : ℝ) * ‖r‖ ^ x‖
have h₁ : ∀ (n : ℕ) (hn : ‖r ^ n‖ ≤ ‖r‖ ^ n), ‖‖(↑(u n) : R) * r ^ n‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u n) : ℝ) * ‖r‖ ^ n‖
Tactic: filter_upwards [eventually_norm_pow_le r] with n hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖‖(↑(u n) : R) * r ^ n‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u n) : ℝ) * ‖r‖ ^ n‖
have h₁ : ‖(↑(u n) : R) * r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)
Tactic: simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖(↑(u n) : R) * r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)
have h₁ : norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)
Tactic: apply (norm_mul_le _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1 * ‖r‖ ^ n
have h₁ : norm.{u_4} (E := R) (↑(u n) : R) ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)
have this : norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1 * ‖r‖ ^ n
Tactic: have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ) * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n
have simp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n
Tactic: simp only [cast_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ r' ^ n
have fun : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ (↑(u n) : ℝ) * ‖r‖ ^ n
Tactic: calc
  fun n ↦ ‖↑(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ u n * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
      apply (norm_mul_le _ _).trans
      have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
      exact this.trans (le_of_eq (by ring))
  _ =O[atTop] fun n ↦ ↑(n ^ k) * ‖r‖ ^ n := hu.mul (isBigO_refl _ _)
  _ =O[atTop] fun n ↦ r' ^ n := by
      simp only [cast_pow]
      exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
fun : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ (↑(u n) : ℝ) * ‖r‖ ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ r' ^ n
have fun₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ) * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n
Tactic: calc
  fun n ↦ ‖↑(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ u n * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
      apply (norm_mul_le _ _).trans
      have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
      exact this.trans (le_of_eq (by ring))
  _ =O[atTop] fun n ↦ ↑(n ^ k) * ‖r‖ ^ n := hu.mul (isBigO_refl _ _)
  _ =O[atTop] fun n ↦ r' ^ n := by
      simp only [cast_pow]
      exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := R) (↑n : R) k * r ^ n‖
have simp : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(n ^ k) : R) * r ^ n‖
Tactic: simp only [← cast_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖
have apply : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑((n + k).choose k) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
Tactic: apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑((n + k).choose k) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
have apply : ∀ᶠ (x : ℕ) in atTop, norm (E := ℝ) (↑((x + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(x ^ k) : ℝ)
Tactic: apply isBigO_iff.2 ⟨2 ^ k, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
n : ℕ
⊢ n ∈ Set.Ioi k → norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)
have h : ∀ (hn : k < n), norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)
Tactic: (hn : k < n)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := ℝ) (↑((x + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(x ^ k) : ℝ)
have h : ∀ (n : ℕ) (hn : k < n), norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)
Tactic: filter_upwards [Ioi_mem_atTop k] with n (hn : k < n)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
n : ℕ
hn : k < n
⊢ norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)
have h : (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * HPow.hPow (α := ℝ) (↑n : ℝ) k
Tactic: simp only [Real.norm_eq_abs, abs_cast, cast_pow, norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
n : ℕ
hn : k < n
⊢ (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * HPow.hPow (α := ℝ) (↑n : ℝ) k
have h : (n + k).choose k ≤ HPow.hPow (α := ℕ) 2 k * n ^ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + (k + 1)).choose (k + 1)) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1 + 1))
have I1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖
Tactic: have I1 : Summable (fun (n : ℕ) ↦ ‖(n + k).choose k * r ^ n‖) := by
        apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr
        apply isBigO_iff.2 ⟨2 ^ k, ?_⟩
        filter_upwards [Ioi_mem_atTop k] with n (hn : k < n)
        simp only [Real.norm_eq_abs, abs_cast, cast_pow, norm_pow]
        norm_cast
        calc (n + k).choose k
          _ ≤ (2 * n).choose k := choose_le_choose k (by lia)
          _ ≤ (2 * n) ^ k := Nat.choose_le_pow _ _
          _ = 2 ^ k * n ^ k := Nat.mul_pow 2 n k
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + (k + 1)).choose (k + 1)) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1 + 1))
have h : ∀ (n : ℕ),
  (↑((n + (k + 1)).choose (k + 1)) : R) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), (↑((k_1 + k).choose k) : R) * r ^ k_1 * r ^ (n - k_1)
Tactic: convert!
        hasSum_sum_range_mul_of_summable_norm' I1 ih.summable
          (summable_norm_geometric_of_norm_lt_one hr) (summable_geometric_of_norm_lt_one hr) with
        n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖
h :
  ∀ (n : ℕ),
    (↑((n + (k + 1)).choose (k + 1)) : R) * r ^ n =
      ∑ k_1 ∈ Finset.range (n + 1), (↑((k_1 + k).choose k) : R) * r ^ k_1 * r ^ (n - k_1)
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + (k + 1)).choose (k + 1)) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1 + 1))
have h₁ : (1 - r)⁻¹ʳ ^ (k + 1 + 1) = HMul.hMul (α := R) (∑' (n : ℕ), (↑((n + k).choose k) : R) * r ^ n) (∑' (n : ℕ), r ^ n)
Tactic: convert!
        hasSum_sum_range_mul_of_summable_norm' I1 ih.summable
          (summable_norm_geometric_of_norm_lt_one hr) (summable_geometric_of_norm_lt_one hr) with
        n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖
n : ℕ
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ Finset.range (n + 1), (↑((i + k).choose k) : R) * r ^ i * r ^ (n - i))
    (∑ i ∈ Finset.range (n + 1), (↑((i + k).choose k) : R) * r ^ n)
have apply : ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)),
  (↑((i + k).choose k) : R) * r ^ i * r ^ (n - i) = (↑((i + k).choose k) : R) * r ^ n
Tactic: apply Finset.sum_congr rfl (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (↑((i + k).choose k) : R) * r ^ i * r ^ (n - i) = (↑((i + k).choose k) : R) * r ^ n
have hi₁ : i < n + 1
Tactic: simp only [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ (↑((i + k).choose k) : R) * r ^ i * r ^ (n - i) = (↑((i + k).choose k) : R) * r ^ n
have rw : (↑((i + k).choose k) : R) * (r ^ i * r ^ (n - i)) = (↑((i + k).choose k) : R) * r ^ n
Tactic: rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]