apply List.elem_eq_true_of_mem
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 false with
    | true => true
    | false => List.elem x (support t)) =
    true
case a.h
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
⊢ x ∈ support t