no goals
α : Type ?u.59864
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ x ∈ l
simpa [hy] using h
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ x ∈ l

case x_ne
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ x ≠ getLast l (_ : l ≠ [])
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ next (y :: l) x h = next l x (_ : x ∈ l)
rw [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_of_ne]
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ l ≠ []
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ x ∈ l
rwa [getLast_cons] at hx
no goals
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ l ≠ []
exact ne_nil_of_mem (by assumption)
no goals
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ ?m.65092 ∈ l
assumption
no goals
case x_ne
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ getLast (y :: l) (_ : y :: l ≠ [])
⊢ x ≠ getLast l (_ : l ≠ [])
rwa [getLast_cons] at hx