@[simp]

theorem Multiset.nodup_toList_iff {α : Type u_1} {m : Multiset α} : m.toList.Nodup ↔ m.Nodup

@[simp]

theorem Multiset.ofList_toList_perm {α : Type u_1} {xs : List α} : (↑xs).toList.Perm xs

@[simp]

theorem Multiset.ofList_cons {α : Type u_1} {m : Multiset α} {x : α} : ↑(x :: m.toList) = x ::ₘ m

@[simp]

theorem Multiset.toList_append_perm {α : Type u_1} {m : Multiset α} {x : α} : (x ::ₘ m).toList.Perm (x :: m.toList)

@[simp]

theorem Multiset.length_filter_toList_cons_eq {α : Type u_1} {P : α → Bool} {ms : Multiset α} {x : α} : (List.filter P (x ::ₘ ms).toList).length = (List.filter P ms.toList).length + if P x = true then 1 else 0