awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
rw rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
          MvPowerSeries σ R) :
      R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
    (0 : R)

Tactic:
classical
  rw [monomial_def]
  exact Pi.single_eq_of_ne h _

Premises used: MvPowerSeries.monomial_def
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a : R
h :
  Ne.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
    (0 : R)
⊢ m = n

Tactic:
by_contra fun h' => h <| coeff_monomial_ne h' a

Premises used: by_contra, MvPowerSeries.coeff_monomial_ne
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
⊢ coeff n ∘ₗ monomial n = LinearMap.id

Tactic:
LinearMap.ext <| coeff_monomial_same n

Premises used: LinearMap.ext, MvPowerSeries.coeff_monomial_same
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R) (0 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ f = 0 ↔ ∀ (d : σ →₀ ℕ), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
MvPowerSeries.ext_iff

Premises used: MvPowerSeries.ext_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ (d : σ →₀ ℕ), Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
simp only [MvPowerSeries.ext_iff, ne_eq, coeff_zero, not_forall]

Premises used: MvPowerSeries.coeff_zero, MvPowerSeries.ext_iff, ne_eq, Classical.not_forall
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
inst_1 : DecidableEq σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) (if n = 0 then 1 else 0 : R)

Tactic:
coeff_monomial _ _ _

Premises used: MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) 1 : R) (1 : R)

Tactic:
coeff_monomial_same 0 1

Premises used: MvPowerSeries.coeff_monomial_same, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq (α := MvPowerSeries σ R) ((monomial 0 : (a : R) → MvPowerSeries σ R) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R) ((monomial 0 : (a : R) → MvPowerSeries σ R) (↑0 : R)) 0

Tactic:
simp [Nat.cast]

Premises used: Nat.cast
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
⊢ ∀ (n : ℕ),
    (monomial 0 : (a : R) → MvPowerSeries σ R) (↑(n + 1) : R) =
      HAdd.hAdd (α := MvPowerSeries σ R) ((monomial 0 : (a : R) → MvPowerSeries σ R) (↑n : R)) 1

Tactic:
simp [Nat.cast, monomial_zero_one]

Premises used: Nat.cast, MvPowerSeries.monomial_zero_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst_1 : DecidableEq σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R) :
      R)

Tactic:
Finset.sum_congr ?_ fun _ _ => rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum_congr, Finset.sum, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst_1 : DecidableEq σ
refine : @antidiagonal _ Finsupp.instAddMonoid _ n = @antidiagonal _ Finsupp.instAddMonoid _ n
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R) :
      R)

Tactic:
refine Finset.sum_congr ?_ fun _ _ => rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst_1 : DecidableEq σ
rw rw₁ : @antidiagonal _ Finsupp.instAddMonoid _ n = @antidiagonal _ Finsupp.instAddMonoid _ n
⊢ @antidiagonal _ Finsupp.instAddMonoid _ n = @antidiagonal _ Finsupp.instAddMonoid _ n

Tactic:
rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›]

Premises used: Subsingleton.elim, Classical.decEq
-- 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) (0 * φ) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
simp [coeff_mul]

Premises used: 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) (0 * φ) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
classical simp [coeff_mul]

Premises used: 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) (φ * 0) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
simp [coeff_mul]

Premises used: 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) (φ * 0) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
classical simp [coeff_mul]

