-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
x : ↥X
⊢ 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.left : Discrete WalkingPair })
              (BinaryCofan.inl ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat)) :
                Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                    { as := WalkingPair.left : 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.left : 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.left : Discrete WalkingPair } ⟶
                  Scheme.forgetToTop.obj (X ⨿ Y))) :
          (a :
              (↑((pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)).obj
                    { as := WalkingPair.left }) :
                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 X) (Y := Scheme.forgetToTop.obj (X ⨿ Y)) (Scheme.forgetToTop.map coprod.inl) :
          (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj (X ⨿ Y)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (X ⨿ Y)) : Type u))
have e_a : Eq (α :=
  Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
      { as := WalkingPair.left : 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.left : Discrete WalkingPair })
    (BinaryCofan.inl ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat)) :
      Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
          { as := WalkingPair.left : 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.left : 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.left : Discrete WalkingPair } ⟶
        Scheme.forgetToTop.obj (X ⨿ Y)))
  (Scheme.forgetToTop.map coprod.inl)
Tactic: congr 2