no goals
X : Type u_1
Y : Type ?u.91061
Z : Type ?u.91064
α : Type ?u.91067
ι : Type ?u.91070
π : ι → Type ?u.91075
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y z : X
s✝ : Set X
f : X → Y
t s : Set (SeparationQuotient X)
x : X
⊢ Filter.map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]