rw [Finset.prod_insert hS, Finset.sum_insert hS]
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ ((insert p S).prod id).support ⊆ (insert p S).sum support
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ (id p * ∏ x ∈ S, id x).support ⊆ p.support + ∑ x ∈ S, x.support