awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h : Subsingleton R
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h : Nontrivial R
inr :
  Eq.{u_4 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

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_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h : Nontrivial R
⊢ Eq.{u_4 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)

Tactic:
le_antisymm degree_prod_le (m.le_degree ?_)

Premises used: MonomialOrder.le_degree, le_antisymm, MonomialOrder.degree_prod_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h : Nontrivial R
inr : Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))
⊢ Eq.{u_4 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)

Tactic:
refine le_antisymm degree_prod_le (m.le_degree ?_)

Premises used: MonomialOrder.le_degree, le_antisymm, MonomialOrder.degree_prod_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h : Nontrivial R
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))

Tactic:
simpa [m.coeff_prod_sum_degree, Finset.prod_eq_zero_iff]

Premises used: MonomialOrder.coeff_prod_sum_degree, Finset.prod_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
⊢ Subsingleton R ∨ Nontrivial R

Tactic:
cases subsingleton_or_nontrivial R with
  | inl _ => simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]
  | inr _ =>
    apply m.toSyn.injective
    refine le_antisymm degree_prod_le (m.le_degree ?_)
    simpa [m.coeff_prod_sum_degree, Finset.prod_eq_zero_iff]

Premises used: MonomialOrder.le_degree, MonomialOrder.coeff_prod_sum_degree, subsingleton_or_nontrivial, le_antisymm, Finset.prod_eq_zero_iff, MonomialOrder.degree_prod_le, 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
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f * g ≠ 0
⊢ f ≠ 0 ∧ g ≠ 0

Tactic:
apply ne_zero_and_ne_zero_of_mul at hf

Premises used: ne_zero_and_ne_zero_of_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
f g : MvPolynomial σ R
hf : f ≠ 0 ∧ g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
m.degree_mul hf.1 hf.2

Premises used: And.right, And.left, 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
f g : MvPolynomial σ R
hf : f ≠ 0 ∧ g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
exact m.degree_mul hf.1 hf.2

Premises used: And.right, And.left, 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
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.support

Tactic:
simp [coeff_eq_zero_of_lt h]

Premises used: MonomialOrder.coeff_eq_zero_of_lt
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
⊢ Eq.{u_2 + 1} (α := R) (m.leadingCoeff (∏ i ∈ s, P i)) (∏ i ∈ s, m.leadingCoeff (P i))

Tactic:
simp only [leadingCoeff, degree_prod_of_mem_nonZeroDivisors H, coeff_prod_sum_degree]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.coeff_prod_sum_degree, MonomialOrder.degree_prod_of_mem_nonZeroDivisors
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
⊢ Eq.{u_2 + 1} (α := R) (m.leadingCoeff (∏ i ∈ s, P i)) (∏ i ∈ s, m.leadingCoeff (P i))

Tactic:
simp only [leadingCoeff, degree_prod_of_regular H, coeff_prod_sum_degree]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.coeff_prod_sum_degree, MonomialOrder.degree_prod_of_regular
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
rw : Eq.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 1
rw₁ : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
⊢ Monic.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)

Tactic:
rw [Monic, leadingCoeff_prod_of_regular]

Premises used: MonomialOrder.Monic, MonomialOrder.leadingCoeff_prod_of_regular
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 1

Tactic:
Finset.prod_eq_one H

Premises used: Finset.prod_eq_one
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 1

Tactic:
exact Finset.prod_eq_one H

Premises used: Finset.prod_eq_one
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
rw : IsRegular.{u_2} (R := R) 1
⊢ IsRegular (m.leadingCoeff (P i))

Tactic:
rw [(H i hi).leadingCoeff_eq_one]

Premises used: MonomialOrder.Monic.leadingCoeff_eq_one
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular.{u_2} (R := R) 1

Tactic:
isRegular_one

Premises used: isRegular_one
-- 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
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular.{u_2} (R := R) 1

Tactic:
exact isRegular_one

Premises used: isRegular_one
-- 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.leadingTerm p = 0 ↔ p = 0

Tactic:
simp only [leadingTerm, monomial_eq_zero, leadingCoeff_eq_zero_iff]

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, MonomialOrder.leadingTerm, MvPolynomial.monomial_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
rw rw₁ : Eq (α := MvPolynomial σ R) 0 0
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm 0) 0

Tactic:
rw [leadingTerm_eq_zero_iff]

Premises used: MonomialOrder.leadingTerm_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
B : Set (MvPolynomial σ R)
⊢ m.leadingTerm '' (B \ {0}) = m.leadingTerm '' B \ {0}

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
B : Set (MvPolynomial σ R)
⊢ m.leadingTerm '' insert 0 B = insert 0 (m.leadingTerm '' B)

Tactic:
aesop
-- 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
simp : f = 0 → 0 = m.degree f
⊢ m.degree (m.leadingTerm f) = m.degree f

Tactic:
simp only [leadingTerm, degree_monomial, leadingCoeff_eq_zero_iff, ite_eq_right_iff]

Premises used: MonomialOrder.degree_monomial, MonomialOrder.leadingCoeff_eq_zero_iff, MonomialOrder.leadingTerm, ite_eq_right_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
⊢ f = 0 → 0 = m.degree f

Tactic:
simp_intro h
-- 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
simp : f = 0 → 0 = m.degree f
⊢ m.degree (m.leadingTerm f) = m.degree f

