-- 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 π)
h_1 :
  ∀ (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
e : ∀ (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 :=
  h_1
b : (↑(B.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
t : α
x : (↑((X t).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
h :
  (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)) (π t) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (X t)) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B)
      x =
    b
⊢ ∃ (a :
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : 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)) (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)
        a =
      b
have refine : (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)
    ((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)) (Y := ∐ X) (Sigma.ι X t) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (X t)) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (∐ X))
        x :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        (∐ X)) =
  b
Tactic: refine ⟨Sigma.ι X t x, ?_⟩