apply sum_monomial_ne_zero_of_exists_mem_ne_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) ≠ 0
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, ∃ (_ : s ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support), coeff s p ≠ 0