-- Lean 4 proof step from Mathlib.Topology.Category.CompHausLike.Limits (goal)
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 b : Z ⟶ pullback (P := P) f g
z : (↑(Z.toTop (P := P)) : Type u)
hfst :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    ((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 ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
    ((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 ≫ fst (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X)
hsnd :
  Eq (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((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 ≫ snd (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
    ((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 ≫ snd (P := P) f g) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Z) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
        z :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
⊢ Eq (α := (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
    ((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 : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z :
      (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
    ((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 : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z :
      (↑((pullback (P := P) f g).toTop (P := P)) : Type u))
have h : Eq.{u + 1} (α := (↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))
  (↑((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 : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z) :
    (↑X.toTop : Type u) × (↑Y.toTop : Type u))
  (↑((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 : (↑Z.toTop : Type u)) → (↑(pullback f g).toTop : Type u))
        z) :
    (↑X.toTop : Type u) × (↑Y.toTop : Type u))
Tactic: apply Subtype.ext