-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
e_a :
  Eq (α := (f i).toTopCat ⟶ Scheme.forgetToTop.obj (∐ f))
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
        (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
        (f i).toTopCat ⟶
          Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
          (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
        Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
          Scheme.forgetToTop.obj (∐ f)))
    (Scheme.forgetToTop.map (Sigma.ι f i))
⊢ Eq (α := (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            Scheme.forgetToTop.obj (∐ f))
            (CategoryStruct.comp (Y :=
              Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
              (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
                (f i).toTopCat ⟶
                  Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                    (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
              (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
                  (Iso.inv
                    (colimit.isoColimitCocone
                      { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                        isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
                  (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
                Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                    (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
                  Scheme.forgetToTop.obj (∐ f))) :
          (a : (↑(f i).toTopCat : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            Scheme.forgetToTop.obj (∐ f)) (Scheme.forgetToTop.map (Sigma.ι f i)) :
          (a : (↑(Scheme.forgetToTop.obj (f i)) : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))

Tactic:
congr 2