-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (hypothesis)
Goal:
P : TopCat.{u} → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst : HasExplicitPullback (P := P) f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
z : (↑(Z.toTop (P := P)) : Type u)
⊢ Membership.mem (α := (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)) (γ :=
    Set ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
    {xy : (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u) |
      Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) f :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
            xy.1 :
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
                (↑(X.toTop (P := P)) : Type u)) g :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
            xy.2 :
          (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)}
    (((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) a :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
          z,
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) b :
            (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) →
              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
          z) :
      (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))
have w₁ : Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) (a ≫ f) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
      z :
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
          C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
          (↑(X.toTop (P := P)) : Type u)) (b ≫ g) :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) B)
      z :
    (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) B)
Tactic: apply_fun (fun q ↦ q z) at w
Cleared hypotheses: w