-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥Y
e_a :
  Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      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)))
    (Scheme.forgetToTop.map coprod.inr)
⊢ 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))

Tactic:
congr 2