-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
theorem coequalizer_π_stalk_isLocalHom (x : Y) :
    IsLocalHom ((coequalizer.π f.toShHom g.toShHom :).stalkMap x).hom

Proof state:
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier) =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
          (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier),
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier)
VleU :
  { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier,
      is_open' := V_open } ≤
    U
hxV : x ∈ V
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x) hU))
      s)

Tactic:
rw [← (coequalizer f.toShHom g.toShHom).presheaf.germ_res_apply (homOfLE VleU) _
    (@Set.mem_image_of_mem _ _ (coequalizer.π f.toShHom g.toShHom).base x V.1 hxV) s]

Result:
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier) =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
          (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier),
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier)
VleU :
  { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier,
      is_open' := V_open } ≤
    U
hxV : x ∈ V
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ
          { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier,
            is_open' := V_open }
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x) ⋯))
      ((ConcreteCategory.hom ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.map (homOfLE VleU).op)) s))

Proof state:
case map_nonunit.intro.intro.intro.a
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
      (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier) =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) ⁻¹'
          (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier),
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier)
VleU :
  { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) '' V.carrier,
      is_open' := V_open } ≤
    U
hxV : x ∈ V
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U) ≫
          Y.presheaf.map
            ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).op.map (homOfLE VleU).op ≫
              (eqToHom hV').op)))
      s)

Tactic:
convert @RingedSpace.isUnit_res_basicOpen Y.toRingedSpace (unop _)
    (((coequalizer.π f.toShHom g.toShHom).c.app (op U)) s)

Result:
no goals

Proof state:
case map_nonunit
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
⊢ ∀
    (a :
      ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x))),
    IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)) x)) a) →
      IsUnit a

Tactic:
rintro a ha

Result:
case map_nonunit
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
a :
  ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
      ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x))
ha : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)) x)) a)
⊢ IsUnit a

Proof state:
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x) hU))
      s)

Tactic:
let V := imageBasicOpen f g U s

Result:
case map_nonunit.intro.intro.intro
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).base) x) hU))
      s)