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_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
⊢ f =
      HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
            (Finsupp.single i (⋯.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 (⋯.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
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)
Tactic: constructor
-- 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
h :
  f =
    HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
          (Finsupp.single i (⋯.unit⁻¹ • f)) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ f =
      HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
            (Finsupp.single i (⋯.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 (⋯.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
have h₁ : (∀ (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: constructor
-- 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
⊢ f =
    HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
          (Finsupp.single i (⋯.unit⁻¹ • f)) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have h : f = sorry.unit⁻¹ • f * b i
Tactic: simp only [Finsupp.linearCombination_single, smul_eq_mul, add_zero]
-- 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
⊢ f = ⋯.unit⁻¹ • f * b i
have h : m.leadingCoeff (b i) • f = f * b i
Tactic: simp only [smul_mul_assoc, ← smul_eq_iff_eq_inv_smul, Units.smul_isUnit]
-- 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
⊢ m.leadingCoeff (b i) • f = f * b i
have h : m.leadingCoeff (b i) • f =
  HMul.hMul (β := MvPolynomial σ R) f ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff (b i)) : MvPolynomial σ R)
Tactic: nth_rewrite 2 [eq_C_of_degree_eq_zero hb0]
-- 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
⊢ m.leadingCoeff (b i) • f =
    HMul.hMul (β := MvPolynomial σ R) f ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff (b i)) : MvPolynomial σ R)
have h : m.leadingCoeff (b i) • f =
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff (b i)) : MvPolynomial σ R) f
Tactic: rw [mul_comm, smul_eq_C_mul]
-- 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
h :
  m.leadingCoeff (b i) • f =
    HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff (b i)) : MvPolynomial σ R) f
⊢ m.leadingCoeff (b i) • f =
    HMul.hMul (β := MvPolynomial σ R) f ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff (b i)) : MvPolynomial σ R)
have h₁ : HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff (b i)) : MvPolynomial σ R) f =
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff (b i)) : MvPolynomial σ R) f
Tactic: rw [mul_comm, smul_eq_C_mul]
-- 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
⊢ (∀ (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 (⋯.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
have h : ∀ (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)
Tactic: constructor
-- 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
h :
  ∀ (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 (⋯.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ (∀ (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 (⋯.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
have h₁ : ∀ (c : σ →₀ ℕ), Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) 0) c → ∀ (i : ι), ¬m.degree (b i) ≤ c
Tactic: constructor
-- 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
j : ι
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (β := MvPolynomial σ R) (b j)
            ((Finsupp.single i (⋯.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have pos : ∀ (hj : j = i),
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (β := MvPolynomial σ R) (b j)
            ((Finsupp.single i (sorry.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: by_cases hj : j = i
-- 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
j : ι
pos :
  ∀ (hj : j = i),
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (β := MvPolynomial σ R) (b j)
              ((Finsupp.single i (⋯.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (β := MvPolynomial σ R) (b j)
            ((Finsupp.single i (⋯.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have neg : ∀ (hj : ¬j = i),
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (β := MvPolynomial σ R) (b j)
            ((Finsupp.single i (sorry.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: by_cases hj : j = i
-- 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
j : ι
hj : j = i
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (β := MvPolynomial σ R) (b j)
            ((Finsupp.single i (⋯.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have pos : LE.le.{u_4} (α := m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
      (m.degree (b j) +
        degree.{u_1, u_2, u_4} m (R := R) ((Finsupp.single i (sorry.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j)) :
    m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply le_trans degree_mul_le
-- 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
j : ι
hj : j = i
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree (b j) +
          degree.{u_1, u_2, u_4} m (R := R) ((Finsupp.single i (⋯.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have pos : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (sorry.unit⁻¹ • f)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: simp only [hj, hb0, Finsupp.single_eq_same, zero_add]
-- 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
j : ι
hj : j = i
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (⋯.unit⁻¹ • f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have pos : Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (sorry.unit⁻¹ • f)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply le_of_eq
-- 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
j : ι
hj : j = i
⊢ Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (⋯.unit⁻¹ • f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have pos : m.degree (sorry.unit⁻¹ • f) = m.degree f
Tactic: simp only [EmbeddingLike.apply_eq_iff_eq]
-- 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
j : ι
hj : ¬j = i
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (β := MvPolynomial σ R) (b j)
            ((Finsupp.single i (⋯.unit⁻¹ • f) : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have neg : LE.le.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: simp only [Finsupp.single_eq_of_ne hj, mul_zero, degree_zero, map_zero]
-- 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 : ∀ (hf0 : f = 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 hf0 : f = 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
pos :
  ∀ (hf0 : f = 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 : ∀ (hf0 : ¬f = 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 hf0 : f = 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
hf0 : f = 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 : ι),
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree (HMul.hMul (β := MvPolynomial σ R) (b i) ((0 : (a : ι) → MvPolynomial σ R) i : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: refine ⟨0, 0, by simp [hf0], ?_, by simp⟩
-- 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_1 : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b_1 i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b_1 i) ≠ 0
hf0 : f = 0
b : ι
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree (HMul.hMul (β := MvPolynomial σ R) (b_1 b) ((0 : (a : ι) → MvPolynomial σ R) b : MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have pos : LE.le.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: simp only [Finsupp.coe_zero, Pi.zero_apply, mul_zero, degree_zero, map_zero]
-- 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
hf0 : ¬f = 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 : ∀ (hf : ∃ (i : ι), m.degree (b i) ≤ m.degree f),
  ∃ (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! hf : ∃ i, m.degree (b i) ≤ m.degree f