-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : (↑Y.toTopCat : Type v)
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
hU :
  Membership.mem (α := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
        x :
      (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
s :
  ToType (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := CommRingCat.carrier)
    ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit (M := (↑(Y.presheaf.stalk x) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            CommRingCat.carrier) (X :=
            Y.presheaf.obj
              (op
                (Functor.obj
                  (Opens.map
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                  U)))
            (Y := Y.presheaf.stalk x)
            (Y.presheaf.germ
              (Functor.obj
                (Opens.map
                  (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                U)
              x hU) :
          (a :
              (↑(Y.presheaf.obj (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U))) :
                Type v)) →
            (↑(Y.presheaf.stalk x) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                CommRingCat.carrier) (Y :=
                Y.presheaf.obj
                  (op
                    (Functor.obj
                      (Opens.map
                        (PresheafedSpace.Hom.base
                          (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                      U)))
                (NatTrans.app
                  (PresheafedSpace.Hom.c (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))
                  (op U)) :
              (a : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)) →
                (↑(Y.presheaf.obj (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U))) :
                  Type v))
            s :
          (↑(Y.presheaf.obj
                (op
                  (Functor.obj
                    (Opens.map
                      (PresheafedSpace.Hom.base
                        (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                    U))) :
            Type v)) :
      (↑(Y.presheaf.stalk x) : Type v))
V : Opens (↑Y.toTopCat : Type v) := imageBasicOpen f g U s
hV :
  Set.preimage (β := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
          (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
            (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
        V.carrier) =
    V.carrier
hV' :
  V =
    {
      carrier :=
        Set.preimage (β := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base
                    (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
            V.carrier),
      is_open' := ⋯ }
V_open :
  IsOpen (X := (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
          (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
      V.carrier)
VleU :
  {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
          V.carrier,
      is_open' := V_open :
      Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) } ≤
    U
hxV : x ∈ V
map_nonunit :
  IsUnit (M :=
    (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
            x)) :
      Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            ToType (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := CommRingCat.carrier))
            (X :=
            (coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj
              (op
                {
                  carrier :=
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) (Y :=
                            (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                            (PresheafedSpace.Hom.base
                              (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
                        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                          (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
                      V.carrier,
                  is_open' := V_open }))
            (Y :=
            (coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                    (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                x))
            ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ
              {
                carrier :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (Y :=
                          (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                          (PresheafedSpace.Hom.base
                            (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
                      (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                        (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
                    V.carrier,
                is_open' := V_open }
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                    (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                x)
              ⋯) :
          (a :
              ToType
                ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj
                  (op
                    {
                      carrier :=
                        (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) :
                            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) :
                                Type v)) ''
                          V.carrier,
                      is_open' := V_open }))) →
            ToType
              ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
                ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base :
                    (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                      (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                  x)))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                ToType (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                  CommRingCat.carrier))
                ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.map (homOfLE VleU).op) :
              (a : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))) →
                ToType
                  ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj
                    (op
                      {
                        carrier :=
                          (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) :
                              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) :
                                  Type v)) ''
                            V.carrier,
                        is_open' := V_open })))
            s :
          ToType (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := CommRingCat.carrier)
            ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj
              (op
                {
                  carrier :=
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) (Y :=
                            (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                            (PresheafedSpace.Hom.base
                              (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))))) :
                        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                          (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)) ''
                      V.carrier,
                  is_open' := V_open :
                  Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) }))) :
      ToType (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := CommRingCat.carrier)
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
            x)))
⊢ IsUnit (M :=
    (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
            x)) :
      Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            CommRingCat.carrier) (Y :=
            (coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                    (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                x))
            ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                    (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                x)
              hU) :
          (a : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)) →
            (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
                  ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base :
                      (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                        (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                    x)) :
              Type v))
        s :
      (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                  (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
              x)) :
        Type v))

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

Premises used: TopCat.Presheaf.germ_res_apply, CategoryTheory.ConcreteCategory.hom, Set.mem_image_of_mem, CategoryTheory.homOfLE, CategoryTheory.Limits.coequalizer, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.InducedCategory.Hom.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom, CategoryTheory.Limits.coequalizer.π, DFunLike.coe