awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommSemiring R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommSemiring R
inst_2 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p' + m.degree q) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)

Tactic:
simpa [m.degree_mul hp hq] using h

Premises used: MonomialOrder.degree_mul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn) ↔
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)

Tactic:
⟨m.degree_lt_of_left_ne_zero_of_degree_mul_lt hp, ?_⟩

Premises used: Iff.intro, MonomialOrder.degree_lt_of_left_ne_zero_of_degree_mul_lt
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
refine :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn) →
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn) ↔
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)

Tactic:
refine ⟨m.degree_lt_of_left_ne_zero_of_degree_mul_lt hp, ?_⟩
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
contrapose! :
  ∀ (h : p' = 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
⊢ p' ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h : p' = 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn)

Tactic:
simpa [m.degree_mul hp hq, m.degree_mul (show p' ≠ 0 by contrapose! h; simp [h]) hq] using h

Premises used: MonomialOrder.degree_mul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
⊢ m.Monic (m.leadingTerm p) ↔ m.Monic p

Tactic:
simp [leadingTerm, Monic]

Premises used: MonomialOrder.Monic, MonomialOrder.leadingTerm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : Decidable (p = 0)
⊢ (m.leadingTerm p).support = if p = 0 then ∅ else {m.degree p}

Tactic:
simp [leadingTerm, support_monomial]

Premises used: MvPolynomial.support_monomial, MonomialOrder.leadingTerm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : Decidable (p = 0)
⊢ (m.leadingTerm p).support = if p = 0 then ∅ else {m.degree p}

Tactic:
classical
  simp [leadingTerm, support_monomial]

Premises used: MvPolynomial.support_monomial, MonomialOrder.leadingTerm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
hp : p ≠ 0
⊢ (m.leadingTerm p).support = {m.degree p}

Tactic:
simp [leadingTerm, support_monomial, hp]

Premises used: MvPolynomial.support_monomial, MonomialOrder.leadingTerm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
hp : p ≠ 0
⊢ (m.leadingTerm p).support = {m.degree p}

Tactic:
classical
  simp [leadingTerm, support_monomial, hp]

Premises used: MvPolynomial.support_monomial, MonomialOrder.leadingTerm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
a : σ →₀ ℕ
ha : a ∈ p.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)

Tactic:
simp [degree, Finset.le_sup ha]

Premises used: MonomialOrder.degree, Finset.le_sup
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
rw :
  m.degree p = m.degree q ∧ m.leadingCoeff p = m.leadingCoeff q ∨ m.leadingCoeff p = 0 ∧ m.leadingCoeff q = 0 ↔
    m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q
⊢ m.leadingTerm p = m.leadingTerm q ↔ m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q

Tactic:
rw [leadingTerm, leadingTerm, monomial_eq_monomial_iff]

Premises used: MvPolynomial.monomial_eq_monomial_iff, MonomialOrder.leadingTerm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
⊢ m.degree p = m.degree q ∧ m.leadingCoeff p = m.leadingCoeff q ∨ m.leadingCoeff p = 0 ∧ m.leadingCoeff q = 0 ↔
    m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : ∀ (h0 : p * q ≠ 0), m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q
⊢ m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q

Tactic:
by_cases! h0 : p * q = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
h0 : p * q = 0
⊢ m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q

Tactic:
simp [h0, zero_eq_mul.mp]

Premises used: zero_eq_mul, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
h0 : p * q ≠ 0
⊢ m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q

Tactic:
simp [leadingTerm, m.degree_mul' h0]

Premises used: MonomialOrder.leadingTerm, MonomialOrder.degree_mul'
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : Subsingleton R
p : MvPolynomial σ R
⊢ m.Monic p

Tactic:
simp [Subsingleton.eq_one (α := MvPolynomial σ R)]

Premises used: Subsingleton.eq_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
simp_rw :
  LE.le.{u_3} (α := m.syn) (p.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
    (q.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
⊢ 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)

Tactic:
simp_rw [degree, m.toSyn.apply_symm_apply]

Premises used: AddEquiv.apply_symm_apply, MonomialOrder.degree, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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) (p.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
    (q.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))

Tactic:
Finset.sup_mono h

Premises used: Finset.sup_mono
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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) (p.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
    (q.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))

Tactic:
exact Finset.sup_mono h

Premises used: Finset.sup_mono
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
⊢ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f * g)) ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
map_add m.toSyn _ _ ▸ degree_mul_le

