rw [monomCoeff]
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ monomCoeff R X x₀ (0, x) = 0
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ (match (0, x).2 == x₀ with
    | true => (0, x).1
    | false => 0) =
    0