mathlib3

a7589864 - feat(measure_theory/integral/set_integral): remove or weaken some integrability assumptions (#18395)

feat(measure_theory/integral/set_integral): remove or weaken some integrability assumptions (#18395) When dealing with integrals on sets, we assume almost always that the set is measurable or null-measurable. However, there are situations where these assumptions can be removed, making the lemmas easier to apply, but at the cost of more involved proofs. We implement this in this PR. As an example, we prove `set_integral_eq_of_subset_of_forall_diff_eq_zero`: if `s` is contained in `t`, and `t` is null-measurable and a function vanishes on `t \ s`, then its integrals on `s` and `t` coincide (no measurability assumptions on `s` or `f`). The special case `t = univ` is especially useful.