-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat → Prop
α : Type w
inst : Finite α
X : α → CompHausLike P
inst_1 : HasExplicitFiniteCoproduct.{w, u} (P := P) X
a : α
e_2 :
  (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)) =
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X)
x : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)
h :
  Eq (α :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.cofan.{w, u} (P := P) X).pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y :=
            (finiteCoproduct.cofan.{w, u} (P := P) X).pt)
            (CategoryStruct.comp (Y := ∐ X) (Sigma.ι X a)
              (Iso.hom
                (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
                  (finiteCoproduct.isColimit (P := P) X)))) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct.cofan X).pt)
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.cofan.{w, u} (P := P) X).pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (finiteCoproduct.ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))
⊢ Eq (α := (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
    (Function.comp (β := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (∐ X))
        (⇑(homeoOfIso (P := P)
              (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
                (finiteCoproduct.isColimit (P := P) X))) :
          (a : (↑(colimit.cocone (Discrete.functor X)).pt.toTop : Type (max u w))) →
            (↑(finiteCoproduct.cofan X).pt.toTop : Type (max u w)))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
              fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := ∐ X) (Sigma.ι X a)) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (∐ X))
        x :
      (↑((finiteCoproduct.cofan.{w, u} (P := P) X).pt.toTop (P := P)) : Type (max u w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
            C((↑(x1.toTop (P := P)) : Type (max u w)), (↑(x2.toTop (P := P)) : Type (max u w)))) (CC :=
            fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (Y := finiteCoproduct.{w, u} (P := P) X)
            (finiteCoproduct.ι (P := P) X a) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X))
        x :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (finiteCoproduct.{w, u} (P := P) X))

Tactic:
change (Sigma.ι X a ≫ _) x = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Sigma.ι, CategoryTheory.CategoryStruct.comp, DFunLike.coe