awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHausLike.Cartesian
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
inst : HasProp P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u))
refine :
  ∀ (x : BinaryCofan X Y) (x_1 : of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ x.pt)
    (h₁ : ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ x_1 = x.inl)
    (h₂ : ofHom P { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ x_1 = x.inr),
    x_1 =
      (fun (s : BinaryCofan X Y) ↦
          (ofHom P
              {
                toFun :=
                  Sum.elim
                    (⇑(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)) s.inl) :
                      (a :
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                            ((pair X Y).obj { as := WalkingPair.left })) →
                        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                          (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }))
                    (⇑(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)) s.inr) :
                      (a :
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                            ((pair X Y).obj { as := WalkingPair.right })) →
                        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                          (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })),
                continuous_toFun := ⋯ } :
            of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ of P (↑s.1.1 : Type u)))
        x
⊢ IsColimit (X.coproductCocone (P := P) Y)

Tactic:
refine BinaryCofan.isColimitMk (fun s ↦ ofHom _ { toFun := Sum.elim s.inl s.inr })
    (by rfl_cat) (by rfl_cat) fun _ _ h₁ h₂ ↦ ?_

Premises used: CompHausLike.ofHom, CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.BinaryCofan.isColimitMk, ContinuousMap.mk, CategoryTheory.Limits.BinaryCofan.inl, DFunLike.coe, Sum.elim
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
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
a b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (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)
        a :
      (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)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
h₁ :
  ∀ (a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)),
    Eq (α := (↑(B.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)) (X := of P (↑X.1 : Type u))
              (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
          a_1 :
        (↑(B.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)) (X := of P (↑X.1 : Type u))
              (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
          a_1 :
        (↑(B.toTop (P := P)) : Type u))
⊢ Eq (α := of P (↑X.1 : Type u) ⟶ B) (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)

Tactic:
ext
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
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
a b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (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)
        a :
      (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)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)
⊢ Eq (α := (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.toTop (P := P)) : Type u))

Tactic:
hab
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
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
a b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (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)
        a :
      (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)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)
⊢ Eq (α := (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.toTop (P := P)) : Type u))

Tactic:
exact hab
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
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 b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (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)
        a :
      (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)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
h₁ :
  ∀ (a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)),
    Eq (α := (↑(B.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)) (X := of P (↑X.1 : Type u))
              (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
          a_1 :
        (↑(B.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)) (X := of P (↑X.1 : Type u))
              (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
          a_1 :
        (↑(B.toTop (P := P)) : Type u))
⊢ Eq (α := of P (↑X.1 : Type u) ⟶ B) (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)

Tactic:
ext
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
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 b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (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)
        a :
      (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)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)
⊢ Eq (α := (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.toTop (P := P)) : Type u))

Tactic:
hab
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
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 b : (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X
hab :
  Eq (α := (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)
        a :
      (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)
        b :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
a_1 : (↑((of P (↑X.1 : Type u)).toTop (P := P)) : Type u)
⊢ Eq (α := (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.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)) (X := of P (↑X.1 : Type u))
            (ofHom P { toFun := fun (x : (↑X.1 : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of P (↑X.1 : Type u)).toTop : Type u)) → (↑B.toTop : Type u))
        a_1 :
      (↑(B.toTop (P := P)) : Type u))

Tactic:
exact hab
-- Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
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
this :
  g =
    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) ⋯))
⊢ g = ofHom P (⋯.lift (TopCat.Hom.hom e.hom) ⋯)

Tactic:
assumption