no goals
α : Type u
β : Type v
ι✝ : Type ?u.89027
π : ι✝ → Type ?u.89032
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : CompactSpace α
f : ι → Set α
hf : LocallyFinite f
⊢ Set.Finite {i | Set.Nonempty (f i)}
simpa only [inter_univ] using hf.finite_nonempty_inter_compact isCompact_univ