feat(measure/pi): prove extensionality for `measure.pi` (#6304)
* If two measures in a finitary product are equal on cubes with measurable sides (or with sides in a set generating the corresponding sigma-algebra), then the measures are equal.
* Add `sigma_finite` instance for `measure.pi`
* Some basic lemmas about sets (more specifically `Union` and `set.pi`)
* rename `measurable_set.pi_univ` -> `measurable_set.univ_pi` (`pi univ t` is called `univ_pi` consistently in `set/basic`, but it's not always consistent elsewhere)
* rename `[bs]?Union_prod` -> `[bs]?Union_prod_const`
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
