-- 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)
⊢ ∀ (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))

Tactic:
simp [-homDiagram_obj]

Premises used: CategoryTheory.Cat.HasLimits.homDiagram_obj