-- 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 :
  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)) })
⊢ Hom.hom g =
    Hom.hom
      (ofHom
        ((hπ.liftEquiv :
            (a :
                { 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)) }) →
              C((↑B : Type u), (↑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) ⋯)))

Tactic:
rw [hom_ofHom, ← Equiv.symm_apply_eq hπ.liftEquiv]

Premises used: TopCat.hom_ofHom, Topology.IsQuotientMap.liftEquiv, Equiv.symm_apply_eq