awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
neg :
  Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply lt_of_le_of_ne (m.degree_sub_leadingTerm_le f)

Premises used: MonomialOrder.degree_sub_leadingTerm_le, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
neg :
  ∀
    (h' :
      Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
    False
⊢ Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
by_contra! h'
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
h' :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree (f - m.leadingTerm f) = m.degree f

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq] at h'

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
h' : m.degree (f - m.leadingTerm f) = m.degree f
⊢ m.degree (f - m.leadingTerm f) ∈ (f - m.leadingTerm f).support

Tactic:
apply m.degree_mem_support at hl

Premises used: MonomialOrder.degree_mem_support
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
h' : m.degree (f - m.leadingTerm f) = m.degree f
hl : m.degree (f - m.leadingTerm f) ∈ (f - m.leadingTerm f).support
⊢ coeff (m.degree f) (f - m.leadingTerm f) ≠ 0

Tactic:
rw [h', mem_support_iff] at hl

Premises used: MvPolynomial.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
h' : m.degree (f - m.leadingTerm f) = m.degree f
hl : coeff (m.degree f) (f - m.leadingTerm f) ≠ 0
⊢ False

Tactic:
simp [leadingTerm, leadingCoeff] at hl

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.leadingTerm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
pos :
  ∀ (hl : f - m.leadingTerm f = 0),
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
neg neg₁ :
  ∀ (hl : ¬f - m.leadingTerm f = 0),
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
classical
  by_cases hl : f - m.leadingTerm f = 0
  · simpa [hl, toSyn_lt_iff_ne_zero]
  · apply lt_of_le_of_ne (m.degree_sub_leadingTerm_le f)
    by_contra! h'
    simp only [EmbeddingLike.apply_eq_iff_eq] at h'
    apply m.degree_mem_support at hl
    rw [h', mem_support_iff] at hl
    simp [leadingTerm, leadingCoeff] at hl

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.leadingCoeff, MonomialOrder.toSyn_lt_iff_ne_zero, MonomialOrder.leadingTerm, EmbeddingLike.apply_eq_iff_eq, MonomialOrder.degree_mem_support, MonomialOrder.degree_sub_leadingTerm_le, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ↔
    m.degree f ≠ 0

Tactic:
⟨?_, degree_sub_leadingTerm_lt_degree⟩

Premises used: Iff.intro, MonomialOrder.degree_sub_leadingTerm_lt_degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
refine :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) →
    m.degree f ≠ 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ↔
    m.degree f ≠ 0

Tactic:
refine ⟨?_, degree_sub_leadingTerm_lt_degree⟩
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h' : m.degree f = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn) (0 : m.syn)

Tactic:
simp only [h', map_zero] at h

Premises used: map_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h' : m.degree f = 0
h : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn) (0 : m.syn)
⊢ False

Tactic:
not_lt_bot h

Premises used: not_lt_bot
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
h' : m.degree f = 0
h : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f - m.leadingTerm f)) : m.syn) (0 : m.syn)
⊢ False

Tactic:
exact not_lt_bot h

Premises used: not_lt_bot
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ m.sPolynomial f g = -m.sPolynomial g f

Tactic:
(neg_sub (_ * g) (_ * f)).symm

Premises used: neg_sub, HMul.hMul, Eq.symm, MonomialOrder.sPolynomial
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
g : MvPolynomial σ R
⊢ m.sPolynomial 0 g = 0

Tactic:
simp [sPolynomial]

Premises used: MonomialOrder.sPolynomial
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
rw : -m.sPolynomial 0 f = 0
rw₁ : Eq (α := MvPolynomial σ R) (-0) 0
rw₂ rw₃ : Eq (α := MvPolynomial σ R) 0 0
⊢ m.sPolynomial f 0 = 0

Tactic:
rw [sPolynomial_antisymm, sPolynomial_left_zero, neg_zero]

Premises used: MonomialOrder.sPolynomial_antisymm, MonomialOrder.sPolynomial_left_zero, neg_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
⊢ m.sPolynomial f f = 0

Tactic:
sub_self _

Premises used: sub_self, MonomialOrder.sPolynomial
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
        (h0 : f ≠ 0 ∧ g ≠ 0),
        LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn))
    (h0 : f = 0 ∨ g = 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
wlog! :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)

Tactic:
wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
h0 : f = 0 ∨ g = 0
inr :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial 0 g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0 ⊔ m.degree g) : m.syn)
inr₁ :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f 0)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)

Tactic:
obtain rfl | rfl := h0

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial 0 g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0 ⊔ m.degree g) : m.syn)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f 0)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommRing R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
simp :
  LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
                MvPolynomial σ R)
              f -
            HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
                MvPolynomial σ R)
              g)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)

Tactic:
simp only [sPolynomial_def]

