Theorem: MvPolynomial.totalDegree_leadingTerms (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.totalDegree = p.totalDegree
Tactic:
by_cases hp : p = 0
State after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ¬p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ¬p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree
Tactic:
exact totalDegree_homogenous_component_of_ne_zero (leadingTerms_ne_zero hp)
State after:
no goals

State before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree
Tactic:
simp [hp]
State after:
no goals