no goals
ι : Type u_2
κ : Type ?u.8721
R : Type ?u.8724
α : Type u_1
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i => a₂ * f i) (a₂ * a₁)
⊢ HasSum f a₁
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