no goals
α : Type u
β : Type v
ι : Type ?u.142587
π : ι → Type ?u.142592
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace α
x : α
⊢ ∀ (t : Set α), t ∈ 𝓝 x → ∃ r, r ∈ 𝓝 x ∧ IsCompact r ∧ r ⊆ t
simpa only [and_comm] using LocallyCompactSpace.local_compact_nhds x