-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.EffectiveEpi (goal)
Goal:
α : Type
inst : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
tfae_3_to_2 :
  ∀
    (a :
      ∀ (b : (↑(B.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)),
        ∃ (a : α) (x : (↑((X a).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                  C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                    (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                  (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                  (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) (π a) :
                (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (X a)) →
                  (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B)
              x =
            b),
    Epi (X := ∐ X) (Sigma.desc π)
h : Epi (X := ∐ X) (Sigma.desc π)
e :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      (∐ X))
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) (X := ∐ X) (Sigma.desc π)) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (∐ X)) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B)
i : ∐ X ≅ finiteCoproduct (P := fun (x : TopCat.{u}) ↦ True) X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X))
    (finiteCoproduct.isColimit (P := fun (x : TopCat.{u}) ↦ True) X)
t : (↑((∐ X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
q : (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
  (finiteCoproduct (P := fun (x : TopCat.{u}) ↦ True) X) :=
  (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
        C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
          (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
        (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) i.hom :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (∐ X)) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (finiteCoproduct X))
    t
this :
  t =
    (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) i.inv :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (finiteCoproduct X)) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (∐ X))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) i.hom :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (∐ X)) →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (finiteCoproduct X))
          t :
        (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (finiteCoproduct (P := fun (x : TopCat.{u}) ↦ True) X))
a : α
⊢ Eq (α := Functor.obj (Discrete.functor X) { as := a : Discrete α } ⟶ B)
    (CategoryStruct.comp (Y := colimit (Discrete.functor X)) (colimit.ι (Discrete.functor X) { as := a })
      (Sigma.desc π))
    (colimit.ι (Discrete.functor X) { as := a } ≫ i.hom ≫ finiteCoproduct.desc (P := fun (x : TopCat.{u}) ↦ True) X π)
have w : π a =
  CategoryStruct.comp (Y := finiteCoproduct (P := fun (x : TopCat.{u}) ↦ True) X)
    (finiteCoproduct.ι (P := fun (x : TopCat.{u}) ↦ True) X a)
    (finiteCoproduct.desc (P := fun (x : TopCat.{u}) ↦ True) X π)
Tactic: simp only [i, Discrete.functor_obj, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
      colimit.comp_coconePointUniqueUpToIso_hom_assoc]