mathlib

313db47a - feat(measure_theory/covering/besicovitch): remove measurability assumptions (#9679)

feat(measure_theory/covering/besicovitch): remove measurability assumptions (#9679) For applications, it is important to allow non-measurable sets in the Besicovitch covering theorem. We tweak the proof to allow this. Also give an improved statement that is easier to use in applications.