mathlib

7592a8f4 - chore(analysis/normed_space/finite_dimension,topology/metric_space): golf (#6285)

chore(analysis/normed_space/finite_dimension,topology/metric_space): golf (#6285) * golf two proofs about `finite_dimension`; * move `proper_image_of_proper` to `antilipschitz`, rename to `antilipschitz_with.proper_space`, golf.