Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: 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)).hom.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)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier)
VleU :
  { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := V_open } ≤
    U
hxV : x ∈ V
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U) ≫
          Y.presheaf.map
            ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.map (homOfLE VleU).op ≫
              (eqToHom hV').op)))
      s)

Tactic:
]

Goal state after:
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)).hom.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)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier)
VleU :
  { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := V_open } ≤
    U
hxV : x ∈ V
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U) ≫
          Y.presheaf.map
            ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.map (homOfLE VleU).op ≫
              (eqToHom hV').op)))
      s)