∀ {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (t : Set α) [inst : MeasurableSpace α],
  MeasurableSet t →
    (PMF.ofMultiset s hs).toMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑s.card