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 : CommSemiring R
inst_1 : NoZeroDivisors R
p q : MvPolynomial σ R
⊢ m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q
have pos : ∀ (h0 : p * q = 0), m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q
Tactic: by_cases! h0 : p * q = 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 : CommSemiring R
inst_1 : NoZeroDivisors R
p q : MvPolynomial σ R
pos : ∀ (h0 : p * q = 0), m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q
⊢ m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q
have neg : ∀ (h0 : p * q ≠ 0), m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q
Tactic: by_cases! h0 : p * q = 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 : CommSemiring R
p q : MvPolynomial σ R
h : p.support ⊆ q.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree q) : m.syn)
have simp_rw : LE.le.{u_3} (α := m.syn) (p.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
  (q.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
Tactic: simp_rw [degree, m.toSyn.apply_symm_apply]
-- 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 : CommSemiring R
f : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
⊢ Membership.mem (γ := Submonoid (MvPolynomial σ R)) (MvPolynomial σ R)⁰ f
have rw : ∀ (y : MvPolynomial σ R), f * y = 0 → y = 0
Tactic: rw [← nonZeroDivisorsLeft_eq_nonZeroDivisors, mem_nonZeroDivisorsLeft_iff]
-- 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 : ∀ (f g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
⊢ m.sPolynomial f 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 -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
          MvPolynomial σ R)
        g
have rw : HMul.hMul (α := MvPolynomial σ R)
      ((monomial (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) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) 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 -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
        MvPolynomial σ R)
      g
Tactic: rw [sPolynomial, this, this, sup_comm]
-- 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 : ∀ (f g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
rw :
  HMul.hMul (α := MvPolynomial σ R)
        ((monomial (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) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) 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 -
      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.sPolynomial f 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 -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
          MvPolynomial σ R)
        g
have rw₁ : 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) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) 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 -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
        MvPolynomial σ R)
      g
Tactic: rw [sPolynomial, this, this, sup_comm]
-- 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 : ∀ (f g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
rw :
  HMul.hMul (α := MvPolynomial σ R)
        ((monomial (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) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) 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 -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
          MvPolynomial σ R)
        g
rw₁ :
  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) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) 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 -
      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.sPolynomial f 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 -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
          MvPolynomial σ R)
        g
have rw₂ : 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 g ⊔ m.degree f - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
        MvPolynomial σ R)
      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 -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
        MvPolynomial σ R)
      g
Tactic: rw [sPolynomial, this, this, sup_comm]
-- 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.sPolynomial f 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 -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
          MvPolynomial σ R)
        g
