-- 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₁ :
  Eq (α := (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
            ((pullbackIsoProdSubtype f g).inv ≫
              (BinaryFan.mk (P := pullback f g) (pullback.fst f g) (pullback.snd f g)).π.app
                { as := WalkingPair.left }) :
          (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)) →
            (↑((pair X Y).obj { as := WalkingPair.left }) : 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)) }) :
      (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (pair X Y)) (Y := Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
            (limit.π (pair X Y) { as := WalkingPair.left }) :
          (a : (↑(limit (pair X Y)) : Type u)) → (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (pair X Y)) (Y := Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
            (limit.π (pair X Y) { as := WalkingPair.left }) :
          (a : (↑(limit (pair X Y)) : Type u)) → (↑((pair X Y).obj { as := WalkingPair.left }) : 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) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (pair X Y)) (Y := Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
            (limit.π (pair X Y) { as := WalkingPair.left }) :
          (a : (↑(limit (pair X Y)) : Type u)) → (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Limits.limit.lift_π