awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ 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)
have 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)
Tactic: apply le_trans degree_sub_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ 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)
have 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)
Tactic: simp only [sup_le_iff, le_refl, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ 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)
have 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)
Tactic: apply le_of_le_of_eq degree_mul_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ 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)
have 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
Tactic: rw [m.toSyn.injective.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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)
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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)
⊢ 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)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
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)
⊢ False
have K₁ : m.degree (m.reduce hb f) = m.degree f
Tactic: simp only [EmbeddingLike.apply_eq_iff_eq] at K
Cleared hypotheses: K
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
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
⊢ False
have H'₁ : coeff (m.degree (m.reduce hb f)) (m.reduce hb f) = 0
Tactic: nth_rewrite 1 [← K] at H'
Cleared hypotheses: H', K
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
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
⊢ False
have H'₁ : m.reduce hb f = 0
Tactic: rw [← leadingCoeff, leadingCoeff_eq_zero_iff] at H'
Cleared hypotheses: H', K
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
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
⊢ False
have K₁ : 0 = m.degree f
Tactic: rw [H', degree_zero] at K
Cleared hypotheses: K
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ ∃ (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
have 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
Tactic: by_cases! hb' : ∃ i, m.degree (b i) = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ ∃ (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
have 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
Tactic: by_cases! hb' : ∃ i, m.degree (b i) = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
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
have pos : ∀ (i : ι) (hb0 : 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
Tactic: obtain ⟨i, hb0⟩ := hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
i : ι
hb0 : 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
have h : f =
    HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
          (Finsupp.single i (sorry.unit⁻¹ • f)) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R) ∧
  (∀ (i_1 : ι),
      LE.le.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
            (m.degree
              (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                ((Finsupp.single i (sorry.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
          m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
    ∀ (c : σ →₀ ℕ),
      Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) 0) c → ∀ (i : ι), ¬m.degree (b i) ≤ c
Tactic: use Finsupp.single i ((hb i).unit⁻¹ • f), 0