∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s)
  (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ⊤), edist x (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) < ⊤