-- 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
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ :
  ∀ (x : (↑((X a).toTop (P := P)) : Type (max u w))),
    Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
      ((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))) (X :=
              finiteCoproduct.{w, u} (P := P) X) (desc (P := P) X π) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X)) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
          ((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) (ι (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))) B)
      ((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))) (π a) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
          x :
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
⊢ ∀ (x : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) (X a)),
    Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)
      ((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))) (X :=
              finiteCoproduct.{w, u} (P := P) X) (desc (P := P) X π) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (finiteCoproduct X)) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
          ((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) (ι (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))) B)
      ((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))) (π a) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) (X a)) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type (max u w))) B)
          x :
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type (max u w))) B)

Tactic:
tauto