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