simp [totalDegree_monomial _ hr]
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = ((monomial s) r).totalDegree
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = s.sum fun x e => e