∀ {J : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F)
  (U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ) (j : Jᵒᵖ),
  (TopologicalSpace.Opens.map (s.ι.app (Opposite.unop j)).base).op.obj U =
    (TopologicalSpace.Opens.map
            (CategoryTheory.Limits.colimit.ι (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
              (Opposite.unop j))).op.obj
      ((TopologicalSpace.Opens.map
              (CategoryTheory.Limits.colimit.desc (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
                ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).op.obj
        U)