-- 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)
F : J ⥤ PresheafedSpace.{v, u, v} C
j j' : J
f : j ⟶ j'
⊢ 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))
have 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 sorry) (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' }))
Tactic: ext ⟨⟩