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
rw :
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
      ((m.toSyn.symm : (a : 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 [← m.toSyn.apply_symm_apply (_ ⊔ _)]

Premises used: AddEquiv.apply_symm_apply, Max.max, 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
conv_rhs :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : 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:
conv_rhs => rw [← m.toSyn.apply_symm_apply (_ ⊔ _)]

Premises used: AddEquiv.apply_symm_apply, Max.max, 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
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.toSyn.symm : (a : 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)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
          (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (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
simp :
  ∀ 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.syn) ∨
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ ∀ c ∈ (f + g).support,
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
            (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)))) :
        m.syn)

Tactic:
simp only [AddEquiv.apply_symm_apply, le_sup_iff]

Premises used: AddEquiv.apply_symm_apply, le_sup_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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
pos :
  ∀ (hf : b ∈ f.support),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg :
  ∀ (hf : b ∉ f.support),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
by_cases hf : b ∈ f.support

Premises used: MvPolynomial.support
-- 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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
pos :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
m.le_degree hf

Premises used: MonomialOrder.le_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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
exact m.le_degree hf

Premises used: MonomialOrder.le_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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
neg :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
right
-- 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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
neg : b ∈ g.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
apply m.le_degree

Premises used: MonomialOrder.le_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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ coeff b f = 0

Tactic:
simp only [notMem_support_iff] at hf

Premises used: MvPolynomial.notMem_support_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
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : coeff b f = 0
⊢ b ∈ g.support

Tactic:
simpa only [mem_support_iff, coeff_add, hf, zero_add] using hb

Premises used: MvPolynomial.mem_support_iff, zero_add, MvPolynomial.coeff_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ ∅, f x)) : m.syn)
    (Finset.sup ∅ fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
    (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
cons :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a + ∑ x ∈ s, f x)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a)))
        (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x))) :
      m.syn)
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ Finset.cons a s haA, f x)) : m.syn)
    ((Finset.cons a s haA).sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]

Premises used: Finset.sum_cons, Finset.sup_cons
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
    (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a + ∑ x ∈ s, f x)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a)))
        (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x))) :
      m.syn)

Tactic:
le_trans m.degree_add_le (max_le_max le_rfl h)

Premises used: le_rfl, MonomialOrder.degree_add_le, max_le_max, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
    (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a + ∑ x ∈ s, f x)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a)))
        (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x))) :
      m.syn)

Tactic:
exact le_trans m.degree_add_le (max_le_max le_rfl h)

Premises used: le_rfl, MonomialOrder.degree_add_le, max_le_max, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
α : Type u_3
s : Finset α
f : α → MvPolynomial σ R
empty :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ ∅, f x)) : m.syn)
    (Finset.sup ∅ fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
cons :
  ∀ (a : α) (s : Finset α) (haA : a ∉ s)
    (h :
      LE.le.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
        (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)),
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ Finset.cons a s haA, f x)) : m.syn)
      ((Finset.cons a s haA).sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
    (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s haA h =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact le_trans m.degree_add_le (max_le_max le_rfl h)

Premises used: Finset.sum_cons, Finset.sup_cons
-- 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 :
  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)
a :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree (f + g) = m.degree f

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
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)
a :
  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.syn)
a₁ :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 :
  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)
a :
  LE.le.{u_3} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : 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 + g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply le_trans degree_add_le

Premises used: MonomialOrder.degree_add_le, le_trans
-- 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 :
  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)
⊢ LE.le.{u_3} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
simp only [sup_le_iff, le_refl, true_and, le_of_lt h]

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

Tactic:
apply le_degree

Premises used: MonomialOrder.le_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
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)
a : f ≠ 0
⊢ m.degree f ∈ (f + g).support

Tactic:
rw [mem_support_iff, coeff_add, m.coeff_eq_zero_of_lt h, add_zero,
      ← leadingCoeff, leadingCoeff_ne_zero_iff]

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.leadingCoeff, MonomialOrder.coeff_eq_zero_of_lt, MvPolynomial.coeff_add, MonomialOrder.leadingCoeff_ne_zero_iff, add_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
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)
hf : f = 0
⊢ ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
rw [← not_le, hf] at h

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
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)
hf : f = 0
h₁ :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ f = 0

Tactic:
rw [← not_le, hf] at h

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
h :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
hf : f = 0
a :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ 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
h :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
hf : f = 0
a : LE.le.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
simp only [degree_zero, map_zero]

Premises used: map_zero, MonomialOrder.degree_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
h :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
hf : f = 0
⊢ LE.le.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)

Tactic:
apply bot_le

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

Tactic:
rw [add_comm]

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

Tactic:
degree_add_of_lt h

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 : CommSemiring R
f g : MvPolynomial σ R
h :
  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)
⊢ m.degree (g + f) = m.degree g

Tactic:
exact degree_add_of_lt h

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 : CommSemiring 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

Tactic:
simp only [leadingCoeff, m.degree_add_of_lt h, coeff_add, coeff_eq_zero_of_lt h, add_zero]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.coeff_eq_zero_of_lt, MvPolynomial.coeff_add, MonomialOrder.degree_add_of_lt, add_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
hf : m.Monic f
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.Monic (f + g)

Tactic:
simp only [Monic, leadingCoeff_add_of_lt h, hf.leadingCoeff_eq_one]

Premises used: MonomialOrder.Monic, MonomialOrder.Monic.leadingCoeff_eq_one, 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 : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
pos :
  ∀
    (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)),
    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)
neg :
  ∀
    (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)),
    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)
⊢ 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:
by_cases h' : m.degree g ≺[m] m.degree f

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
h : m.degree f ≠ m.degree g
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)
⊢ 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:
simp [degree_add_of_lt h', le_of_lt h']

Premises used: le_of_lt, 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' :
  ¬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 = 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)

Tactic:
rw [not_lt, le_iff_eq_or_lt, Classical.or_iff_not_imp_left, EmbeddingLike.apply_eq_iff_eq] at h'

Premises used: le_iff_eq_or_lt, EmbeddingLike.apply_eq_iff_eq, not_lt, Classical.or_iff_not_imp_left