-- 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
inst_5 : HasColimit F
U : Opens (↑(↑(Limits.colimit F) : TopCat) : Type v)
app :
  (X : Jᵒᵖ) →
    obj
        (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)
              (obj
                (Functor.op
                  (Opens.map
                    (Hom.base
                      (Iso.hom
                        (Iso.symm
                          (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))))
                (op U)) :
            CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C))
        X ≅
      (componentwiseDiagram F U).obj X
naturality :
  autoParam
    (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y),
      Eq (α :=
        obj
            (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)
                  (obj
                    (Functor.op
                      (Opens.map
                        (Hom.base
                          (Iso.hom
                            (Iso.symm
                              (colimit.isoColimitCocone
                                { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                                  ColimitCocone F }))))))
                    (op U)) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C))
            X ⟶
          (componentwiseDiagram F U).obj Y)
        (map
            (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)
                  (obj
                    (Functor.op
                      (Opens.map
                        (Hom.base
                          (Iso.hom
                            (Iso.symm
                              (colimit.isoColimitCocone
                                { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                                  ColimitCocone F }))))))
                    (op U)) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C))
            f ≫
          Iso.hom (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)))
        (Iso.hom (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ≫ (componentwiseDiagram F U).map f))
    NatIso.ofComponents._auto_1
⊢ 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)
          (obj
            (Functor.op
              (Opens.map
                (Hom.base
                  (Iso.hom
                    (Iso.symm
                      (colimit.isoColimitCocone
                        { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))))
            (op U)) :
        CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C) ≅
    componentwiseDiagram F U

Tactic:
fapply NatIso.ofComponents

Premises used: CategoryTheory.NatIso.ofComponents