English
Let f : α → Option α be a map whose outputs, when present, belong to the input element itself, i.e. for all a and all b ∈ f(a) we have a = b. Then for every list l, applying lookmap along f leaves l unchanged: lookmap f l = l.
Русский
Пусть f : α → Option α удовлетворяет условию: для каждого a и любого b ∈ f(a) выполняется a = b. Тогда для любого списка l выполняется lookmap f l = l.
LaTeX
$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\alpha\\ ,\\ \\big(\\forall a\\,\\forall b\\in f(a),\\ a=b\\big) \\Rightarrow \\forall l:\\text{List }\\alpha,\\ \\operatorname{lookmap} f\\ l = l$$$
Lean4
theorem lookmap_id' (h : ∀ (a), ∀ b ∈ f a, a = b) (l : List α) : l.lookmap f = l := by
rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]; exact h
