rw [support_zero, support_add_eq h,
  Finset.union_eq_empty,MvPolynomial.support_eq_empty] at this
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : (p + q).support = support 0
⊢ p = 0
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : p = 0 ∧ q.support = ∅
⊢ p = 0