awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply degree_mul_of_mul_leadingCoeff_ne_zero

Premises used: MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 ∧ ¬g = 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero_iff, not_or]

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, mul_eq_zero, ne_eq, not_or
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
hfg₁ : ¬g = 0
⊢ ¬f = 0 ∧ ¬g = 0

Tactic:
tauto
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : ∀ (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

Tactic:
by_cases! +distrib h : f = 0 ∨ g = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
pos₁ : g = 0 → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
cases h
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ f ≠ 0

Tactic:
obtain ⟨hf, hg⟩ := h
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ g ≠ 0

Tactic:
obtain ⟨hf, hg⟩ := h
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg₂ neg₃ : coeff (m.degree f + m.degree g) (f * g) = coeff (m.degree f + m.degree g) (f * g)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
rw [leadingCoeff, degree_mul hf hg, ← coeff_mul_of_degree_add]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.coeff_mul_of_degree_add, MonomialOrder.degree_mul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ 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:
simp [m.degree_one]

Premises used: MonomialOrder.degree_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)
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)
⊢ 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:
simp only [pow_add, pow_one, add_smul, one_smul]

Premises used: pow_add, one_smul, add_smul, pow_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)
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)
⊢ 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:
apply le_trans m.degree_mul_le

Premises used: MonomialOrder.degree_mul_le, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)
succ :
  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) + m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f + m.degree f) : m.syn)

Tactic:
simp only [map_add, add_le_add_iff_right]

Premises used: map_add, add_le_add_iff_right
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)

Tactic:
hrec
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (n • m.degree f) : m.syn)

Tactic:
exact hrec
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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)
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)
⊢ 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)

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

Premises used: pow_add, map_add, MonomialOrder.degree_mul_le, one_smul, MonomialOrder.degree_one, add_le_add_iff_right, add_smul, pow_one, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ coeff (HSMul.hSMul (α := ℕ) 0 (m.degree f)) (HPow.hPow (β := ℕ) f 0) = HPow.hPow (β := ℕ) (m.leadingCoeff f) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 + m.degree f) (f ^ n * f) = m.leadingCoeff f ^ n * m.leadingCoeff f
⊢ coeff ((n + 1) • m.degree f) (f ^ (n + 1)) = m.leadingCoeff f ^ (n + 1)

Tactic:
simp only [add_smul, one_smul, pow_add, pow_one]

Premises used: pow_add, one_smul, add_smul, pow_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
succ₂ succ₃ : coeff (m.degree f) f ^ n * coeff (m.degree f) f = coeff (m.degree f) f ^ n * coeff (m.degree f) f
⊢ coeff (n • m.degree f + m.degree f) (f ^ n * 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]

Premises used: le_rfl, MonomialOrder.leadingCoeff, MonomialOrder.degree_pow_le, MonomialOrder.coeff_mul_of_add_of_degree_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
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)
⊢ coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n

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]

Premises used: le_rfl, MonomialOrder.leadingCoeff, pow_add, MonomialOrder.degree_pow_le, one_smul, add_smul, pow_one, MonomialOrder.coeff_mul_of_add_of_degree_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
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)
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
apply m.toSyn.injective

Premises used: AddEquiv.injective, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
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)
⊢ 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 le_antisymm (m.degree_pow_le n)

Premises used: MonomialOrder.degree_pow_le, le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
a : n • m.degree f ∈ (f ^ n).support
⊢ 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_degree

Premises used: MonomialOrder.le_degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf a : m.leadingCoeff f ^ n ≠ 0
⊢ n • m.degree f ∈ (f ^ n).support

Tactic:
rw [mem_support_iff, coeff_pow_nsmul_degree]

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.coeff_pow_nsmul_degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 ≠ 0

Tactic:
hf
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 ≠ 0

Tactic:
exact hf
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
rw₂ rw₃ : m.leadingCoeff f ^ n = m.leadingCoeff f ^ n
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Tactic:
rw [leadingCoeff, degree_pow_of_pow_leadingCoeff_ne_zero hf, coeff_pow_nsmul_degree]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.coeff_pow_nsmul_degree, MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
rw : m.leadingCoeff f ^ n ≠ 0
⊢ m.Monic (f ^ n)

Tactic:
rw [Monic, leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, hf.leadingCoeff_eq_one, one_pow]

Premises used: one_pow, MonomialOrder.Monic, MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, MonomialOrder.Monic.leadingCoeff_eq_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
rw : Ne.{u_2 + 1} (α := R) 1 0
⊢ m.leadingCoeff f ^ n ≠ 0

Tactic:
rw [hf.leadingCoeff_eq_one, one_pow]

Premises used: one_pow, MonomialOrder.Monic.leadingCoeff_eq_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ Ne.{u_2 + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ Ne.{u_2 + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : ∀ (hf : ¬f = 0), m.degree (f ^ n) = n • m.degree f
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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 : m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
rw [hf, degree_zero, smul_zero]

Premises used: smul_zero, MonomialOrder.degree_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : ∀ (hn : ¬n = 0), m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
pos₂ pos₃ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0

Tactic:
rw [hn, pow_zero, degree_one]

Premises used: pow_zero, MonomialOrder.degree_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg₁ neg₂ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
⊢ m.degree (HPow.hPow (α := MvPolynomial σ R) 0 n) = 0

Tactic:
rw [zero_pow hn, degree_zero]

Premises used: MonomialOrder.degree_zero, zero_pow
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : m.leadingCoeff f ^ n ≠ 0
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
apply degree_pow_of_pow_leadingCoeff_ne_zero

Premises used: MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : m.leadingCoeff f ≠ 0
⊢ m.leadingCoeff f ^ n ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : f ≠ 0
⊢ m.leadingCoeff f ≠ 0

Tactic:
rw [leadingCoeff_ne_zero_iff]

Premises used: MonomialOrder.leadingCoeff_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ f ≠ 0

Tactic:
hf
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
⊢ f ≠ 0

Tactic:
exact hf
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
rw₂ rw₃ : m.leadingCoeff f ^ n = m.leadingCoeff f ^ n
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Tactic:
rw [leadingCoeff, degree_pow, coeff_pow_nsmul_degree]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.coeff_pow_nsmul_degree, MonomialOrder.degree_pow
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
f : MvPolynomial σ R
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)
⊢ 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)

Tactic:
rw [smul_eq_C_mul]

Premises used: MvPolynomial.smul_eq_C_mul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
f : MvPolynomial σ R
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)
⊢ 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:
apply le_of_le_of_eq degree_mul_le

Premises used: le_of_le_of_eq, MonomialOrder.degree_mul_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ 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:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : ∀ (hf : ¬f = 0), m.degree (r • f) = m.degree f
⊢ m.degree (r • f) = m.degree f

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
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)
⊢ m.degree (r • f) = m.degree f

Tactic:
apply m.toSyn.injective

Premises used: AddEquiv.injective, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
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)
⊢ 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 le_antisymm degree_smul_le

Premises used: MonomialOrder.degree_smul_le, le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
neg : m.degree f ∈ (r • f).support
⊢ 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_degree

Premises used: MonomialOrder.le_degree