have eqn : x₀ = x := of_decide_eq_true p
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
p : (x₀ == x) = true
⊢ x ∈ x₀ :: support t
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
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x₀ :: support t