∀ {α : Type u_2} [inst : PseudoMetricSpace α] {β : Type u_1} {x : α} {r : β → ℝ} (a : α) (r_1 : ℝ)
  (motive : (∃ x_1, IsCompact (Metric.closedBall x (r x_1)) ∧ r_1 + dist a x ≤ r x_1) → Prop)
  (x_1 : ∃ x_1, IsCompact (Metric.closedBall x (r x_1)) ∧ r_1 + dist a x ≤ r x_1),
  (∀ (_i : β) (hci : IsCompact (Metric.closedBall x (r _i))) (hir : r_1 + dist a x ≤ r _i), motive ⋯) → motive x_1