-- 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
U : Opens (↑(↑(Limits.colimit F) : TopCat) : Type v)
j : J
rw :
  Eq (α :=
    limit (componentwiseDiagram F U) ⟶ (F.obj j).presheaf.obj (op (obj (Opens.map (Hom.base (colimit.ι F j))) U)))
    (limit.π (componentwiseDiagram F U) (op j) ≫
      CategoryStruct.comp (Y :=
        (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
                        (Hom.base
                          (Iso.inv
                            (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                      U)) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)).obj
          (op j))
        (NatTrans.app (Iso.inv (NatIso.ofComponents (fun (X : Jᵒᵖ) ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯))
          (op j))
        (CategoryStruct.comp (Y :=
          (obj
                (pushforward C
                  (CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F j)
                      (Iso.hom
                        (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                            ColimitCocone F }))).base)
                (F.obj j).presheaf).obj
            (op
              (obj
                (Opens.map
                  (Hom.base
                    (Iso.inv
                      (colimit.isoColimitCocone
                        { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                U)))
          ((F.obj j).presheaf.map (eqToHom ⋯))
          (map (obj (pushforward C (Hom.base (colimit.ι F j))) (F.obj j).presheaf) (eqToHom ⋯))))
    (limit.π (componentwiseDiagram F U) (op j))
⊢ Eq (α :=
    limit (componentwiseDiagram F U) ⟶ (F.obj j).presheaf.obj (op (obj (Opens.map (Hom.base (colimit.ι F j))) U)))
    (CategoryStruct.comp (Y :=
        obj
          (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
                (Hom.base
                  (Iso.inv
                    (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
              U)))
        (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
                          (Hom.base
                            (Iso.inv
                              (colimit.isoColimitCocone
                                { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                                  ColimitCocone F }))))
                        U)) :
                  CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)))
            (limMap (Iso.inv (NatIso.ofComponents (fun (X : Jᵒᵖ) ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)) :
              limit (componentwiseDiagram F 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
                              (Hom.base
                                (Iso.inv
                                  (colimit.isoColimitCocone
                                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                                      ColimitCocone F }))))
                            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
                        (Hom.base
                          (Iso.inv
                            (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                      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
                              (Hom.base
                                (Iso.inv
                                  (colimit.isoColimitCocone
                                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                                      ColimitCocone F }))))
                            U)) :
                      CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤
                        C)) ⟶
                obj
                  (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
                        (Hom.base
                          (Iso.inv
                            (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                      U))) :
          limit (componentwiseDiagram F U) ⟶
            obj
              (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
                    (Hom.base
                      (Iso.inv
                        (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                  U)))
        (CategoryStruct.comp (Y :=
            (Limits.colimit F).presheaf.obj
              (op
                (obj
                  (Opens.map
                    (Hom.base
                      (Iso.hom
                        (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                  (obj
                    (Opens.map
                      (Hom.base
                        (Iso.inv
                          (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                    U))))
            (NatTrans.app
                (Hom.c
                  (Iso.hom
                    (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F })))
                (op
                  (obj
                    (Opens.map
                      (Hom.base
                        (Iso.inv
                          (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                    U)) ≫
              (Limits.colimit F).presheaf.map
                (𝟙
                  (op
                    (obj
                      (Opens.map
                        (Hom.base
                          (Iso.hom
                            (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                      (obj
                        (Opens.map
                          (Hom.base
                            (Iso.inv
                              (colimit.isoColimitCocone
                                { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                                  ColimitCocone F }))))
                        U)))))
            ((Limits.colimit F).presheaf.map (eqToHom ⋯)) :
          obj
              (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
                    (Hom.base
                      (Iso.inv
                        (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                  U)) ⟶
            (Limits.colimit F).presheaf.obj (op U)) ≫
      NatTrans.app (Hom.c (colimit.ι F j)) (op U))
    (limit.π (componentwiseDiagram F U) (op j))

Tactic:
rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality,
      ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc,
      colimitCocone_ι_app_c, limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limMap_π_assoc, CategoryTheory.Category.comp_id, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app_assoc, AlgebraicGeometry.PresheafedSpace.congr_app, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom, AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c