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

Tactic:
have := CommRingCat.equalizer_ι_is_local_ring_hom' (PresheafedSpace.componentwiseDiagram _
      ((Opens.map
            (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                  (Hom.toShHom g)).hom.base).obj
        (unop (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))
this✝ : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
this :
  IsLocalHom
    (CommRingCat.Hom.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)))
⊢ 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)) ≫
      (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
this :
  IsLocalHom
    (CommRingCat.Hom.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)))
⊢ 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:
infer_instance

Result:
no goals