-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
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
⊢ 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
have 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
Tactic: constructor