awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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)))
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2
have 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)))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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)))
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2
have 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)))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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)))
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2
have 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)))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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)))
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (hypothesis)
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) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, f kl.1 * g kl.2)
have this : 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 _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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)
have 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‖
Tactic: refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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 : ℕ
⊢ LE.le (α := ℝ) (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f kl.1 * g kl.2‖)
    (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖)
have h : ∀ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, ‖f i.1 * g i.2‖ ≤ ‖f i.1‖ * ‖g i.2‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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 _ AddCommMonoid.toAddMonoid _ n, ‖f kl.1‖ * ‖g kl.2‖
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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) (∑ k ∈ range (n + 1), f k * g (n - k))
have simp_rw : Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_1} (E := R) (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2)
Tactic: simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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 : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)
have simp_rw : Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
Tactic: simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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 : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
have simp_rw : HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
  ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
Tactic: simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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 (fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) (HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n))
have h : HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)
Tactic: convert! (summable_norm_sum_mul_range_of_summable_norm hf hg).of_norm.hasSum
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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 : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
have simp_rw : HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
  ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
Tactic: simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
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 (fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) (HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n))
have h : HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)
Tactic: convert! (summable_sum_mul_range_of_summable_norm' hf h'f hg h'g).hasSum
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Summable f
have refine_1 : ∀ (i : ℕ), 0 ≤ ‖f i‖
Tactic: refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
refine_1 : ∀ (i : ℕ), 0 ≤ ‖f i‖
⊢ Summable f
have refine_2 : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)
Tactic: refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
e : ℤˣ
⊢ ‖(↑e : ℤ)‖₊ = 1
have inl : nnnorm (E := ℤ) (↑1 : ℤ) = 1
Tactic: obtain rfl | rfl := units_eq_one_or e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
e : ℤˣ
inl : nnnorm (E := ℤ) (↑1 : ℤ) = 1
⊢ ‖(↑e : ℤ)‖₊ = 1
have inr : nnnorm (E := ℤ) (↑(-1) : ℤ) = 1
Tactic: obtain rfl | rfl := units_eq_one_or e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
e : ℤˣ
⊢ ‖(↑e : ℤ)‖ = 1
have rw : (↑‖(↑e : ℤ)‖₊ : ℝ) = 1
Tactic: rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
e : ℤˣ
rw : (↑‖(↑e : ℤ)‖₊ : ℝ) = 1
⊢ ‖(↑e : ℤ)‖ = 1
have rw₁ : (↑1 : ℝ) = 1
Tactic: rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
e : ℤˣ
rw : (↑‖(↑e : ℤ)‖₊ : ℝ) = 1
rw₁ : (↑1 : ℝ) = 1
⊢ ‖(↑e : ℤ)‖ = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
n : ℤ
⊢ HAdd.hAdd (α := NNReal) (↑n.toNat : NNReal) (↑(-n).toNat : NNReal) = ‖n‖₊
have rw : (↑(n.toNat + (-n).toNat) : NNReal) = ‖n‖₊
Tactic: rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
n : ℤ
rw : (↑(n.toNat + (-n).toNat) : NNReal) = ‖n‖₊
⊢ HAdd.hAdd (α := NNReal) (↑n.toNat : NNReal) (↑(-n).toNat : NNReal) = ‖n‖₊
have rw₁ : (↑n.natAbs : NNReal) = ‖n‖₊
Tactic: rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Int (goal)
Goal:
n : ℤ
rw : (↑(n.toNat + (-n).toNat) : NNReal) = ‖n‖₊
rw₁ : (↑n.natAbs : NNReal) = ‖n‖₊
⊢ HAdd.hAdd (α := NNReal) (↑n.toNat : NNReal) (↑(-n).toNat : NNReal) = ‖n‖₊
have rw₂ : ‖n‖₊ = ‖n‖₊
Tactic: rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : SeminormedRing 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
σ' : 𝕜₂ →+* 𝕜₁
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomIsometric σ
x : 𝕜₂
⊢ norm.{u_4} (E := 𝕜₁) ((σ' : (a : 𝕜₂) → 𝕜₁) x : 𝕜₁) = ‖x‖
have rw : norm.{u_5} (E := 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) ((σ' : (a : 𝕜₂) → 𝕜₁) x : 𝕜₁) : 𝕜₂) = ‖x‖
Tactic: rw [← RingHomIsometric.norm_map (σ := σ), RingHomInvPair.comp_apply_eq₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : SeminormedRing 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
σ' : 𝕜₂ →+* 𝕜₁
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomIsometric σ
x : 𝕜₂
rw : norm.{u_5} (E := 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) ((σ' : (a : 𝕜₂) → 𝕜₁) x : 𝕜₁) : 𝕜₂) = ‖x‖
⊢ norm.{u_4} (E := 𝕜₁) ((σ' : (a : 𝕜₂) → 𝕜₁) x : 𝕜₁) = ‖x‖
have rw₁ : ‖x‖ = ‖x‖
Tactic: rw [← RingHomIsometric.norm_map (σ := σ), RingHomInvPair.comp_apply_eq₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖
have rw : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 - x.1) * x.2‖
Tactic: rw [mul_sub, sub_mul, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x e : α × α
rw : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 - x.1) * x.2‖
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖
have rw₁ : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 * x.2 - x.1 * x.2)‖
Tactic: rw [mul_sub, sub_mul, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x e : α × α
rw : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 - x.1) * x.2‖
rw₁ : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 * x.2 - x.1 * x.2)‖
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖
have rw₂ : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - x.1 * x.2‖
Tactic: rw [mul_sub, sub_mul, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
have rw : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖
Tactic: calc
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
⊢ Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 * e.2 - (fun (p : α × α) ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)
have this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
Tactic: have : ∀ e : α × α,
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := by
          intro e
          calc
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
⊢ Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 * e.2 - (fun (p : α × α) ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)
have refine : Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1‖ * ‖t.2 - x.2‖ + ‖t.1 - x.1‖ * ‖x.2‖) (𝓝 x) (𝓝 0)
Tactic: refine squeeze_zero (fun e => norm_nonneg _) this ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
⊢ Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1‖ * ‖t.2 - x.2‖ + ‖t.1 - x.1‖ * ‖x.2‖) (𝓝 x) (𝓝 0)
have h : 0 = ‖x.1‖ * ‖x.2 - x.2‖ + ‖x.1 - x.1‖ * ‖x.2‖
Tactic: convert!
          ((continuous_fst.tendsto x).norm.mul
                ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
            (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul tendsto_const_nhds)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (hypothesis)
Goal:
⊢ LipschitzWith (α := ℝ≥0 × ℝ≥0) 2 (toReal ∘ fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2)
have this : Isometry (Prod.map toReal toReal)
Tactic: have : Isometry (Prod.map ((↑) : ℝ≥0 → ℝ) ((↑) : ℝ≥0 → ℝ)) :=
    NNReal.isometry_coe.prodMap NNReal.isometry_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Lemmas (goal)
Goal:
this : Isometry (Prod.map toReal toReal)
⊢ LipschitzWith (α := ℝ≥0 × ℝ≥0) 2 (toReal ∘ fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2)
have h : 2 = HMul.hMul (α := ℝ≥0) 1 1 + HMul.hMul (α := ℝ≥0) 1 1
Tactic: convert!
    (((LipschitzWith.prod_fst.comp this.lipschitz).sub
          (LipschitzWith.prod_snd.comp this.lipschitz)).max_const
      0)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Ultra (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
n : ℕ
⊢ nnnorm.{u_1} (E := R) (↑n : R) ≤ 1
have zero : nnnorm.{u_1} (E := R) (↑0 : R) ≤ 1
Tactic: induction n with
  | zero => simp only [Nat.cast_zero, nnnorm_zero, zero_le]
  | succ n hn => simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
    nnnorm_add_one_le_max_nnnorm_one (n : R)
Cleared hypotheses: n