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
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
⊢ ∃ (g' : ι →₀ MvPolynomial σ R) (r' : MvPolynomial σ R),
    m.subLTerm 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 (m.subLTerm f)) : m.syn)) ∧
        ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
have pos : ∀ (hf'0 : m.subLTerm f = 0),
  ∃ (g' : ι →₀ MvPolynomial σ R) (r' : MvPolynomial σ R),
    m.subLTerm 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 (m.subLTerm f)) : m.syn)) ∧
        ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Tactic: by_cases hf'0 : m.subLTerm 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
pos :
  ∀ (hf'0 : m.subLTerm f = 0),
    ∃ (g' : ι →₀ MvPolynomial σ R) (r' : MvPolynomial σ R),
      m.subLTerm 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 (m.subLTerm f)) : m.syn)) ∧
          ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∃ (g' : ι →₀ MvPolynomial σ R) (r' : MvPolynomial σ R),
    m.subLTerm 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 (m.subLTerm f)) : m.syn)) ∧
        ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
have neg : ∀ (hf'0 : ¬m.subLTerm f = 0),
  ∃ (g' : ι →₀ MvPolynomial σ R) (r' : MvPolynomial σ R),
    m.subLTerm 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 (m.subLTerm f)) : m.syn)) ∧
        ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Tactic: by_cases hf'0 : m.subLTerm 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
hf'0 : m.subLTerm f = 0
⊢ ∃ (g' : ι →₀ MvPolynomial σ R) (r' : MvPolynomial σ R),
    m.subLTerm 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 (m.subLTerm 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 (m.subLTerm f)) : m.syn)
Tactic: refine ⟨0, 0, by simp [hf'0], ?_, 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
hf : ∀ (i : ι), ¬m.degree (b_1 i) ≤ m.degree f
hf'0 : m.subLTerm 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 (m.subLTerm f)) : m.syn)
have pos : LE.le.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm 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
h :
  ∀ (y : MvPolynomial σ R),
    (invImage (β := { x : m.syn // Acc (fun (x x_1 : m.syn) ↦ x < x_1) x })
              (fun (x : MvPolynomial σ R) ↦
                ⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree x)))
              (Acc.wfRel (r := fun (x x_1 : m.syn) ↦ x < x_1)) :
            WellFoundedRelation (MvPolynomial σ R)).1
        y f →
      ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
        y =
            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 y) : m.syn)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ (i : ι), m.degree (b i) = 0
hf0 : ¬f = 0
hf : ¬∃ (i : ι), m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
⊢ (↑(⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)))) :
      m.syn) <
    (↑(⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))) : m.syn)
have hf₁ : m.degree f ≠ 0
Tactic: apply degree_sub_LTerm_lt
-- 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
h :
  ∀ (y : MvPolynomial σ R),
    (invImage (β := { x : m.syn // Acc (fun (x x_1 : m.syn) ↦ x < x_1) x })
              (fun (x : MvPolynomial σ R) ↦
                ⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree x)))
              (Acc.wfRel (r := fun (x x_1 : m.syn) ↦ x < x_1)) :
            WellFoundedRelation (MvPolynomial σ R)).1
        y f →
      ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
        y =
            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 y) : m.syn)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ (i : ι), m.degree (b i) = 0
hf0_1 : ¬f = 0
hf : ¬∃ (i : ι), m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
hf0 : m.degree f = 0
⊢ False
have hf₁ : m.subLTerm f = 0
Tactic: apply hf'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
h :
  ∀ (y : MvPolynomial σ R),
    (invImage (β := { x : m.syn // Acc (fun (x x_1 : m.syn) ↦ x < x_1) x })
              (fun (x : MvPolynomial σ R) ↦
                ⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree x)))
              (Acc.wfRel (r := fun (x x_1 : m.syn) ↦ x < x_1)) :
            WellFoundedRelation (MvPolynomial σ R)).1
        y f →
      ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
        y =
            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 y) : m.syn)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ (i : ι), m.degree (b i) = 0
hf0_1 : ¬f = 0
hf : ¬∃ (i : ι), m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
hf0 : m.degree f = 0
⊢ m.subLTerm f = 0
have hf₁ : f = (monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)
Tactic: simp only [subLTerm, sub_eq_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
h :
  ∀ (y : MvPolynomial σ R),
    (invImage (β := { x : m.syn // Acc (fun (x x_1 : m.syn) ↦ x < x_1) x })
              (fun (x : MvPolynomial σ R) ↦
                ⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree x)))
              (Acc.wfRel (r := fun (x x_1 : m.syn) ↦ x < x_1)) :
            WellFoundedRelation (MvPolynomial σ R)).1
        y f →
      ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
        y =
            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 y) : m.syn)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ (i : ι), m.degree (b i) = 0
