mathlib3

cdaa6d2b - refactor(analysis/normed_space/pi_Lp): golf some instances (#14339)

refactor(analysis/normed_space/pi_Lp): golf some instances (#14339) * drop `pi_Lp.emetric_aux`; * use `T₀` to get `(e)metric_space` from `pseudo_(e)metric_space`; * restate `pi_Lp.(anti)lipschitz_with_equiv` with correct `pseudo_emetric_space` instances; while they're defeq, it's better not to leak auxiliary instances unless necessary.