convert Finset.Subset.trans (support_sum_monomial_subset' _ _ _) (Finset.Subset.refl _)
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial (x.1 + x.2)) (coeff x.1 p * coeff x.2 q)).support ⊆ p.support + q.support
no goals