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'
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true