intro h₁
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
⊢ degree x = n → coeff x p = 0
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
h₁ : degree x = n
⊢ coeff x p = 0