∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} (x : α × ℕ),
  x ∈
      m.toFinset.disjiUnion (fun x => Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (Multiset.count x m)))
        ⋯ ↔
    x ∈ {p | p.2 < Multiset.count p.1 m}