∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {s : Set α}
  (ε : (x : α) → x ∈ s → ℝ) (x : α) (hx : x ∈ s)
  (motive : BddAbove ((fun y => dist (f x) (f y) / dist x y) '' (s \ Metric.ball x (ε x hx))) → Prop)
  (x_1 : BddAbove ((fun y => dist (f x) (f y) / dist x y) '' (s \ Metric.ball x (ε x hx)))),
  (∀ (K' : ℝ) (hK' : K' ∈ upperBounds ((fun y => dist (f x) (f y) / dist x y) '' (s \ Metric.ball x (ε x hx)))),
      motive ⋯) →
    motive x_1