rw [support_homogeneousComponent]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ ((homogeneousComponent n) p).support ⊆ p.support
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ filter (fun d => (d.sum fun x m => m) = n) p.support ⊆ p.support