∀ {I : Type u_1} [inst : CategoryTheory.Category.{u_1, u_1} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (i : I) (U : (D.obj i).Opens) ⦃X Y : CategoryTheory.Over i⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const (CategoryTheory.Over i)).obj
            ↑((TopologicalSpace.Opens.map (c.π.app i).base).obj U)).map
        f)
      (AlgebraicGeometry.Scheme.Hom.resLE (c.π.app Y.left) ((TopologicalSpace.Opens.map (D.map Y.hom).base).obj U)
        ((TopologicalSpace.Opens.map (c.π.app i).base).obj U) ⋯) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.resLE (c.π.app X.left) ((TopologicalSpace.Opens.map (D.map X.hom).base).obj U)
        ((TopologicalSpace.Opens.map (c.π.app i).base).obj U) ⋯)
      ((AlgebraicGeometry.opensDiagram D i U).map f)