no goals
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
S : Set (Set α)
H : ∀ (s : Set α), s ∈ S → IsOpen s
T : Set ↑S
cT : Set.Countable T
hT : (⋃ (i : ↑S) (_ : i ∈ T), ↑i) = ⋃ (i : ↑S), ↑i
⊢ ⋃₀ (Subtype.val '' T) = ⋃₀ S
rwa [sUnion_image, sUnion_eq_iUnion]