mathlib3

c1b10417 - feat(topology/metric_space/basic): add `fin.dist_insert_nth_insert_nth` (#11183)