awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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))
apply : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑((n + k).choose k) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑((n + k).choose k) : R) * r ^ n‖

Tactic:
apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr

Premises used: summable_norm_mul_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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))
apply :
  ∀ᶠ (x : ℕ) in atTop, norm (E := ℝ) (↑((x + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(x ^ k) : ℝ)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑((n + k).choose k) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)

Tactic:
apply isBigO_iff.2 ⟨2 ^ k, ?_⟩

Premises used: Iff.mpr, Asymptotics.isBigO_iff, HPow.hPow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ
h : ∀ (hn : k < n), norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)
⊢ n ∈ Set.Ioi k → norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)

Tactic:
(hn : k < n)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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))
h :
  ∀ (n : ℕ) (hn : k < n),
    norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)
⊢ ∀ᶠ (x : ℕ) in atTop, norm (E := ℝ) (↑((x + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(x ^ k) : ℝ)

Tactic:
filter_upwards [Ioi_mem_atTop k] with n (hn : k < n)

Premises used: Filter.Ioi_mem_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
h : (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ norm (E := ℝ) (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * norm (E := ℝ) (↑(n ^ k) : ℝ)

Tactic:
simp only [Real.norm_eq_abs, abs_cast, cast_pow, norm_pow]

Premises used: norm_pow, Nat.abs_cast, Nat.cast_pow, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
h : (n + k).choose k ≤ HPow.hPow (α := ℕ) 2 k * n ^ k
⊢ (↑((n + k).choose k) : ℝ) ≤ HPow.hPow (α := ℝ) 2 k * HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 ≤ 2 * n

Tactic:
lia
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ (2 * n).choose k ≤ (2 * n) ^ k

Tactic:
Nat.choose_le_pow _ _

Premises used: Nat.choose_le_pow
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ (2 * n) ^ k = HPow.hPow (α := ℕ) 2 k * n ^ k

Tactic:
Nat.mul_pow 2 n k

Premises used: Nat.mul_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 * n ^ k

Tactic:
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

Premises used: Nat.choose, HMul.hMul, HAdd.hAdd, Nat.mul_pow, Nat.choose_le_choose, Nat.choose_le_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖

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
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ) ↦ ∑ k_1 ∈ Finset.range (n + 1), (↑((k_1 + k).choose k) : R) * r ^ k_1 * r ^ (n - k_1))
    (HMul.hMul (α := R) (∑' (n : ℕ), (↑((n + k).choose k) : R) * r ^ n) (∑' (n : ℕ), r ^ n))

Tactic:
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)

Premises used: hasSum_sum_range_mul_of_summable_norm', HasSum.summable, summable_norm_geometric_of_norm_lt_one, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
h₁ : (1 - r)⁻¹ʳ ^ (k + 1 + 1) = HMul.hMul (α := R) (∑' (n : ℕ), (↑((n + k).choose k) : R) * r ^ n) (∑' (n : ℕ), r ^ n)
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + (k + 1)).choose (k + 1)) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1 + 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

Premises used: hasSum_sum_range_mul_of_summable_norm', HasSum.summable, summable_norm_geometric_of_norm_lt_one, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ
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
⊢ 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:
apply Finset.sum_congr rfl (fun i hi ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 < n + 1

Tactic:
simp only [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 + (n - i) = n

Tactic:
lia
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
rw₂ rw₃ : (↑((i + k).choose k) : R) * r ^ n = (↑((i + k).choose k) : R) * r ^ n
⊢ (↑((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]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)

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]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ
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)
⊢ (↑((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:
simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc]

Premises used: add_assoc, Nat.sum_range_add_choose, Nat.cast_sum, Finset.sum_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)⁻¹ʳ
h₂ h₃ : (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ = (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)

Tactic:
rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]

Premises used: pow_succ, hasSum_geom_series_inverse, HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
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))
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 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]

Premises used: pow_succ, add_assoc, hasSum_geom_series_inverse, HasSum.tsum_eq, Nat.cast_sum, Nat.zero, Nat.succ, Finset.sum_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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).choose k) : R) * r ^ n

