-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
suffices suffices₁ suffices₂ :
  HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
suffices₃ : HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
suffices₄ :
  Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop
    (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
suffices₅ :
  Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2)
    (SProd.sprod (α := Filter (Finset ι)) (β := Filter (Finset ι')) atTop atTop)
    (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
suffices₆ :
  ∀
    (this :
      Tendsto (Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
        ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
        (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 (∑' (b : ι), f b)) (𝓝 (∑' (b : ι'), g b)))),
    Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2)
      (SProd.sprod (α := Filter (Finset ι)) (β := Filter (Finset ι')) atTop atTop)
      (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
suffices₇ :
  ∀
    (this :
      Tendsto (β := R × R) (Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
        ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
        (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))),
    Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2)
      (SProd.sprod (α := Filter (Finset ι)) (β := Filter (Finset ι')) atTop atTop)
      (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
h :
  ∀
    (this :
      Tendsto (β := R × R) (Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
        ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
        (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b)))
    (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ p.1 ×ˢ p.2, f i.1 * g i.2)
      (((fun (p : R × R) ↦ p.1 * p.2) ∘ Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
        p)
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2

Tactic:
classical
  suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable
  let s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
  apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finsetProd_atTop
  rw [← prod_atTop_atTop_eq]
  have := Tendsto.prodMap h'f.hasSum h'g.hasSum
  rw [← nhds_prod_eq] at this
  convert!
    ((continuous_mul (M := R)).continuousAt (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp
      this with
    p
  simp [sum_product, ← mul_sum, ← sum_mul]

Premises used: Finset.mul_sum, nhds_prod_eq, Filter.prod_atTop_atTop_eq, Finset.sum_product, Finset.sum_mul