no goals
α : Type u
β : Type v
ι : Type ?u.143197
π : ι → Type ?u.143202
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
U : Set α
⊢ ConnectedComponents.mk ⁻¹' (ConnectedComponents.mk '' U) = ⋃ (x : α) (_ : x ∈ U), connectedComponent x
simp only [connectedComponents_preimage_singleton, preimage_iUnion₂, image_eq_iUnion]