classical
rw [leadingTerms_apply]
apply sum_monomial_ne_zero_of_exists_mem_ne_zero
simp only [exists_prop, mem_support_iff, Finset.mem_filter]
obtain ⟨f, hf, hf0⟩ := exists_coeff_ne_zero_totalDegree hp
exact ⟨f, ⟨hf0, hf⟩,  hf0⟩
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ p.leadingTerms ≠ 0
no goals