awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
H' :
  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
c : σ →₀ ℕ
hc :
  c ∈
    (HAdd.hAdd (β := MvPolynomial σ R) r'
        ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)).support
i : ι
hc' : c ∉ r'.support
this :
  c ∈ r'.support ∪ support.{u_2, u_1} (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))
⊢ c ∉ r'.support →
    Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u_2, u_1} (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) c

Tactic:
rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this

Premises used: Classical.or_iff_not_imp_left, Finset.mem_union
-- 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
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
H' :
  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
c : σ →₀ ℕ
hc :
  c ∈
    (HAdd.hAdd (β := MvPolynomial σ R) r'
        ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)).support
i : ι
hc' : c ∉ r'.support
this :
  c ∉ r'.support →
    Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u_2, u_1} (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) c
⊢ c = m.degree f

Tactic:
simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')

Premises used: Finset.mem_singleton, MvPolynomial.support_monomial_subset
-- 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
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
H' :
  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
c : σ →₀ ℕ
hc :
  c ∈
    (HAdd.hAdd (β := MvPolynomial σ R) r'
        ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)).support
i : ι
hc' : c ∉ r'.support
h h₁ h₂ :
  ∀
    (this :
      c ∈
        r'.support ∪
          support.{u_2, u_1} (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))),
    c = m.degree f
h₃ :
  ∀
    (this :
      c ∉ r'.support →
        Membership.mem (γ := Finset (σ →₀ ℕ))
          (support.{u_2, u_1} (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) c),
    c = m.degree f
⊢ c = m.degree f

Tactic:
classical
          have := MvPolynomial.support_add hc
          rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this
          simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')

Premises used: Finset.mem_singleton, Classical.or_iff_not_imp_left, Finset.mem_union
-- 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
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
neg :
  ∃ (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),
    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:
suffices ∃ (g' : ι →₀ MvPolynomial σ R), ∃ r',
        (m.subLTerm f = Finsupp.linearCombination (MvPolynomial σ R) b g' + r') ∧
        (∀ i, m.degree ((b i) * (g' i)) ≼[m] m.degree (m.subLTerm f)) ∧
        (∀ c ∈ r'.support, ∀ i, ¬ m.degree (b i) ≤ c) by
      obtain ⟨g', r', H'⟩ := this
      use g', r' + monomial (m.degree f) (m.leadingCoeff f)
      constructor
      · simp [← add_assoc, ← H'.1, subLTerm]
      constructor
      · exact fun b ↦ le_trans (H'.2.1 b) (degree_sub_LTerm_le f)
      · intro c hc i
        by_cases hc' : c ∈ r'.support
        · exact H'.2.2 c hc' i
        · convert! hf i
          classical
          have := MvPolynomial.support_add hc
          rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this
          simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')
-- 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
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
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
⊢ ∃ (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

Premises used: MonomialOrder.subLTerm
-- 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
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
⊢ m.subLTerm f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) 0) 0

Tactic:
simp [hf'0]
-- 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
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
⊢ ∀ (c : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) 0) c → ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
simp
-- 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
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
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)
⊢ ∃ (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:
refine ⟨0, 0, by simp [hf'0], ?_, by simp⟩
-- 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_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 : ι
pos : LE.le.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
⊢ 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)

Tactic:
simp only [Finsupp.coe_zero, Pi.zero_apply, mul_zero, degree_zero, map_zero]

Premises used: Pi.zero_apply, map_zero, MulZeroClass.mul_zero, MonomialOrder.degree_zero, Finsupp.coe_zero
-- 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_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) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)

Tactic:
bot_le

Premises used: bot_le
-- 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_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) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)

Tactic:
exact bot_le

Premises used: bot_le
-- 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
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

Tactic:
(div hb) (m.subLTerm f)

Premises used: MonomialOrder.subLTerm
-- 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
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

Tactic:
exact (div hb) (m.subLTerm f)

Premises used: MonomialOrder.subLTerm
-- 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
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_1 : ∃ (i : ι), m.degree (b i) ≤ m.degree f
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ (↑(⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)))) :
      m.syn) <
    (↑(⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))) : m.syn)

Tactic:
deg_reduce
-- 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
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_1 : ∃ (i : ι), m.degree (b i) ≤ m.degree f
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ (↑(⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)))) :
      m.syn) <
    (↑(⋯.wrap (r := fun (x x_1 : m.syn) ↦ x < x_1) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))) : m.syn)

Tactic:
exact deg_reduce
-- 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
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
hf₁ : m.degree 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)

Tactic:
apply degree_sub_LTerm_lt

Premises used: MonomialOrder.degree_sub_LTerm_lt
-- 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
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
hf₁ : m.subLTerm f = 0
⊢ False

Tactic:
apply hf'0