-- Module: Mathlib.Topology.Category.CompHausLike.Limits
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
h :
  ∀ (val : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))
    (h :
      Membership.mem (γ := Set ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
        {xy : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u) |
          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)) f :
                  (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                    (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                xy.1 :
              (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)) g :
                  (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                    (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                xy.2 :
              (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)}
        val),
    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 := pullback (P := P) f g) (fst (P := P) f g ≫ f) :
            (a : (↑(pullback f g).toTop : Type u)) → (↑B.toTop : Type u))
          (Subtype.mk (p := fun (x : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)) ↦
            Membership.mem (γ := Set ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
              {xy : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u) |
                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)) f :
                        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                      xy.1 :
                    (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)) g :
                        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                      xy.2 :
                    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)}
              x)
            val h) :
        (↑(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 := pullback (P := P) f g) (snd (P := P) f g ≫ g) :
            (a : (↑(pullback f g).toTop : Type u)) → (↑B.toTop : Type u))
          (Subtype.mk (p := fun (x : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)) ↦
            Membership.mem (γ := Set ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
              {xy : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u) |
                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)) f :
                        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                      xy.1 :
                    (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)) g :
                        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
                      xy.2 :
                    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)}
              x)
            val h) :
        (↑(B.toTop (P := P)) : Type u))
⊢ Eq (α := pullback (P := P) f g ⟶ B) (fst (P := P) f g ≫ f) (snd (P := P) f g ≫ g)

Tactic:
ext ⟨_, h⟩