rw [← hp (mem_support_iff.mp hx), weightedDegree_one]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ p.totalDegree ≤ x.sum fun _x m => m
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ degree x ≤ x.sum fun _x m => m