English
If x is a member of a list l, then the predecessor of x in l is also a member of l.
Русский
Если x принадлежит списку l, то предшественник x в этом списке тоже принадлежит этому списку.
LaTeX
$$$\forall l:\\ List\ α\, \forall x:\\ α\, (h: x\in l)\quad l.prev\ x\ h \in l$$$
Lean4
theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l :=
by
rcases l with - | ⟨hd, tl⟩
· simp at h
induction tl generalizing hd with
| nil => simp
| cons hd' tl hl =>
by_cases hx : x = hd
· simp only [hx, prev_cons_cons_eq]
exact mem_cons_of_mem _ (getLast_mem _)
· rw [prev, dif_neg hx]
split_ifs with hm
· exact mem_cons_self
· exact mem_cons_of_mem _ (hl _ _)