Premises used: MonomialOrder.sPolynomial_def
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommRing R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
apply :
  LE.le.{u_3} (α := m.syn)
    (max
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
                MvPolynomial σ R)
              f)))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
                MvPolynomial σ R)
              g))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
                MvPolynomial σ R)
              f -
            HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
                MvPolynomial σ R)
              g)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)

Tactic:
apply degree_sub_le.trans

Premises used: MonomialOrder.degree_sub_le, LE.le.trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommRing R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
apply :
  LE.le.{u_3} (α := m.syn)
    (max
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (degree.{u_1, u_2, u_3} m (R := R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g)) +
            m.degree f))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (degree.{u_1, u_2, u_3} m (R := R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)) +
            m.degree g)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn)
    (max
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
                MvPolynomial σ R)
              f)))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
                MvPolynomial σ R)
              g))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)

Tactic:
apply (sup_le_sup degree_mul_le degree_mul_le).trans

Premises used: sup_le_sup, MonomialOrder.degree_mul_le, LE.le.trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommRing R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
⊢ LE.le.{u_3} (α := m.syn)
    (max
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (degree.{u_1, u_2, u_3} m (R := R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g)) +
            m.degree f))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (degree.{u_1, u_2, u_3} m (R := R)
              ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)) +
            m.degree g)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)

Tactic:
simp [degree_monomial, h0.1, h0.2, tsub_add_cancel_of_le, le_sup_left, le_sup_right]

Premises used: MonomialOrder.degree_monomial, le_sup_left, tsub_add_cancel_of_le, le_sup_right, And.right, And.left
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
rw :
  coeff (m.degree f ⊔ m.degree g)
        (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
            MvPolynomial σ R)
          f) -
      coeff (m.degree f ⊔ m.degree g)
        (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
            MvPolynomial σ R)
          g) =
    0
⊢ coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0

Tactic:
rw [sPolynomial_def, coeff_sub]

Premises used: MonomialOrder.sPolynomial_def, MvPolynomial.coeff_sub
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
nth_rewrite :
  m.leadingCoeff g * coeff (m.degree f) f -
      coeff (m.degree f ⊔ m.degree g)
        (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
            MvPolynomial σ R)
          g) =
    0
⊢ coeff (m.degree f ⊔ m.degree g)
        (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
            MvPolynomial σ R)
          f) -
      coeff (m.degree f ⊔ m.degree g)
        (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
            MvPolynomial σ R)
          g) =
    0

Tactic:
nth_rewrite 1 [← tsub_add_cancel_of_le le_sup_left, coeff_monomial_mul]

Premises used: le_sup_left, tsub_add_cancel_of_le, MvPolynomial.coeff_monomial_mul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
nth_rewrite : m.leadingCoeff g * coeff (m.degree f) f - m.leadingCoeff f * coeff (m.degree g) g = 0
⊢ m.leadingCoeff g * coeff (m.degree f) f -
      coeff (m.degree f ⊔ m.degree g)
        (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
            MvPolynomial σ R)
          g) =
    0

Tactic:
nth_rewrite 1 [← tsub_add_cancel_of_le le_sup_right, coeff_monomial_mul]

Premises used: tsub_add_cancel_of_le, MvPolynomial.coeff_monomial_mul, le_sup_right
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
unfold : coeff (m.degree g) g * coeff (m.degree f) f - coeff (m.degree f) f * coeff (m.degree g) g = 0
⊢ m.leadingCoeff g * coeff (m.degree f) f - m.leadingCoeff f * coeff (m.degree g) g = 0

Tactic:
unfold leadingCoeff

Premises used: MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree g) g * coeff (m.degree f) f - coeff (m.degree f) f * coeff (m.degree g) g = 0

Tactic:
ring
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
pos :
  ∀ (hf : m.degree f = 0 ∧ m.degree g = 0),
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn) ∨
      m.sPolynomial f g = 0
neg :
  ∀ (hf : ¬(m.degree f = 0 ∧ m.degree g = 0)),
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn) ∨
      m.sPolynomial f g = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn) ∨
    m.sPolynomial f g = 0

Tactic:
by_cases hf : m.degree f = 0 ∧ m.degree g = 0

Premises used: MonomialOrder.degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
hf : m.degree f = 0 ∧ m.degree g = 0
⊢ m.degree f = 0

Tactic:
rcases hf with ⟨h₁, h₂⟩
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
hf : m.degree f = 0 ∧ m.degree g = 0
h₁ : m.degree f = 0
⊢ m.degree g = 0

Tactic:
rcases hf with ⟨h₁, h₂⟩
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
pos : m.sPolynomial f g = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn) ∨
    m.sPolynomial f g = 0

Tactic:
right
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
this :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R) f -
      HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
    0
⊢ m.sPolynomial f g = 0

Tactic:
simp_all [sPolynomial_def]

Premises used: MonomialOrder.sPolynomial_def
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
pos :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R) f -
      HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
    0
⊢ m.sPolynomial f g = 0

Tactic:
suffices C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0 by simp_all [sPolynomial_def]