Premises used: MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R)
          ((coeff p.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
        0 →
      p.1 = n

Tactic:
have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this :
  ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R)
          ((coeff p.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
        0 →
      p.1 = n
rw :
  (if n ≤ m then
      ∑ x ∈ {(n, m - n)},
        HMul.hMul (α := R) (β := R)
          ((coeff x.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)
    else
      ∑ x ∈ ∅,
        HMul.hMul (α := R) (β := R)
          ((coeff x.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0

Tactic:
rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n,
    Finset.sum_ite_index]

Premises used: Finset.filter_fst_eq_antidiagonal, Finset.sum_filter_of_ne, Finset.sum_ite_index, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this :
  ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R)
          ((coeff p.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
        0 →
      p.1 = n
⊢ (if n ≤ m then
      ∑ x ∈ {(n, m - n)},
        HMul.hMul (α := R) (β := R)
          ((coeff x.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)
    else
      ∑ x ∈ ∅,
        HMul.hMul (α := R) (β := R)
          ((coeff x.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0

Tactic:
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Premises used: MvPowerSeries.coeff_monomial_same, Finset.sum_singleton, Finset.sum_empty
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
have have₁ have₂ :
  ∀
    (this :
      ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
        HMul.hMul (α := R) (β := R)
              ((coeff p.1 : (a : MvPowerSeries σ R) → R)
                  ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
                R)
              ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
            0 →
          p.1 = n),
    (coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
      if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have₃ :
  ∀
    (this :
      ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
        HMul.hMul (α := R) (β := R)
              ((coeff p.1 : (a : MvPowerSeries σ R) → R)
                  ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
                R)
              ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
            0 →
          p.1 = n),
    (if n ≤ m then
        ∑ x ∈ {(n, m - n)},
          HMul.hMul (α := R) (β := R)
            ((coeff x.1 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)
      else
        ∑ x ∈ ∅,
          HMul.hMul (α := R) (β := R)
            ((coeff x.1 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)) =
      if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0

Tactic:
classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n,
    Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Premises used: MvPowerSeries.coeff_monomial_same, Finset.sum_singleton, Finset.sum_empty, Finset.sum_ite_index, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R) ≠
        0 →
      p.2 = n

Tactic:
have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff p.2 (monomial n a) ≠ 0 → p.2 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this :
  ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R) ≠
        0 →
      p.2 = n
rw :
  (if n ≤ m then
      ∑ x ∈ {(m - n, n)},
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
    else
      ∑ x ∈ ∅,
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0

Tactic:
rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n,
    Finset.sum_ite_index]

Premises used: Finset.filter_snd_eq_antidiagonal, Finset.sum_filter_of_ne, Finset.sum_ite_index, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this :
  ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R) ≠
        0 →
      p.2 = n
⊢ (if n ≤ m then
      ∑ x ∈ {(m - n, n)},
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
    else
      ∑ x ∈ ∅,
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0

Tactic:
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Premises used: MvPowerSeries.coeff_monomial_same, Finset.sum_singleton, Finset.sum_empty
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
have have₁ have₂ :
  ∀
    (this :
      ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff p.2 : (a : MvPowerSeries σ R) → R)
                  ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
                R) ≠
            0 →
          p.2 = n),
    (coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
      if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
have₃ :
  ∀
    (this :
      ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff p.2 : (a : MvPowerSeries σ R) → R)
                  ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
                R) ≠
            0 →
          p.2 = n),
    (if n ≤ m then
        ∑ x ∈ {(m - n, n)},
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R)
      else
        ∑ x ∈ ∅,
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R)) =
      if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0

Tactic:
classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff p.2 (monomial n a) ≠ 0 → p.2 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n,
    Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Premises used: MvPowerSeries.coeff_monomial_same, Finset.sum_singleton, Finset.sum_empty, Finset.sum_ite_index, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
hc : m ≤ m + n
⊢ (coeff (m + n) : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    HMul.hMul (β := R) a ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
rw [coeff_monomial_mul, if_pos, add_tsub_cancel_left]

Premises used: MvPowerSeries.coeff_monomial_mul, add_tsub_cancel_left, if_pos
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n

Tactic:
le_add_right le_rfl

Premises used: le_rfl, le_add_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n

Tactic:
exact le_add_right le_rfl

Premises used: le_rfl, le_add_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
hc : n ≤ m + n
⊢ (coeff (m + n) : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a

Tactic:
rw [coeff_mul_monomial, if_pos, add_tsub_cancel_right]

Premises used: MvPowerSeries.coeff_mul_monomial, if_pos, add_tsub_cancel_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ n ≤ m + n

Tactic:
le_add_left le_rfl

Premises used: le_rfl, le_add_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ n ≤ m + n

Tactic:
exact le_add_left le_rfl

Premises used: le_rfl, le_add_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
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
⊢ Commute φ ((monomial n : (a : R) → MvPowerSeries σ R) a) ↔
    ∀ (m : σ →₀ ℕ), Commute ((coeff m : (a : MvPowerSeries σ R) → R) φ) a

Tactic:
rw [commute_iff_eq, MvPowerSeries.ext_iff]

Premises used: MvPowerSeries.ext_iff, commute_iff_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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

Tactic:
⟨fun h m => ?_, fun h m => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
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)
⊢ (∀ (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 => ?_⟩