∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} [inst_1 : Nonempty α] [inst_2 : CompleteSpace α]
  {n : ℕ} (hf : ContractingWith K f^[n]), Function.IsFixedPt f (ContractingWith.fixedPoint f^[n] hf)