-- 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
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)
h :
  ∀ (U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ) (j : Jᵒᵖ),
    Eq (α :=
      s.pt.presheaf.obj U ⟶
        obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
          (obj
              (Functor.leftOp (pushforwardDiagramToColimit F) :
                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
              j :
            CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
          (obj
              (Functor.op (Opens.map (Hom.base (desc F s))) :
                (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ ⥤ (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ)
              U :
            (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ))
      (NatTrans.app (m.c ≫ whiskerRight (eqToHom ⋯) (colimitCocone F).pt.presheaf) U ≫
          NatTrans.app (limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) j)
            (obj
              (Functor.op (Opens.map (Hom.base (desc F s))) :
                (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ ⥤ (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ)
              U) :
        s.pt.presheaf.obj U ⟶
          obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
            (obj
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                j :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (obj
                (Functor.op (Opens.map (Hom.base (desc F s))) :
                  (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ ⥤ (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ)
                U :
              (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ))
      (NatTrans.app (Hom.c (desc F s)) U ≫
          NatTrans.app (limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) j)
            (obj
              (Functor.op (Opens.map (Hom.base (desc F s))) :
                (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ ⥤ (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ)
              U) :
        s.pt.presheaf.obj U ⟶
          obj (C := (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ)
            (obj
                (Functor.leftOp (pushforwardDiagramToColimit F) :
                  Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
                j :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
            (obj
                (Functor.op (Opens.map (Hom.base (desc F s))) :
                  (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ ⥤ (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ)
                U :
              (Opens (↑(↑(colimitCocone F).pt : TopCat) : Type v))ᵒᵖ))
⊢ Eq (α := s.pt.presheaf ⟶ Functor.op (Opens.map (Hom.base (desc F s))) ⋙ (colimitCocone F).pt.presheaf)
    (m.c ≫ whiskerRight (eqToHom ⋯) (colimitCocone F).pt.presheaf) (Hom.c (desc F s))

Tactic:
refine NatTrans.ext (funext fun U => limit_obj_ext fun j => ?_)

Premises used: CategoryTheory.Limits.limit_obj_ext, CategoryTheory.NatTrans.ext, funext