∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (ε δ : ℝ) (s : Set α) ⦃x : α⦄
  (motive : (∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) → Prop)
  (x_1 : ∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε),
  (∀ (y z : α) (hz : z ∈ s) (hy : edist y z < ENNReal.ofReal δ) (hx : edist x y < ENNReal.ofReal ε), motive ⋯) →
    motive x_1