rw [Finsupp.sum] at hp
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ m = 0
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∑ a ∈ m.support, m a = ⊥
⊢ m = 0