-- 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)
h :
  Membership.mem (γ := Set (↑Y : Type u))
      (Set.image (α := (↑(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) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type 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)) ⁻¹'
          U))
      x →
    Membership.mem (γ := Set (↑Y : Type u))
      (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          U))
      x
h₁ :
  Membership.mem (γ := Set (↑Y : Type u))
      (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          U))
      x →
    Membership.mem (γ := Set (↑Y : Type u))
      (Set.image (α := (↑(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) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type 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)) ⁻¹'
          U))
      x
⊢ Membership.mem (γ := Set (↑Y : Type u))
      (Set.image (α := (↑(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) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type 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)) ⁻¹'
          U))
      x ↔
    Membership.mem (γ := Set (↑Y : Type u))
      (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          U))
      x

Tactic:
constructor