∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  AlgebraicGeometry.Scheme.Hom.appLE f U V e =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (X.presheaf.map (CategoryTheory.homOfLE e).op)