-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (↑(X ⨯ Y) : Type u)
h :
  Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      (Set.range (ι := (↑(pullback f g) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
          (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
      x →
    Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      {x : (↑(X ⨯ Y) : Type u) |
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  X ⨯ Y) (prod.fst ≫ f) :
                (a : (↑(X ⨯ Y) : 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 :=
                  X ⨯ Y) (prod.snd ≫ g) :
                (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
              x :
            (↑Z : Type u))}
      x
h₁ :
  Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      {x : (↑(X ⨯ Y) : Type u) |
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  X ⨯ Y) (prod.fst ≫ f) :
                (a : (↑(X ⨯ Y) : 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 :=
                  X ⨯ Y) (prod.snd ≫ g) :
                (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
              x :
            (↑Z : Type u))}
      x →
    Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      (Set.range (ι := (↑(pullback f g) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
          (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
      x
⊢ Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      (Set.range (ι := (↑(pullback f g) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
          (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
      x ↔
    Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
      {x : (↑(X ⨯ Y) : Type u) |
        Eq (α := (↑Z : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  X ⨯ Y) (prod.fst ≫ f) :
                (a : (↑(X ⨯ Y) : 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 :=
                  X ⨯ Y) (prod.snd ≫ g) :
                (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
              x :
            (↑Z : Type u))}
      x

Tactic:
constructor