awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
hd :
  ∀ a ∈ B,
    Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
        IsUnit (m.leadingCoeff (g a)) ∨
      g a = 0
h₁ :
  Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
    (∑ b₁ ∈ insert b B,
      ∑ b₂ ∈ insert b B,
        HSMul.hSMul (α := R) ((fun (b₁ b₂ : ι) ↦ if b₂ = b then (↑isunit_gb.unit⁻¹ : R) else 0) b₁ b₂)
          (m.sPolynomial (g b₁) (g b₂)))
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
      (∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0

Premises used: OfNat.ofNat, Eq, ite
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
hd :
  ∀ a ∈ B,
    Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
        IsUnit (m.leadingCoeff (g a)) ∨
      g a = 0
h₁ : g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)
⊢ Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
    (∑ b₁ ∈ insert b B,
      ∑ b₂ ∈ insert b B,
        HSMul.hSMul (α := R) ((fun (b₁ b₂ : ι) ↦ if b₂ = b then (↑isunit_gb.unit⁻¹ : R) else 0) b₁ b₂)
          (m.sPolynomial (g b₁) (g b₂)))

Tactic:
simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]

Premises used: Finset.sum_ite_eq', MonomialOrder.sPolynomial_self, smul_zero, zero_add, zero_smul, reduceIte, ite_smul, Finset.sum_insert, add_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
hd :
  ∀ a ∈ B,
    Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
        IsUnit (m.leadingCoeff (g a)) ∨
      g a = 0
h₁ : g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)
⊢ Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
    (∑ b₁ ∈ insert b B,
      ∑ b₂ ∈ insert b B,
        HSMul.hSMul (α := R) ((fun (b₁ b₂ : ι) ↦ if b₂ = b then (↑isunit_gb.unit⁻¹ : R) else 0) b₁ b₂)
          (m.sPolynomial (g b₁) (g b₂)))

Tactic:
simp? [Finset.sum_insert hb, hb] says
      simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]

Premises used: Finset.sum_ite_eq', MonomialOrder.sPolynomial_self, smul_zero, zero_add, zero_smul, reduceIte, ite_smul, Finset.sum_insert, add_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
hd :
  ∀ a ∈ B,
    Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
        IsUnit (m.leadingCoeff (g a)) ∨
      g a = 0
⊢ ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
simp only [m.toSyn.injective.eq_iff] at *

Premises used: Function.Injective.eq_iff, AddEquiv.injective, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
hd :
  ∀ a ∈ B,
    Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
        IsUnit (m.leadingCoeff (g a)) ∨
      g a = 0
h₁ :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
⊢ ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0

Tactic:
simp only [m.toSyn.injective.eq_iff] at *

Premises used: Function.Injective.eq_iff, AddEquiv.injective, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
trans : g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
trans₁ :
  Eq (α := MvPolynomial σ R) (∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b))
    (∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b))
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)

Tactic:
trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
rw : ∑ b ∈ B, g b + g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
rw₁ :
  ∑ b ∈ B, g b + g b =
    HSub.hSub (α := MvPolynomial σ R) (∑ x ∈ B, g x) (∑ x ∈ B, (m.leadingCoeff (g x) * (↑isunit_gb.unit⁻¹ : R)) • g b)
rw₂ :
  ∑ b ∈ B, g b + g b =
    HAdd.hAdd (α := MvPolynomial σ R) (∑ x ∈ B, g x) (-∑ x ∈ B, (m.leadingCoeff (g x) * (↑isunit_gb.unit⁻¹ : R)) • g b)
rw₃ :
  ∑ b ∈ B, g b + g b =
    ∑ x ∈ B, g x + -HSMul.hSMul (α := R) (∑ i ∈ B, m.leadingCoeff (g i) * (↑isunit_gb.unit⁻¹ : R)) (g b)
rw₄ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + -(((∑ i ∈ B, m.leadingCoeff (g i)) * (↑isunit_gb.unit⁻¹ : R)) • g b)
rw₅ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + -((∑ i ∈ B, m.leadingCoeff (g i)) * (↑isunit_gb.unit⁻¹ : R)) • g b
rw₆ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + ((-∑ i ∈ B, m.leadingCoeff (g i)) * (↑isunit_gb.unit⁻¹ : R)) • g b
rw₇ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + (m.leadingCoeff (g b) * (↑isunit_gb.unit⁻¹ : R)) • g b
rw₈ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + HSMul.hSMul (α := R) 1 (g b)
rw₉ rw₁₀ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + g b
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)

Tactic:
rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]

Premises used: Finset.sum_smul, neg_smul, IsUnit.mul_val_inv, sub_eq_add_neg, add_comm, one_smul, Finset.sum_sub_distrib, neg_mul, Finset.sum_mul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
suffices : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)

Tactic:
suffices (-(∑ i ∈ B, m.leadingCoeff (g i))) = m.leadingCoeff (g b) by
        rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
rw : m.leadingCoeff (g b) + ∑ i ∈ B, m.leadingCoeff (g i) = 0
⊢ -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)

Tactic:
rw [← add_eq_zero_iff_neg_eq']

Premises used: add_eq_zero_iff_neg_eq'
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
trans :
  m.leadingCoeff (g b) + ∑ i ∈ B, m.leadingCoeff (g i) =
    coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i)
trans₁ : coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i) = 0
⊢ m.leadingCoeff (g b) + ∑ i ∈ B, m.leadingCoeff (g i) = 0

Tactic:
trans (g b).coeff (m.degree <| g b) + ∑ i ∈ B, (g i).coeff (m.degree <| g b)

Premises used: MvPolynomial.coeff, MonomialOrder.degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
unfold :
  coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g i)) (g i) =
    coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i)
⊢ m.leadingCoeff (g b) + ∑ i ∈ B, m.leadingCoeff (g i) =
    coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i)

Tactic:
unfold leadingCoeff

Premises used: MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
e_a : Eq.{u_2 + 1} (α := R) (∑ i ∈ B, coeff (m.degree (g i)) (g i)) (∑ i ∈ B, coeff (m.degree (g b)) (g i))
⊢ coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g i)) (g i) =
    coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
e_a : ∀ x ∈ B, coeff (m.degree (g x)) (g x) = coeff (m.degree (g b)) (g x)
⊢ Eq.{u_2 + 1} (α := R) (∑ i ∈ B, coeff (m.degree (g i)) (g i)) (∑ i ∈ B, coeff (m.degree (g b)) (g i))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
e_a :
  ∀ (h : m.degree (g b') = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b'))),
    coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')
e_a₁ : ∀ (h : g b' = 0), coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

Tactic:
rcases hd b' hb' with h | h
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h_1 :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : m.degree (g b') = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b'))
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

Tactic:
simp [h]