have suffices : ∀ (f g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
Tactic: suffices ∀ f g, m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f by
    rw [sPolynomial, this, this, sup_comm]
-- 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_1 g_1 f g : MvPolynomial σ R
⊢ m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
have h : ∀ (a : σ),
  Eq (α := ℕ) ((m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
    ((m.degree f ⊔ m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
Tactic: ext a
-- 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_1 g_1 f g : MvPolynomial σ R
a : σ
⊢ Eq (α := ℕ) ((m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
    ((m.degree f ⊔ m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
have h : ∀ (h : LE.le (α := ℕ) ((m.degree f : (a : σ) → ℕ) a : ℕ) ((m.degree g : (a : σ) → ℕ) a : ℕ)),
  Eq (α := ℕ) ((m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
    ((m.degree f ⊔ m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
Tactic: obtain (h | h) := le_total (m.degree f a) (m.degree g a)
-- 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_1 g_1 f g : MvPolynomial σ R
a : σ
h :
  ∀ (h : LE.le (α := ℕ) ((m.degree f : (a : σ) → ℕ) a : ℕ) ((m.degree g : (a : σ) → ℕ) a : ℕ)),
    Eq (α := ℕ) ((m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
      ((m.degree f ⊔ m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
⊢ Eq (α := ℕ) ((m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
    ((m.degree f ⊔ m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
have h₁ : ∀ (h : LE.le (α := ℕ) ((m.degree g : (a : σ) → ℕ) a : ℕ) ((m.degree f : (a : σ) → ℕ) a : ℕ)),
  Eq (α := ℕ) ((m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
    ((m.degree f ⊔ m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
Tactic: obtain (h | h) := le_total (m.degree f a) (m.degree g a)
-- 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
h : f - m.leadingTerm f ≠ 0
⊢ m.degree f ≠ 0
have contrapose : ∀ (h : m.degree f = 0), f - m.leadingTerm f = 0
Tactic: contrapose 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
h : m.degree f = 0
⊢ f - m.leadingTerm f = 0
have rw : HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
    (m.leadingTerm ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) =
  0
Tactic: rw [m.degree_eq_zero_iff.mp h, leadingTerm_C, sub_eq_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
h : m.degree f = 0
rw :
  HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
      (m.leadingTerm ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) =
    0
⊢ f - m.leadingTerm f = 0
have rw₁ : HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) =
  0
Tactic: rw [m.degree_eq_zero_iff.mp h, leadingTerm_C, sub_eq_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
h : m.degree f = 0
rw :
  HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
      (m.leadingTerm ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) =
    0
rw₁ :
  HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) =
    0
⊢ f - m.leadingTerm f = 0
have rw₂ : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
Tactic: rw [m.degree_eq_zero_iff.mp h, leadingTerm_C, sub_eq_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
⊢ Eq.{u_1 + 1} (α := σ →₀ ℕ)
    ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) ((-f).support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)))
    ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)))
have rw : Eq.{u_1 + 1} (α := σ →₀ ℕ) ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)))
  ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)))
Tactic: rw [support_neg]
-- 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 (f - g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have rw : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + -g)) : m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
Tactic: rw [sub_eq_add_neg]
-- 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 (f + -g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have apply : Eq.{u_3 + 1} (α := m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (-g))) : m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
Tactic: apply le_of_le_of_eq m.degree_add_le
-- 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
⊢ Eq.{u_3 + 1} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (-g))) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have rw : Eq.{u_3 + 1} (α := m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
Tactic: rw [degree_neg]
-- 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
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree (f - g) = m.degree f
have rw : m.degree (f + -g) = m.degree f
Tactic: rw [sub_eq_add_neg]
-- 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
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree (f + -g) = m.degree f
have h₁ : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (-g)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply degree_add_of_lt
-- 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
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.leadingCoeff (f - g) = m.leadingCoeff f
have rw : m.leadingCoeff (f + -g) = m.leadingCoeff f
Tactic: rw [sub_eq_add_neg]
-- 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
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.leadingCoeff (f + -g) = m.leadingCoeff f
have h₁ : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (-g)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply leadingCoeff_add_of_lt
-- 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
⊢ LE.le.{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)
have apply : LE.le.{u_3} (α := m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.leadingTerm f))) :
    m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply le_trans degree_sub_le
-- 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
h : 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)
have 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)
Tactic: by_cases hl : f - m.leadingTerm f = 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 : 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)
⊢ 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)
have 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)
Tactic: by_cases hl : f - m.leadingTerm f = 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 : MvPolynomial σ R
h : m.degree f ≠ 0
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)
have 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)
Tactic: apply lt_of_le_of_ne (m.degree_sub_leadingTerm_le f)
-- 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 : 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)
⊢ False
have h'₁ : m.degree (f - m.leadingTerm f) = m.degree f
Tactic: simp only [EmbeddingLike.apply_eq_iff_eq] at h'
Cleared hypotheses: h'
-- 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 : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
h' : m.degree (f - m.leadingTerm f) = m.degree f
⊢ False
have hl₁ : m.degree (f - m.leadingTerm f) ∈ (f - m.leadingTerm f).support
Tactic: apply m.degree_mem_support at hl
Cleared hypotheses: hl
-- 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 : 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
⊢ False
have hl₁ : coeff (m.degree f) (f - m.leadingTerm f) ≠ 0
Tactic: rw [h', mem_support_iff] at hl
Cleared hypotheses: hl
-- 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
h : 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)
have 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)
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
-- 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
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)
⊢ 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)
have 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)
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