Tactic:
(hasSum_choose_mul_geometric_of_norm_lt_one' k hr).summable

Premises used: HasSum.summable, hasSum_choose_mul_geometric_of_norm_lt_one'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ ∑' (n : ℕ), (↑((n + k).choose k) : R) * r ^ n = (1 - r)⁻¹ʳ ^ (k + 1)

Tactic:
(hasSum_choose_mul_geometric_of_norm_lt_one' k hr).tsum_eq

Premises used: hasSum_choose_mul_geometric_of_norm_lt_one', HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : 𝕜) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))

Tactic:
hasSum_choose_mul_geometric_of_norm_lt_one' k hr

Premises used: hasSum_choose_mul_geometric_of_norm_lt_one'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
h : 1 / (1 - r) ^ (k + 1) = (1 - r)⁻¹ʳ ^ (k + 1)
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + k).choose k) : 𝕜) * r ^ n) (1 / (1 - r) ^ (k + 1))

Tactic:
convert! hasSum_choose_mul_geometric_of_norm_lt_one' k hr

Premises used: hasSum_choose_mul_geometric_of_norm_lt_one'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ 1 / (1 - r) ^ (k + 1) = (1 - r)⁻¹ʳ ^ (k + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ ∑' (n : ℕ), (↑((n + k).choose k) : 𝕜) * r ^ n = 1 / (1 - r) ^ (k + 1)

Tactic:
(hasSum_choose_mul_geometric_of_norm_lt_one k hr).tsum_eq

Premises used: hasSum_choose_mul_geometric_of_norm_lt_one, HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable.{u_4, 0} (α := R) fun (i : ℕ) ↦ (↑k ! : R) * ((↑((i + k).choose k) : R) * r ^ i)

Tactic:
(summable_choose_mul_geometric_of_norm_lt_one k hr).mul_left (k.factorial : R)

Premises used: summable_choose_mul_geometric_of_norm_lt_one, Nat.cast, Summable.mul_left, Nat.factorial
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
h : ∀ (n : ℕ), (↑((n + k).descFactorial k) : R) * r ^ n = (↑k ! : R) * ((↑((n + k).choose k) : R) * r ^ n)
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ (↑((n + k).descFactorial 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

Premises used: summable_choose_mul_geometric_of_norm_lt_one, Nat.cast, Summable.mul_left, Nat.factorial
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
n : ℕ
⊢ (↑((n + k).descFactorial k) : R) * r ^ n = (↑k ! : R) * ((↑((n + k).choose k) : R) * r ^ n)

Tactic:
simp [← mul_assoc, descFactorial_eq_factorial_mul_choose (n + k) k]

Premises used: mul_assoc, HAdd.hAdd, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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

Tactic:
Nat.strong_induction_on k fun k hk => ?_

Premises used: Nat.strong_induction_on
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
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
⊢ 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 => ?_
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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

Tactic:
⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩

Premises used: Polynomial.coeff, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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))
refine : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
⊢ ∃ (a : ℕ → ℕ), ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i

Tactic:
refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ
⊢ P.Monic

Tactic:
have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ P.natDegree = k

Tactic:
simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]

Premises used: Polynomial.natDegree_comp, Polynomial.natDegree_X_add_C, ascPochhammer_natDegree, mul_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ P.natDegree = k

Tactic:
have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 + 1 + k - 1 = n + k

Tactic:
lia
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 + 1 + k - 1 = n + k

Tactic:
have : n + 1 + k - 1 = n + k := by lia
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
this : n + 1 + k - 1 = n + k
⊢ (n + k).descFactorial k = Polynomial.eval n P

Tactic:
simp [P, ascPochhammer_nat_eq_descFactorial, this]

Premises used: ascPochhammer_nat_eq_descFactorial
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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

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]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
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))
| (n + k).descFactorial k

Tactic:
rw [A, mP.as_sum, dP]

Premises used: Polynomial.Monic.as_sum