∀ (α : Type u_1) [inst : UniformSpace α],
  Filter.Tendsto Prod.swap
    (Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity (CauchyFilter α)))
    (Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity (CauchyFilter α)))