-- 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)
F : J ⥤ PresheafedSpace.{v, u, v} C
j j' : J
f : j ⟶ j'
h :
  ∀ (carrier : Set (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v)) (is_open' : IsOpen carrier),
    Eq (α :=
      (obj (obj (Functor.const J) (colimit F)) j').presheaf.obj
          (op
            { carrier := carrier, is_open' := is_open' :
              Opens (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v) }) ⟶
        obj
          (Functor.op
              (Opens.map
                (Hom.base
                  ({ base := colimit.ι (F ⋙ forget C) j,
                      c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) :
                      (F.obj j).Hom (obj (obj (Functor.const J) (colimit F)) j) } ≫
                    map (obj (Functor.const J) (colimit F)) f))) ⋙
            (F.obj j).presheaf)
          (op
            { carrier := carrier, is_open' := is_open' :
              Opens (↑(↑(obj (obj (Functor.const J) (colimit F)) j') : TopCat) : Type v) }))
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          obj
            (pushforward C
              (Hom.base
                (F.map f ≫
                  { base := colimit.ι (F ⋙ forget C) j',
                    c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') :
                    (F.obj j').Hom (obj (obj (Functor.const J) (colimit F)) j') })))
            (F.obj j).presheaf)
          (Hom.c
            (F.map f ≫
              { base := colimit.ι (F ⋙ forget C) j',
                c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') }))
          (whiskerRight (eqToHom ⋯) (F.obj j).presheaf))
        (op { carrier := carrier, is_open' := is_open' }))
      (NatTrans.app
        (Hom.c
          ({ base := colimit.ι (F ⋙ forget C) j,
              c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
            map (obj (Functor.const J) (colimit F)) f))
        (op { carrier := carrier, is_open' := is_open' }))
⊢ Eq (α :=
    (obj (obj (Functor.const J) (colimit F)) j').presheaf ⟶
      Functor.op
          (Opens.map
            (Hom.base
              ({ base := colimit.ι (F ⋙ forget C) j,
                  c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
                map (obj (Functor.const J) (colimit F)) f))) ⋙
        (F.obj j).presheaf)
    (CategoryStruct.comp (Y :=
      obj
        (pushforward C
          (Hom.base
            (F.map f ≫
              { base := colimit.ι (F ⋙ forget C) j',
                c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') :
                (F.obj j').Hom (obj (obj (Functor.const J) (colimit F)) j') })))
        (F.obj j).presheaf)
      (Hom.c
        (F.map f ≫
          { base := colimit.ι (F ⋙ forget C) j',
            c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j') }))
      (whiskerRight (eqToHom ⋯) (F.obj j).presheaf))
    (Hom.c
      ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) } ≫
        map (obj (Functor.const J) (colimit F)) f))

Tactic:
ext ⟨⟩