-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.EffectiveEpi (hypothesis)
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 π)
⊢ [EffectiveEpiFamily X π, Epi (X := ∐ X) (Sigma.desc π),
      ∀ (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].TFAE
have tfae_2_to_3 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)) (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
Tactic: tfae_have 2 → 3
  | e => by
    rw [epi_iff_surjective] at e
    let i : ∐ X ≅ finiteCoproduct X :=
      (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _)
    intro b
    obtain ⟨t, rfl⟩ := e b
    let q := i.hom t
    refine ⟨q.1,q.2,?_⟩
    have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id]; rfl
    rw [this]
    change _ = (i.inv ≫ Sigma.desc π) (i.hom t)
    suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by
      rw [this]; rfl
    rw [Iso.inv_comp_eq]
    apply colimit.hom_ext
    rintro ⟨a⟩
    simp only [i, Discrete.functor_obj, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
      colimit.comp_coconePointUniqueUpToIso_hom_assoc]
    ext; rfl