-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem hasSum_coe_mul_geometric_of_norm_lt_one'
    {x : R} (h : ‖x‖ < 1) :
    HasSum (fun n ↦ n * x ^ n : ℕ → R) (x * (Ring.inverse (1 - x)) ^ 2)

Proof state:
case h.e'_5
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ (fun n => ↑n * x ^ n) = fun b => (↑b + 1) * x ^ b - x ^ b

Tactic:
ext n

Result:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
n : ℕ
⊢ ↑n * x ^ n = (↑n + 1) * x ^ n - x ^ n

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)

Tactic:
convert hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n

Result:
case h.e'_5.h.h.e'_5
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
n : ℕ
⊢ ↑n + 1 = ↑((n + 1).choose 1)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x) =
    Ring.inverse (1 - x) ^ 2 - (1 - x) * Ring.inverse (1 - x) * Ring.inverse (1 - x)

Tactic:
simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun n => ↑n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)

Tactic:
have A : HasSum (fun (n : ℕ) ↦ (n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2) := by
  convert hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n
  simp

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
⊢ HasSum (fun n => ↑n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)

Proof state:
case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x) = x * Ring.inverse (1 - x) ^ 2

Tactic:
calc Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x)
_ = Ring.inverse (1 - x) ^ 2 - ((1 - x) * Ring.inverse (1 - x)) * Ring.inverse (1 - x) := by
  simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]
_ = x * Ring.inverse (1 - x) ^ 2 := by noncomm_ring

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ Ring.inverse (1 - x) ^ 2 - (1 - x) * Ring.inverse (1 - x) * Ring.inverse (1 - x) = x * Ring.inverse (1 - x) ^ 2

Tactic:
noncomm_ring

Result:
no goals

Proof state:
case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ x * Ring.inverse (1 - x) ^ 2 = Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x)

Tactic:
symm

Result:
case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x) = x * Ring.inverse (1 - x) ^ 2

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
⊢ HasSum (fun n => ↑n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)

Tactic:
have B : HasSum (fun (n : ℕ) ↦ x ^ n) (Ring.inverse (1 - x)) := hasSum_geom_series_inverse x h

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ HasSum (fun n => ↑n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ HasSum (fun n => ↑n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)

Tactic:
convert A.sub B using 1

Result:
case h.e'_5
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ (fun n => ↑n * x ^ n) = fun b => (↑b + 1) * x ^ b - x ^ b

case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
⊢ x * Ring.inverse (1 - x) ^ 2 = Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x)

Proof state:
case h.e'_5.h.h.e'_5
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
n : ℕ
⊢ ↑n + 1 = ↑((n + 1).choose 1)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n => (↑n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2)
B : HasSum (fun n => x ^ n) (Ring.inverse (1 - x))
n : ℕ
⊢ ↑n * x ^ n = (↑n + 1) * x ^ n - x ^ n

Tactic:
simp [add_mul]

Result:
no goals