-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem summable_mul_of_summable_norm' {f : ι → R} {g : ι' → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    Summable fun x : ι × ι' => f x.1 * g x.2

Proof state:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
⊢ HasSum (fun x => f x.1 * g x.2) ((∑' (i : ι), f i) * ∑' (j : ι'), g j)

Tactic:
apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finset_prod_atTop

Result:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Proof state:
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
⊢ HasSum (fun x => f x.1 * g x.2) ((∑' (i : ι), f i) * ∑' (j : ι'), g j)

Tactic:
let s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2

Result:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
⊢ HasSum (fun x => f x.1 * g x.2) ((∑' (i : ι), f i) * ∑' (j : ι'), g j)

Proof state:
case h.e'_3.h
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) (atTop ×ˢ atTop)
    (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
p : Finset ι × Finset ι'
⊢ ∑ i ∈ p.1 ×ˢ p.2, f i.1 * g i.2 = ((fun p => p.1 * p.2) ∘ Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) p

Tactic:
simp [s, sum_product, ← mul_sum, ← sum_mul]

Result:
no goals

Proof state:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) (atTop ×ˢ atTop)
    (𝓝 (∑' (b : ι), f b) ×ˢ 𝓝 (∑' (b : ι'), g b))
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
rw [← nhds_prod_eq] at this

Result:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) (atTop ×ˢ atTop)
    (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Proof state:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
have := Tendsto.prod_map h'f.hasSum h'g.hasSum

Result:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) (atTop ×ˢ atTop)
    (𝓝 (∑' (b : ι), f b) ×ˢ 𝓝 (∑' (b : ι'), g b))
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Proof state:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
rw [← prod_atTop_atTop_eq]

Result:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Proof state:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) (atTop ×ˢ atTop)
    (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
⊢ Tendsto (fun b => ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
convert ((continuous_mul (M := R)).continuousAt
    (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp this with p

Result:
case h.e'_3.h
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p => p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) (atTop ×ˢ atTop)
    (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
p : Finset ι × Finset ι'
⊢ ∑ i ∈ p.1 ×ˢ p.2, f i.1 * g i.2 = ((fun p => p.1 * p.2) ∘ Prod.map (fun s => ∑ b ∈ s, f b) fun s => ∑ b ∈ s, g b) p

Proof state:
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
⊢ Summable fun x => f x.1 * g x.2

Tactic:
suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable

Result:
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
⊢ HasSum (fun x => f x.1 * g x.2) ((∑' (i : ι), f i) * ∑' (j : ι'), g j)

Proof state:
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
⊢ Summable 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_finset_prod_atTop
rw [← prod_atTop_atTop_eq]
have := Tendsto.prod_map 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 [s, sum_product, ← mul_sum, ← sum_mul]

Result:
no goals