-- 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)
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))ᵒᵖ))

Tactic:
simp [desc, descCApp,
        PresheafedSpace.congr_app (w (unop j)).symm U,
        NatTrans.congr (limit.π (pushforwardDiagramToColimit F).leftOp j)
        (congr_arg op (Functor.congr_obj (congr_arg Opens.map t) (unop U)))]

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Functor.congr_obj, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc, congr_arg, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit, Opposite.op, AlgebraicGeometry.PresheafedSpace.congr_app, TopologicalSpace.Opens.map, CategoryTheory.NatTrans.congr, CategoryTheory.Functor.leftOp, Eq.symm, Opposite.unop, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp