-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ 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)
have 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))
Tactic: rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.toShHom
    g.toShHom)).isOpen_preimage, TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]