-- Mathlib/Analysis/SpecificLimits/Normed.lean
lemma hasSum_choose_mul_geometric_of_norm_lt_one'
    (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
    HasSum (fun n ↦ (n + k).choose k * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))

Proof state:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

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 omega]

Result:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
this :
  ∑ 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
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑((x + k).choose k)‖ ≤ 2 ^ k * ‖↑(x ^ k)‖

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

Result:
case h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
n : ℕ
hn : k < n
⊢ ‖↑((n + k).choose k)‖ ≤ 2 ^ k * ‖↑(n ^ k)‖

Proof state:
case succ
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
⊢ HasSum (fun n => ↑((n + (k + 1)).choose (k + 1)) * r ^ n) (Ring.inverse (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

Result:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
⊢ Ring.inverse (1 - r) ^ (k + 1 + 1) = (∑' (n : ℕ), ↑((n + k).choose k) * r ^ n) * ∑' (n : ℕ), r ^ n