-- 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
S : PullbackCone f g
property :
  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)) }) } ≫
      (pullbackCone f g).fst =
    S.fst
property₁ :
  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)) }) } ≫
      (pullbackCone f g).snd =
    S.snd
⊢ 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)) }) } ≫
        (pullbackCone f g).fst =
      S.fst ∧
    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)) }) } ≫
          (pullbackCone f g).snd =
        S.snd ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ (pullbackCone f g).fst = S.fst →
          m ≫ (pullbackCone f g).snd = S.snd →
            m =
              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 := ⋯ }
have property₂ : ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
  m ≫ (pullbackCone f g).fst = S.fst →
    m ≫ (pullbackCone f g).snd = S.snd →
      m =
        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)
                sorry,
            continuous_toFun := sorry }
Tactic: refine ⟨?_, ?_, ?_⟩