no goals
R : Type ?u.14
ι : Type u_1
ι' : Type u_2
inst✝ : NormedRing R
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable fun x => ∑' (y : ι'), f (x, y).fst * g (x, y).snd
simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)