no goals
α : Type u_1
β : Type u_3
γ✝ : Type ?u.282136
δ : Type ?u.282139
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : T3Space α
γ : β → Type u_2
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum g a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
hf' : Summable f
⊢ HasSum f a
simpa [(hf'.hasSum.sigma hf).unique ha] using hf'.hasSum