no goals
α : Type u_1
β : Type ?u.798357
γ : Type ?u.798360
δ : Type ?u.798363
ι : Type u_3
π : α → Type u_2
inst✝¹ : (x : α) → AddCommMonoid (π x)
inst✝ : (x : α) → TopologicalSpace (π x)
f : ι → (x : α) → π x
g : (x : α) → π x
⊢ HasSum f g ↔ ∀ (x : α), HasSum (fun i => f i x) (g x)
simp only [HasSum, tendsto_pi_nhds, sum_apply]