mathlib3

cd2b5495 - chore(measure_theory/*): make measurable_space arguments implicit, determined by the measure argument (#8571)

chore(measure_theory/*): make measurable_space arguments implicit, determined by the measure argument (#8571) In the measure theory library, most of the definitions that depend on a measure have that form: ``` def example_def {α} [measurable_space α] (μ : measure α) : some_type := sorry ``` Suppose now that we have two `measurable_space` structures on `α` : `{m m0 : measurable_space α}` and we have the measures `μ : measure α` (which is a measure on `m0`) and `μm : @measure α m`. This will be common for probability theory applications. See for example the `conditional_expectation` file. Then we can write `example_def μ` but we cannot write `example_def μm` because the `measurable_space` inferred is `m0`, which does not match the measurable space on which `μm` is defined. We have to use `@example_def _ m μm` instead. This PR implements a simple fix: change `[measurable_space α] (μ : measure α)` into `{m : measurable_space α} (μ : measure α)`. Advantage: we can now use `example_def μm` since the `measurable_space` argument is deduced from the `measure` argument. This removes many `@` in all places where `measure.trim` is used. Downsides: - I have to write `(0 : measure α)` instead of `0` in some lemmas. - I had to add two `apply_instance` to find `borel_space` instances. - Whenever a lemma takes an explicit measure argument, we have to write `{m : measurable_space α} (μ : measure α)` instead of simply `(μ : measure α)`.