awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b

Tactic:
have H : m.degree f =
      m.degree ((monomial (m.degree f - m.degree b)) (hb.unit⁻¹ * m.leadingCoeff f)) +
        m.degree b := by
    classical
    rw [degree_monomial, if_neg]
    · ext d
      rw [tsub_add_cancel_of_le hbf]
    · simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
simp :
  coeff (m.degree f) f =
    coeff (m.degree f)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
⊢ coeff (m.degree f) (m.reduce hb f) = 0

Tactic:
simp only [reduce, coeff_sub, sub_eq_zero]

Premises used: sub_eq_zero, MonomialOrder.reduce, MvPolynomial.coeff_sub
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
nth_rewrite :
  coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
⊢ coeff (m.degree f) f =
    coeff (m.degree f)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)

Tactic:
nth_rewrite 2 [H]
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
rw :
  coeff (m.degree f) f =
    m.leadingCoeff
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
      m.leadingCoeff b
rw₁ : coeff (m.degree f) f = (↑hb.unit⁻¹ : R) * m.leadingCoeff f * m.leadingCoeff b
rw₂ : coeff (m.degree f) f = m.leadingCoeff b * ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)
rw₃ : coeff (m.degree f) f = m.leadingCoeff b * (↑hb.unit⁻¹ : R) * m.leadingCoeff f
rw₄ : coeff (m.degree f) f = 1 * m.leadingCoeff f
rw₅ : coeff (m.degree f) f = m.leadingCoeff f
rw₆ rw₇ : m.leadingCoeff f = m.leadingCoeff f
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)

Tactic:
rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]

Premises used: IsUnit.mul_val_inv, MonomialOrder.leadingCoeff, mul_assoc, MonomialOrder.leadingCoeff_monomial, mul_comm, MonomialOrder.coeff_mul_of_degree_add, one_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
⊢ coeff (m.degree f) (m.reduce hb f) = 0

Tactic:
have H' : coeff (m.degree f) (m.reduce hb f) = 0 := by
    simp only [reduce, coeff_sub, sub_eq_zero]
    nth_rewrite 2 [H]
    rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
rw :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
    Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
rw [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
left :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
right :
  Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
    Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
left :
  LE.le.{u_3} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
                MvPolynomial σ R)
              b))) :
      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 (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply le_trans degree_sub_le

Premises used: MonomialOrder.degree_sub_le, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
left :
  LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
              MvPolynomial σ R)
            b)) :
      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
            (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
                MvPolynomial σ R)
              b))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
simp only [sup_le_iff, le_refl, true_and]

Premises used: le_refl, sup_le_iff, true_and
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
left :
  Eq.{u_3 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (degree.{u_1, u_2, u_3} m (R := R)
            ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
          m.degree b) :
      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
          (HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
              MvPolynomial σ R)
            b)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply le_of_le_of_eq degree_mul_le

Premises used: le_of_le_of_eq, MonomialOrder.degree_mul_le
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
left :
  degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b =
    m.degree f
⊢ Eq.{u_3 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (degree.{u_1, u_2, u_3} m (R := R)
            ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
          m.degree b) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
rw [m.toSyn.injective.eq_iff]

Premises used: Function.Injective.eq_iff, AddEquiv.injective, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b =
    m.degree f

Tactic:
H.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b =
    m.degree f

Tactic:
exact H.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
left :
  LE.le.{u_3} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (α := MvPolynomial σ R)
              ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
                MvPolynomial σ R)
              b))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
left₁ :
  LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
              MvPolynomial σ R)
            b)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
left₂ :
  Eq.{u_3 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (degree.{u_1, u_2, u_3} m (R := R)
            ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
          m.degree b) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
left₃ :
  degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b =
    m.degree f
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
classical
    apply le_trans degree_sub_le
    simp only [sup_le_iff, le_refl, true_and]
    apply le_of_le_of_eq degree_mul_le
    rw [m.toSyn.injective.eq_iff]
    exact H.symm

Premises used: le_refl, MonomialOrder.degree_sub_le, le_of_le_of_eq, Function.Injective.eq_iff, MonomialOrder.degree_mul_le, sup_le_iff, AddEquiv.injective, Eq.symm, true_and, MonomialOrder.toSyn, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree (m.reduce hb f) = m.degree f

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq] at K

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ coeff (m.degree (m.reduce hb f)) (m.reduce hb f) = 0

Tactic:
nth_rewrite 1 [← K] at H'
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.degree (m.reduce hb f) = m.degree f
H'₁ : coeff (m.degree (m.reduce hb f)) (m.reduce hb f) = 0
⊢ m.degree (m.reduce hb f) = m.degree f

Tactic:
nth_rewrite 1 [← K] at H'
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree (m.reduce hb f)) (m.reduce hb f) = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ m.reduce hb f = 0

Tactic:
rw [← leadingCoeff, leadingCoeff_eq_zero_iff] at H'

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree (m.reduce hb f)) (m.reduce hb f) = 0
K : m.degree (m.reduce hb f) = m.degree f
H'₁ : m.reduce hb f = 0
⊢ m.degree (m.reduce hb f) = m.degree f

Tactic:
rw [← leadingCoeff, leadingCoeff_eq_zero_iff] at H'

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : m.reduce hb f = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ 0 = m.degree f

Tactic:
rw [H', degree_zero] at K

Premises used: MonomialOrder.degree_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : m.reduce hb f = 0
K : 0 = m.degree f
⊢ False

Tactic:
hf K.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : m.reduce hb f = 0
K : 0 = m.degree f
⊢ False

Tactic:
exact hf K.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
pos :
  ∀ (hb' : ∃ (i : ι), m.degree (b i) = 0),
    ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
      f =
          HAdd.hAdd (α := MvPolynomial σ R)
            ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g :
              MvPolynomial σ R)
            r ∧
        (∀ (i : ι),
            LE.le.{u_4} (α := m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
                  (m.degree
                    (HMul.hMul (β := MvPolynomial σ R) (b i) ((g : (a : ι) → MvPolynomial σ R) i : MvPolynomial σ R))) :
                m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
          ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
neg :
  ∀ (hb' : ∀ (i : ι), m.degree (b i) ≠ 0),
    ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
      f =
          HAdd.hAdd (α := MvPolynomial σ R)
            ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g :
              MvPolynomial σ R)
            r ∧
        (∀ (i : ι),
            LE.le.{u_4} (α := m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
                  (m.degree
                    (HMul.hMul (β := MvPolynomial σ R) (b i) ((g : (a : ι) → MvPolynomial σ R) i : MvPolynomial σ R))) :
                m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
          ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
    f =
        HAdd.hAdd (α := MvPolynomial σ R)
          ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g :
            MvPolynomial σ R)
          r ∧
      (∀ (i : ι),
          LE.le.{u_4} (α := m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
                (m.degree
                  (HMul.hMul (β := MvPolynomial σ R) (b i) ((g : (a : ι) → MvPolynomial σ R) i : MvPolynomial σ R))) :
              m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
by_cases! hb' : ∃ i, m.degree (b i) = 0