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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
neg :
  coeff (m.degree f) (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) f) ≠ 0
⊢ m.degree f ∈ (r • f).support

Tactic:
simp only [mem_support_iff, smul_eq_C_mul]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.smul_eq_C_mul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
neg : m.leadingCoeff ((C : (a : R) → MvPolynomial σ R) r) * m.leadingCoeff f ≠ 0
⊢ coeff (m.degree f) (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) f) ≠ 0

Tactic:
rw [← zero_add (degree m f), ← degree_C r, coeff_mul_of_degree_add]

Premises used: MonomialOrder.degree_C, zero_add, MonomialOrder.degree, MonomialOrder.coeff_mul_of_degree_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.leadingCoeff ((C : (a : R) → MvPolynomial σ R) r) * m.leadingCoeff f ≠ 0

Tactic:
simp [not_imp_not.mpr ((mem_nonZeroDivisors_iff.mp hr).1 _) <| m.leadingCoeff_ne_zero_iff.mpr hf]

Premises used: Iff.mpr, mem_nonZeroDivisors_iff, And.left, Iff.mp, MonomialOrder.leadingCoeff_ne_zero_iff, 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
r : R
hr : IsRegular r
f : MvPolynomial σ R
⊢ m.degree (r • f) = m.degree f

Tactic:
m.degree_smul_of_mem_nonZeroDivisors hr.mem_nonZeroDivisors

Premises used: IsRegular.mem_nonZeroDivisors, MonomialOrder.degree_smul_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
empty :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) 1) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)

Tactic:
simp only [Finset.prod_empty, Finset.sum_empty]

Premises used: Finset.prod_empty, Finset.sum_empty
-- 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
empty :
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial σ R) 1)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
empty₁ : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0)
empty₂ empty₃ : LE.le.{u_4} (α := m.syn) 0 0
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) 1) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)

Tactic:
rw [← C_1, m.degree_C, map_zero]

Premises used: MvPolynomial.C_1, map_zero, MonomialOrder.degree_C
-- 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
a : ι
s : Finset ι
has : a ∉ s
hrec :
  LE.le.{u_4} (α := 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)
insert :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a * ∏ x ∈ s, P x)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + ∑ x ∈ s, m.degree (P x)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ Insert.insert a s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ Insert.insert a s, m.degree (P i)) : m.syn)

Tactic:
rw [Finset.prod_insert has, Finset.sum_insert has]

Premises used: Finset.prod_insert, Finset.sum_insert
-- 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
a : ι
s : Finset ι
has : a ∉ s
hrec :
  LE.le.{u_4} (α := 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)
insert :
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + degree.{u_1, u_2, u_4} m (R := R) (∏ x ∈ s, P x)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + ∑ x ∈ s, m.degree (P x)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a * ∏ x ∈ s, P x)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + ∑ x ∈ s, m.degree (P x)) : m.syn)

Tactic:
apply le_trans degree_mul_le

Premises used: MonomialOrder.degree_mul_le, 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
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec :
  LE.le.{u_4} (α := 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)
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + degree.{u_1, u_2, u_4} m (R := R) (∏ x ∈ s, P x)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + ∑ x ∈ s, m.degree (P x)) : m.syn)

Tactic:
simp only [map_add, add_le_add_iff_left, hrec]

Premises used: add_le_add_iff_left, map_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
P : ι → MvPolynomial σ R
s : Finset ι
empty :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (hrec :
      LE.le.{u_4} (α := 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)),
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ Insert.insert a s, P i)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ Insert.insert a s, m.degree (P i)) : m.syn)
⊢ LE.le.{u_4} (α := 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:
induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.prod_empty, Finset.sum_empty]
    rw [← C_1, m.degree_C, map_zero]
  | insert a s has hrec =>
    rw [Finset.prod_insert has, Finset.sum_insert has]
    apply le_trans degree_mul_le
    simp only [map_add, add_le_add_iff_left, hrec]

Premises used: Finset.prod_empty, add_le_add_iff_left, MvPolynomial.C_1, map_zero, map_add, Insert.insert, MonomialOrder.degree_mul_le, MonomialOrder.degree_C, Finset.sum_empty, 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
P : ι → MvPolynomial σ R
s : Finset ι
empty :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (hrec :
      LE.le.{u_4} (α := 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)),
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ Insert.insert a s, P i)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ Insert.insert a s, m.degree (P i)) : m.syn)
⊢ LE.le.{u_4} (α := 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:
classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.prod_empty, Finset.sum_empty]
    rw [← C_1, m.degree_C, map_zero]
  | insert a s has hrec =>
    rw [Finset.prod_insert has, Finset.sum_insert has]
    apply le_trans degree_mul_le
    simp only [map_add, add_le_add_iff_left, hrec]

