mathlib3

3d197c69 - fix(topology/metric_space/gromov_hausdorff): squeeze all simps (#17049)