English
Let l be a finite list and p a predicate. Filtering the attached elements of l by p is the same as attaching the sublist consisting of elements of l that satisfy p and then mapping the resulting proofs back to mem_of_mem_filter.
Русский
Пусть l — конечный список и p — предикат. Фильтрация привязанных к списку элементов по p эквивалентна привязке подсписка, состоящего из элементов l, удовлетворяющих p, с последующим отображением доказательств принадлежности.
LaTeX
$$$ (l.\\text{attach}.\\text{filter} \\ (\\lambda x . p x)) = ((l.\\text{filter} p).\\text{attach}).\\text{map} (\\text{Subtype.map} \\\\ id \\\\ (\\\\lambda _ . \\\\ mem\\_of\\_mem\\_filter)) $$$
Lean4
theorem filter_attach (l : List α) (p : α → Bool) :
(l.attach.filter fun x => p x : List { x // x ∈ l }) =
(l.filter p).attach.map (Subtype.map id fun _ => mem_of_mem_filter) :=
map_injective_iff.2 Subtype.coe_injective <| by
simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val), ← filter_map,
attach_map_subtype_val]
