-- 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)
erw :
  IsOpen (X := (↑(Functor.obj (SheafedSpace.forget CommRingCat) Y.toSheafedSpace) : Type v))
    (Set.preimage (β :=
      (↑(Functor.obj (SheafedSpace.forget CommRingCat) (coequalizer (Hom.toShHom f) (Hom.toShHom g))) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := Functor.obj (SheafedSpace.forget CommRingCat) Y.toSheafedSpace) (Y :=
            Functor.obj (SheafedSpace.forget CommRingCat) (coequalizer (Hom.toShHom f) (Hom.toShHom g)))
            (CategoryStruct.comp (Y :=
              coequalizer (X := Functor.obj (SheafedSpace.forget CommRingCat) X.toSheafedSpace)
                (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom f))
                (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom g)))
              (coequalizer.π (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom f))
                (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom g)))
              (Iso.hom (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g))))) :
        (a : (↑((SheafedSpace.forget CommRingCat).obj Y.toSheafedSpace) : Type v)) →
          (↑((SheafedSpace.forget CommRingCat).obj (coequalizer (Hom.toShHom f) (Hom.toShHom g))) : 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)) ''
        (imageBasicOpen f g U s).carrier))
⊢ IsOpen (X := (↑(Functor.obj (SheafedSpace.forget CommRingCat) Y.toSheafedSpace) : Type v))
    (Set.preimage (β :=
      (↑(Functor.obj (SheafedSpace.forget CommRingCat) (coequalizer (Hom.toShHom f) (Hom.toShHom g))) : Type v))
      (Function.comp (β :=
        (↑(coequalizer (X := Functor.obj (SheafedSpace.forget CommRingCat) X.toSheafedSpace)
              (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom f))
              (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom g))) :
          Type v))
        (⇑(TopCat.homeoOfIso
              (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g))) :
          (a :
              (↑(coequalizer ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
                    ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g))) :
                Type v)) →
            (↑((SheafedSpace.forget CommRingCat).obj (coequalizer (Hom.toShHom f) (Hom.toShHom g))) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := Functor.obj (SheafedSpace.forget CommRingCat) Y.toSheafedSpace) (Y :=
              coequalizer (X := Functor.obj (SheafedSpace.forget CommRingCat) X.toSheafedSpace)
                (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom f))
                (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom g)))
              (coequalizer.π (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom f))
                (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat) (Hom.toShHom g)))) :
          (a : (↑((SheafedSpace.forget CommRingCat).obj Y.toSheafedSpace) : Type v)) →
            (↑(coequalizer ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
                  ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g))) :
              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)) ''
        (imageBasicOpen f g U s).carrier))

Tactic:
erw [← TopCat.coe_comp]

Premises used: TopCat.coe_comp