-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Goal:
P : TopCat.{u} → Prop
B X : CompHausLike P
π : X ⟶ B
hπ :
  Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) π) :
      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
W : CompHausLike P
e : X ⟶ W
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
h₁ :
  ∀ (a : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X),
    Eq (α := (↑(W.toTop (P := P)) : Type u))
      (((↑((Equiv.symm ⋯.liftEquiv :
                    (a : C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B, (↑W.toTop : Type u))) →
                      { g : C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X, (↑W.toTop : Type u)) //
                        Function.FactorsThrough
                          (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
                          (⇑(ConcreteCategory.hom π) :
                            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) })
                  (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                    C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                    fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) g)) :
              C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X, (↑W.toTop : Type u))) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
          a :
        (↑(W.toTop (P := P)) : Type u))
      (((↑(Subtype.mk (p :=
                  fun
                    (g :
                      C((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X,
                        (↑(W.toTop (P := P)) : Type u))) ↦
                  Function.FactorsThrough (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
                    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) (γ := (↑(W.toTop (P := P)) : Type u))
                    (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                          fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) π) :
                      (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B))
                  (TopCat.Hom.hom e.hom) ⋯) :
              C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X, (↑W.toTop : Type u))) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
          a :
        (↑(W.toTop (P := P)) : Type u))
⊢ Eq (α :=
    { g : C((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X, (↑(W.toTop (P := P)) : Type u)) //
      Function.FactorsThrough (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) (γ := (↑(W.toTop (P := P)) : Type u))
        (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) π) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) })
    ((Equiv.symm ⋯.liftEquiv :
          (a : C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B, (↑W.toTop : Type u))) →
            { g : C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X, (↑W.toTop : Type u)) //
              Function.FactorsThrough
                (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
                (⇑(ConcreteCategory.hom π) :
                  (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                    (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) })
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) g) :
      { g : C((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X, (↑(W.toTop (P := P)) : Type u)) //
        Function.FactorsThrough (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) (γ := (↑(W.toTop (P := P)) : Type u))
          (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) π) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) })
    (Subtype.mk (p :=
        fun (g : C((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X, (↑(W.toTop (P := P)) : Type u))) ↦
        Function.FactorsThrough (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) (γ := (↑(W.toTop (P := P)) : Type u))
          (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) π) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B))
        (TopCat.Hom.hom e.hom) ⋯ :
      { g : C((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X, (↑(W.toTop (P := P)) : Type u)) //
        Function.FactorsThrough (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) (γ := (↑(W.toTop (P := P)) : Type u))
          (⇑g : (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (↑W.toTop : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) π) :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B) })

Tactic:
ext