-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y Z : limit (F ⋙ objects)
f : limit (homDiagram X Y)
g : limit (homDiagram Y Z)
j j' : J
h : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X Z).obj j'))
    ((hom (FC := TypeCat.Fun) ((homDiagram X Z).map h) :
        (a : (fun (X : Type v) ↦ X) ((homDiagram X Z).obj j)) → (fun (X : Type v) ↦ X) ((homDiagram X Z).obj j'))
      ((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))
                f)
              ((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))
                g) :
            Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
              ((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 :
                (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
              ((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))
                  Z :
                (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))))
        j))
    ((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))
              f)
            ((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))
              g) :
          Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
            ((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 :
              (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
            ((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))
                Z :
              (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))))
      j')

Tactic:
simp [-homDiagram_obj, ← limit.w_apply (homDiagram X Y) h f,
      ← limit.w_apply (homDiagram Y Z) h g]

Premises used: CategoryTheory.Cat.HasLimits.homDiagram, CategoryTheory.Cat.HasLimits.homDiagram_obj, CategoryTheory.Limits.limit.w_apply