-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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 :
  Membership.mem (α := (↑(pullback f g) : Type u)) (γ := Set (↑(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.fst f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
      U)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (pullbackIsoProdSubtype f g).inv :
          (a :
              (↑(of
                    { 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 }) :
                Type u)) →
            (↑(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))
⊢ 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
have h₁ : (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)
            (pullbackIsoProdSubtype f g).inv :
          (a :
              (↑(of
                    { 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 }) :
                Type u)) →
            (↑(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
Tactic: refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