no goals
α : Type u
β : Type v
ι✝ : Type ?u.89316
π : ι✝ → Type ?u.89321
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : CompactSpace α
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
⊢ Set.Finite univ
simpa only [hne] using hf.finite_nonempty_of_compact