mathlib3

refactor (topology/metric_space/lipschitz): Simplify proof in banach contraction

#788

Merged