-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.EffectiveEpi (goal)
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
⊢ 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 =
    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)) (X := B) (Y := W)
      (ofHom P
          ((⋯.liftEquiv :
              (a :
                  { 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) }) →
                C((fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B, (↑W.toTop : 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) ⋯)) :
        of P ((fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B) ⟶ of P (↑(W.toTop (P := P)) : Type u))
have h₁ : 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 sorry.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) sorry :
    { 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: rw [hom_ofHom, ← Equiv.symm_apply_eq
      (IsQuotientMap.of_surjective_continuous hπ π.hom.hom.continuous).liftEquiv]