Theorem: MvPolynomial.support_homogeneousComponent_subset (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ ((homogeneousComponent n) p).support ⊆ p.support
Tactic:
rw [support_homogeneousComponent]
State after:
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

State before:
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
Tactic:
exact Finset.filter_subset _ _
State after:
no goals