-- 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
s : Cocone F
U V : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
i : U ⟶ V
⊢ Eq (α :=
    s.pt.presheaf.obj U ⟶
      obj
        (obj (C := Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
          (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)) :
            Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)) ⥤
              Presheaf.{v, v, u} C (Cocone.pt (F := F ⋙ forget C) (mapCocone (forget C) s)))
          (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))))
        V)
    (s.pt.presheaf.map i ≫ descCApp F s V :
      s.pt.presheaf.obj U ⟶
        obj
          (obj (C := Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
            (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)) :
              Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)) ⥤
                Presheaf.{v, v, u} C (Cocone.pt (F := F ⋙ forget C) (mapCocone (forget C) s)))
            (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))))
          V)
    (CategoryStruct.comp (Y :=
        obj
          (obj (C := Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
            (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)) :
              Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)) ⥤
                Presheaf.{v, v, u} C (Cocone.pt (F := F ⋙ forget C) (mapCocone (forget C) s)))
            (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))))
          U)
        (descCApp F s U :
          s.pt.presheaf.obj U ⟶
            obj
              (obj (C := Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)) :
                  Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)) ⥤
                    Presheaf.{v, v, u} C (Cocone.pt (F := F ⋙ forget C) (mapCocone (forget C) s)))
                (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))))
              U)
        (map (obj (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (colimitCocone F).pt.presheaf)
            i :
          obj (obj (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (colimitCocone F).pt.presheaf)
              U ⟶
            obj
              (obj (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (colimitCocone F).pt.presheaf)
              V) :
      s.pt.presheaf.obj U ⟶
        obj (obj (pushforward C (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s))) (colimitCocone F).pt.presheaf)
          V)
have dsimp : 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 sorry),
                naturality := sorry :
                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 sorry),
                  naturality := sorry :
                  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 sorry),
                naturality := sorry :
                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 sorry),
                  naturality := sorry :
                  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: dsimp [descCApp]