∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {f : X → Y}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)},
  ContinuousWithinAt (SeparationQuotient.lift f hf) s (SeparationQuotient.mk x) =
    ContinuousWithinAt f (SeparationQuotient.mk ⁻¹' s) x