awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ ∃ (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₂))
have 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₂)))
Tactic: use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ 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₂)))
have h₁ : g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ 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₂)))
have h₁ : g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)
have 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₂))
Tactic: simp only [m.toSyn.injective.eq_iff] at *
Cleared hypotheses: h, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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₂))
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)
have hd₁ : ∀ 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 *
Cleared hypotheses: h, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)
have trans : g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
Tactic: trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)
have 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))
Tactic: trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
have rw : ∑ b ∈ B, g 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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
have rw₄ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + -(((∑ i ∈ B, m.leadingCoeff (g i)) * (↑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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b)
have rw₅ : ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + -((∑ i ∈ B, m.leadingCoeff (g i)) * (↑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]