simp only [exists_prop, mem_support_iff, Finset.mem_filter]
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
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0