-- 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
U : (Opens (↑(↑s.pt : TopCat) : Type v))ᵒᵖ
refine_1 :
  (j : Jᵒᵖ) →
    obj.{v', v, u', u} (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj U)) j ⟶
      (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)
                (obj (Functor.op (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)))) U) :
              CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)).obj
        j
refine_2 :
  ∀ (j j' : Jᵒᵖ) (f : j ⟶ j'),
    map (obj (Functor.const Jᵒᵖ) (s.pt.presheaf.obj U)) f ≫
        CategoryStruct.comp (Y := (obj (pushforward C (Hom.base (s.ι.app (unop j')))) (F.obj (unop j')).presheaf).obj U)
          (NatTrans.app (Hom.c (s.ι.app (unop j'))) U) ((F.obj (unop j')).presheaf.map (eqToHom ⋯)) =
      CategoryStruct.comp (Y := (obj (pushforward C (Hom.base (s.ι.app (unop j)))) (F.obj (unop j)).presheaf).obj U)
          (NatTrans.app (Hom.c (s.ι.app (unop j))) U) ((F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
        (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)
                  (obj (Functor.op (Opens.map (colimit.desc (F ⋙ forget C) (mapCocone (forget C) s)))) U) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)).map
          f
⊢ 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

Tactic:
refine
    limit.lift _
        { pt := s.pt.presheaf.obj U
          π :=
            { app := fun j => ?_
              naturality := fun j j' f => ?_ } } ≫
      (limitObjIsoLimitCompEvaluation _ _).inv

Premises used: CategoryTheory.NatTrans.mk, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.Cone.mk, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cocone.pt