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