∀ (R : Type u_1) [inst : CommRing R] {X Y : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInCommRingCat R)
            (CategoryTheory.forget CommRingCat)).map
        f)
      ((fun x =>
            CategoryTheory.Iso.refl
              ((CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInCommRingCat R)
                    (CategoryTheory.forget CommRingCat)).obj
                x))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Iso.refl
              ((CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInCommRingCat R)
                    (CategoryTheory.forget CommRingCat)).obj
                x))
          X).hom
      ((AlgebraicGeometry.structureSheafInType R R).val.map f)