-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
⊢ Eq (α :=
    { g : C((↑X : Type u), (↑W : Type u)) //
      Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
        (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
          (a : (↑X : Type u)) → (↑B : Type u)) })
    ((Equiv.symm hπ.liftEquiv :
          (a : C((↑B : Type u), (↑W : Type u))) →
            { g : C((↑X : Type u), (↑W : Type u)) //
              Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) })
        (Hom.hom g) :
      { g : C((↑X : Type u), (↑W : Type u)) //
        Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
          (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
            (a : (↑X : Type u)) → (↑B : Type u)) })
    (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
        Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
          (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
            (a : (↑X : Type u)) → (↑B : Type u)))
        (Hom.hom e) ⋯ :
      { g : C((↑X : Type u), (↑W : Type u)) //
        Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
          (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
            (a : (↑X : Type u)) → (↑B : Type u)) })
have hf : ∀ (a : (↑X : Type u)),
  Eq (α := (↑W : Type u))
    (((↑((Equiv.symm hπ.liftEquiv :
                  (a : C((↑B : Type u), (↑W : Type u))) →
                    { g : C((↑X : Type u), (↑W : Type u)) //
                      Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                        (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) })
                (Hom.hom g)) :
            C((↑X : Type u), (↑W : Type u))) :
          (a : (↑X : Type u)) → (↑W : Type u))
        a :
      (↑W : Type u))
    (((↑(Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
                Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
                  (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) π) :
                    (a : (↑X : Type u)) → (↑B : Type u)))
                (Hom.hom e) sorry) :
            C((↑X : Type u), (↑W : Type u))) :
          (a : (↑X : Type u)) → (↑W : Type u))
        a :
      (↑W : Type u))
Tactic: ext