-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X Y : Scheme
x : ↥X
⊢ Eq (α := ↥(X ⨿ Y)) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y)) (coprod.inl x : ↥(X ⨿ Y))
have 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.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))
Tactic: change ((TopCat.binaryCofan X Y).inl ≫
    (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map coprod.inl x