no goals
α : Type u_2
β : Type u_1
γ : Type ?u.29909
δ : Type ?u.29912
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
s : Set β
⊢ HasSum (f ∘ Subtype.val) a ↔ HasSum (Set.indicator s f) a
rw [← Set.indicator_range_comp, Subtype.range_coe,
  hasSum_subtype_iff_of_support_subset Set.support_indicator_subset]