no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.796690
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : AddCommMonoid γ
inst✝ : TopologicalSpace γ
f : β → α
g : β → γ
a : α
b : γ
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun x => (f x, g x)) (a, b)
simp [HasSum, ← prod_mk_sum, Filter.Tendsto.prod_mk_nhds hf hg]