awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
⊢ Summable (α := ℝ) fun (x : ι × ι') ↦ ‖f x.1 * g x.2‖

Tactic:
.of_nonneg_of_le (fun _ ↦ norm_nonneg _)
    (fun x => norm_mul_le (f x.1) (g x.2))
    (hf.mul_of_nonneg hg (fun x => norm_nonneg <| f x) fun x => norm_nonneg <| g x :)

Premises used: HMul.hMul, Summable.of_nonneg_of_le, Prod.fst, Summable.mul_of_nonneg, norm_mul_le, Prod.snd, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
inst_1 : CompleteSpace R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2

Tactic:
(hf.mul_norm hg).of_norm

Premises used: Summable.of_norm, Summable.mul_norm
-- 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 : HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
⊢ Summable (α := R) 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
-- 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
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
apply :
  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)))
⊢ HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))

Tactic:
apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finsetProd_atTop

Premises used: Filter.tendsto_finsetProd_atTop, Summable.mul_norm, hasSum_of_subseq_of_summable
-- 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
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
rw :
  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)))
⊢ 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)))

Tactic:
rw [← prod_atTop_atTop_eq]

Premises used: Filter.prod_atTop_atTop_eq
-- 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
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
⊢ 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)))

Tactic:
have := Tendsto.prodMap h'f.hasSum h'g.hasSum
-- 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
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
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 (β := 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))

Tactic:
rw [← nhds_prod_eq] at this

Premises used: nhds_prod_eq
-- 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
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
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 (p : R × R) ↦ p.1 * p.2) ∘ Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
    ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
    (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i, ∑' (j : ι'), g j).1 (∑' (i : ι), f i, ∑' (j : ι'), g j).2))

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

Premises used: continuous_mul, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
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))
h :
  ∀ (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)
⊢ 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)))

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

Premises used: continuous_mul, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
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)

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

Premises used: Finset.mul_sum, Finset.sum_product, Finset.sum_mul
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
inst_1 : CompleteSpace R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
⊢ HMul.hMul (α := R) (∑' (x : ι), f x) (∑' (y : ι'), g y) = ∑' (z : ι × ι'), f z.1 * g z.2

Tactic:
hf.of_norm.tsum_mul_tsum hg.of_norm (summable_mul_of_summable_norm hf hg)

Premises used: Summable.tsum_mul_tsum, Summable.of_norm, summable_mul_of_summable_norm
-- 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
⊢ HMul.hMul (α := R) (∑' (x : ι), f x) (∑' (y : ι'), g y) = ∑' (z : ι × ι'), f z.1 * g z.2

Tactic:
h'f.tsum_mul_tsum h'g (summable_mul_of_summable_norm' hf h'f hg h'g)

Premises used: Summable.tsum_mul_tsum, summable_mul_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖

Tactic:
have :=
    summable_sum_mul_antidiagonal_of_summable_mul
      (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_1} (E := R) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2)

Tactic:
this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)

Premises used: HMul.hMul, Summable.of_nonneg_of_le, Prod.fst, Prod.snd, Finset.HasAntidiagonal.antidiagonal, norm_nonneg, Finset.sum
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
refine :
  ∀ (n : ℕ),
    norm.{u_1} (E := R) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2) ≤
      ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_1} (E := R) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2)

Tactic:
refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)

Premises used: Summable.of_nonneg_of_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
⊢ norm.{u_1} (E := R) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2) ≤
    ∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f kl.1 * g kl.2‖

Tactic:
norm_sum_le _ _

Premises used: norm_sum_le
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
h : ∀ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f i.1 * g i.2‖ ≤ ‖f i.1‖ * ‖g i.2‖
⊢ LE.le (α := ℝ) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f kl.1 * g kl.2‖)
    (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
i : ℕ × ℕ
h : i ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ ‖f i.1 * g i.2‖ ≤ ‖f i.1‖ * ‖g i.2‖

Tactic:
apply norm_mul_le

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
kl :
  LE.le (α := ℝ) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f kl.1 * g kl.2‖)
    (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖)
⊢ norm.{u_1} (E := R) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2) ≤
    ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖

Tactic:
calc
    ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ :=
      norm_sum_le _ _
    _ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le

Premises used: norm_sum_le, Finset.HasAntidiagonal.antidiagonal
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ ∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2

Tactic:
summable_sum_mul_antidiagonal_of_summable_mul (summable_mul_of_summable_norm' hf h'f hg h'g)

Premises used: summable_sum_mul_antidiagonal_of_summable_mul, summable_mul_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2

Tactic:
hf.of_norm.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg.of_norm (summable_mul_of_summable_norm hf hg)

Premises used: Summable.of_norm, summable_mul_of_summable_norm, Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2

Tactic:
h'f.tsum_mul_tsum_eq_tsum_sum_antidiagonal h'g (summable_mul_of_summable_norm' hf h'f hg h'g)

Premises used: Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal, summable_mul_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
simp_rw :
  Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_1} (E := R) (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_1} (E := R) (∑ k ∈ range (n + 1), f k * g (n - k))

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_1} (E := R) (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2)

Tactic:
summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg

Premises used: summable_norm_sum_mul_antidiagonal_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_1} (E := R) (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2)

Tactic:
exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg

Premises used: summable_norm_sum_mul_antidiagonal_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
simp_rw : Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
⊢ Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
summable_sum_mul_antidiagonal_of_summable_norm' hf h'f hg h'g

Premises used: summable_sum_mul_antidiagonal_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
exact summable_sum_mul_antidiagonal_of_summable_norm' hf h'f hg h'g

Premises used: summable_sum_mul_antidiagonal_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
simp_rw :
  HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg

Premises used: tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg

Premises used: tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ HasSum.{u_1, 0} (α := R) (fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k))
    (∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k))

Tactic:
(summable_norm_sum_mul_range_of_summable_norm hf hg).of_norm.hasSum

Premises used: Summable.of_norm, summable_norm_sum_mul_range_of_summable_norm, Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h : HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)
⊢ HasSum (fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) (HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n))

Tactic:
convert! (summable_norm_sum_mul_range_of_summable_norm hf hg).of_norm.hasSum

Premises used: Summable.of_norm, summable_norm_sum_mul_range_of_summable_norm, Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)

Tactic:
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm hf hg

Premises used: tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm hf hg

Premises used: tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
simp_rw :
  HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' hf h'f hg h'g

Premises used: tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' hf h'f hg h'g

Premises used: tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ HasSum.{u_1, 0} (α := R) (fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k))
    (∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k))

Tactic:
(summable_sum_mul_range_of_summable_norm' hf h'f hg h'g).hasSum

Premises used: summable_sum_mul_range_of_summable_norm', Summable.hasSum