Banach fixed-point theorem

import Mathlib

theorem banach_fixed {X : Type*} [MetricSpace X] [CompleteSpace X] [Nonempty X] {f : X → X} (hf : ContractingWith (1/2 : NNReal) f) : ∃! x, f x = x :=
by
  use ContractingWith.fixedPoint f hf
  constructor
  · show f (ContractingWith.fixedPoint f hf) = ContractingWith.fixedPoint f hf
    exact ContractingWith.fixedPoint_isFixedPt hf
  · intro y (hy : f y = y)
    show y = ContractingWith.fixedPoint f hf
    exact ContractingWith.fixedPoint_unique hf hy