-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
s : Cocone F
U V : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
i : U ⟶ V
refine :
  ∀ (j : Jᵒᵖ),
    Eq (α :=
      s.pt.presheaf.obj U ⟶
        obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
          (obj
              (Functor.leftOp (pushforwardDiagramToColimit F) :
                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
              j :
            CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
          (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
            (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
      (CategoryStruct.comp (Y :=
          obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
            (limit
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
              (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
          (s.pt.presheaf.map i ≫
              CategoryStruct.comp (Y :=
                limit
                  (Functor.comp (D :=
                    CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                    (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)))
                (limit.lift
                    (Functor.comp (D :=
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                      (Functor.leftOp (pushforwardDiagramToColimit F) :
                        Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                      (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                          (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                          C))
                    { pt := s.pt.presheaf.obj V,
                      π :=
                        {
                          app := fun (j : Jᵒᵖ) ↦
                            NatTrans.app (Hom.c (s.ι.app (unop j))) V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                          naturality := ⋯ :
                          NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj V))
                            (Functor.comp (D :=
                              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ
                                C)
                              (Functor.leftOp (pushforwardDiagramToColimit F) :
                                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                              (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                  (op
                                    (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                                CategoryTheory.Functor.{v, v, v, u}
                                    (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                                  C)) } } :
                  Cone.pt (F :=
                      Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C))
                      { pt := s.pt.presheaf.obj V,
                        π :=
                          {
                            app := fun (j : Jᵒᵖ) ↦
                              NatTrans.app (Hom.c (s.ι.app (unop j))) V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                            naturality := ⋯ :
                            NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj V))
                              (Functor.comp (D :=
                                CategoryTheory.Functor.{v, v, v, u}
                                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                (Functor.leftOp (pushforwardDiagramToColimit F) :
                                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                    (op
                                      (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)))
                                        (unop V))) :
                                  CategoryTheory.Functor.{v, v, v, u}
                                      (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                                    C)) } :
                        Cone
                          (Functor.comp (D :=
                            CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (Functor.leftOp (pushforwardDiagramToColimit F) :
                              Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                            (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ
                                  C ⥤
                                C)) } ⟶
                    limit
                      (Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C)))
                (Iso.inv
                    (limitObjIsoLimitCompEvaluation (Functor.leftOp (pushforwardDiagramToColimit F))
                      (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)))) :
                  limit
                      (Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C)) ⟶
                    obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                      (limit
                          (Functor.leftOp (pushforwardDiagramToColimit F) :
                            Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                      (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                        (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)) :
            s.pt.presheaf.obj U ⟶
              obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                (limit
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                  Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
          (NatTrans.app (limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) j)
              (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
            obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                (limit
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ) ⟶
              obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                (obj
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                    j :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)) :
        s.pt.presheaf.obj U ⟶
          obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
            (obj
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                j :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
              (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
      (CategoryStruct.comp (Y :=
          obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
            (limit
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
              (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
          (CategoryStruct.comp (Y :=
              obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                (limit
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                  Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)) :
                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
              (CategoryStruct.comp (Y :=
                limit
                  (Functor.comp (D :=
                    CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                    (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)))
                (limit.lift
                    (Functor.comp (D :=
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                      (Functor.leftOp (pushforwardDiagramToColimit F) :
                        Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                      (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                          (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                          C))
                    { pt := s.pt.presheaf.obj U,
                      π :=
                        {
                          app := fun (j : Jᵒᵖ) ↦
                            NatTrans.app (Hom.c (s.ι.app (unop j))) U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                          naturality := ⋯ :
                          NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj U))
                            (Functor.comp (D :=
                              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ
                                C)
                              (Functor.leftOp (pushforwardDiagramToColimit F) :
                                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                              (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                  (op
                                    (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                                CategoryTheory.Functor.{v, v, v, u}
                                    (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                                  C)) } } :
                  Cone.pt (F :=
                      Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C))
                      { pt := s.pt.presheaf.obj U,
                        π :=
                          {
                            app := fun (j : Jᵒᵖ) ↦
                              NatTrans.app (Hom.c (s.ι.app (unop j))) U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                            naturality := ⋯ :
                            NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj U))
                              (Functor.comp (D :=
                                CategoryTheory.Functor.{v, v, v, u}
                                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                (Functor.leftOp (pushforwardDiagramToColimit F) :
                                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                    (op
                                      (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)))
                                        (unop U))) :
                                  CategoryTheory.Functor.{v, v, v, u}
                                      (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                                    C)) } :
                        Cone
                          (Functor.comp (D :=
                            CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (Functor.leftOp (pushforwardDiagramToColimit F) :
                              Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                            (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ
                                  C ⥤
                                C)) } ⟶
                    limit
                      (Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C)))
                (Iso.inv
                    (limitObjIsoLimitCompEvaluation (Functor.leftOp (pushforwardDiagramToColimit F))
                      (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))) :
                  limit
                      (Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C)) ⟶
                    obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                      (limit
                          (Functor.leftOp (pushforwardDiagramToColimit F) :
                            Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                      (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)) :
                        (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)))
              (map
                (limit
                  (Functor.leftOp (pushforwardDiagramToColimit F) :
                    Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))))
                (Quiver.Hom.op (map (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) i.unop))) :
            s.pt.presheaf.obj U ⟶
              obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                (limit
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                  Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
          (NatTrans.app (limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) j)
              (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
            obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                (limit
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ) ⟶
              obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
                (obj
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                    j :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                  (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)) :
        s.pt.presheaf.obj U ⟶
          obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
            (obj
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                j :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
              (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
⊢ Eq (α :=
    s.pt.presheaf.obj U ⟶
      obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
        (limit
            (Functor.leftOp (pushforwardDiagramToColimit F) :
              Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
          Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
        (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
          (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
    (s.pt.presheaf.map i ≫
      CategoryStruct.comp (Y :=
        limit
          (Functor.comp (D :=
            CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (Functor.leftOp (pushforwardDiagramToColimit F) :
              Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
            (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)))
        (limit.lift
            (Functor.comp (D :=
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
              (Functor.leftOp (pushforwardDiagramToColimit F) :
                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
              (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                  (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C))
            { pt := s.pt.presheaf.obj V,
              π :=
                {
                  app := fun (j : Jᵒᵖ) ↦
                    NatTrans.app (Hom.c (s.ι.app (unop j))) V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                  naturality := ⋯ :
                  NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj V))
                    (Functor.comp (D :=
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                      (Functor.leftOp (pushforwardDiagramToColimit F) :
                        Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                      (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                          (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                          C)) } } :
          Cone.pt (F :=
              Functor.comp (D :=
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C))
              { pt := s.pt.presheaf.obj V,
                π :=
                  {
                    app := fun (j : Jᵒᵖ) ↦
                      NatTrans.app (Hom.c (s.ι.app (unop j))) V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                    naturality := ⋯ :
                    NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj V))
                      (Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C)) } :
                Cone
                  (Functor.comp (D :=
                    CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                    (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                        C)) } ⟶
            limit
              (Functor.comp (D :=
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)))
        (Iso.inv
            (limitObjIsoLimitCompEvaluation (Functor.leftOp (pushforwardDiagramToColimit F))
              (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)))) :
          limit
              (Functor.comp (D :=
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)) ⟶
            obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
              (limit
                  (Functor.leftOp (pushforwardDiagramToColimit F) :
                    Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
              (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop V)) :
                (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)))
    (CategoryStruct.comp (Y :=
      obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
        (limit
            (Functor.leftOp (pushforwardDiagramToColimit F) :
              Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
          Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
        (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)) :
          (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ))
      (CategoryStruct.comp (Y :=
        limit
          (Functor.comp (D :=
            CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (Functor.leftOp (pushforwardDiagramToColimit F) :
              Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
            (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)))
        (limit.lift
            (Functor.comp (D :=
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
              (Functor.leftOp (pushforwardDiagramToColimit F) :
                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
              (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                  (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C))
            { pt := s.pt.presheaf.obj U,
              π :=
                {
                  app := fun (j : Jᵒᵖ) ↦
                    NatTrans.app (Hom.c (s.ι.app (unop j))) U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                  naturality := ⋯ :
                  NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj U))
                    (Functor.comp (D :=
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                      (Functor.leftOp (pushforwardDiagramToColimit F) :
                        Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                      (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                          (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                          C)) } } :
          Cone.pt (F :=
              Functor.comp (D :=
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C))
              { pt := s.pt.presheaf.obj U,
                π :=
                  {
                    app := fun (j : Jᵒᵖ) ↦
                      NatTrans.app (Hom.c (s.ι.app (unop j))) U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                    naturality := ⋯ :
                    NatTrans (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj U))
                      (Functor.comp (D :=
                        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (Functor.leftOp (pushforwardDiagramToColimit F) :
                          Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                        (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                            (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                          CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                            C)) } :
                Cone
                  (Functor.comp (D :=
                    CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                    (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                        (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                        C)) } ⟶
            limit
              (Functor.comp (D :=
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)))
        (Iso.inv
            (limitObjIsoLimitCompEvaluation (Functor.leftOp (pushforwardDiagramToColimit F))
              (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)))) :
          limit
              (Functor.comp (D :=
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                    (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U))) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)) ⟶
            obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
              (limit
                  (Functor.leftOp (pushforwardDiagramToColimit F) :
                    Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
              (op (obj (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (unop U)) :
                (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)))
      (map
        (limit
          (Functor.leftOp (pushforwardDiagramToColimit F) : Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))))
        (Quiver.Hom.op (map (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) i.unop))))

Tactic:
refine limit_obj_ext (fun j => ?_)

Premises used: CategoryTheory.Limits.limit_obj_ext