-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
w :
  ∀ (x : (↑X : Type u) × (↑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))
            x.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))
            x.2 :
          (↑Z : Type u))),
    Eq (α := (↑Z : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (ofHom
                  {
                    toFun :=
                      fun
                        (x :
                          { 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)) }) ↦
                      (↑x : (↑X : Type u) × (↑Y : Type u)).1,
                    continuous_toFun := ⋯ :
                    C({ 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)) },
                      (↑X : Type u)) } ≫
                f) :
            (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)) →
              (↑Z : 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)))
            x h) :
        (↑Z : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (ofHom
                  {
                    toFun :=
                      fun
                        (x :
                          { 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)) }) ↦
                      (↑x : (↑X : Type u) × (↑Y : Type u)).2,
                    continuous_toFun := ⋯ :
                    C({ 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)) },
                      (↑Y : Type u)) } ≫
                g) :
            (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)) →
              (↑Z : 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)))
            x h) :
        (↑Z : Type u))
⊢ ofHom
        {
          toFun :=
            fun
              (x :
                { 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)) }) ↦
            (↑x : (↑X : Type u) × (↑Y : Type u)).1,
          continuous_toFun := ⋯ :
          C({ 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)) },
            (↑X : Type u)) } ≫
      f =
    ofHom
        {
          toFun :=
            fun
              (x :
                { 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)) }) ↦
            (↑x : (↑X : Type u) × (↑Y : Type u)).2,
          continuous_toFun := ⋯ :
          C({ 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)) },
            (↑Y : Type u)) } ≫
      g

Tactic:
ext ⟨x, h⟩