α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : ¬x ∈ l
h : optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])
⊢ get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = y

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : ¬x ∈ l
h : optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])
⊢ ¬x ∈ y :: l
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : ¬x ∈ l
h : optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])
⊢ next (y :: l ++ [x]) x h = y
rw [next, nextOr_concat]
no goals
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : ¬x ∈ l
h : optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])
⊢ get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = y
rfl
no goals
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : ¬x ∈ l
h : optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])
⊢ ¬x ∈ y :: l
simp [hy, hx]