-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x : (↑(pullback g₁ g₂) : Type u)
x₁ : (↑W : Type u)
hx₁ :
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (pullback.fst g₁ g₂) :
          (a : (↑(pullback g₁ g₂) : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
x₂ : (↑X : Type u)
hx₂ :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (pullback.snd g₁ g₂) :
          (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
this :
  Eq (α := (↑S : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
          (a : (↑W : Type u)) → (↑S : Type u))
        x₁ :
      (↑S : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₂ :
          (a : (↑X : Type u)) → (↑S : Type u))
        x₂ :
      (↑S : Type u))
h :
  ∀ (j : WalkingCospan),
    Eq (α := (↑((cospan g₁ g₂).obj j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              limit (cospan g₁ g₂)) (limit.π (cospan g₁ g₂) j) :
            (a : (↑(limit (cospan g₁ g₂)) : Type u)) → (↑((cospan g₁ g₂).obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :
                (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (pullbackIsoProdSubtype f₁ f₂).inv :
                    (a :
                        (↑(of
                              { p : (↑W : Type u) × (↑X : Type u) //
                                (ConcreteCategory.hom f₁ : (a : (↑W : Type u)) → (↑S : Type u)) p.1 =
                                  (ConcreteCategory.hom f₂ : (a : (↑X : Type u)) → (↑S : Type u)) p.2 }) :
                          Type u)) →
                      (↑(pullback f₁ f₂) : Type u))
                  (Subtype.mk (p := fun (p : (↑W : Type u) × (↑X : Type u)) ↦
                    Eq (α := (↑S : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) f₁ :
                            (a : (↑W : Type u)) → (↑S : Type u))
                          p.1 :
                        (↑S : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) f₂ :
                            (a : (↑X : Type u)) → (↑S : Type u))
                          p.2 :
                        (↑S : Type u)))
                    (x₁, x₂) this) :
                (↑(pullback f₁ f₂) : Type u)) :
            (↑(pullback g₁ g₂) : Type u)) :
        (↑((cospan g₁ g₂).obj j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              limit (cospan g₁ g₂)) (limit.π (cospan g₁ g₂) j) :
            (a : (↑(limit (cospan g₁ g₂)) : Type u)) → (↑((cospan g₁ g₂).obj j) : Type u))
          x :
        (↑((cospan g₁ g₂).obj j) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f₁ f₂).inv :
            (a :
                (↑(of
                      { p : (↑W : Type u) × (↑X : Type u) //
                        (ConcreteCategory.hom f₁ : (a : (↑W : Type u)) → (↑S : Type u)) p.1 =
                          (ConcreteCategory.hom f₂ : (a : (↑X : Type u)) → (↑S : Type u)) p.2 }) :
                  Type u)) →
              (↑(pullback f₁ f₂) : Type u))
          (Subtype.mk (p := fun (p : (↑W : Type u) × (↑X : Type u)) ↦
            Eq (α := (↑S : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f₁ :
                    (a : (↑W : Type u)) → (↑S : Type u))
                  p.1 :
                (↑S : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f₂ :
                    (a : (↑X : Type u)) → (↑S : Type u))
                  p.2 :
                (↑S : Type u)))
            (x₁, x₂) this) :
        (↑(pullback f₁ f₂) : Type u)) =
    x

Tactic:
apply Concrete.limit_ext

Premises used: CategoryTheory.Limits.Concrete.limit_ext