mathlib

04d7099d - chore(measure_theory/function/l1_space): golf downstream results