no goals
α : Type u_1
β : Type ?u.453865
γ : Type ?u.453868
δ : Type ?u.453871
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) (a - ∑ i in range k, f i) ↔ HasSum f a
simp [hasSum_nat_add_iff]