∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  autoParam (AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f))
      AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal._autoParam →
    AlgebraicGeometry.IsSeparated f