no goals
α : Type u_2
β : Type u_1
γ : Type ?u.256561
δ : Type ?u.256564
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
s t : Set β
hs : IsCompl s t
ha : HasSum (f ∘ Subtype.val) a
hb : HasSum (f ∘ Subtype.val) b
⊢ HasSum f (a + b)
simpa [← hs.compl_eq] using
  (hasSum_subtype_iff_indicator.1 ha).add (hasSum_subtype_iff_indicator.1 hb)