-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits (goal)
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)
⊢ 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))
have 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 := sorry :
                              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))
Tactic: simp only [colimitCocone, colimit, ← TopCat.comp_app]