-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
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
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) ⋯) :
              C((↑X : Type u), (↑W : Type u))) :
            (a : (↑X : Type u)) → (↑W : Type u))
          a :
        (↑W : Type u))
⊢ 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)) })

Tactic:
ext