hf0_1 : ¬f = 0
hf : ¬∃ (i : ι), m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
hf0 : m.degree f = 0
⊢ f = (monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)
have hf₁ : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
  ((monomial 0 : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
Tactic: nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0]
-- 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
B : Set (MvPolynomial σ R)
hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∃ (g : (↑B : Type (max u_1 u_2)) →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
    f =
        HAdd.hAdd (α := MvPolynomial σ R)
          ((Finsupp.linearCombination (MvPolynomial σ R) fun (b : (↑B : Type (max u_1 u_2))) ↦ (↑b : MvPolynomial σ R) :
                (a : (↑B : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
              g :
            MvPolynomial σ R)
          r ∧
      (∀ (b : (↑B : Type (max u_1 u_2))),
          LE.le.{u_3} (α := m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
                (m.degree
                  (HMul.hMul (β := MvPolynomial σ R) (↑b : MvPolynomial σ R)
                    ((g : (a : (↑B : Type (max u_1 u_2))) → MvPolynomial σ R) b : MvPolynomial σ R))) :
              m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
        ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c
have obtain : ∀ (g : (↑B : Type (max u_1 u_2)) →₀ MvPolynomial σ R) (r : MvPolynomial σ R)
  (H :
    f =
        HAdd.hAdd (α := MvPolynomial σ R)
          ((Finsupp.linearCombination (MvPolynomial σ R) fun (p : (↑B : Type (max u_1 u_2))) ↦ (↑p : MvPolynomial σ R) :
                (a : (↑B : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
              g :
            MvPolynomial σ R)
          r ∧
      (∀ (i : (↑B : Type (max u_1 u_2))),
          LE.le.{u_3} (α := m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
                (m.degree
                  (HMul.hMul (β := MvPolynomial σ R) (↑i : MvPolynomial σ R)
                    ((g : (a : (↑B : Type (max u_1 u_2))) → MvPolynomial σ R) i : MvPolynomial σ R))) :
              m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
        ∀ c ∈ r.support, ∀ (i : (↑B : Type (max u_1 u_2))), ¬m.degree (↑i : MvPolynomial σ R) ≤ c),
  ∃ (g : (↑B : Type (max u_1 u_2)) →₀ MvPolynomial σ R) (r : MvPolynomial σ R),
    f =
        HAdd.hAdd (α := MvPolynomial σ R)
          ((Finsupp.linearCombination (MvPolynomial σ R) fun (b : (↑B : Type (max u_1 u_2))) ↦ (↑b : MvPolynomial σ R) :
                (a : (↑B : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
              g :
            MvPolynomial σ R)
          r ∧
      (∀ (b : (↑B : Type (max u_1 u_2))),
          LE.le.{u_3} (α := m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
                (m.degree
                  (HMul.hMul (β := MvPolynomial σ R) (↑b : MvPolynomial σ R)
                    ((g : (a : (↑B : Type (max u_1 u_2))) → MvPolynomial σ R) b : MvPolynomial σ R))) :
              m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
        ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c
Tactic: obtain ⟨g, r, H⟩ := m.div (b := fun (p : B) ↦ p) (fun b ↦ hB b b.prop) f
-- 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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∃ (g : MvPolynomial σ R) (r : MvPolynomial σ R),
    f = g * b + r ∧
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
        ∀ c ∈ r.support, ¬m.degree b ≤ c
have obtain : ∀ (g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) (r : MvPolynomial σ R)
  (hgr :
    f =
      HAdd.hAdd (α := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
                (↑b_1 : MvPolynomial σ R) :
              (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
            g :
          MvPolynomial σ R)
        r)
  (h1 :
    ∀ (b_1 : (↑{b} : Type (max u_1 u_2))),
      LE.le.{u_3} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
            (m.degree
              (HMul.hMul (β := MvPolynomial σ R) (↑b_1 : MvPolynomial σ R)
                ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R) b_1 : MvPolynomial σ R))) :
          m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn))
  (h2 :
    ∀ c ∈ r.support,
      ∀ (b_1 : MvPolynomial σ R), Membership.mem (γ := Set (MvPolynomial σ R)) {b} b_1 → ¬m.degree b_1 ≤ c),
  ∃ (g : MvPolynomial σ R) (r : MvPolynomial σ R),
    f = g * b + r ∧
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
        ∀ c ∈ r.support, ¬m.degree b ≤ c
Tactic: obtain ⟨g, r, hgr, h1, h2⟩ := div_set (B := {b}) (m := m) (by simp [hb]) f
-- 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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
h1 :
  ∀ (b_1 : (↑{b} : Type (max u_1 u_2))),
    LE.le.{u_3} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (β := MvPolynomial σ R) (↑b_1 : MvPolynomial σ R)
              ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R) b_1 : MvPolynomial σ R))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 :
  ∀ c ∈ r.support, ∀ (b_1 : MvPolynomial σ R), Membership.mem (γ := Set (MvPolynomial σ R)) {b} b_1 → ¬m.degree b_1 ≤ c
⊢ ∃ (g : MvPolynomial σ R) (r : MvPolynomial σ R),
    f = g * b + r ∧
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
        ∀ c ∈ r.support, ¬m.degree b ≤ c
have h1₁ : LE.le.{u_3} (α := m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
      (m.degree
        (HMul.hMul (β := MvPolynomial σ R)
          (↑(Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b sorry) :
            MvPolynomial σ R)
          ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
              (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b sorry) :
            MvPolynomial σ R))) :
    m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: specialize h1 ⟨b, by simp⟩
Cleared hypotheses: h1
-- 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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
h2 :
  ∀ c ∈ r.support, ∀ (b_1 : MvPolynomial σ R), Membership.mem (γ := Set (MvPolynomial σ R)) {b} b_1 → ¬m.degree b_1 ≤ c
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          ((↑(Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯) :
              MvPolynomial σ R) *
            q)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ ∃ (g : MvPolynomial σ R) (r : MvPolynomial σ R),
    f = g * b + r ∧
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
        ∀ c ∈ r.support, ¬m.degree b ≤ c
have h2₁ : ∀ c ∈ r.support, ¬m.degree b ≤ c
Tactic: simp only [Set.mem_singleton_iff, forall_eq] at h2
Cleared hypotheses: h2
-- 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
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∃ (g : MvPolynomial σ R) (r : MvPolynomial σ R),
    f = g * b + r ∧
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
        ∀ c ∈ r.support, ¬m.degree b ≤ c
have refine : f = q * b + r
Tactic: refine ⟨q, r, ?_, h1, h2⟩