-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
ι : Type v
inst : Small.{u, v} ι
F : CategoryTheory.Functor.{v, u, v, u + 1} (Discrete ι) LocallyRingedSpace
s : Cocone F
x : (↑(coproductCofan F).pt.toTopCat : Type u)
obtain :
  ∀ (i : Discrete ι) (y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)),
    IsLocalHom (R :=
      (↑(s.pt.presheaf.stalk
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (X := (↑(coproductCofan F).pt.toPresheafedSpace : TopCat)) (Y :=
                    (↑s.pt.toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                        (InducedCategory.Hom.hom
                          (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))) :
                      (↑(coproductCofan F).pt.toPresheafedSpace : TopCat) ⟶ (↑s.pt.toPresheafedSpace : TopCat)) :
                  C((↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u),
                    (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))) :
                (a : (↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                      (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
                    (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                      (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
                  y :
                (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u)))) :
        Type u))
      (S :=
      (↑((coproductCofan F).pt.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
                (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
              y)) :
        Type u))
      (F :=
      (↑(s.pt.presheaf.stalk
              (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) (X := (↑(coproductCofan F).pt.toPresheafedSpace : TopCat)) (Y :=
                      (↑s.pt.toPresheafedSpace : TopCat))
                      (PresheafedSpace.Hom.base
                          (InducedCategory.Hom.hom
                            (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))) :
                        (↑(coproductCofan F).pt.toPresheafedSpace : TopCat) ⟶ (↑s.pt.toPresheafedSpace : TopCat)) :
                    C((↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u),
                      (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))) :
                  (a : (↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u)) →
                    (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                        (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
                      (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                        (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
                    y :
                  (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u)))) :
          Type u) →+*
        (↑((coproductCofan F).pt.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
                  (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                    (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
                y)) :
          Type u))
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap
          (InducedCategory.Hom.hom (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (Y := (↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i))) :
              (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
            y)))
⊢ IsLocalHom (R :=
    (↑(s.pt.presheaf.stalk
          (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) (X := (↑(coproductCofan F).pt.toPresheafedSpace : TopCat)) (Y :=
                  (↑s.pt.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom
                        (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))) :
                    (↑(coproductCofan F).pt.toPresheafedSpace : TopCat) ⟶ (↑s.pt.toPresheafedSpace : TopCat)) :
                C((↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u),
                  (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))) :
              (a : (↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑((coproductCofan F).pt.presheaf.stalk x) : Type u)) (F :=
    (↑(s.pt.presheaf.stalk
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (X := (↑(coproductCofan F).pt.toPresheafedSpace : TopCat)) (Y :=
                    (↑s.pt.toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                        (InducedCategory.Hom.hom
                          (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))) :
                      (↑(coproductCofan F).pt.toPresheafedSpace : TopCat) ⟶ (↑s.pt.toPresheafedSpace : TopCat)) :
                  C((↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u),
                    (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))) :
                (a : (↑(↑(coproductCofan F).pt.toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑((coproductCofan F).pt.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (InducedCategory.Hom.hom (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))) x))

Tactic:
obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x

Premises used: AlgebraicGeometry.SheafedSpace.colimit_exists_rep, CategoryTheory.Functor.comp, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace