no goals
ι : Type u_2
X : Type u_1
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι X] using
  exists_continuous_forall_mem_convex_of_local_const exists_forall_closedBall_subset_aux₂
    (exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)