∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] {C : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C] [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) [inst_5 : CategoryTheory.Limits.HasColimit F]
  (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)) {X Y : Jᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp.comp
            ((CategoryTheory.evaluation
                  (TopologicalSpace.Opens
                      ↑(CategoryTheory.Limits.colimit (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))))ᵒᵖ
                  C).obj
              ((TopologicalSpace.Opens.map
                      (CategoryTheory.Limits.colimit.isoColimitCocone
                              { cocone := AlgebraicGeometry.PresheafedSpace.colimitCocone F,
                                isColimit :=
                                  AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (Opposite.op U)))).map
        f)
      (CategoryTheory.Functor.mapIso (F.obj (Opposite.unop Y)).presheaf (CategoryTheory.eqToIso ⋯)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.mapIso (F.obj (Opposite.unop X)).presheaf (CategoryTheory.eqToIso ⋯)).hom
      ((AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U).map f)