rw [Finset.filter_eq_self]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ filter (fun s => ∑ i ∈ s.support, s i = p.totalDegree) p.support = p.support
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∀ x ∈ p.support, ∑ i ∈ x.support, x i = p.totalDegree