simp only [_root_.not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] 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 : ∑ a ∈ m.support, m a = ⊥
⊢ 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 : ∀ (x : ι), m x = 0
⊢ m = 0