α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
a x : α
hx1 : abs' x < 1
this : IsCauSeq abs' fun m => a * ∑ n in range m, x ^ n
⊢ IsCauSeq abs' fun m => ∑ n in range m, a * x ^ n
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
a x : α
hx1 : abs' x < 1
⊢ IsCauSeq abs' fun m => ∑ n in range m, a * x ^ n
have : IsCauSeq abs fun m => a * ∑ n in range m, (x ^ n) :=
  (CauSeq.const abs a *
    (show CauSeq α abs from ⟨fun n => ∑ m in range n, x ^ m, isCauSeq_geo_series x hx1⟩)).2
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
a x : α
hx1 : abs' x < 1
this : IsCauSeq abs' fun m => a * ∑ n in range m, x ^ n
⊢ IsCauSeq abs' fun m => ∑ n in range m, a * x ^ n
simpa [mul_sum] using this