-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  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))
        y :
      (↑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 :
      (↑Z : Type u))
h :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.fst f g) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                { 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 }) →
              (↑(pullback f g) : 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)))
            (y, x) eq) :
        (↑(pullback f g) : Type u)) =
    y
⊢ Membership.mem (α := (↑X : Type u)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.fst f g) :
          (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (pullbackIsoProdSubtype f g).inv :
              (a :
                  { 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 }) →
                (↑(pullback f g) : 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)))
              (y, x) eq) :
          (↑(pullback f g) : Type u)) :
      (↑X : Type u))

Tactic:
convert! hy