theorem exists_countable_locallyFinite_cover {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [SigmaCompactSpace X] {c : ι → X} {W B : ι → ℝ → Set X} {p : ι → ℝ → Prop} (hc : Function.Surjective c) (hW₀ : ∀ (i : ι) (r : ℝ), p i r → c i ∈ W i r) (hW₁ : ∀ (i : ι) (r : ℝ), p i r → IsOpen (W i r)) (hB : ∀ (i : ι), (nhds (c i)).HasBasis (p i) (B i)) : ∃ (s : Set (ι × ℝ)), s.Countable ∧ (∀ z ∈ s, (↿p) z) ∧ ⋃ z ∈ s, (↿W) z = Set.univ ∧ LocallyFinite (↿B ∘ Subtype.val)

We could generalise and replace ι × ℝ with a dependent family of types but it doesn't seem worth it. Proof partly based on refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set.