-- 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)
⊢ 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)))
have H : Eq.{v + 1} (α := Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v))
  (X.toRingedSpace.basicOpen (U :=
    (Opens.map f.base).obj
      ((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
        U))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
          CommRingCat.carrier) (X :=
          Y.presheaf.obj
            (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
                U)))
          (f.c.app
            (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
                U))) :
        (a :
            (↑(Y.presheaf.obj (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))) :
              Type v)) →
          (↑(X.presheaf.obj
                (op
                  ((Opens.map f.base).obj
                    ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U)))) :
            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))))
  (X.toRingedSpace.basicOpen (U :=
    (Opens.map g.base).obj
      ((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
        U))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
          CommRingCat.carrier) (X :=
          Y.presheaf.obj
            (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
                U)))
          (g.c.app
            (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
                U))) :
        (a :
            (↑(Y.presheaf.obj (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))) :
              Type v)) →
          (↑(X.presheaf.obj
                (op
                  ((Opens.map g.base).obj
                    ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U)))) :
            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))))
Tactic: dsimp