-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
H :
  Eq.{v + 1} (α := Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v))
    (X.toRingedSpace.basicOpen (U :=
      (Opens.map f.base).obj
        (unop
          (op
            ((Opens.map
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                    Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
              (unop (op U))))))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            CommRingCat.carrier) (X :=
            Y.presheaf.obj
              (op
                (unop
                  (op
                    ((Opens.map
                            (PresheafedSpace.Hom.base
                              (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                          Opens
                              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                            Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                      (unop (op U)))))))
            (f.c.app
              (op
                (unop
                  (op
                    ((Opens.map
                            (PresheafedSpace.Hom.base
                              (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                          Opens
                              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                            Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                      (unop (op U))))))) :
          (a :
              (↑(Y.presheaf.obj
                    (op
                      (unop
                        (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))) :
                Type v)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj
                  (op
                    (unop
                      (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))) :
              Type v))
        (have this :
          (↑(Y.presheaf.obj
                (op
                  (unop
                    (op
                      ((Opens.map
                              (PresheafedSpace.Hom.base
                                (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                            Opens
                                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) :
                                  Type v) ⥤
                              Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                        (unop (op U))))))) :
            Type v) :=
          (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                CommRingCat.carrier) (Y :=
                Functor.obj
                  (Functor.obj
                    (TopCat.Presheaf.pushforward CommRingCat
                      (PresheafedSpace.Hom.base
                        (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                    Y.presheaf)
                  (op 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)) →
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj
                          Y.presheaf).obj
                      (op U)) :
                  Type v))
            s;
        this)))
    (X.toRingedSpace.basicOpen (U :=
      (Opens.map g.base).obj
        (unop
          (op
            ((Opens.map
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                    Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
              (unop (op U))))))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
            CommRingCat.carrier) (X :=
            Y.presheaf.obj
              (op
                (unop
                  (op
                    ((Opens.map
                            (PresheafedSpace.Hom.base
                              (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                          Opens
                              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                            Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                      (unop (op U)))))))
            (g.c.app
              (op
                (unop
                  (op
                    ((Opens.map
                            (PresheafedSpace.Hom.base
                              (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                          Opens
                              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                            Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                      (unop (op U))))))) :
          (a :
              (↑(Y.presheaf.obj
                    (op
                      (unop
                        (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))) :
                Type v)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat g.base).obj X.presheaf).obj
                  (op
                    (unop
                      (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))) :
              Type v))
        (have this :
          (↑(Y.presheaf.obj
                (op
                  (unop
                    (op
                      ((Opens.map
                              (PresheafedSpace.Hom.base
                                (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                            Opens
                                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) :
                                  Type v) ⥤
                              Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                        (unop (op U))))))) :
            Type v) :=
          (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                CommRingCat.carrier) (Y :=
                Functor.obj
                  (Functor.obj
                    (TopCat.Presheaf.pushforward CommRingCat
                      (PresheafedSpace.Hom.base
                        (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                    Y.presheaf)
                  (op 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)) →
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj
                          Y.presheaf).obj
                      (op U)) :
                  Type v))
            s;
        this)))
⊢ (Opens.map f.base).obj
      (Y.toRingedSpace.basicOpen (U :=
        unop
          (op
            ((Opens.map
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                    Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
              (unop (op U)))))
        (have this :
          (↑(Y.presheaf.obj
                (op
                  (unop
                    (op
                      ((Opens.map
                              (PresheafedSpace.Hom.base
                                (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                            Opens
                                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) :
                                  Type v) ⥤
                              Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                        (unop (op U))))))) :
            Type v) :=
          (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                CommRingCat.carrier) (Y :=
                Functor.obj
                  (Functor.obj
                    (TopCat.Presheaf.pushforward CommRingCat
                      (PresheafedSpace.Hom.base
                        (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                    Y.presheaf)
                  (op 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)) →
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj
                          Y.presheaf).obj
                      (op U)) :
                  Type v))
            s;
        this)) =
    (Opens.map g.base).obj
      (Y.toRingedSpace.basicOpen (U :=
        unop
          (op
            ((Opens.map
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                  Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v) ⥤
                    Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
              (unop (op U)))))
        (have this :
          (↑(Y.presheaf.obj
                (op
                  (unop
                    (op
                      ((Opens.map
                              (PresheafedSpace.Hom.base
                                (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                            Opens
                                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) :
                                  Type v) ⥤
                              Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)).1
                        (unop (op U))))))) :
            Type v) :=
          (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                CommRingCat.carrier) (Y :=
                Functor.obj
                  (Functor.obj
                    (TopCat.Presheaf.pushforward CommRingCat
                      (PresheafedSpace.Hom.base
                        (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))))
                    Y.presheaf)
                  (op 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)) →
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj
                          Y.presheaf).obj
                      (op U)) :
                  Type v))
            s;
        this))

Tactic:
rw [preimage_basicOpen f, preimage_basicOpen g]

Premises used: AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen