no goals
α : Type ?u.460879
β : Type ?u.460882
γ : Type ?u.460885
δ : Type ?u.460888
inst✝⁶ : AddCommGroup α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : T2Space M
f : ℕ → M
hf : Summable fun n => f (n + 1)
⊢ (∑' (b : ℕ), f b) = f 0 + ∑' (b : ℕ), f (b + 1)
simpa only [sum_range_one] using (sum_add_tsum_nat_add' hf).symm