no goals
α : Type ?u.86825
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ x ∈ z :: l
simpa [hy] using h
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
h : x ∈ [y, z]
⊢ prev [y, z] x h = prev [z] x (_ : x ∈ [z])

case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ prev (y :: z :: head✝ :: tail✝) x h = prev (z :: head✝ :: tail✝) x (_ : x ∈ z :: head✝ :: tail✝)
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ prev (y :: z :: l) x h = prev (z :: l) x (_ : x ∈ z :: l)
cases l
no goals
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
h : x ∈ [y, z]
⊢ prev [y, z] x h = prev [z] x (_ : x ∈ [z])
simp [hy, hz] at h
no goals
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ prev (y :: z :: head✝ :: tail✝) x h = prev (z :: head✝ :: tail✝) x (_ : x ∈ z :: head✝ :: tail✝)
rw [prev, dif_neg hy, if_neg hz]