no goals
X : Type u_1
Y : Type ?u.79044
Z : Type ?u.79047
α : Type ?u.79050
ι : Type ?u.79053
π : ι → Type ?u.79058
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)
⊢ comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]