rw [leadingTerms_eq_self_iff_isHomogeneous]
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).IsHomogeneous ((monomial s) r).totalDegree