no goals
X : Type u_1
Y : Type ?u.48723
Z : Type ?u.48726
α : Type ?u.48729
ι : Type ?u.48732
π : ι → Type ?u.48737
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)
s : Set X
hs : IsOpen s
⊢ IsOpen (mk ⁻¹' (mk '' s))
rwa [preimage_image_mk_open hs]