∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] (_U : Set α)
  (r : ENNReal) (motive : (∃ K ⊆ _U, IsCompact K ∧ r < μ K) → Prop) (x : ∃ K ⊆ _U, IsCompact K ∧ r < μ K),
  (∀ (K : Set α) (KU : K ⊆ _U) (K_comp : IsCompact K) (hK : r < μ K), motive ⋯) → motive x