awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
have 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
Tactic: refine ⟨?_, degree_sub_leadingTerm_lt_degree⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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
⊢ False
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
⊢ m.sPolynomial f 0 = 0
have rw : -m.sPolynomial 0 f = 0
Tactic: rw [sPolynomial_antisymm, sPolynomial_left_zero, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ m.sPolynomial f 0 = 0
have rw₁ : Eq (α := MvPolynomial σ R) (-0) 0
Tactic: rw [sPolynomial_antisymm, sPolynomial_left_zero, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ m.sPolynomial f 0 = 0
have rw₂ : Eq (α := MvPolynomial σ R) 0 0
Tactic: rw [sPolynomial_antisymm, sPolynomial_left_zero, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ 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)
have 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)
Tactic: wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ 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)
have 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)
Tactic: wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
Cleared hypotheses: f, g
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ 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)
have 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)
Tactic: obtain rfl | rfl := h0
Cleared hypotheses: f, h0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ 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)
have 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)
Tactic: obtain rfl | rfl := h0
Cleared hypotheses: g, h0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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) ((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)
have 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)
Tactic: simp only [sPolynomial_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
    ((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)
have 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)
Tactic: apply degree_sub_le.trans
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
          (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)
have 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)
Tactic: apply (sup_le_sup degree_mul_le degree_mul_le).trans
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ 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)
have 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)
Tactic: classical
  wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
  · (obtain rfl | rfl := h0) <;> simp
  simp only [sPolynomial_def]
  apply degree_sub_le.trans
  apply (sup_le_sup degree_mul_le degree_mul_le).trans
  simp [degree_monomial, h0.1, h0.2, tsub_add_cancel_of_le, le_sup_left, le_sup_right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ 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)
have 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)
Tactic: classical
  wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
  · (obtain rfl | rfl := h0) <;> simp
  simp only [sPolynomial_def]
  apply degree_sub_le.trans
  apply (sup_le_sup degree_mul_le degree_mul_le).trans
  simp [degree_monomial, h0.1, h0.2, tsub_add_cancel_of_le, le_sup_left, le_sup_right]
Cleared hypotheses: f, g
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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! 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)
have 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
          (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: classical
  wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
  · (obtain rfl | rfl := h0) <;> simp
  simp only [sPolynomial_def]
  apply degree_sub_le.trans
  apply (sup_le_sup degree_mul_le degree_mul_le).trans
  simp [degree_monomial, h0.1, h0.2, tsub_add_cancel_of_le, le_sup_left, le_sup_right]
Cleared hypotheses: f, g
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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! 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)
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
            (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)
have 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)
    (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: classical
  wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
  · (obtain rfl | rfl := h0) <;> simp
  simp only [sPolynomial_def]
  apply degree_sub_le.trans
  apply (sup_le_sup degree_mul_le degree_mul_le).trans
  simp [degree_monomial, h0.1, h0.2, tsub_add_cancel_of_le, le_sup_left, le_sup_right]
Cleared hypotheses: f, g
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0
have 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
Tactic: rw [sPolynomial_def, coeff_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ 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
have 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
Tactic: nth_rewrite 1 [← tsub_add_cancel_of_le le_sup_left, coeff_monomial_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ 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
have nth_rewrite : m.leadingCoeff g * coeff (m.degree f) f - m.leadingCoeff f * coeff (m.degree g) g = 0
Tactic: nth_rewrite 1 [← tsub_add_cancel_of_le le_sup_right, coeff_monomial_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ m.leadingCoeff g * coeff (m.degree f) f - m.leadingCoeff f * coeff (m.degree g) g = 0
have unfold : coeff (m.degree g) g * coeff (m.degree f) f - coeff (m.degree f) f * coeff (m.degree g) g = 0
Tactic: unfold leadingCoeff
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
⊢ 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
have 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
Tactic: by_cases hf : m.degree f = 0 ∧ m.degree g = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ 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
have 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
Tactic: by_cases hf : m.degree f = 0 ∧ m.degree g = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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
⊢ 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
have h₁ : m.degree f = 0
Tactic: rcases hf with ⟨h₁, h₂⟩
Cleared hypotheses: hf