∀ (toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace)
  (local_affine :
    ∀ (x : ↑toLocallyRingedSpace.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R)))
  (toLocallyRingedSpace_1 : AlgebraicGeometry.LocallyRingedSpace)
  (local_affine_1 :
    ∀ (x : ↑toLocallyRingedSpace_1.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace_1.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))),
  ({ toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine } =
      { toLocallyRingedSpace := toLocallyRingedSpace_1, local_affine := local_affine_1 }) =
    (toLocallyRingedSpace = toLocallyRingedSpace_1)