Tactic:
classical
  simp only [leadingTerm, degree_monomial, leadingCoeff_eq_zero_iff, ite_eq_right_iff]
  simp_intro h

Premises used: MonomialOrder.degree_monomial, MonomialOrder.leadingCoeff_eq_zero_iff, MonomialOrder.leadingTerm, ite_eq_right_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
⊢ m.leadingCoeff (m.leadingTerm f) = m.leadingCoeff f

Tactic:
simp [leadingTerm, leadingCoeff_monomial]

Premises used: MonomialOrder.leadingTerm, MonomialOrder.leadingCoeff_monomial
-- 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
pos : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
neg : ∀ (h : ¬f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

Tactic:
by_cases h : f = 0
-- 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
h : f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

Tactic:
simp [leadingTerm, h, degree_monomial]

Premises used: MonomialOrder.degree_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
f : MvPolynomial σ R
h : ¬f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

Tactic:
simp [leadingTerm, h, degree_monomial]

Premises used: MonomialOrder.degree_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
f : MvPolynomial σ R
pos : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
neg : ∀ (h : ¬f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
pos₁ : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
neg₁ : ∀ (h : ¬f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
pos₂ : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
neg₂ : ∀ (h : ¬f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
pos₃ : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
neg₃ : ∀ (h : ¬f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

Tactic:
classical
  by_cases h : f = 0 <;> simp [leadingTerm, h, degree_monomial]

Premises used: MonomialOrder.degree_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
c : R
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((C : (a : R) → MvPolynomial σ R) c)) ((C : (a : R) → MvPolynomial σ R) c)

Tactic:
simp [leadingTerm, leadingCoeff_C]

Premises used: MonomialOrder.leadingTerm, MonomialOrder.leadingCoeff_C
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
c : R
pos :
  ∀ (h : c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
neg :
  ∀ (h : ¬c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)

Tactic:
by_cases h : c = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
c : R
h : c = 0
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)

Tactic:
simp [leadingTerm, degree_monomial, h]

Premises used: MonomialOrder.degree_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
s : σ →₀ ℕ
c : R
h : ¬c = 0
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)

Tactic:
simp [leadingTerm, degree_monomial, h]

Premises used: MonomialOrder.degree_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
s : σ →₀ ℕ
c : R
pos :
  ∀ (h : c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
neg :
  ∀ (h : ¬c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
pos₁ :
  ∀ (h : c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
neg₁ :
  ∀ (h : ¬c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
pos₂ :
  ∀ (h : c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
neg₂ :
  ∀ (h : ¬c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
pos₃ :
  ∀ (h : c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
neg₃ :
  ∀ (h : ¬c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)

Tactic:
classical
  by_cases h : c = 0 <;> simp [leadingTerm, degree_monomial, h]

Premises used: MonomialOrder.degree_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
inst_1 : NoZeroDivisors R
p q : MvPolynomial σ R
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
        (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q))
    (h : p = 0 ∨ q = 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
wlog! :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)

Tactic:
wlog! +distrib h : p ≠ 0 ∧ 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
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
h : p = 0 ∨ q = 0
inr : m.degree (m.leadingTerm 0 * q) = m.degree (0 * q)
inr₁ : m.degree (m.leadingTerm p * 0) = m.degree (p * 0)
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)

Tactic:
obtain rfl | rfl := h

Premises used: rfl
-- 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
q : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm 0 * q) = m.degree (0 * q)

Tactic:
simp
-- 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 : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm p * 0) = m.degree (p * 0)

Tactic:
simp
-- 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 q : MvPolynomial σ R
h : p ≠ 0 ∧ q ≠ 0
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)

Tactic:
simp [leadingTerm, degree_mul, h, degree_monomial]

Premises used: MonomialOrder.degree_monomial, MonomialOrder.leadingTerm, MonomialOrder.degree_mul
-- 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 q : MvPolynomial σ R
h : p ≠ 0 ∧ q ≠ 0
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)

Tactic:
classical
  simp [leadingTerm, degree_mul, h, degree_monomial]

Premises used: MonomialOrder.degree_monomial, 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 : NoZeroDivisors R
p q : MvPolynomial σ R
⊢ m.degree (p * m.leadingTerm q) = m.degree (p * q)

Tactic:
mul_comm _ p ▸ mul_comm _ p ▸ m.degree_leadingTerm_mul q p

Premises used: Eq.rec, MonomialOrder.degree_leadingTerm_mul, mul_comm
-- 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
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' * q)) : m.syn)
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
        {p p' q : MvPolynomial σ R} (hp : p ≠ 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' * q)) : m.syn))
        (hq : q ≠ 0),
        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))
    (hq : q = 0),
    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)
wlog! :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    {p p' q : MvPolynomial σ R} (hp : p ≠ 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' * q)) : m.syn))
    (hq : q ≠ 0),
    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) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)

Tactic:
wlog! hq : 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 p' q : MvPolynomial σ R
hp : p ≠ 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' * q)) : m.syn)
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    {p p' q : MvPolynomial σ R} (hp : p ≠ 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' * q)) : m.syn))
    (hq : q ≠ 0),
    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)
hq : q = 0
⊢ 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:
simp [hq] at h
-- 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
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' * q)) : m.syn)
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' + m.degree q) : m.syn)

Tactic:
apply lt_of_le_of_lt' m.degree_mul_le at h

Premises used: MonomialOrder.degree_mul_le, lt_of_le_of_lt'