exact hx.2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = p.totalDegree
⊢ x.support.sum ⇑x = p.totalDegree
no goals