no goals
α : Type u_3
β : Type u_2
γ : Type u_1
δ : Type ?u.22083
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : γ → β
hg : Injective g
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 0
⊢ HasSum (f ∘ g) a ↔ HasSum f a
simp only [HasSum, Tendsto, comp_apply, hg.map_atTop_finset_sum_eq hf]