no goals
α : Type u_1
β : Type ?u.27075
γ : Type ?u.27078
ι : Type ?u.27081
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
T : Set (Set α)
s : Set α
hs : IsGδ s
hd : Dense s
hc : Set.Countable T
hc' : ∀ (t : Set α), t ∈ T → IsClosed t
hU : s ⊆ ⋃₀ T
⊢ s ⊆ ⋃ (i : Set α) (_ : i ∈ T), i
rwa [← sUnion_eq_biUnion]