-- 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 :
  ∀
    (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))),
    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)
⊢ Eq.{v + 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)) ⟶
      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)))
    (↾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 ⋯)
    (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 ⋯))

Tactic:
ext h