-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ :
      (fun (X : Type u) ↦ X) X₂)
    ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) y₁ :
      (fun (X : Type u) ↦ X) X₂)
h₂ :
  Eq (α := (fun (X : Type u) ↦ X) X₃)
    ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ :
      (fun (X : Type u) ↦ X) X₃)
    ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) y₁ :
      (fun (X : Type u) ↦ X) X₃)
a :
  Eq.{u + 1} (α := X₂)
    (↑(((h.isLimit.conePointUniqueUpToIso
                  ((pullbackCone r b).isLimitAux
                    (fun (s : PullbackCone r b) ↦
                      ↾fun (x : s.pt) ↦
                        Subtype.mk (p := fun (p : X₂ × X₃) ↦
                          Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                            ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                          ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                            (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                          ⋯)
                    ⋯ ⋯ ⋯)).toEquiv :
              (a : h.cone.pt) → PullbackObj r b)
            x₁) :
        X₂ × X₃).1
    (↑(((h.isLimit.conePointUniqueUpToIso
                  ((pullbackCone r b).isLimitAux
                    (fun (s : PullbackCone r b) ↦
                      ↾fun (x : s.pt) ↦
                        Subtype.mk (p := fun (p : X₂ × X₃) ↦
                          Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                            ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                          ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                            (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                          ⋯)
                    ⋯ ⋯ ⋯)).toEquiv :
              (a : h.cone.pt) → PullbackObj r b)
            y₁) :
        X₂ × X₃).1
⊢ Eq (α := PullbackObj r b)
    (((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux
                (fun (s : PullbackCone r b) ↦
                  ↾fun (x : s.pt) ↦
                    Subtype.mk (p := fun (p : X₂ × X₃) ↦
                      Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                        ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                      ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                        (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                      ⋯)
                ⋯ ⋯ ⋯)).toEquiv :
          (a : h.cone.pt) → PullbackObj r b)
        x₁ :
      PullbackObj r b)
    (((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux
                (fun (s : PullbackCone r b) ↦
                  ↾fun (x : s.pt) ↦
                    Subtype.mk (p := fun (p : X₂ × X₃) ↦
                      Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                        ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                      ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                        (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                      ⋯)
                ⋯ ⋯ ⋯)).toEquiv :
          (a : h.cone.pt) → PullbackObj r b)
        y₁ :
      PullbackObj r b)
have a₁ : Eq.{u + 1} (α := X₃)
  (↑(((h.isLimit.conePointUniqueUpToIso
                ((pullbackCone r b).isLimitAux
                  (fun (s : PullbackCone r b) ↦
                    ↾fun (x : s.pt) ↦
                      Subtype.mk (p := fun (p : X₂ × X₃) ↦
                        Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                          ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                        ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                          (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                        sorry)
                  sorry sorry sorry)).toEquiv :
            (a : h.cone.pt) → PullbackObj r b)
          x₁) :
      X₂ × X₃).2
  (↑(((h.isLimit.conePointUniqueUpToIso
                ((pullbackCone r b).isLimitAux
                  (fun (s : PullbackCone r b) ↦
                    ↾fun (x : s.pt) ↦
                      Subtype.mk (p := fun (p : X₂ × X₃) ↦
                        Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                          ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                        ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                          (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                        sorry)
                  sorry sorry sorry)).toEquiv :
            (a : h.cone.pt) → PullbackObj r b)
          y₁) :
      X₂ × X₃).2
Tactic: ext