-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
W X Y Z : limit (F ⋙ objects)
x : limit (homDiagram W X)
x_1 : limit (homDiagram X Y)
x_2 : limit (homDiagram Y Z)
⊢ Eq (α := limit (homDiagram W Z))
    (Types.Limit.mk (homDiagram W Z)
      (fun (j : J) ↦
        CategoryStruct.comp (Y :=
          (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
              (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
            Y)
          ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W Y) j) :
              (a : (fun (X : Type v) ↦ X) (limit (homDiagram W Y))) → (fun (X : Type v) ↦ X) ((homDiagram W Y).obj j))
            (Types.Limit.mk (homDiagram W Y)
              (fun (j : J) ↦
                CategoryStruct.comp (Y :=
                  (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
                      (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
                    X)
                  ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W X) j) :
                      (a : (fun (X : Type v) ↦ X) (limit (homDiagram W X))) →
                        (fun (X : Type v) ↦ X) ((homDiagram W X).obj j))
                    x)
                  ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X Y) j) :
                      (a : (fun (X : Type v) ↦ X) (limit (homDiagram X Y))) →
                        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
                    x_1))
              ⋯))
          ((hom (FC := TypeCat.Fun) (limit.π (homDiagram Y Z) j) :
              (a : (fun (X : Type v) ↦ X) (limit (homDiagram Y Z))) → (fun (X : Type v) ↦ X) ((homDiagram Y Z).obj j))
            x_2))
      ⋯)
    (Types.Limit.mk (homDiagram W Z)
      (fun (j : J) ↦
        CategoryStruct.comp (Y :=
          (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
              (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
            X)
          ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W X) j) :
              (a : (fun (X : Type v) ↦ X) (limit (homDiagram W X))) → (fun (X : Type v) ↦ X) ((homDiagram W X).obj j))
            x)
          ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X Z) j) :
              (a : (fun (X : Type v) ↦ X) (limit (homDiagram X Z))) → (fun (X : Type v) ↦ X) ((homDiagram X Z).obj j))
            (Types.Limit.mk (homDiagram X Z)
              (fun (j : J) ↦
                CategoryStruct.comp (Y :=
                  (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
                      (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
                    Y)
                  ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X Y) j) :
                      (a : (fun (X : Type v) ↦ X) (limit (homDiagram X Y))) →
                        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
                    x_1)
                  ((hom (FC := TypeCat.Fun) (limit.π (homDiagram Y Z) j) :
                      (a : (fun (X : Type v) ↦ X) (limit (homDiagram Y Z))) →
                        (fun (X : Type v) ↦ X) ((homDiagram Y Z).obj j))
                    x_2))
              ⋯)))
      ⋯)
have w : ∀ (j : J),
  Eq (α := (fun (X : Type v) ↦ X) ((homDiagram W Z).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W Z) j) :
          (a : (fun (X : Type v) ↦ X) (limit (homDiagram W Z))) → (fun (X : Type v) ↦ X) ((homDiagram W Z).obj j))
        (Types.Limit.mk (homDiagram W Z)
          (fun (j : J) ↦
            CategoryStruct.comp (Y :=
              (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
                  (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
                Y)
              ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W Y) j) :
                  (a : (fun (X : Type v) ↦ X) (limit (homDiagram W Y))) →
                    (fun (X : Type v) ↦ X) ((homDiagram W Y).obj j))
                (Types.Limit.mk (homDiagram W Y)
                  (fun (j : J) ↦
                    CategoryStruct.comp (Y :=
                      (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
                          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) →
                            (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
                        X)
                      ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W X) j) :
                          (a : (fun (X : Type v) ↦ X) (limit (homDiagram W X))) →
                            (fun (X : Type v) ↦ X) ((homDiagram W X).obj j))
                        x)
                      ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X Y) j) :
                          (a : (fun (X : Type v) ↦ X) (limit (homDiagram X Y))) →
                            (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
                        x_1))
                  sorry))
              ((hom (FC := TypeCat.Fun) (limit.π (homDiagram Y Z) j) :
                  (a : (fun (X : Type v) ↦ X) (limit (homDiagram Y Z))) →
                    (fun (X : Type v) ↦ X) ((homDiagram Y Z).obj j))
                x_2))
          sorry) :
      (fun (X : Type v) ↦ X) ((homDiagram W Z).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W Z) j) :
          (a : (fun (X : Type v) ↦ X) (limit (homDiagram W Z))) → (fun (X : Type v) ↦ X) ((homDiagram W Z).obj j))
        (Types.Limit.mk (homDiagram W Z)
          (fun (j : J) ↦
            CategoryStruct.comp (Y :=
              (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
                  (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
                X)
              ((hom (FC := TypeCat.Fun) (limit.π (homDiagram W X) j) :
                  (a : (fun (X : Type v) ↦ X) (limit (homDiagram W X))) →
                    (fun (X : Type v) ↦ X) ((homDiagram W X).obj j))
                x)
              ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X Z) j) :
                  (a : (fun (X : Type v) ↦ X) (limit (homDiagram X Z))) →
                    (fun (X : Type v) ↦ X) ((homDiagram X Z).obj j))
                (Types.Limit.mk (homDiagram X Z)
                  (fun (j : J) ↦
                    CategoryStruct.comp (Y :=
                      (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
                          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) →
                            (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
                        Y)
                      ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X Y) j) :
                          (a : (fun (X : Type v) ↦ X) (limit (homDiagram X Y))) →
                            (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
                        x_1)
                      ((hom (FC := TypeCat.Fun) (limit.π (homDiagram Y Z) j) :
                          (a : (fun (X : Type v) ↦ X) (limit (homDiagram Y Z))) →
                            (fun (X : Type v) ↦ X) ((homDiagram Y Z).obj j))
                        x_2))
                  sorry)))
          sorry) :
      (fun (X : Type v) ↦ X) ((homDiagram W Z).obj j))
Tactic: apply Types.limit_ext.{v, v}