-- 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 := (↑(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))
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))
    (⇑(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))
Tactic: rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]