awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
intro :
  ∀
    (hf' :
      Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
    False
intro₁ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f), False
intro₂ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : m.subLTerm f ≠ 0), False
⊢ Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have intro₃ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : coeff (m.degree f) (m.subLTerm f) ≠ 0), False
Tactic: classical
  intro hf'
  simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
  have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
  rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
  apply this
  simp [subLTerm, coeff_monomial, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
intro :
  ∀
    (hf' :
      Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
    False
intro₁ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f), False
intro₂ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : m.subLTerm f ≠ 0), False
intro₃ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : coeff (m.degree f) (m.subLTerm f) ≠ 0), False
⊢ Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have intro₄ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : coeff (m.degree f) (m.subLTerm f) ≠ 0),
  coeff (m.degree f) (m.subLTerm f) = 0
Tactic: classical
  intro hf'
  simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
  have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
  rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
  apply this
  simp [subLTerm, coeff_monomial, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
have rw : m.degree f = m.degree f - m.degree b + m.degree b
Tactic: rw [degree_monomial, if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
rw : m.degree f = m.degree f - m.degree b + m.degree b
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
have hnc : ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0
Tactic: rw [degree_monomial, if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f = m.degree f - m.degree b + m.degree b
have h : ∀ (d : σ), Eq (α := ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ) ((m.degree f - m.degree b + m.degree b : (a : σ) → ℕ) d : ℕ)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
d : σ
⊢ Eq (α := ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ) ((m.degree f - m.degree b + m.degree b : (a : σ) → ℕ) d : ℕ)
have h : Eq (α := ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ)
Tactic: rw [tsub_add_cancel_of_le hbf]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0
have hnc : ¬f = 0
Tactic: simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
hf0 : f = 0
⊢ False
have hnc : m.degree f = 0
Tactic: apply hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
have rw : m.degree f = (if (↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0 then 0 else m.degree f - m.degree b) + m.degree b
Tactic: classical
    rw [degree_monomial, if_neg]
    · ext d
      rw [tsub_add_cancel_of_le hbf]
    · simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
rw : m.degree f = (if (↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0 then 0 else m.degree f - m.degree b) + m.degree b
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
have rw₁ : m.degree f = m.degree f - m.degree b + m.degree b
Tactic: classical
    rw [degree_monomial, if_neg]
    · ext d
      rw [tsub_add_cancel_of_le hbf]
    · simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
rw : m.degree f = (if (↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0 then 0 else m.degree f - m.degree b) + m.degree b
rw₁ : m.degree f = m.degree f - m.degree b + m.degree b
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
have hnc : ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0
Tactic: classical
    rw [degree_monomial, if_neg]
    · ext d
      rw [tsub_add_cancel_of_le hbf]
    · simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have H : m.degree f =
  degree.{u_1, u_2, u_3} m (R := R)
      ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
    m.degree b
Tactic: have H : m.degree f =
      m.degree ((monomial (m.degree f - m.degree b)) (hb.unit⁻¹ * m.leadingCoeff f)) +
        m.degree b := by
    classical
    rw [degree_monomial, if_neg]
    · ext d
      rw [tsub_add_cancel_of_le hbf]
    · simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
⊢ coeff (m.degree f) (m.reduce hb f) = 0
have simp : coeff (m.degree f) f =
  coeff (m.degree f)
    (HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
        MvPolynomial σ R)
      b)
Tactic: simp only [reduce, coeff_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
⊢ coeff (m.degree f) f =
    coeff (m.degree f)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have nth_rewrite : coeff (m.degree f) f =
  coeff
    (degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b)
    (HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
        MvPolynomial σ R)
      b)
Tactic: nth_rewrite 2 [H]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have rw : coeff (m.degree f) f =
  m.leadingCoeff
      ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
    m.leadingCoeff b
Tactic: rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
rw :
  coeff (m.degree f) f =
    m.leadingCoeff
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
      m.leadingCoeff b
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have rw₁ : coeff (m.degree f) f = (↑hb.unit⁻¹ : R) * m.leadingCoeff f * m.leadingCoeff b
Tactic: rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
rw :
  coeff (m.degree f) f =
    m.leadingCoeff
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
      m.leadingCoeff b
rw₁ : coeff (m.degree f) f = (↑hb.unit⁻¹ : R) * m.leadingCoeff f * m.leadingCoeff b
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have rw₂ : coeff (m.degree f) f = m.leadingCoeff b * ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)
Tactic: rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
rw :
  coeff (m.degree f) f =
    m.leadingCoeff
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
      m.leadingCoeff b
rw₁ : coeff (m.degree f) f = (↑hb.unit⁻¹ : R) * m.leadingCoeff f * m.leadingCoeff b
rw₂ : coeff (m.degree f) f = m.leadingCoeff b * ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have rw₃ : coeff (m.degree f) f = m.leadingCoeff b * (↑hb.unit⁻¹ : R) * m.leadingCoeff f
Tactic: rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
rw :
  coeff (m.degree f) f =
    m.leadingCoeff
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
      m.leadingCoeff b
rw₁ : coeff (m.degree f) f = (↑hb.unit⁻¹ : R) * m.leadingCoeff f * m.leadingCoeff b
rw₂ : coeff (m.degree f) f = m.leadingCoeff b * ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)
rw₃ : coeff (m.degree f) f = m.leadingCoeff b * (↑hb.unit⁻¹ : R) * m.leadingCoeff f
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have rw₄ : coeff (m.degree f) f = 1 * m.leadingCoeff f
Tactic: rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
rw :
  coeff (m.degree f) f =
    m.leadingCoeff
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
      m.leadingCoeff b
rw₁ : coeff (m.degree f) f = (↑hb.unit⁻¹ : R) * m.leadingCoeff f * m.leadingCoeff b
rw₂ : coeff (m.degree f) f = m.leadingCoeff b * ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)
rw₃ : coeff (m.degree f) f = m.leadingCoeff b * (↑hb.unit⁻¹ : R) * m.leadingCoeff f
rw₄ : coeff (m.degree f) f = 1 * m.leadingCoeff f
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have rw₅ : coeff (m.degree f) f = m.leadingCoeff f
Tactic: rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
rw :
  coeff (m.degree f) f =
    m.leadingCoeff
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) *
      m.leadingCoeff b
rw₁ : coeff (m.degree f) f = (↑hb.unit⁻¹ : R) * m.leadingCoeff f * m.leadingCoeff b
rw₂ : coeff (m.degree f) f = m.leadingCoeff b * ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)
rw₃ : coeff (m.degree f) f = m.leadingCoeff b * (↑hb.unit⁻¹ : R) * m.leadingCoeff f
rw₄ : coeff (m.degree f) f = 1 * m.leadingCoeff f
rw₅ : coeff (m.degree f) f = m.leadingCoeff f
⊢ coeff (m.degree f) f =
    coeff
      (degree.{u_1, u_2, u_3} m (R := R)
          ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
        m.degree b)
      (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f) :
          MvPolynomial σ R)
        b)
have rw₆ : m.leadingCoeff f = m.leadingCoeff f
Tactic: rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have H' : coeff (m.degree f) (m.reduce hb f) = 0
Tactic: have H' : coeff (m.degree f) (m.reduce hb f) = 0 := by
    simp only [reduce, coeff_sub, sub_eq_zero]
    nth_rewrite 2 [H]
    rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
      IsUnit.mul_val_inv, one_mul, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have rw : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
  Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: rw [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H :
  m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
    Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have left : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.reduce hb f)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: constructor