Premises used: Eq.rec, map_add, MonomialOrder.degree_mul_le, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)
rw : ∀ (y : MvPolynomial σ R), f * y = 0 → y = 0
⊢ Membership.mem (γ := Submonoid (MvPolynomial σ R)) (MvPolynomial σ R)⁰ f

Tactic:
rw [← nonZeroDivisorsLeft_eq_nonZeroDivisors, mem_nonZeroDivisorsLeft_iff]

Premises used: nonZeroDivisorsLeft_eq_nonZeroDivisors, mem_nonZeroDivisorsLeft_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)
g : MvPolynomial σ R
⊢ f * g = 0 → g = 0

Tactic:
simp [← m.leadingCoeff_eq_zero_iff (f := f * g),
    m.leadingCoeff_mul_of_left_mem_nonZeroDivisors hf, mul_left_mem_nonZeroDivisors_eq_zero_iff hf]

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, mul_left_mem_nonZeroDivisors_eq_zero_iff, MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors
-- 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
suffices : ∀ (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

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]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
h :
  ∀ (a : σ),
    Eq (α := ℕ) ((m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
      ((m.degree f ⊔ m.degree g - m.degree f : (a : σ) → ℕ) a : ℕ)
⊢ m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f

Tactic:
ext a
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 : ℕ)
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 : ℕ)
⊢ 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)

Premises used: le_total, MonomialOrder.degree, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 : 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:
simp [h]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 : 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:
simp [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 : f - m.leadingTerm f ≠ 0
contrapose : ∀ (h : m.degree f = 0), f - m.leadingTerm f = 0
⊢ m.degree f ≠ 0

Tactic:
contrapose 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
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
rw₂ rw₃ :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
⊢ f - m.leadingTerm f = 0

Tactic:
rw [m.degree_eq_zero_iff.mp h, leadingTerm_C, sub_eq_zero]

Premises used: sub_eq_zero, MonomialOrder.degree_eq_zero_iff, MonomialOrder.leadingTerm_C, Iff.mp
-- 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 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)))
⊢ 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]

Premises used: MvPolynomial.support_neg
-- 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.leadingCoeff (-f) = -m.leadingCoeff f

Tactic:
simp only [leadingCoeff, degree_neg, coeff_neg]

Premises used: MvPolynomial.coeff_neg, MonomialOrder.leadingCoeff, MonomialOrder.degree_neg
-- 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 :
  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)
⊢ 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]

Premises used: sub_eq_add_neg
-- 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
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)
⊢ 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:
apply le_of_le_of_eq m.degree_add_le

Premises used: le_of_le_of_eq, MonomialOrder.degree_add_le
-- 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 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)
⊢ 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]

Premises used: MonomialOrder.degree_neg
-- 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 :
  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)
rw : m.degree (f + -g) = m.degree f
⊢ m.degree (f - g) = m.degree f

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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 :
  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)
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

Tactic:
apply degree_add_of_lt

Premises used: MonomialOrder.degree_add_of_lt
-- 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 :
  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)
⊢ 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:
simp only [degree_neg, h]

Premises used: MonomialOrder.degree_neg
-- 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 :
  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)
rw : m.leadingCoeff (f + -g) = m.leadingCoeff f
⊢ m.leadingCoeff (f - g) = m.leadingCoeff f

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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 :
  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)
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

Tactic:
apply leadingCoeff_add_of_lt

Premises used: MonomialOrder.leadingCoeff_add_of_lt
-- 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
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)
⊢ 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)

Tactic:
apply le_trans degree_sub_le

Premises used: MonomialOrder.degree_sub_le, le_trans
-- 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
⊢ 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:
simp [degree_leadingTerm]

Premises used: MonomialOrder.degree_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 :
  ∀ (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:
by_cases hl : f - m.leadingTerm f = 0

Premises used: 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
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:
simpa [hl, toSyn_lt_iff_ne_zero]

Premises used: MonomialOrder.toSyn_lt_iff_ne_zero