Theorem: MvPolynomial.support_mul' (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (p * q).support ⊆ p.support + q.support
Tactic:
rw [p.as_sum, q.as_sum, Finset.sum_mul_sum, ← Finset.sum_product']
State after:
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

State before:
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
Tactic:
simp_rw [monomial_mul]
State after:
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

State before:
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
Tactic:
rw [support_sum_monomial_coeff, support_sum_monomial_coeff]
State after:
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

State before:
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
Tactic:
convert Finset.Subset.trans (support_sum_monomial_subset' _ _ _) (Finset.Subset.refl _)
State after:
no goals