mathlib3

d41781cf - refactor(topology/metric_space): simplify `dist_triangle` proofs (#5916)