refine ⟨fun hx ↦ ⟨fun h ↦ hx <| by simp [coeff_homogeneousComponent, h], ?_⟩,
  fun ⟨h₁, h₂⟩ ↦ fun h ↦ h₁ ?_⟩
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ ¬coeff x ((homogeneousComponent n) p) = 0 ↔ ¬coeff x 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 : ¬coeff x ((homogeneousComponent n) p) = 0
⊢ (x.sum fun x m => m) = n

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