-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
theorem coequalizer_π_app_isLocalHom
    (U : TopologicalSpace.Opens (coequalizer f.toShHom g.toShHom).carrier) :
    IsLocalHom ((coequalizer.π f.toShHom g.toShHom :).c.app (op U)).hom

Proof state:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
        (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)) ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
            (op U) ≫
          (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit
                (parallelPair (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
                  (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)))
                ((Opens.map
                      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                            (Hom.toShHom g)).hom.base).obj
                  (unop (op U)))).hom ≫
            limit.π
              (PresheafedSpace.componentwiseDiagram
                (parallelPair (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
                  (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)))
                ((Opens.map
                      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                            (Hom.toShHom g)).hom.base).obj
                  (unop (op U))))
              (op WalkingParallelPair.one)) ≫
        Y.presheaf.map (eqToHom ⋯)))

Tactic:
haveI : IsIso (PreservesCoequalizer.iso
    SheafedSpace.forgetToPresheafedSpace f.toShHom g.toShHom).hom.c :=
  PresheafedSpace.c_isIso_of_iso _

Result:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
        (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)) ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
            (op U) ≫
          (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit
                (parallelPair (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
                  (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)))
                ((Opens.map
                      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                            (Hom.toShHom g)).hom.base).obj
                  (unop (op U)))).hom ≫
            limit.π
              (PresheafedSpace.componentwiseDiagram
                (parallelPair (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
                  (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)))
                ((Opens.map
                      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                            (Hom.toShHom g)).hom.base).obj
                  (unop (op U))))
              (op WalkingParallelPair.one)) ≫
        Y.presheaf.map (eqToHom ⋯)))

Proof state:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
        (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)) ≫
      coequalizerComparison (Hom.toShHom f) (Hom.toShHom g) SheafedSpace.forgetToPresheafedSpace =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U)))

Tactic:
rw [← PreservesCoequalizer.iso_hom] at this

Result:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
        (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)) ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U)))