mathlib

1444fa52 - fix(haar_measure): minor changes (#4623)

fix(haar_measure): minor changes (#4623) There were some mistakes in the doc, which made it sound like `chaar` and `haar_outer_measure` coincide on compact sets, which is not generally true. Also cleanup various proofs.