no goals
X : Type u_1
Y : Type ?u.60142
Z : Type ?u.60145
α : Type ?u.60148
ι : Type ?u.60151
π : ι → Type ?u.60156
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ Filter.map mk (𝓝 x) = 𝓝 (mk x)
rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]