simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne,
  not_false_iff, not_forall, ite_eq_left_iff]
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ ¬degree h_w = p.totalDegree