-- 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))
      (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))
⊢ IsOpen (X := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).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)) ''
      (imageBasicOpen f g U s).carrier)

Tactic:
rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.toShHom
    g.toShHom)).isOpen_preimage, TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]

Premises used: TopCat.coequalizer_isOpen_iff, CategoryTheory.Limits.PreservesCoequalizer.iso, AlgebraicGeometry.SheafedSpace.forget, Set.preimage_comp, TopCat.homeoOfIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom, Homeomorph.isOpen_preimage