mathlib

bf868344 - chore(probability_theory/integration): style changes. Make arguments implicit, remove spaces, etc. (#8286)

chore(probability_theory/integration): style changes. Make arguments implicit, remove spaces, etc. (#8286) - make the measurable_space arguments of indep_fun implicit again. They were made explicit to accommodate the way `lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun` was written, with explicit `(borel ennreal)` arguments. Those arguments are not needed and are removed. - use `measurable_set T` instead of `M.measurable_set' T`. - write the type of several `have` explicitly. - remove some spaces - ensure there is only one tactic per line - use `exact` instead of `apply` when the tactic is finishing Co-authored-by: Rémy Degenne <remydegenne@gmail.com>