-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
e :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Eq (α := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                  (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)))))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) g.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
            (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                  (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)))))
        x)
⊢ Eq (α :=
    (↑(↑X.toPresheafedSpace : TopCat) : Type v) ⟶
      (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
    (CategoryStruct.comp (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
      (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))))
    (CategoryStruct.comp (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
      (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              g.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      (↾(⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))))

Tactic:
ext