-- 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
i : Discrete ι
y : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)
this :
  Eq (α :=
    (forgetToSheafedSpace.mapCocone s).pt.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Y := (↑(forgetToSheafedSpace.mapCocone s).pt.toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom
                  (CategoryStruct.comp (Y := colimit (F ⋙ forgetToSheafedSpace))
                    (colimit.ι (F ⋙ forgetToSheafedSpace) i)
                    (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s))))) :
            (a : (↑(↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(forgetToSheafedSpace.mapCocone s).pt.toPresheafedSpace : TopCat) : Type u))
          y) ⟶
      (colimit (F ⋙ forgetToSheafedSpace)).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))
    ((eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
      inv (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i)) y))
    (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))
dsimp :
  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.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.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.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.obj i).toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace : TopCat) : Type u))
              y)) :
        Type u))
    (RingHom.comp
      (CommRingCat.Hom.hom
        (inv (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i)) y)))
      (RingHom.comp (CommRingCat.Hom.hom ((s.ι.app i).stalkMap y)) (CommRingCat.Hom.hom (eqToHom ⋯))))
⊢ 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
      ((eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
        inv (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i)) y)))

Tactic:
dsimp