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_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
pos : ∀ (hg : g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg : ∀ (hg : ¬g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases hg : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff g)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have pos : ∀ (hf : f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff g)
pos : ∀ (hf : f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg : ∀ (hf : ¬f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g
have hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
Tactic: apply degree_mul_of_mul_leadingCoeff_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0
have hfg : ¬g = 0
Tactic: simp only [ne_eq, hf, IsRegular.left, IsLeftRegular.mul_left_eq_zero_iff,
    leadingCoeff_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have pos : ∀ (hg : g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases hg : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
pos : ∀ (hg : g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg : ∀ (hg : ¬g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases hg : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
⊢ m.degree (f * g) = m.degree f + m.degree g
have rw : m.degree (g * f) = m.degree f + m.degree g
Tactic: rw [mul_comm, m.degree_mul_of_isRegular_left hg hf, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
rw : m.degree (g * f) = m.degree f + m.degree g
⊢ m.degree (f * g) = m.degree f + m.degree g
have rw₁ : m.degree g + m.degree f = m.degree f + m.degree g
Tactic: rw [mul_comm, m.degree_mul_of_isRegular_left hg hf, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
rw : m.degree (g * f) = m.degree f + m.degree g
rw₁ : m.degree g + m.degree f = m.degree f + m.degree g
⊢ m.degree (f * g) = m.degree f + m.degree g
have rw₂ : m.degree f + m.degree g = m.degree f + m.degree g
Tactic: rw [mul_comm, m.degree_mul_of_isRegular_left hg hf, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have pos : ∀ (hf : f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
pos : ∀ (hf : f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg : ∀ (hf : ¬f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
⊢ m.Monic (f * g)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.Monic (f * g)
have rw : m.leadingCoeff f * m.leadingCoeff g ≠ 0
Tactic: rw [Monic, MonomialOrder.leadingCoeff,
      degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0
have rw : Ne.{u_2 + 1} (α := R) 1 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
⊢ m.Monic (f * g)
have suffices : m.leadingCoeff f * m.leadingCoeff g = 1
Tactic: suffices m.leadingCoeff f * m.leadingCoeff g = 1 by
    rw [Monic, MonomialOrder.leadingCoeff,
      degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]
    rw [this]
    exact one_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
⊢ m.leadingCoeff f * m.leadingCoeff g = 1
have rw : 1 * m.leadingCoeff g = 1
Tactic: rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
rw : 1 * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g = 1
have rw₁ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
rw : 1 * m.leadingCoeff g = 1
rw₁ : HMul.hMul (α := R) 1 1 = 1
⊢ m.leadingCoeff f * m.leadingCoeff g = 1
have rw₂ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g
have hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
Tactic: apply degree_mul_of_mul_leadingCoeff_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0
have hfg : ¬f = 0 ∧ ¬g = 0
Tactic: simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero_iff, not_or]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ ¬f = 0 ∧ ¬g = 0
have hfg : ¬f = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
hfg : ¬f = 0
⊢ ¬f = 0 ∧ ¬g = 0
have hfg₁ : ¬g = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have pos : ∀ (h : f = 0 ∨ g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases! +distrib h : f = 0 ∨ g = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
pos : ∀ (h : f = 0 ∨ g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg : ∀ (h : f ≠ 0 ∧ g ≠ 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: by_cases! +distrib h : f = 0 ∨ g = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have pos : f = 0 → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
pos : f = 0 → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have pos₁ : g = 0 → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have hf : f ≠ 0
Tactic: obtain ⟨hf, hg⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
hf : f ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have hg : g ≠ 0
Tactic: obtain ⟨hf, hg⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg : coeff (m.degree (f * g)) (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: rw [leadingCoeff, degree_mul hf hg, ← coeff_mul_of_degree_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
neg : coeff (m.degree (f * g)) (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg₁ : coeff (m.degree f + m.degree g) (f * g) = m.leadingCoeff f * m.leadingCoeff g
Tactic: rw [leadingCoeff, degree_mul hf hg, ← coeff_mul_of_degree_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
neg : coeff (m.degree (f * g)) (f * g) = m.leadingCoeff f * m.leadingCoeff g
neg₁ : coeff (m.degree f + m.degree g) (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
have neg₂ : coeff (m.degree f + m.degree g) (f * g) = coeff (m.degree f + m.degree g) (f * g)
Tactic: rw [leadingCoeff, degree_mul hf hg, ← coeff_mul_of_degree_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ (n + 1))) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) ((n + 1) • m.degree f) : m.syn)
have succ : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n * f)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f + m.degree f) : m.syn)
Tactic: simp only [pow_add, pow_one, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n * f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f + m.degree f) : m.syn)
have succ : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n) + m.degree f) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f + m.degree f) : m.syn)
Tactic: apply le_trans m.degree_mul_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
have zero : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (HPow.hPow (β := ℕ) f 0)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (HSMul.hSMul (α := ℕ) 0 (m.degree f)) : m.syn)
Tactic: induction n with
  | zero => simp [m.degree_one]
  | succ n hrec =>
      simp only [pow_add, pow_one, add_smul, one_smul]
      apply le_trans m.degree_mul_le
      simp only [map_add, add_le_add_iff_right]
      exact hrec
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
zero :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (HPow.hPow (β := ℕ) f 0)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (HSMul.hSMul (α := ℕ) 0 (m.degree f)) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
have succ : ∀ (n : ℕ)
  (hrec :
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)),
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ (n + 1))) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) ((n + 1) • m.degree f) : m.syn)
Tactic: induction n with
  | zero => simp [m.degree_one]
  | succ n hrec =>
      simp only [pow_add, pow_one, add_smul, one_smul]
      apply le_trans m.degree_mul_le
      simp only [map_add, add_le_add_iff_right]
      exact hrec
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ coeff ((n + 1) • m.degree f) (f ^ (n + 1)) = m.leadingCoeff f ^ (n + 1)
have succ : coeff (n • m.degree f + m.degree f) (f ^ n * f) = m.leadingCoeff f ^ n * m.leadingCoeff f
Tactic: simp only [add_smul, one_smul, pow_add, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ coeff (n • m.degree f + m.degree f) (f ^ n * f) = m.leadingCoeff f ^ n * m.leadingCoeff f
have succ : coeff (n • m.degree f) (f ^ n) * coeff (m.degree f) f = m.leadingCoeff f ^ n * m.leadingCoeff f
Tactic: rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
succ : coeff (n • m.degree f) (f ^ n) * coeff (m.degree f) f = m.leadingCoeff f ^ n * m.leadingCoeff f
⊢ coeff (n • m.degree f + m.degree f) (f ^ n * f) = m.leadingCoeff f ^ n * m.leadingCoeff f
have succ₁ : m.leadingCoeff f ^ n * coeff (m.degree f) f = m.leadingCoeff f ^ n * m.leadingCoeff f
Tactic: rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
succ : coeff (n • m.degree f) (f ^ n) * coeff (m.degree f) f = m.leadingCoeff f ^ n * m.leadingCoeff f
succ₁ : m.leadingCoeff f ^ n * coeff (m.degree f) f = m.leadingCoeff f ^ n * m.leadingCoeff f
⊢ coeff (n • m.degree f + m.degree f) (f ^ n * f) = m.leadingCoeff f ^ n * m.leadingCoeff f
have succ₂ : coeff (m.degree f) f ^ n * coeff (m.degree f) f = coeff (m.degree f) f ^ n * coeff (m.degree f) f
Tactic: rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
⊢ coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
have zero : coeff (HSMul.hSMul (α := ℕ) 0 (m.degree f)) (HPow.hPow (β := ℕ) f 0) = HPow.hPow (β := ℕ) (m.leadingCoeff f) 0
Tactic: induction n with
  | zero => simp
  | succ n hrec =>
    simp only [add_smul, one_smul, pow_add, pow_one]
    rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
zero : coeff (HSMul.hSMul (α := ℕ) 0 (m.degree f)) (HPow.hPow (β := ℕ) f 0) = HPow.hPow (β := ℕ) (m.leadingCoeff f) 0
⊢ coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
have succ : ∀ (n : ℕ) (hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n),
  coeff ((n + 1) • m.degree f) (f ^ (n + 1)) = m.leadingCoeff f ^ (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n hrec =>
    simp only [add_smul, one_smul, pow_add, pow_one]
    rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.degree (f ^ n) = n • m.degree f
have a : Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
Tactic: apply m.toSyn.injective
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
have a : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
Tactic: apply le_antisymm (m.degree_pow_le n)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f ^ n)) : m.syn)
have a : n • m.degree f ∈ (f ^ n).support
Tactic: apply le_degree
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n
have rw : coeff (m.degree (f ^ n)) (f ^ n) = m.leadingCoeff f ^ n
Tactic: rw [leadingCoeff, degree_pow_of_pow_leadingCoeff_ne_zero hf, coeff_pow_nsmul_degree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
rw : coeff (m.degree (f ^ n)) (f ^ n) = m.leadingCoeff f ^ n
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n
have rw₁ : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
Tactic: rw [leadingCoeff, degree_pow_of_pow_leadingCoeff_ne_zero hf, coeff_pow_nsmul_degree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
rw : coeff (m.degree (f ^ n)) (f ^ n) = m.leadingCoeff f ^ n
rw₁ : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n
have rw₂ : m.leadingCoeff f ^ n = m.leadingCoeff f ^ n
Tactic: rw [leadingCoeff, degree_pow_of_pow_leadingCoeff_ne_zero hf, coeff_pow_nsmul_degree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
⊢ m.Monic (f ^ n)
have a : Nontrivial R
Tactic: nontriviality R