mathlib

09b58946 - feat(measure_theory/measure/haar_lebesgue): the Lebesgue measure is doubling (#16885)

feat(measure_theory/measure/haar_lebesgue): the Lebesgue measure is doubling (#16885) Also split the file `measure_theory/covering/density_theorem` in two, to avoid importing all the differentiation theory into `haar_lebesgue.lean`.