mathlib

454b8848 - chore(topology/metric_space/basic): golf an instance (#13664)

chore(topology/metric_space/basic): golf an instance (#13664) Golf the proof of `prod.pseudo_metric_space_max` using `pseudo_emetric_space.to_pseudo_metric_space_of_dist`.