∀ (R : Type u) [inst : CommRing R]
  {U V :
    (TopologicalSpace.Opens
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj { carrier := R, commRing := inst }).toPresheafedSpace)ᵒᵖ}
  (i : U ⟶ V),
  (AlgebraicGeometry.Spec.locallyRingedSpaceObj { carrier := R, commRing := inst }).presheaf.map i =
    (AlgebraicGeometry.Spec.structureSheaf R).val.map i