mathlib

2f07ff21 - chore(topology/metric_space): more `norm_cast` lemmas, golf proofs (#4911)