English
For any list l and any n, the n-th take of l equals the filter selecting elements from l that are in the initial take of l.
Русский
Для любого списка l и числа n равенство take n l = filter (elem (take n l)) l.
LaTeX
$$$ \\text{[DecidableEq α]} :\\n\\forall \\{l : List α\\} {n : \\mathbb{N}}, l.Nodup \\Rightarrow l.\\mathrm{take} \\ n = l.\\mathrm{filter} (\\mathrm{elem} (l.\\mathrm{take} n)).$$$
Lean4
theorem take_eq_filter_mem [DecidableEq α] : ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (l.take n).elem
| [], n, _ => by simp
| b :: l, 0, _ => by simp
| b :: l, n + 1, hl =>
by
rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]
congr 1
refine List.filter_congr ?_
intro x hx
have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
simp +contextual [List.mem_filter, this, hx]
