simp_rw [monomial_mul]
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial x.1) (coeff x.1 p) * (monomial x.2) (coeff x.2 q)).support ⊆
    (∑ v ∈ p.support, (monomial v) (coeff v p)).support + (∑ v ∈ q.support, (monomial v) (coeff v q)).support
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 ⊆
    (∑ v ∈ p.support, (monomial v) (coeff v p)).support + (∑ v ∈ q.support, (monomial v) (coeff v q)).support