exact ⟨f, ⟨hf0, hf⟩,  hf0⟩
case h.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
f : ι →₀ ℕ
hf : (f.sum fun x e => e) = p.totalDegree
hf0 : coeff f p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0
no goals