-- 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)
X : Jᵒᵖ
x : (↑((F ⋙ forget C).obj (unop X)) : Type v)
app :
  Eq (α := (↑(↑(Limits.colimit F) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (F ⋙ forget C).obj (unop X)) (Y := (↑(Limits.colimit F) : TopCat))
            (colimit.ι (F ⋙ forget C) (unop X) ≫
              Hom.base
                (Iso.hom
                  (Iso.symm
                    (colimit.isoColimitCocone
                      {
                        cocone :=
                          {
                            pt :=
                              { carrier := Limits.colimit (F ⋙ forget C),
                                presheaf :=
                                  (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))) :
                                PresheafedSpace.{v, u, v} C },
                            ι :=
                              {
                                app := fun (j : J) ↦
                                  { base := colimit.ι (F ⋙ forget C) j,
                                    c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) :
                                    (F.obj j).Hom
                                      (obj
                                        (obj (Functor.const J)
                                          { carrier := Limits.colimit (F ⋙ forget C),
                                            presheaf :=
                                              (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))) :
                                            PresheafedSpace.{v, u, v} C })
                                        j) },
                                naturality := ⋯ :
                                NatTrans F
                                  (obj (Functor.const J)
                                    { carrier := Limits.colimit (F ⋙ forget C),
                                      presheaf :=
                                        (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))) :
                                      PresheafedSpace.{v, u, v} C }) } :
                            Cocone F },
                        isColimit := (colimitCoconeIsColimit F : IsColimit (colimitCocone F)) : ColimitCocone F })))) :
          (a : (↑((F ⋙ forget C).obj (unop X)) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit F) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(F.obj (unop X)) : TopCat)) (Y := (↑(Limits.colimit F) : TopCat)) (Hom.base (colimit.ι F (unop X))) :
          (a : (↑(↑(F.obj (unop X)) : TopCat) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit F) : TopCat) : Type v))
⊢ Eq (α := (↑(↑(Limits.colimit F) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑(Limits.colimit F) : TopCat))
            (Hom.base
              (Iso.hom
                (Iso.symm
                  (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F })))) :
          (a : (↑(↑(colimitCocone F).pt : TopCat) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (X := (F ⋙ forget C).obj (unop X)) (Y := Limits.colimit (F ⋙ forget C))
                (colimit.ι (F ⋙ forget C) (unop X)) :
              (a : (↑((F ⋙ forget C).obj (unop X)) : Type v)) → (↑(Limits.colimit (F ⋙ forget C)) : Type v))
            x :
          (↑(Limits.colimit (F ⋙ forget C)) : Type v)) :
      (↑(↑(Limits.colimit F) : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(F.obj (unop X)) : TopCat)) (Y := (↑(Limits.colimit F) : TopCat)) (Hom.base (colimit.ι F (unop X))) :
          (a : (↑(↑(F.obj (unop X)) : TopCat) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit F) : TopCat) : Type v))

Tactic:
simp only [colimitCocone, colimit, ← TopCat.comp_app]

Premises used: TopCat.comp_app, AlgebraicGeometry.PresheafedSpace.colimit, AlgebraicGeometry.PresheafedSpace.colimitCocone