mathlib

854e5c6b - refactor(measure_theory/measure/regular): add `inner_regular`, `outer_regular`, generalize (#9283)

refactor(measure_theory/measure/regular): add `inner_regular`, `outer_regular`, generalize (#9283) ### Regular measures * add a non-class predicate `inner_regular` to prove some lemmas once, not twice; * add TC `outer_regular`, drop primed lemmas; * consistently use `≠ ∞`, `≠ 0` in the assumptions; * drop some typeclass requirements. ### Other changes * add a few lemmas about subtraction to `data.real.ennreal`; * add `ennreal.add_lt_add_left`, `ennreal.add_lt_add_right`, and use them;