feat(measure_theory): finite_spanning_sets_in (#4668)
* We define a new Type-valued structure `finite_spanning_sets_in` which consists of a countable sequence of sets that span the type, have finite measure, and live in a specified collection of sets,
* `sigma_finite` is redefined in terms of `finite_spanning_sets_in`
* One of the ext lemmas is now conveniently formulated in terms of `finite_spanning_sets_in`
* `finite_spanning_sets_in` is also used to remove a little bit of code duplication in `prod` (which occurred because `sigma_finite` was a `Prop`, and forgot the actual construction)
* Define a predicate `is_countably_spanning` which states that a collection of sets has a countable spanning subset. This is useful for one particular lemma in `prod`.
* Generalize some lemmas about products in the case that the σ-algebras are generated by a collection of sets. This can be used to reason about iterated products.
* Prove `prod_assoc_prod`.
* Cleanup in `measurable_space` and somewhat in `measure_space`.
* Rename `measurable.sum_rec -> measurable.sum_elim` (and give a different but definitionally equal statement)
