-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (↑(X ⨯ Y) : Type u)
h :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        (((Hom.hom' prod.fst : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u)) x,
              (Hom.hom' prod.snd : (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u)) x).1 :
          (↑X : Type u)) :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (((Hom.hom' prod.fst : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u)) x,
              (Hom.hom' prod.snd : (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u)) x).2 :
          (↑Y : Type u)) :
      (↑Z : Type u))
h₁ :
  ∀ (j : Discrete WalkingPair),
    Eq (α := (↑(Functor.obj (pair X Y) j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              limit (pair X Y)) (limit.π (pair X Y) j) :
            (a : (↑(limit (pair X Y)) : Type u)) → (↑((pair X Y).obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (pullbackIsoProdSubtype f g).inv :
                    (a :
                        (↑(of
                              { p : (↑X : Type u) × (↑Y : Type u) //
                                (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                                  (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
                          Type u)) →
                      (↑(pullback f g) : Type u))
                  (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
                      Eq (α := (↑Z : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) f :
                              (a : (↑X : Type u)) → (↑Z : Type u))
                            p.1 :
                          (↑Z : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) g :
                              (a : (↑Y : Type u)) → (↑Z : Type u))
                            p.2 :
                          (↑Z : Type u)))
                      ((Hom.hom' prod.fst : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u)) x,
                        (Hom.hom' prod.snd : (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u)) x)
                      h :
                    { p : (↑X : Type u) × (↑Y : Type u) //
                      Eq (α := (↑Z : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) f :
                              (a : (↑X : Type u)) → (↑Z : Type u))
                            p.1 :
                          (↑Z : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) g :
                              (a : (↑Y : Type u)) → (↑Z : Type u))
                            p.2 :
                          (↑Z : Type u)) }) :
                (↑(pullback f g) : Type u)) :
            (↑(X ⨯ Y) : Type u)) :
        (↑(Functor.obj (pair X Y) j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              limit (pair X Y)) (limit.π (pair X Y) j) :
            (a : (↑(limit (pair X Y)) : Type u)) → (↑((pair X Y).obj j) : Type u))
          x :
        (↑(Functor.obj (pair X Y) j) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                (↑(of
                      { p : (↑X : Type u) × (↑Y : Type u) //
                        (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                          (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
                  Type u)) →
              (↑(pullback f g) : Type u))
          (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
              Eq (α := (↑Z : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        f :
                      (a : (↑X : Type u)) → (↑Z : Type u))
                    p.1 :
                  (↑Z : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        g :
                      (a : (↑Y : Type u)) → (↑Z : Type u))
                    p.2 :
                  (↑Z : Type u)))
              ((Hom.hom' prod.fst : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u)) x,
                (Hom.hom' prod.snd : (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u)) x)
              h :
            { p : (↑X : Type u) × (↑Y : Type u) //
              Eq (α := (↑Z : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        f :
                      (a : (↑X : Type u)) → (↑Z : Type u))
                    p.1 :
                  (↑Z : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        g :
                      (a : (↑Y : Type u)) → (↑Z : Type u))
                    p.2 :
                  (↑Z : Type u)) }) :
        (↑(pullback f g) : Type u)) =
    x

Tactic:
apply Concrete.limit_ext

Premises used: CategoryTheory.Limits.Concrete.limit_ext