-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ 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
have 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 := sorry :
                  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 := sorry :
                  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))
Tactic: ext ⟨x, h⟩