∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} (x y : α),
  x ≠ y →
    Function.onFun Disjoint (fun x => Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (Multiset.count x m)))
      x y