-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥Y
change :
  Eq (α := (↑(Scheme.forgetToTop.obj (X ⨿ Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            Scheme.forgetToTop.obj (X ⨿ Y))
            (CategoryStruct.comp (Y :=
              Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                    ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
                { as := WalkingPair.right : Discrete WalkingPair })
              (BinaryCofan.inr ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat)) :
                Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                    { as := WalkingPair.right : Discrete WalkingPair } ⟶
                  Functor.obj
                    (Functor.obj (Functor.const (Discrete WalkingPair))
                      (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                        ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
                    { as := WalkingPair.right : Discrete WalkingPair })
              (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
                  (Iso.inv
                    (colimit.isoColimitCocone
                      { cocone := (↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat),
                        isColimit :=
                          (↑X.toPresheafedSpace : TopCat).binaryCofanIsColimit (↑Y.toPresheafedSpace : TopCat) }))
                  (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)) :
                Functor.obj
                    (Functor.obj (Functor.const (Discrete WalkingPair))
                      (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                        ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
                    { as := WalkingPair.right : Discrete WalkingPair } ⟶
                  Scheme.forgetToTop.obj (X ⨿ Y))) :
          (a :
              (↑((pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)).obj
                    { as := WalkingPair.right }) :
                Type u)) →
            (↑(Scheme.forgetToTop.obj (X ⨿ Y)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (X ⨿ Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            Scheme.forgetToTop.obj Y) (Y := Scheme.forgetToTop.obj (X ⨿ Y)) (Scheme.forgetToTop.map coprod.inr) :
          (a : (↑(Scheme.forgetToTop.obj Y) : Type u)) → (↑(Scheme.forgetToTop.obj (X ⨿ Y)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (X ⨿ Y)) : Type u))
⊢ Eq (α := ↥(X ⨿ Y)) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y)) (coprod.inr x : ↥(X ⨿ Y))

Tactic:
change ((TopCat.binaryCofan X Y).inr ≫
    (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map coprod.inr x

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.Limits.colimit.isoColimitCocone, AlgebraicGeometry.PresheafedSpace.carrier, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.forgetToTop, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.coprod.inr, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, TopCat.binaryCofan, DFunLike.coe, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace, TopCat.binaryCofanIsColimit