∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ℝ),
  Set.MapsTo (⇑f) (Metric.closedBall x r') (Metric.closedBall (f x) (↑(Dilation.ratio f) * r'))