-- 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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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))

Tactic:
simp only [← IsIso.comp_inv_eq,
          ← InducedCategory.comp_hom,
          PresheafedSpace.stalkMap.congr_hom _ _
            (congr_arg (InducedCategory.Hom.hom) (colimit.ι_desc
              (forgetToSheafedSpace.mapCocone s) i))] at this

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.InducedCategory.comp_hom, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, congr_arg, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.IsIso.comp_inv_eq, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, CategoryTheory.InducedCategory.Hom.hom