-- 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)
rw :
  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)))
            (CategoryTheory.Functor.map (SheafedSpace.forget CommRingCat)
              (coequalizer.π (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))
      (⇑(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))

Tactic:
rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]

Premises used: CategoryTheory.Limits.PreservesCoequalizer.iso_hom, CategoryTheory.Limits.ι_comp_coequalizerComparison