-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
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)
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))
                    ⋯))
                ((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))
            ⋯) :
        (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))
                    ⋯)))
            ⋯) :
        (fun (X : Type v) ↦ X) ((homDiagram W Z).obj j))
⊢ 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))
              ⋯)))
      ⋯)

Tactic:
apply Types.limit_ext.{v, v}