match p : x₀ == x with
| true =>
  have eqn : x₀ = x := of_decide_eq_true p
  rw [eqn]
  apply List.mem_of_elem_eq_true
  simp [List.elem]
| false =>
  rw [coords, monomCoeff, p, zero_add] at hyp
  let step := nonzero_coord_in_support t x hyp
  apply List.mem_of_elem_eq_true
  simp [List.elem]
  have p' : (x == x₀) = false := by
    have eqn := of_decide_eq_false p
    have eqn' : ¬(x = x₀) := by
      intro contra
      let contra' := Eq.symm contra
      contradiction
    exact decide_eq_false eqn'
  rw [p']
  apply List.elem_eq_true_of_mem
  exact step
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ x₀ :: support t
no goals