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 : MvPolynomial σ R
n : ℕ
hf : m.Monic f
h : Nontrivial R
⊢ m.Monic (f ^ n)
have rw : m.leadingCoeff f ^ n ≠ 0
Tactic: rw [Monic, leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, hf.leadingCoeff_eq_one, one_pow]
-- 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.Monic f
h : Nontrivial R
⊢ m.leadingCoeff f ^ n ≠ 0
have rw : Ne.{u_2 + 1} (α := R) 1 0
Tactic: rw [hf.leadingCoeff_eq_one, one_pow]
-- 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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
⊢ m.degree (f ^ n) = n • m.degree f
have pos : ∀ (hf : f = 0), m.degree (f ^ n) = n • m.degree f
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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
pos : ∀ (hf : f = 0), m.degree (f ^ n) = n • m.degree f
⊢ m.degree (f ^ n) = n • m.degree f
have neg : ∀ (hf : ¬f = 0), m.degree (f ^ n) = n • m.degree f
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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (f ^ n) = n • m.degree f
have pos : m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
Tactic: rw [hf, degree_zero, smul_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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
have pos : ∀ (hn : n = 0), m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
Tactic: by_cases hn : n = 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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
pos : ∀ (hn : n = 0), m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
have neg : ∀ (hn : ¬n = 0), m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
Tactic: by_cases hn : n = 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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
have pos : m.degree (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) 0 0) = 0
Tactic: rw [hn, pow_zero, degree_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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
pos : m.degree (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) 0 0) = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
have pos₁ : degree.{u_1, u_2, u_3} m (R := R) 1 = 0
Tactic: rw [hn, pow_zero, degree_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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
pos : m.degree (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) 0 0) = 0
pos₁ : degree.{u_1, u_2, u_3} m (R := R) 1 = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
have pos₂ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
Tactic: rw [hn, pow_zero, degree_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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
have neg : degree.{u_1, u_2, u_3} m (R := R) 0 = 0
Tactic: rw [zero_pow hn, degree_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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
neg : degree.{u_1, u_2, u_3} m (R := R) 0 = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
have neg₁ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
Tactic: rw [zero_pow hn, degree_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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ m.degree (f ^ n) = n • m.degree f
have neg : m.leadingCoeff f ^ n ≠ 0
Tactic: apply degree_pow_of_pow_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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ m.leadingCoeff f ^ n ≠ 0
have neg : m.leadingCoeff f ≠ 0
Tactic: apply pow_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 : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ m.leadingCoeff f ≠ 0
have neg : f ≠ 0
Tactic: rw [leadingCoeff_ne_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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
⊢ 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, 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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
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, 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
inst_1 : IsReduced R
f : MvPolynomial σ R
n : ℕ
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, 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
r : R
f : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (r • 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 (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) f)) :
    m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: rw [smul_eq_C_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
r : R
f : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (m.degree (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) f)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have apply : Eq.{u_3 + 1} (α := m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
      (degree.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) r) + m.degree f) :
    m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply le_of_le_of_eq 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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
⊢ m.degree (r • f) = m.degree f
have pos : ∀ (hf : f = 0), m.degree (r • f) = m.degree f
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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
pos : ∀ (hf : f = 0), m.degree (r • f) = m.degree f
⊢ m.degree (r • f) = m.degree f
have neg : ∀ (hf : ¬f = 0), m.degree (r • f) = m.degree f
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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree (r • f) = m.degree f
have neg : Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (r • f)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (r • f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have neg : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (r • f)) : m.syn)
Tactic: apply le_antisymm degree_smul_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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (r • f)) : m.syn)
have neg : m.degree f ∈ (r • f).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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree f ∈ (r • f).support
have neg : coeff (m.degree f) (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) f) ≠ 0
Tactic: simp only [mem_support_iff, smul_eq_C_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
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ coeff (m.degree f) (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) f) ≠ 0
have neg : m.leadingCoeff ((C : (a : R) → MvPolynomial σ R) r) * m.leadingCoeff f ≠ 0
Tactic: rw [← zero_add (degree m f), ← degree_C r, coeff_mul_of_degree_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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)
have empty : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) 1) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
Tactic: simp only [Finset.prod_empty, Finset.sum_empty]
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) 1) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
have empty : LE.le.{u_4} (α := m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial σ R) 1)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
Tactic: rw [← C_1, m.degree_C, map_zero]
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
empty :
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial σ R) 1)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) 1) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
have empty₁ : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0)
Tactic: rw [← C_1, m.degree_C, map_zero]
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
empty :
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial σ R) 1)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
empty₁ : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) 1) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
have empty₂ : LE.le.{u_4} (α := m.syn) 0 0
Tactic: rw [← C_1, m.degree_C, map_zero]
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ insert a s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ insert a s, m.degree (P i)) : m.syn)
have insert : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a * ∏ x ∈ s, P x)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + ∑ x ∈ s, m.degree (P x)) : m.syn)
Tactic: rw [Finset.prod_insert has, Finset.sum_insert has]
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a * ∏ x ∈ s, P x)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + ∑ x ∈ s, m.degree (P x)) : m.syn)
have insert : LE.le.{u_4} (α := m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + degree.{u_1, u_2, u_4} m (R := R) (∏ x ∈ s, P x)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (P a) + ∑ x ∈ s, m.degree (P x)) : m.syn)
Tactic: apply le_trans degree_mul_le
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
have empty : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.prod_empty, Finset.sum_empty]
    rw [← C_1, m.degree_C, map_zero]
  | insert a s has hrec =>
    rw [Finset.prod_insert has, Finset.sum_insert has]
    apply le_trans degree_mul_le
    simp only [map_add, add_le_add_iff_left, hrec]
