-- 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
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U)))

Tactic:
have := ι_comp_coequalizerComparison f.toShHom g.toShHom SheafedSpace.forgetToPresheafedSpace

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)) ≫
      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)))

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 ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U)))

Tactic:
erw [SheafedSpace.congr_app this.symm (op U)]

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.π (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
                  (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)) ≫
                (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                    (Hom.toShHom g)).hom).c.app
          (op U) ≫
        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)) ≫
      (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.π (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
                  (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)) ≫
                (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                    (Hom.toShHom g)).hom).c.app
          (op U) ≫
        Y.presheaf.map (eqToHom ⋯)))

Tactic:
rw [PresheafedSpace.comp_c_app, ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]

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
      (((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 ⋯)))