awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ Commute φ ((monomial n : (a : R) → MvPowerSeries σ R) a) ↔
    ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
have rw : (∀ (n_1 : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
        R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
        R)) ↔
  ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
Tactic: rw [commute_iff_eq, MvPowerSeries.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ (∀ (n_1 : σ →₀ ℕ),
      Eq.{u_2 + 1} (α := R)
        ((coeff n_1 : (a : MvPowerSeries σ R) → R)
            (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
          R)
        ((coeff n_1 : (a : MvPowerSeries σ R) → R)
            (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
          R)) ↔
    ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
have refine_1 : ∀
  (h :
    ∀ (n_1 : σ →₀ ℕ),
      Eq.{u_2 + 1} (α := R)
        ((coeff n_1 : (a : MvPowerSeries σ R) → R)
            (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
          R)
        ((coeff n_1 : (a : MvPowerSeries σ R) → R)
            (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
          R))
  (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
Tactic: refine ⟨fun h m => ?_, fun h m => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
refine_1 :
  ∀
    (h :
      ∀ (n_1 : σ →₀ ℕ),
        Eq.{u_2 + 1} (α := R)
          ((coeff n_1 : (a : MvPowerSeries σ R) → R)
              (HMul.hMul (β := MvPowerSeries σ R) φ
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
            R)
          ((coeff n_1 : (a : MvPowerSeries σ R) → R)
              (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
                φ) :
            R))
    (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
⊢ (∀ (n_1 : σ →₀ ℕ),
      Eq.{u_2 + 1} (α := R)
        ((coeff n_1 : (a : MvPowerSeries σ R) → R)
            (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
          R)
        ((coeff n_1 : (a : MvPowerSeries σ R) → R)
            (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
          R)) ↔
    ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
have refine_2 : ∀ (h : ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a) (m : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
      R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
      R)
Tactic: refine ⟨fun h m => ?_, fun h m => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h :
  ∀ (n_1 : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
        R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
        R)
m : σ →₀ ℕ
⊢ Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
have this : Eq.{u_2 + 1} (α := R)
  ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
    R)
  ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
    R)
Tactic: have := h (m + n)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h :
  ∀ (n_1 : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
        R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
        R)
m : σ →₀ ℕ
this :
  Eq.{u_2 + 1} (α := R)
    ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
      R)
    ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
      R)
⊢ Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
have refine_1 : ∀
  (this :
    HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a =
      (coeff (m + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ)),
  Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
Tactic: rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h :
  ∀ (n_1 : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
        R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
        R)
m : σ →₀ ℕ
this :
  Eq.{u_2 + 1} (α := R)
    ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
      R)
    ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
      R)
refine_1 :
  ∀
    (this :
      HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a =
        (coeff (m + n) : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ)),
    Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
⊢ Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
have refine_1₁ : ∀
  (this :
    HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a =
      (coeff (n + m) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ)),
  Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
Tactic: rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h :
  ∀ (n_1 : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
        R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
        R)
m : σ →₀ ℕ
this :
  Eq.{u_2 + 1} (α := R)
    ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
      R)
    ((coeff (m + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
      R)
refine_1 :
  ∀
    (this :
      HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a =
        (coeff (m + n) : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ)),
    Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
refine_1₁ :
  ∀
    (this :
      HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a =
        (coeff (n + m) : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ)),
    Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
⊢ Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
have refine_1₂ : ∀
  (this :
    HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a =
      HMul.hMul (β := R) a ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)),
  Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
Tactic: rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
m : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) :
      R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) :
      R)
have refine_2 : (if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0) =
  if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
Tactic: rw [coeff_mul_monomial, coeff_monomial_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have pos : n ≤ m →
  HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a =
    HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
m : σ →₀ ℕ
pos :
  n ≤ m →
    HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a =
      HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R)
⊢ (if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have neg : ¬n ≤ m → Eq.{u_2 + 1} (α := R) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have pos : n ≤ m →
  HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a =
    HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R)
Tactic: split_ifs <;> [apply h; rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a
m : σ →₀ ℕ
pos :
  n ≤ m →
    HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a =
      HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R)
⊢ (if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have neg : ¬n ≤ m → Eq.{u_2 + 1} (α := R) 0 0
Tactic: split_ifs <;> [apply h; rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
⊢ φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * φ₂ * φ₃) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * (φ₂ * φ₃)) : R)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * φ₂ * φ₃) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * (φ₂ * φ₃)) : R)
have h : Eq.{u_2 + 1} (α := R)
  (∑
    x ∈
      (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
        fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1,
    HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ :
          R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₂ :
          R))
      ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ : R))
  (∑
    x ∈
      (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
        fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2,
    HMul.hMul (α := R)
      ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ : R)
      (HMul.hMul (α := R) (β := R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₂ :
          R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
          R)))
Tactic: simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (∑
      x ∈
        (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ :
            R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₂ :
            R))
        ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
          R))
    (∑
      x ∈
        (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2,
      HMul.hMul (α := R)
        ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ :
          R)
        (HMul.hMul (α := R) (β := R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₂ :
            R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
            R)))
have h : ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
  Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
      ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
        fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1)
      a →
    Membership.mem (α := (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) (γ :=
      Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
      ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
        fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2)
      (match (motive :=
          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) a with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j) :
        (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
Tactic: apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * φ₂ * φ₃) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * (φ₂ * φ₃)) : R)
have h : Eq.{u_2 + 1} (α := R)
  (∑
    x ∈
      (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
        fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1,
    HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ :
          R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₂ :
          R))
      ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ : R))
  (∑
    x ∈
      (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
        fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2,
    HMul.hMul (α := R)
      ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ : R)
      (HMul.hMul (α := R) (β := R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₂ :
          R)
        ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
          R)))
Tactic: classical
  simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']
  apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;> aesop (add simp [add_assoc, mul_assoc])
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
      ((monomial n : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R) =
    (monomial (m + n) : (a : R) → MvPowerSeries σ R) (a * b)
have h : ∀ (k : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R)
    ((coeff k : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
          ((monomial n : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R)) :
      R)
    ((coeff k : (a : MvPowerSeries σ R) → R)
        ((monomial (m + n) : (a : R) → MvPowerSeries σ R) (a * b) : MvPowerSeries σ R) :
      R)
Tactic: ext k
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff k : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
          ((monomial n : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R)) :
      R)
    ((coeff k : (a : MvPowerSeries σ R) → R)
        ((monomial (m + n) : (a : R) → MvPowerSeries σ R) (a * b) : MvPowerSeries σ R) :
      R)
have h : (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
Tactic: simp only [coeff_mul_monomial, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
have pos : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : k = m + n), a * b = a * b
Tactic: split_ifs with h₁ h₂ h₃ h₃ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
pos : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : k = m + n), a * b = a * b
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
have neg : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : ¬k = m + n), a * b = 0
Tactic: split_ifs with h₁ h₂ h₃ h₃ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
pos : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : k = m + n), a * b = a * b
neg : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : ¬k = m + n), a * b = 0
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
have pos₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : k = m + n), 0 * b = a * b
Tactic: split_ifs with h₁ h₂ h₃ h₃ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
pos : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : k = m + n), a * b = a * b
neg : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : ¬k = m + n), a * b = 0
pos₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : k = m + n), 0 * b = a * b
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
have neg₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
Tactic: split_ifs with h₁ h₂ h₃ h₃ h₂