Cleared hypotheses: s
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
empty :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hrec :
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)),
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ insert a s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ insert a s, m.degree (P i)) : m.syn)
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.prod_empty, Finset.sum_empty]
    rw [← C_1, m.degree_C, map_zero]
  | insert a s has hrec =>
    rw [Finset.prod_insert has, Finset.sum_insert has]
    apply le_trans degree_mul_le
    simp only [map_add, add_le_add_iff_left, hrec]
Cleared hypotheses: s
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
have empty : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.prod_empty, Finset.sum_empty]
    rw [← C_1, m.degree_C, map_zero]
  | insert a s has hrec =>
    rw [Finset.prod_insert has, Finset.sum_insert has]
    apply le_trans degree_mul_le
    simp only [map_add, add_le_add_iff_left, hrec]
Cleared hypotheses: s
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
empty :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ ∅, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ ∅, m.degree (P i)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hrec :
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)),
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ insert a s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ insert a s, m.degree (P i)) : m.syn)
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.prod_empty, Finset.sum_empty]
    rw [← C_1, m.degree_C, map_zero]
  | insert a s has hrec =>
    rw [Finset.prod_insert has, Finset.sum_insert has]
    apply le_trans degree_mul_le
    simp only [map_add, add_le_add_iff_left, hrec]
Cleared hypotheses: s
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ insert a s, m.degree (P i)) (∏ i ∈ insert a s, P i))
    (∏ i ∈ insert a s, m.leadingCoeff (P i))
have insert : coeff (m.degree (P a) + ∑ i ∈ s, m.degree (P i)) (P a * ∏ i ∈ s, P i) =
  m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)
Tactic: simp only [Finset.prod_insert has, Finset.sum_insert has]
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
⊢ coeff (m.degree (P a) + ∑ i ∈ s, m.degree (P i)) (P a * ∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)
have insert : coeff (m.degree (P a)) (P a) * coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) =
  m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)
Tactic: rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
have empty : Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i))
  (∏ i ∈ ∅, m.leadingCoeff (P i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert a s has hrec =>
    simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec
Cleared hypotheses: s
-- 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 : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
empty :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i))
    (∏ i ∈ ∅, m.leadingCoeff (P i))
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hrec :
    Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
      (∏ i ∈ s, m.leadingCoeff (P i))),
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ insert a s, m.degree (P i)) (∏ i ∈ insert a s, P i))
    (∏ i ∈ insert a s, m.leadingCoeff (P i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert a s has hrec =>
    simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec
Cleared hypotheses: s