-- 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
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))
have h₁ : Eq (α := (↑(W.toTop (P := P)) : 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)) g :
        (a : (↑B.toTop : Type u)) → (↑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 : (↑X.toTop : Type u)) → (↑B.toTop : Type u))
          a :
        (↑(B.toTop (P := P)) : Type u)) :
    (↑(W.toTop (P := P)) : Type u))
  ((TopCat.Hom.hom (π ≫ g).hom : (a : (↑X.toTop : Type u)) → (↑W.toTop : Type u)) a : (↑(W.toTop (P := P)) : Type u))
Tactic: simp only [IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]