mathlib3

cb4c9ee7 - refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible (#1052)

refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible (#1052) * refactor(topology/metric/gromov_hausdorff): remove linarith calls * refactor(topology/metric/hausdorff_dist): make hausdorff_dist irreducible