-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X_1 Y : limit (F ⋙ objects)
X : J
h :
  ∀
    (f :
      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_1 :
          (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))),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (↾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_1 :
                    (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 (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯))
        f =
      (hom (FC := TypeCat.Fun)
            (𝟙
              (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_1 :
                  (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))))).toFun
        f
⊢ (↾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_1 :
              (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 (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯) =
    𝟙
      (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_1 :
          (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)))

Tactic:
ext f