awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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 : σ →₀ ℕ
⊢ 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)
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
refine_1₂ refine_1₃ refine_1₄ 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
⊢ Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a

Tactic:
rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this

Premises used: add_comm, MvPowerSeries.coeff_add_mul_monomial, MvPowerSeries.coeff_add_monomial_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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 : σ →₀ ℕ
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
⊢ 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:
rw [coeff_mul_monomial, coeff_monomial_mul]

Premises used: MvPowerSeries.coeff_mul_monomial, MvPowerSeries.coeff_monomial_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)
neg : ¬n ≤ m → Eq.{u_2 + 1} (α := R) 0 0
⊢ (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:
split_ifs
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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 : σ →₀ ℕ
h_1 : 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:
apply h
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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 : σ →₀ ℕ
h_1 : ¬n ≤ m
⊢ Eq.{u_2 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)
neg : ¬n ≤ m → Eq.{u_2 + 1} (α := R) 0 0
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)
neg₁ : ¬n ≤ m → Eq.{u_2 + 1} (α := R) 0 0
⊢ (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:
split_ifs <;> [apply h; rfl]
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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) (1 * φ) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
simpa using coeff_add_monomial_mul 0 n φ 1

Premises used: OfNat.ofNat, MvPowerSeries.coeff_add_monomial_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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) (φ * 1) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
simpa using coeff_add_mul_monomial n 0 φ 1

Premises used: MvPowerSeries.coeff_add_mul_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)

Tactic:
simp only [coeff_mul, mul_add, Finset.sum_add_distrib, map_add]

Premises used: Finset.sum_add_distrib, map_add, mul_add, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)

Tactic:
classical simp only [coeff_mul, mul_add, Finset.sum_add_distrib, map_add]

Premises used: Finset.sum_add_distrib, map_add, mul_add, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)

Tactic:
simp only [coeff_mul, add_mul, Finset.sum_add_distrib, map_add]

Premises used: add_mul, Finset.sum_add_distrib, map_add, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)

Tactic:
classical simp only [coeff_mul, add_mul, Finset.sum_add_distrib, map_add]

Premises used: add_mul, Finset.sum_add_distrib, map_add, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * φ₂ * φ₃) : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * (φ₂ * φ₃)) : R)
⊢ φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
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)))
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * φ₂ * φ₃) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * (φ₂ * φ₃)) : R)

Tactic:
simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']

Premises used: Finset.mul_sum, Finset.sum_sigma', Finset.sum_mul, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (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:
aesop (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2)
        a →
      Membership.mem (α := (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) (γ :=
        Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1)
        (match (motive :=
            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (i + k, l) (i, k) :
          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))

Tactic:
aesop (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1)
        a →
      (match (motive :=
          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
          match (motive :=
            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) a with
          | ⟨(_i, j), (k, l)⟩ =>
            Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j) with
        | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (i + k, l) (i, k)) =
        a

Tactic:
aesop (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2)
        a →
      (match (motive :=
          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
          match (motive :=
            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) a with
          | ⟨(i, _j), (k, l)⟩ =>
            Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (i + k, l) (i, k) with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j)) =
        a

Tactic:
aesop (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1)
        a →
      HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((coeff a.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R)
                φ₁ :
              R)
            ((coeff a.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R)
                φ₂ :
              R))
          ((coeff a.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
            R) =
        HMul.hMul (α := R)
          ((coeff
                  (Sigma.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
                      (match (motive :=
                        (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) →
                          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
                        a with
                      | ⟨(_i, j), (k, l)⟩ =>
                        Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j))).1 :
                (a : MvPowerSeries σ R) → R)
              φ₁ :
            R)
          (HMul.hMul (α := R) (β := R)
            ((coeff
                    (Sigma.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
                        (match (motive :=
                          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) →
                            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
                          a with
                        | ⟨(_i, j), (k, l)⟩ =>
                          Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j))).1 :
                  (a : MvPowerSeries σ R) → R)
                φ₂ :
              R)
            ((coeff
                    (Sigma.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
                        (match (motive :=
                          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) →
                            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
                          a with
                        | ⟨(_i, j), (k, l)⟩ =>
                          Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j))).2 :
                  (a : MvPowerSeries σ R) → R)
                φ₃ :
              R))

Tactic:
aesop (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
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)))
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ₁ * φ₂ * φ₃) : R)
    ((coeff n : (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])

Premises used: Finset.mul_sum, add_assoc, mul_assoc, Finset.sum_sigma', Finset.sum_mul, MvPowerSeries.coeff_mul, Finset.sum_nbij'
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (ψ * φ) : R)

Tactic:
simpa only [coeff_mul, mul_comm] using
        sum_antidiagonal_swap n fun a b => coeff a φ * coeff b ψ

Premises used: HMul.hMul, Finsupp.sum_antidiagonal_swap, MvPowerSeries.coeff, mul_comm, DFunLike.coe, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (ψ * φ) : R)

Tactic:
classical
      simpa only [coeff_mul, mul_comm] using
        sum_antidiagonal_swap n fun a b => coeff a φ * coeff b ψ

Premises used: mul_comm, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
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)
⊢ 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)

Tactic:
ext k
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
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
⊢ 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:
simp only [coeff_mul_monomial, coeff_monomial]

Premises used: MvPowerSeries.coeff_mul_monomial, MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
neg₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
pos₂ : ∀ (h₁ : ¬n ≤ k) (h₂ : k = m + n), 0 = a * b
neg₂ : ∀ (h₁ : ¬n ≤ k) (h₂ : ¬k = m + n), Eq.{u_2 + 1} (α := R) 0 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

Tactic:
split_ifs with h₁ h₂ h₃ h₃ h₂
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : k = m + n
⊢ a * b = a * b

Tactic:
rfl