∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set (SeparationQuotient X)) (x : X),
  Filter.map SeparationQuotient.mk (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) = nhdsWithin (SeparationQuotient.mk x) s