mathlib3

1fc7a93c - chore(topology/metric_space/hausdorff_distance): slightly tidy some proofs (#11203)