mathlib3

edb0ba42 - chore(measure_theory/measure/hausdorff): golf (#8706)

chore(measure_theory/measure/hausdorff): golf (#8706) * add a `mk_metric` version of `hausdorff_measure_le`, add `finset.sum` versions for both `mk_metric` and `hausdorff_measure`; * slightly golf the proof.