-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_smul {r : R} (hr : IsRegular r) {f : MvPolynomial σ R} :
    m.degree (r • f) = m.degree f

Proof state:
case neg.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree f ∈ (r • f).support

Tactic:
simp only [mem_support_iff, smul_eq_C_mul]

Result:
case neg.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ coeff (m.degree f) (C r * f) ≠ 0

Proof state:
case neg.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree (r • f))

Tactic:
apply le_degree

Result:
case neg.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree f ∈ (r • f).support

Proof state:
case neg.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ coeff (m.degree f) (C r * f) ≠ 0

Tactic:
rw [← zero_add (degree m f), ← degree_C r, coeff_mul_of_degree_add]

Result:
case neg.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.leadingCoeff (C r) * m.leadingCoeff f ≠ 0

Proof state:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : f = 0
⊢ m.degree (r • f) = m.degree f

Tactic:
simp [hf]

Result:
no goals

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree (r • f) = m.degree f

Tactic:
apply m.toSyn.injective

Result:
case neg.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.toSyn (m.degree (r • f)) = m.toSyn (m.degree f)

Proof state:
case neg.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.leadingCoeff (C r) * m.leadingCoeff f ≠ 0

Tactic:
simp [leadingCoeff, hr.left.mul_left_eq_zero_iff, hf]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
⊢ m.degree (r • f) = m.degree f

Tactic:
by_cases hf : f = 0

Result:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : f = 0
⊢ m.degree (r • f) = m.degree f

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree (r • f) = m.degree f

Proof state:
case neg.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.toSyn (m.degree (r • f)) = m.toSyn (m.degree f)

Tactic:
apply le_antisymm degree_smul_le

Result:
case neg.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : IsRegular r
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree (r • f))