rw [leadingTerms, Ne, MvPolynomial.ext_iff]
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ p.leadingTerms ≠ p
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ¬∀ (m : ι →₀ ℕ), coeff m ((homogeneousComponent p.totalDegree) p) = coeff m p