-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : (↑Y.toTopCat : Type v)
a :
  (↑((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)
ha :
  IsUnit (M := (↑(Y.presheaf.stalk x) : Type v))
    ((CommRingCat.Hom.hom
            (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))) x) :
          (a :
              (↑((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)) →
            (↑(Y.presheaf.stalk x) : Type v))
        a :
      (↑(Y.presheaf.stalk x) : Type v))
map_nonunit :
  ∀ (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))
        ((CommRingCat.Hom.hom
                (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))
                  x) :
              (a :
                  (↑((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)) →
                (↑(Y.presheaf.stalk 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)) :
          (↑(Y.presheaf.stalk x) : Type v))),
    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))
⊢ IsUnit a

Tactic:
rcases TopCat.Presheaf.exists_germ_eq _ a with ⟨U, hU, s, rfl⟩

Premises used: TopCat.Presheaf.exists_germ_eq, rfl