feat(measure_theory/measure/measure_space): Add parallel set of lemmas about count (#17245)
feat(measure_theory/measure/measure_space): Add parallel set of lemmas about count (#17245)

This PR adds a parallel set of basic lemmas about `measure_theory.measure.count`, which does not assume `[measurable_singleton_class _]` but instead assumes `(measurable set _)`.

The same lemmas are true without the `[measurable_singleton_class _]` assumption, so it often seems inappropriate to require this type class. However, the versions with `(measurable_set _)` assumption are also not strictly generalizations of the ones with the type class, so the PR adds a parallel set of lemmas (many but not all of the existing proofs reduce to the new lemmas at least partially). The new lemma names are a prime appended to the original lemma names; under the common `[measurable_singleton_class _]` assumption for counting measures, the original set of lemmas is more convenient.

One setup where it is, however, appropriate to relax the `[measurable_singleton_class _]` assumption is conditional expected values in finite probability spaces with uniform distribution 

Co-authored-by: kkytola <98284447279c86ba5682f8c28a13975ffe92211e@users.noreply.github.com>
Co-authored-by: kkytola <fbaa3c03433b74ed86c67e5a5304c745a67121d1@aalto.fi”>

leanprover-community/mathlib,leanprover-community/mathlib