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
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
neg :
  ∀ (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
⊢ ∃ (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

Premises used: MonomialOrder.degree
-- 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 :
  ∀ (i : ι) (hf : 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
⊢ ∃ (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, hf⟩ := hf
-- 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
i : ι
hf : m.degree (b i) ≤ m.degree f
apply : m.degree f ≠ 0
⊢ 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)

Tactic:
apply degree_reduce_lt (hb i) hf

Premises used: MonomialOrder.degree_reduce_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
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
hf0' : m.degree f = 0
apply : m.degree (b i) = 0
⊢ False

Tactic:
apply hb' i
-- 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
i : ι
hf : m.degree (b i) ≤ m.degree f
hf0' : m.degree f = 0
⊢ m.degree (b i) = 0

Tactic:
simpa [hf0'] using hf
-- 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
i : ι
hf : m.degree (b i) ≤ m.degree f
⊢ 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)

Tactic:
have deg_reduce : m.degree (m.reduce (hb i) f) ≺[m] m.degree f := by
      apply degree_reduce_lt (hb i) hf
      intro hf0'
      apply hb' i
      simpa [hf0'] using hf
-- 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
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)
pos :
  ∀ (g' : ι →₀ MvPolynomial σ R) (r' : MvPolynomial σ R)
    (H' :
      m.reduce ⋯ f =
          HAdd.hAdd (α := MvPolynomial σ R)
            ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g' :
              MvPolynomial σ R)
            r' ∧
        (∀ (i_1 : ι),
            LE.le.{u_4} (α := m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
                  (m.degree
                    (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                      ((g' : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
                m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ 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
⊢ ∃ (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 ⟨g', r', H'⟩ := div hb (m.reduce (hb i) f)

Premises used: MonomialOrder.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
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
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)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f =
      HAdd.hAdd (α := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g' :
          MvPolynomial σ R)
        r' ∧
    (∀ (i_1 : ι),
        LE.le.{u_4} (α := m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
              (m.degree
                (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                  ((g' : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
            m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
h :
  f =
    HAdd.hAdd (β := MvPolynomial σ R) (m.reduce ⋯ f)
      ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
          (Finsupp.single i
            ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
              ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f))) :
        MvPolynomial σ R)
⊢ f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
          (HAdd.hAdd (β := ι →₀ MvPolynomial σ R) g'
            (Finsupp.single i
                ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                  ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
              ι →₀ MvPolynomial σ R)) :
        MvPolynomial σ R)
      r'

Tactic:
rw [map_add, add_assoc, add_comm _ r', ← add_assoc, ← H'.1]

Premises used: add_assoc, map_add, add_comm, And.left
-- 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
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)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f =
      HAdd.hAdd (α := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g' :
          MvPolynomial σ R)
        r' ∧
    (∀ (i_1 : ι),
        LE.le.{u_4} (α := m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
              (m.degree
                (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                  ((g' : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
            m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ f =
    HAdd.hAdd (β := MvPolynomial σ R) (m.reduce ⋯ f)
      ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R)
          (Finsupp.single i
            ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
              ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f))) :
        MvPolynomial σ R)

Tactic:
simp [reduce]

Premises used: MonomialOrder.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
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
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)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f =
      HAdd.hAdd (α := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g' :
          MvPolynomial σ R)
        r' ∧
    (∀ (i_1 : ι),
        LE.le.{u_4} (α := m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
              (m.degree
                (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                  ((g' : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
            m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
h :
  ∀ (i_1 : ι),
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (β := MvPolynomial σ R) (b i_1)
              ((HAdd.hAdd (β := ι →₀ MvPolynomial σ R) g'
                      (Finsupp.single i
                          ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                            ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                        ι →₀ MvPolynomial σ R) :
                    (a : ι) → MvPolynomial σ R)
                  i_1 :
                MvPolynomial σ R))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h₁ : ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ (∀ (i_1 : ι),
      LE.le.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
            (m.degree
              (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                ((HAdd.hAdd (β := ι →₀ MvPolynomial σ R) g'
                        (Finsupp.single i
                            ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                              ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                          ι →₀ MvPolynomial σ R) :
                      (a : ι) → MvPolynomial σ R)
                    i_1 :
                  MvPolynomial σ R))) :
          m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)) ∧
    ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
constructor
-- 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
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)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f =
      HAdd.hAdd (α := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g' :
          MvPolynomial σ R)
        r' ∧
    (∀ (i_1 : ι),
        LE.le.{u_4} (α := m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
              (m.degree
                (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                  ((g' : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
            m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
h :
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (b j *
            HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
              ((g' : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R)
              (((Finsupp.single i
                        ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                          ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                      ι →₀ MvPolynomial σ R) :
                    (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)
            ((HAdd.hAdd (β := ι →₀ MvPolynomial σ R) g'
                    (Finsupp.single i
                        ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                          ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                      ι →₀ MvPolynomial σ R) :
                  (a : ι) → MvPolynomial σ R)
                j :
              MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
simp only [Finsupp.coe_add, Pi.add_apply]

Premises used: Pi.add_apply, Finsupp.coe_add
-- 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
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)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f =
      HAdd.hAdd (α := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g' :
          MvPolynomial σ R)
        r' ∧
    (∀ (i_1 : ι),
        LE.le.{u_4} (α := m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
              (m.degree
                (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                  ((g' : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
            m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
h :
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree
          (HMul.hMul (β := MvPolynomial σ R) (b j) ((g' : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R) +
            HMul.hMul (β := MvPolynomial σ R) (b j)
              (((Finsupp.single i
                        ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                          ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                      ι →₀ MvPolynomial σ R) :
                    (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
          (b j *
            HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
              ((g' : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R)
              (((Finsupp.single i
                        ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                          ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                      ι →₀ MvPolynomial σ R) :
                    (a : ι) → MvPolynomial σ R)
                  j :
                MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
rw [mul_add]

Premises used: mul_add
-- 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
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)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f =
      HAdd.hAdd (α := MvPolynomial σ R)
        ((Finsupp.linearCombination (MvPolynomial σ R) b : (a : ι →₀ MvPolynomial σ R) → MvPolynomial σ R) g' :
          MvPolynomial σ R)
        r' ∧
    (∀ (i_1 : ι),
        LE.le.{u_4} (α := m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
              (m.degree
                (HMul.hMul (β := MvPolynomial σ R) (b i_1)
                  ((g' : (a : ι) → MvPolynomial σ R) i_1 : MvPolynomial σ R))) :
            m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce ⋯ f)) : m.syn)) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
h :
  LE.le.{u_4} (α := m.syn)
    (max
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree (HMul.hMul (β := MvPolynomial σ R) (b j) ((g' : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R))))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (β := MvPolynomial σ R) (b j)
              (((Finsupp.single i
                        ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                          ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                      ι →₀ MvPolynomial σ R) :
                    (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) ((g' : (a : ι) → MvPolynomial σ R) j : MvPolynomial σ R) +
            HMul.hMul (β := MvPolynomial σ R) (b j)
              (((Finsupp.single i
                        ((monomial (m.degree f - m.degree (b i)) : (a : R) → MvPolynomial σ R)
                          ((↑⋯.unit⁻¹ : R) * m.leadingCoeff f)) :
                      ι →₀ MvPolynomial σ R) :
                    (a : ι) → MvPolynomial σ R)
                  j :
                MvPolynomial σ R))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply le_trans degree_add_le

Premises used: MonomialOrder.degree_add_le, le_trans