no goals
α : Type u
β : Type v
ι : Type ?u.14579
π : ι → Type ?u.14584
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs : IsCompact s
U : α → Set α
hU : ∀ (x : α), x ∈ s → U x ∈ 𝓝 x
t : Finset ↑s
ht : s ⊆ ⋃ (x : ↑s) (_ : x ∈ t), U ↑x
⊢ s ⊆ ⋃ (x : α) (_ : x ∈ Finset.image Subtype.val t), U x
rwa [Finset.set_biUnion_finset_image]