mathlib3

3525d212 - refactor(topology/metric_space/lipschitz): Simplify proof in banach contraction (#788)