∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y)
  [inst : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f.toHom = X