-- 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
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : (↑S.pt : Type u)
property :
  Eq.{u + 1} (α := (↑X : Type u))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).1
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (ofHom
                  {
                    toFun := fun (x : (↑S.1 : 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)))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.fst :
                              (a : (↑S.pt : Type u)) → (↑X : Type u))
                            x,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.snd :
                              (a : (↑S.pt : Type u)) → (↑Y : Type u))
                            x)
                        ⋯,
                    continuous_toFun := ⋯ :
                    C((↑S.1 : Type u),
                      { 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)) }) }) :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).1
property₁ :
  Eq.{u + 1} (α := (↑Y : Type u))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).2
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (ofHom
                  {
                    toFun := fun (x : (↑S.1 : 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)))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.fst :
                              (a : (↑S.pt : Type u)) → (↑X : Type u))
                            x,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.snd :
                              (a : (↑S.pt : Type u)) → (↑Y : Type u))
                            x)
                        ⋯,
                    continuous_toFun := ⋯ :
                    C((↑S.1 : Type u),
                      { 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)) }) }) :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).2
⊢ Eq.{u + 1} (α := (↑X : Type u) × (↑Y : Type u))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
            (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
          x) :
      (↑X : Type u) × (↑Y : Type u))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (ofHom
                {
                  toFun := fun (x : (↑S.1 : 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)))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) S.fst :
                            (a : (↑S.pt : Type u)) → (↑X : Type u))
                          x,
                        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) S.snd :
                            (a : (↑S.pt : Type u)) → (↑Y : Type u))
                          x)
                      ⋯,
                  continuous_toFun := ⋯ :
                  C((↑S.1 : Type u),
                    { 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)) }) }) :
            (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
          x) :
      (↑X : Type u) × (↑Y : Type u))

Tactic:
apply Prod.ext

Premises used: Prod.ext