-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_pow_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
    Summable (fun n ↦ (n : R) ^ k * r ^ n : ℕ → R)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 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

Tactic:
conv_lhs => rw [A, mP.as_sum, dP]

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
⊢ Polynomial.eval n (X ^ k + ∑ i ∈ Finset.range k, C (P.coeff i) * X ^ i) =
    n ^ k + ∑ i ∈ Finset.range k, (fun i => P.coeff i) i * n ^ i

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
⊢ n + 1 + k - 1 = n + k

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ 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 fun b => ↑(a i) * ↑b ^ i * r ^ b

Tactic:
simp_rw [mul_assoc]

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ 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 fun b => ↑(a i) * (↑b ^ i * r ^ b)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun i => P.coeff i) i * n ^ i

Tactic:
have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun i => P.coeff i) i * n ^ i

Proof state:
case intro
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable fun n => ↑n ^ k * 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 _

Result:
case intro
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n => ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
⊢ Summable fun n => ↑n ^ k * r ^ n

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
⊢ Summable fun n => ↑n ^ 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 omega
    simp [P, ascPochhammer_nat_eq_descFactorial, this]
  conv_lhs => rw [A, mP.as_sum, dP]
  simp [eval_finset_sum]

Result:
case intro
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable fun n => ↑n ^ k * r ^ n

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
⊢ P.natDegree = k

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

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
⊢ ∃ 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 ↦ ?_⟩

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun i => P.coeff i) i * n ^ i

Proof state:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n => ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
n : ℕ
⊢ ↑n ^ k * r ^ n = ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n

Tactic:
simp [ha n, add_mul, sum_mul]

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i < k
⊢ Summable fun b => ↑(a i) * (↑b ^ i * r ^ b)

Tactic:
exact (hk _ hi).mul_left _

Result:
no goals

Proof state:
case h.e'_5
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n => ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
⊢ (fun n => ↑n ^ k * r ^ n) = fun n =>
    ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n

Tactic:
ext n

Result:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n => ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n => ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
n : ℕ
⊢ ↑n ^ k * r ^ n = ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n