mathlib3

562bbf52 - feat(measure_theory/measure): add some simp lemmas, golf (#12974)

feat(measure_theory/measure): add some simp lemmas, golf (#12974) * add `top_add`, `add_top`, `sub_top`, `zero_sub`, `sub_self`; * golf the proof of `restrict_sub_eq_restrict_sub_restrict`.