intro x hx
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : x ∈ p.leadingTerms.support
⊢ x.support.sum ⇑x = p.totalDegree