-- Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean
theorem degree_degLexDegree : (degLex.degree f).degree = f.totalDegree

Proof state:
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
⊢ (degLex.degree f).degree = f.totalDegree

Tactic:
by_cases hf : f = 0

Result:
case pos
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : f = 0
⊢ (degLex.degree f).degree = f.totalDegree

case neg
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ (degLex.degree f).degree = f.totalDegree

Proof state:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ f ≠ 0

Tactic:
exact hf

Result:
no goals

Proof state:
case neg.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ f.totalDegree ≤ (degLex.degree f).degree

Tactic:
unfold MvPolynomial.totalDegree

Result:
case neg.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ (f.support.sup fun s => s.sum fun x e => e) ≤ (degLex.degree f).degree

Proof state:
case neg.a.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
b : σ →₀ ℕ
hb : b ∈ f.support
⊢ (b.sum fun x e => e) ≤ (degLex.degree f).degree

Tactic:
exact DegLex.monotone_degree (degLex.le_degree hb)

Result:
no goals

Proof state:
case neg.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ (degLex.degree f).degree ≤ f.totalDegree

Tactic:
apply MvPolynomial.le_totalDegree

Result:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ degLex.degree f ∈ f.support

Proof state:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ coeff (degLex.degree f) f ≠ 0

Tactic:
change degLex.leadingCoeff f ≠ 0

Result:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ degLex.leadingCoeff f ≠ 0

Proof state:
case pos
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : f = 0
⊢ (degLex.degree f).degree = f.totalDegree

Tactic:
simp [hf]

Result:
no goals

Proof state:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ degLex.degree f ∈ f.support

Tactic:
rw [MvPolynomial.mem_support_iff]

Result:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ coeff (degLex.degree f) f ≠ 0

Proof state:
case neg.a.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ ∀ b ∈ f.support, (b.sum fun x e => e) ≤ (degLex.degree f).degree

Tactic:
intro b hb

Result:
case neg.a.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
b : σ →₀ ℕ
hb : b ∈ f.support
⊢ (b.sum fun x e => e) ≤ (degLex.degree f).degree

Proof state:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ degLex.leadingCoeff f ≠ 0

Tactic:
rw [leadingCoeff_ne_zero_iff]

Result:
case neg.a.h
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ f ≠ 0

Proof state:
case neg
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ (degLex.degree f).degree = f.totalDegree

Tactic:
apply le_antisymm

Result:
case neg.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ (degLex.degree f).degree ≤ f.totalDegree

case neg.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ f.totalDegree ≤ (degLex.degree f).degree

Proof state:
case neg.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ (f.support.sup fun s => s.sum fun x e => e) ≤ (degLex.degree f).degree

Tactic:
apply Finset.sup_le

Result:
case neg.a.a
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f : MvPolynomial σ R
hf : ¬f = 0
⊢ ∀ b ∈ f.support, (b.sum fun x e => e) ≤ (degLex.degree f).degree