-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this :
  Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
      (Function.comp (β :=
        { p : X × Y //
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z) })
        (Subtype.val (p := fun (p : X × Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z)))
        (⇑(hom (FC := TypeCat.Fun) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) X))
    (Set.image (α := X × Y) _root_.Prod.fst
      (Set.image (α :=
        { p : X × Y //
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z) })
        (Subtype.val (p := fun (p : X × Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z)))
        Set.univ))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))
have h₁ : ∀ (x : (fun (X : Type u) ↦ X) X),
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.image (α := X × Y) _root_.Prod.fst
        (Set.image (α :=
          { p : X × Y //
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                (fun (X : Type u) ↦ X) Z) })
          (Subtype.val (p := fun (p : X × Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                (fun (X : Type u) ↦ X) Z)))
          Set.univ))
      x ↔
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
        (Set.range (ι := (fun (X : Type u) ↦ X) Y)
          (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))
      x
Tactic: ext