α : Type ?u.455352
β : Type ?u.455355
γ : Type ?u.455358
δ : Type ?u.455361
inst✝⁵ : AddCommGroup α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
f : ℕ → M
k : ℕ
a : M
h : HasSum (fun n => f (n + k)) a
⊢ HasSum (f ∘ Subtype.val) a
α : Type ?u.455352
β : Type ?u.455355
γ : Type ?u.455358
δ : Type ?u.455361
inst✝⁵ : AddCommGroup α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
f : ℕ → M
k : ℕ
a : M
h : HasSum (fun n => f (n + k)) a
⊢ HasSum f (∑ i in range k, f i + a)
refine ((range k).hasSum f).add_compl ?_
no goals
α : Type ?u.455352
β : Type ?u.455355
γ : Type ?u.455358
δ : Type ?u.455361
inst✝⁵ : AddCommGroup α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
f : ℕ → M
k : ℕ
a : M
h : HasSum (fun n => f (n + k)) a
⊢ HasSum (f ∘ Subtype.val) a
rwa [← (notMemRangeEquiv k).symm.hasSum_iff]