English
For lists s, t, the multiset intersection of their ofList representations equals the list bagInter of the lists (viewed as a multiset).
Русский
Для списков s, t пересечение мультимножества, получаемое из их представлений в виде мультимножеств, равно списку bagInter(s, t) (рассматривается как мультимножество).
LaTeX
$$$ (s \\cap t : Multiset \\alpha) = (s . bagInter t : List \\alpha) $$$
Lean4
@[simp]
theorem coe_inter (s t : List α) : (s ∩ t : Multiset α) = (s.bagInter t : List α) := by ext; simp