-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits (goal)
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)
⊢ (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))
have 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)))
Tactic: rw [preimage_basicOpen f, preimage_basicOpen g]