Premises used: Finset.prod_empty, add_le_add_iff_left, MvPolynomial.C_1, map_zero, map_add, Insert.insert, MonomialOrder.degree_mul_le, MonomialOrder.degree_C, Finset.sum_empty, 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
P : ι → MvPolynomial σ R
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i))
    (∏ i ∈ ∅, m.leadingCoeff (P i))

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
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
insert :
  coeff (m.degree (P a) + ∑ i ∈ s, m.degree (P i)) (P a * ∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)
⊢ Eq.{u_2 + 1} (α := R)
    (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ Insert.insert a s, m.degree (P i)) (∏ i ∈ Insert.insert a s, P i))
    (∏ i ∈ Insert.insert a s, m.leadingCoeff (P i))

Tactic:
simp only [Finset.prod_insert has, Finset.sum_insert has]

Premises used: Finset.prod_insert, Finset.sum_insert
-- 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
a : ι
s : Finset ι
has : a ∉ s
hrec :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
insert :
  coeff (m.degree (P a)) (P a) * coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (m.degree (P a) + ∑ i ∈ s, m.degree (P i)) (P a * ∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]

Premises used: MonomialOrder.degree_prod_le, le_of_eq, MonomialOrder.coeff_mul_of_add_of_degree_le, rfl
-- 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
a : ι
s : Finset ι
has : a ∉ s
hrec :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
⊢ coeff (m.degree (P a)) (P a) * coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
congr_arg₂ _ rfl hrec

Premises used: rfl, congr_arg₂
-- 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
a : ι
s : Finset ι
has : a ∉ s
hrec :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
⊢ coeff (m.degree (P a)) (P a) * coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
exact congr_arg₂ _ rfl hrec

Premises used: rfl, congr_arg₂
-- 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 ι
empty :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i))
    (∏ i ∈ ∅, m.leadingCoeff (P i))
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (hrec :
      Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
        (∏ i ∈ s, m.leadingCoeff (P i))),
    Eq.{u_2 + 1} (α := R)
      (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ Insert.insert a s, m.degree (P i)) (∏ i ∈ Insert.insert a s, P i))
      (∏ i ∈ Insert.insert a s, m.leadingCoeff (P i))
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert a s has hrec =>
    simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec

Premises used: Insert.insert, MonomialOrder.degree_prod_le, le_of_eq, MonomialOrder.coeff_mul_of_add_of_degree_le, rfl
-- 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 ι
empty :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i))
    (∏ i ∈ ∅, m.leadingCoeff (P i))
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (hrec :
      Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
        (∏ i ∈ s, m.leadingCoeff (P i))),
    Eq.{u_2 + 1} (α := R)
      (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ Insert.insert a s, m.degree (P i)) (∏ i ∈ Insert.insert a s, P i))
      (∏ i ∈ Insert.insert a s, m.leadingCoeff (P i))
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has hrec =>
    simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec

Premises used: Insert.insert, MonomialOrder.degree_prod_le, le_of_eq, MonomialOrder.coeff_mul_of_add_of_degree_le, rfl
-- 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))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
h : Nontrivial R
inr : Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))

Tactic:
rw [mem_support_iff, m.coeff_prod_sum_degree]

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.coeff_prod_sum_degree
-- 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))
h : Nontrivial R
⊢ Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0

Tactic:
nonZeroDivisors.ne_zero (prod_mem_nonZeroDivisors_of_mem_nonZeroDivisors H)

Premises used: nonZeroDivisors.ne_zero, prod_mem_nonZeroDivisors_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, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
h : Nontrivial R
⊢ Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0

Tactic:
exact nonZeroDivisors.ne_zero (prod_mem_nonZeroDivisors_of_mem_nonZeroDivisors H)

Premises used: nonZeroDivisors.ne_zero, prod_mem_nonZeroDivisors_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, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
⊢ 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 ?_)
    rw [mem_support_iff, m.coeff_prod_sum_degree]
    exact nonZeroDivisors.ne_zero (prod_mem_nonZeroDivisors_of_mem_nonZeroDivisors H)

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.le_degree, MonomialOrder.coeff_prod_sum_degree, subsingleton_or_nontrivial, le_antisymm, MonomialOrder.degree_prod_le, 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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h : Nontrivial R
inr : Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))

Tactic:
rw [mem_support_iff, m.coeff_prod_sum_degree]

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.coeff_prod_sum_degree
-- 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))
h : Nontrivial R
⊢ Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0

Tactic:
(IsRegular.prod H).ne_zero

Premises used: IsRegular.ne_zero, IsRegular.prod
-- 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))
h : Nontrivial R
⊢ Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0

Tactic:
exact (IsRegular.prod H).ne_zero

Premises used: IsRegular.ne_zero, IsRegular.prod
-- 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))
⊢ 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 ?_)
    rw [mem_support_iff, m.coeff_prod_sum_degree]
    exact (IsRegular.prod H).ne_zero

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.le_degree, MonomialOrder.coeff_prod_sum_degree, subsingleton_or_nontrivial, le_antisymm, MonomialOrder.degree_prod_le, AddEquiv.injective, MonomialOrder.toSyn