no goals
α : Type u
β : Type v
ι : Type ?u.111703
π : ι → Type ?u.111708
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : TopologicalSpace β
f : α → β
hf : QuotientMap f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
⊢ f '' connectedComponent a = connectedComponent (f a)
rw [← hf.preimage_connectedComponent h_fibers, image_preimage_eq _ hf.surjective]