simp only [coeff_homogeneousComponent, ite_eq_right_iff] at hx
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬coeff x ((homogeneousComponent n) p) = 0
⊢ (x.sum fun x m => m) = n
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬(degree x = n → coeff x p = 0)
⊢ (x.sum fun x m => m) = n