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 : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' :
  ¬m.degree f = m.degree g →
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ Eq.{u_3 + 1} (α := 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 [add_comm, degree_add_of_lt (h' h), right_eq_sup]

Premises used: right_eq_sup, add_comm, 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 : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' :
  ¬m.degree f = m.degree g →
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
simp only [le_of_lt (h' h)]

Premises used: le_of_lt
-- 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
rw :
  ∀ c ∈ (f * g).support,
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : 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 (f * g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)

Tactic:
rw [degree_le_iff]

Premises used: MonomialOrder.degree_le_iff
-- 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
c : σ →₀ ℕ
rw :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) →
    coeff c (f * g) = 0
⊢ c ∈ (f * g).support →
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)

Tactic:
rw [← not_lt, mem_support_iff, not_imp_not]

Premises used: MvPolynomial.mem_support_iff, not_lt, not_imp_not
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
rw : Eq.{u_2 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g) 0
⊢ coeff c (f * g) = 0

Tactic:
rw [coeff_mul]

Premises used: MvPolynomial.coeff_mul
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
h : ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g = 0
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g) 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : (d, e) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c
⊢ d + e = c

Tactic:
simp only [Finset.mem_antidiagonal] at hde

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
h : coeff d f * coeff e g = 0
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0

Tactic:
dsimp only
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
pos :
  ∀
    (hd :
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)),
    coeff d f * coeff e g = 0
neg :
  ∀
    (hd :
      ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)),
    coeff d f * coeff e g = 0
⊢ coeff d f * coeff e g = 0

Tactic:
by_cases hd : m.degree f ≺[m] d

Premises used: MonomialOrder.degree
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
pos : 0 * coeff e g = 0
pos₁ pos₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ coeff d f * coeff e g = 0

Tactic:
rw [m.coeff_eq_zero_of_lt hd, zero_mul]

Premises used: MulZeroClass.zero_mul, MonomialOrder.coeff_eq_zero_of_lt
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
this :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
rw : coeff d f * 0 = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ coeff d f * coeff e g = 0

Tactic:
rw [m.coeff_eq_zero_of_lt this, mul_zero]

Premises used: MonomialOrder.coeff_eq_zero_of_lt, MulZeroClass.mul_zero
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
neg :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
⊢ coeff d f * coeff e g = 0

Tactic:
suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
simp only [not_lt] at hd

Premises used: not_lt
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
neg :
  HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn) <
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)

Tactic:
apply lt_of_add_lt_add_left (a := m.toSyn d)

Premises used: lt_of_add_lt_add_left
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
neg :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
⊢ HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn) <
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)

Tactic:
grw [← map_add _ _ e, hd, ← map_add, hde]

Premises used: map_add
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : 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.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)

Tactic:
hc
-- 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
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : 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.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)

Tactic:
exact hc
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
h₀ : ∀ b_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0
h₁ : (a, b) ∉ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0
⊢ coeff (a + b) (f * g) = coeff a f * coeff b g

Tactic:
rw [coeff_mul, Finset.sum_eq_single (a, b)]

Premises used: Prod.mk, Finset.sum_eq_single, MvPolynomial.coeff_mul
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
hcd : (c, d) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b)
h : (c, d) ≠ (a, b)
⊢ c + d = a + b

Tactic:
simp only [Finset.mem_antidiagonal] at hcd

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
pos :
  ∀
    (hf :
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)),
    coeff (c, d).1 f * coeff (c, d).2 g = 0
neg :
  ∀
    (hf :
      ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)),
    coeff (c, d).1 f * coeff (c, d).2 g = 0
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
by_cases hf : m.degree f ≺[m] c

Premises used: MonomialOrder.degree
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
pos : 0 * coeff (c, d).2 g = 0
pos₁ pos₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
rw [m.coeff_eq_zero_of_lt hf, zero_mul]

Premises used: MulZeroClass.zero_mul, MonomialOrder.coeff_eq_zero_of_lt
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
this :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
rw : coeff (c, d).1 f * 0 = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
rw [coeff_eq_zero_of_lt this, mul_zero]

Premises used: MonomialOrder.coeff_eq_zero_of_lt, MulZeroClass.mul_zero
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
neg :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
suffices m.degree g ≺[m] d by
        rw [coeff_eq_zero_of_lt this, mul_zero]
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
rw [not_lt] at hf

Premises used: not_lt
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
neg :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
rw [← not_le]

Premises used: not_le
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg : (c, d) = (a, b)
⊢ False

Tactic:
apply h
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
this : c = a
⊢ (c, d) = (a, b)

Tactic:
simpa [Prod.mk.injEq, this] using hcd

Premises used: Prod.mk.injEq
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg : c = a
⊢ (c, d) = (a, b)

Tactic:
suffices c = a by
        simpa [Prod.mk.injEq, this] using hcd
-- 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
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
⊢ c = a

Tactic:
apply m.toSyn.injective

Premises used: AddEquiv.injective, 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 g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)

Tactic:
apply le_antisymm (le_trans hf ha)

Premises used: le_antisymm, le_trans