-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x x_1 Z : J
f : x ⟶ x_1
g : x_1 ⟶ Z
h :
  Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
        X :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
        Y :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
this : Category.{v, v} (objects.obj (F.obj Z)) := inferInstance
⊢ Eq (α :=
    Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Z))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Z) :
            (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Z))
          X :
        (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Z))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Z) :
            (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Z))
          Y :
        (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Z)))
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾fun
            (g_1 :
              Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x) :
                      (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                    X :
                  (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x) :
                      (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                    Y :
                  (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))) ↦
          eqToHom ⋯ ≫ (F.map (f ≫ g)).toFunctor.map g_1 ≫ eqToHom ⋯))
      h)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
            ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x_1) :
                  (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
                X :
              (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
            ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x_1) :
                  (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
                Y :
              (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1)))
          (↾fun
              (g :
                Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                  ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x) :
                        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) →
                          (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                      X :
                    (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                  ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x) :
                        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) →
                          (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))
                      Y :
                    (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))) ↦
            eqToHom ⋯ ≫ (F.map f).toFunctor.map g ≫ eqToHom ⋯)
          (↾fun
              (g_1 :
                Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
                  ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x_1) :
                        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) →
                          (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
                      X :
                    (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
                  ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) x_1) :
                        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) →
                          (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))
                      Y :
                    (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x_1))) ↦
            eqToHom ⋯ ≫ (F.map g).toFunctor.map g_1 ≫ eqToHom ⋯)))
      h)

Tactic:
simp [Functor.congr_hom congr($(F.map_comp f g).toFunctor) h, eqToHom_map]

Premises used: congrArg, CategoryTheory.eqToHom_map, CategoryTheory.Functor.congr_hom, id, CategoryTheory.Functor.map_comp, CategoryTheory.Cat.Hom.toFunctor