English
For any a and multiset m, the attach of the cons a m is equal to the head element paired with a proof of membership, consed with the mapped attach of m.
Русский
Для любого элемента a и мультимножества m, прикрепление (cons) a m равно гол. элементу с доказательством принадлежности, конструируемого к attach m и сопоставленного через отображение.
LaTeX
$$$\\forall a:\\\\alpha\\\\,\\\\forall m:\\\\mathrm{Multiset}\\\\ \\alpha,\\\\ (a\\\\ ::\\\\ m).attach = \\\\langle a,\\\\ mem_cons_self a m\\\\rangle \\\\;::_m\\\\ (m.attach.map\\\\ (\\\\lambda p\\\\,\\\\langle p.1,\\\\ mem_cons_of_mem p.2\\\\rangle)).$$$
Lean4
theorem attach_cons (a : α) (m : Multiset α) :
(a ::ₘ m).attach = ⟨a, mem_cons_self a m⟩ ::ₘ m.attach.map fun p => ⟨p.1, mem_cons_of_mem p.2⟩ :=
Quotient.inductionOn m fun l =>
congr_arg _ <|
congr_arg (List.cons _) <| by rw [List.map_pmap]; exact List.pmap_congr_left _ fun _ _ _ _ => Subtype.eq rfl
