∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp
      {
          val :=
            CategoryTheory.Functor.whiskerRight
              { app := fun U => (AlgebraicGeometry.Scheme.Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
              (CategoryTheory.forget₂ CommRingCat RingCat) }.val
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).op.whiskerLeft
          (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f).val)
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op ⋯.adjunction.unit) X.ringCatSheaf.val)) =
    CategoryTheory.CategoryStruct.id X.ringCatSheaf.val