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
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
rw : (↑((i + k).choose k) : R) * (r ^ i * r ^ (n - i)) = (↑((i + k).choose k) : R) * r ^ n
⊢ (↑((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 + (n - i)) = (↑((i + k).choose k) : R) * r ^ n
Tactic: rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]
-- 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
rw : (↑((i + k).choose k) : R) * (r ^ i * r ^ (n - i)) = (↑((i + k).choose k) : R) * r ^ n
rw₁ : (↑((i + k).choose k) : R) * r ^ (i + (n - i)) = (↑((i + k).choose k) : R) * r ^ n
⊢ (↑((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 ^ n = (↑((i + k).choose k) : R) * r ^ n
Tactic: rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]
-- 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 : ℕ
⊢ (↑((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)
have this : 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)
Tactic: have : ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
            ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n := by
          apply Finset.sum_congr rfl (fun i hi ↦ ?_)
          simp only [Finset.mem_range] at hi
          rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]
-- 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‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = HMul.hMul (α := R) (∑' (n : ℕ), (↑((n + k).choose k) : R) * r ^ n) (∑' (n : ℕ), r ^ n)
have h : (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (1 - r)⁻¹ʳ ^ (k + 1) * ∑' (n : ℕ), r ^ n
Tactic: rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]
-- 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 : (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (1 - r)⁻¹ʳ ^ (k + 1) * ∑' (n : ℕ), r ^ n
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = HMul.hMul (α := R) (∑' (n : ℕ), (↑((n + k).choose k) : R) * r ^ n) (∑' (n : ℕ), r ^ n)
have h₁ : (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ
Tactic: rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]
-- 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 : (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (1 - r)⁻¹ʳ ^ (k + 1) * ∑' (n : ℕ), r ^ n
h₁ : (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = HMul.hMul (α := R) (∑' (n : ℕ), (↑((n + k).choose k) : R) * r ^ n) (∑' (n : ℕ), r ^ n)
have h₂ : (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ = (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ
Tactic: rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
have zero : HasSum (fun (n : ℕ) ↦ (↑((n + 0).choose 0) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ HAdd.hAdd (α := ℕ) 0 1)
Tactic: induction k with
  | zero => simpa using hasSum_geom_series_inverse r hr
  | succ k ih =>
      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
      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
      · have : ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
            ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n := by
          apply Finset.sum_congr rfl (fun i hi ↦ ?_)
          simp only [Finset.mem_range] at hi
          rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]
        simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc]
      · rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
zero : HasSum (fun (n : ℕ) ↦ (↑((n + 0).choose 0) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
have succ : ∀ (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))
Tactic: induction k with
  | zero => simpa using hasSum_geom_series_inverse r hr
  | succ k ih =>
      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
      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
      · have : ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
            ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n := by
          apply Finset.sum_congr rfl (fun i hi ↦ ?_)
          simp only [Finset.mem_range] at hi
          rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]
        simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc]
      · rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : 𝕜) * r ^ n) (1 / (1 - r) ^ (k + 1))
have h : 1 / (1 - r) ^ (k + 1) = (1 - r)⁻¹ʳ ^ (k + 1)
Tactic: convert! hasSum_choose_mul_geometric_of_norm_lt_one' k hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ (↑((n + k).descFactorial k) : R) * r ^ n
have h : ∀ (n : ℕ), (↑((n + k).descFactorial k) : R) * r ^ n = (↑k ! : R) * ((↑((n + k).choose k) : R) * r ^ n)
Tactic: convert! (summable_choose_mul_geometric_of_norm_lt_one k hr).mul_left (k.factorial : R) using
    2 with n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n
have refine : ∀ (k : ℕ) (hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n),
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n
Tactic: refine Nat.strong_induction_on k fun k hk => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
⊢ ∃ (a : ℕ → ℕ), ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
have refine : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
Tactic: refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
have mP : P.Monic
Tactic: have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
mP : P.Monic
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
have dP : P.natDegree = k
Tactic: have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
mP : P.Monic
dP : P.natDegree = k
⊢ (n + k).descFactorial k = Polynomial.eval n P
have this : n + 1 + k - 1 = n + k
Tactic: have : n + 1 + k - 1 = n + k := by lia
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
mP : P.Monic
dP : P.natDegree = k
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
have A : (n + k).descFactorial k = Polynomial.eval n P
Tactic: have A : (n + k).descFactorial k = P.eval n := by
      have : n + 1 + k - 1 = n + k := by lia
      simp [P, ascPochhammer_nat_eq_descFactorial, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
| (n + k).descFactorial k
have rw : Polynomial.eval n
  (HPow.hPow (α := ℕ[X]) X k +
    ∑ i ∈ Finset.range k, HMul.hMul (α := ℕ[X]) ((C : (a : ℕ) → ℕ[X]) (P.coeff i) : ℕ[X]) (HPow.hPow (α := ℕ[X]) X i))
Tactic: rw [A, mP.as_sum, dP]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
have conv_lhs : Polynomial.eval n
    (HPow.hPow (α := ℕ[X]) X k +
      ∑ i ∈ Finset.range k,
        HMul.hMul (α := ℕ[X]) ((C : (a : ℕ) → ℕ[X]) (P.coeff i) : ℕ[X]) (HPow.hPow (α := ℕ[X]) X i)) =
  n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
Tactic: conv_lhs => rw [A, mP.as_sum, dP]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n
have obtain : ∀ (a : ℕ → ℕ) (ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i),
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n
Tactic: obtain ⟨a, ha⟩ : ∃ (a : ℕ → ℕ), ∀ n, (n + k).descFactorial k
      = n ^ k + ∑ i ∈ range k, a i * n ^ i := by
    let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)
    refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
    have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
    have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
    have A : (n + k).descFactorial k = P.eval n := by
      have : n + 1 + k - 1 = n + k := by lia
      simp [P, ascPochhammer_nat_eq_descFactorial, this]
    conv_lhs => rw [A, mP.as_sum, dP]
    simp [eval_finsetSum]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
have apply : Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b
Tactic: apply (summable_descFactorial_mul_geometric_of_norm_lt_one k hr).sub
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b
have apply : ∀ (i : ℕ) (hi : i ∈ Finset.range k),
  Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b
Tactic: apply summable_sum (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b
have simp_rw : Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * (HPow.hPow (α := R) (↑b : R) i * r ^ b)
Tactic: simp_rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * (HPow.hPow (α := R) (↑b : R) i * r ^ b)
have hi₁ : i < k
Tactic: simp only [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n
have this : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
  (↑((n + k).descFactorial k) : R) * r ^ n - ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
Tactic: have : Summable (fun n ↦ (n + k).descFactorial k * r ^ n
      - ∑ i ∈ range k, a i * n ^ (i : ℕ) * r ^ n) := by
    apply (summable_descFactorial_mul_geometric_of_norm_lt_one k hr).sub
    apply summable_sum (fun i hi ↦ ?_)
    simp_rw [mul_assoc]
    simp only [Finset.mem_range] at hi
    exact (hk _ hi).mul_left _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this :
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n
have h : Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n) fun (n : ℕ) ↦
  (↑((n + k).descFactorial k) : R) * r ^ n - ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this :
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
⊢ Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
have h : ∀ (n : ℕ),
  HPow.hPow (α := R) (↑n : R) k * r ^ n =
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
Tactic: ext n
-- 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 (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
have h₁ : ∀ (n : ℕ), HAdd.hAdd (α := R) (↑n : R) 1 = (↑((n + 1).choose 1) : R)
Tactic: convert! hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑n : R) * x ^ n) (x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
have A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
Tactic: have A : HasSum (fun (n : ℕ) ↦ (n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2) := by
    convert! hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n
    simp
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
⊢ HasSum (fun (n : ℕ) ↦ (↑n : R) * x ^ n) (x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
have B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
Tactic: have B : HasSum (fun (n : ℕ) ↦ x ^ n) ((1 - x)⁻¹ʳ) := hasSum_geom_series_inverse x h
-- 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
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ HasSum (fun (n : ℕ) ↦ (↑n : R) * x ^ n) (x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
have h₁ : Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ (↑n : R) * x ^ n) fun (b : ℕ) ↦ HAdd.hAdd (α := R) (↑b : R) 1 * x ^ b - x ^ b
Tactic: convert! A.sub B using 1
-- 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
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
h₁ :
  Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ (↑n : R) * x ^ n) fun (b : ℕ) ↦ HAdd.hAdd (α := R) (↑b : R) 1 * x ^ b - x ^ b
⊢ HasSum (fun (n : ℕ) ↦ (↑n : R) * x ^ n) (x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
have h₂ : x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 = HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ
Tactic: convert! A.sub B using 1
-- 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
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ (↑n : R) * x ^ n) fun (b : ℕ) ↦ HAdd.hAdd (α := R) (↑b : R) 1 * x ^ b - x ^ b
have h₁ : ∀ (n : ℕ), (↑n : R) * x ^ n = HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n - x ^ n
Tactic: ext n
-- 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
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 = HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ
have h₁ : HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2
Tactic: symm