awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X_1 Y_1 : J
f : X_1 ⟶ Y_1
g :
  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))
⊢ (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
      X =
    (F.map f).toFunctor.obj
      ((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)

Tactic:
(congr_hom (limit.w (F ⋙ Cat.objects) f) X).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.Limits.limit.w, CategoryTheory.Cat.objects
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X_1 Y_1 : J
f : X_1 ⟶ Y_1
g :
  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))
⊢ (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
      X =
    (F.map f).toFunctor.obj
      ((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)

Tactic:
exact (congr_hom (limit.w (F ⋙ Cat.objects) f) X).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.Limits.limit.w, CategoryTheory.Cat.objects
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X_1 Y_1 : J
f : X_1 ⟶ Y_1
g :
  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))
⊢ (F.map f).toFunctor.obj
      ((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) =
    (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
      Y

Tactic:
congr_hom (limit.w (F ⋙ Cat.objects) f) Y

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.limit.w, CategoryTheory.Cat.objects
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X_1 Y_1 : J
f : X_1 ⟶ Y_1
g :
  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))
⊢ (F.map f).toFunctor.obj
      ((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) =
    (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
      Y

Tactic:
exact congr_hom (limit.w (F ⋙ Cat.objects) f) Y

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.limit.w, CategoryTheory.Cat.objects
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X_1 Y : limit (F ⋙ objects)
X : J
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))
this : Category.{v, v} (objects.obj (F.obj X)) := inferInstance
⊢ 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

Tactic:
simp [Functor.congr_hom congr($(F.map_id X).toFunctor) f]

Premises used: congrArg, CategoryTheory.Functor.congr_hom, id, CategoryTheory.Functor.map_id, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X X).obj j'))
    ((hom (FC := TypeCat.Fun) ((homDiagram X X).map f) :
        (a : (fun (X : Type v) ↦ X) ((homDiagram X X).obj j)) → (fun (X : Type v) ↦ X) ((homDiagram X X).obj j'))
      ((fun (x : J) ↦
          (𝟙
              ((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) :
            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))
                  X :
                (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))))
        j))
    ((fun (x : J) ↦
        (𝟙
            ((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) :
          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))
                X :
              (fun (X : Type v) ↦ X) ((F ⋙ objects).obj x))))
      j')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x : limit (homDiagram X Y)
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
      ((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))
          (Types.Limit.mk (homDiagram X 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 X X) j) :
                    (a : (fun (X : Type v) ↦ X) (limit (homDiagram X X))) →
                      (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
                  (Types.Limit.mk (homDiagram X X)
                    (fun (x : J) ↦
                      𝟙
                        ((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))
                    ⋯))
                ((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))
            ⋯) :
        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
      ((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 :
        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
⊢ Types.Limit.mk (homDiagram X 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 X X) j) :
              (a : (fun (X : Type v) ↦ X) (limit (homDiagram X X))) → (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
            (Types.Limit.mk (homDiagram X X)
              (fun (x : J) ↦
                𝟙
                  ((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))
              ⋯))
          ((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))
      ⋯ =
    x

Tactic:
apply Types.limit_ext.{v, v}
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x : limit (homDiagram X Y)
⊢ ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
      ((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))
          (Types.Limit.mk (homDiagram X 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 X X) j) :
                    (a : (fun (X : Type v) ↦ X) (limit (homDiagram X X))) →
                      (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
                  (Types.Limit.mk (homDiagram X X)
                    (fun (x : J) ↦
                      𝟙
                        ((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))
                    ⋯))
                ((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))
            ⋯) :
        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
      ((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 :
        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))

Tactic:
simp [-homDiagram_obj]

Premises used: CategoryTheory.Cat.HasLimits.homDiagram_obj
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x : limit (homDiagram X Y)
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
      ((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))
          (Types.Limit.mk (homDiagram X 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))
                  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)
                ((hom (FC := TypeCat.Fun) (limit.π (homDiagram Y Y) j) :
                    (a : (fun (X : Type v) ↦ X) (limit (homDiagram Y Y))) →
                      (fun (X : Type v) ↦ X) ((homDiagram Y Y).obj j))
                  (Types.Limit.mk (homDiagram Y Y)
                    (fun (x : J) ↦
                      𝟙
                        ((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) ((homDiagram X Y).obj j))
      ((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 :
        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
⊢ Types.Limit.mk (homDiagram X 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))
            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)
          ((hom (FC := TypeCat.Fun) (limit.π (homDiagram Y Y) j) :
              (a : (fun (X : Type v) ↦ X) (limit (homDiagram Y Y))) → (fun (X : Type v) ↦ X) ((homDiagram Y Y).obj j))
            (Types.Limit.mk (homDiagram Y Y)
              (fun (x : J) ↦
                𝟙
                  ((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))
              ⋯)))
      ⋯ =
    x

Tactic:
apply Types.limit_ext.{v, v}
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x : limit (homDiagram X Y)
⊢ ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
      ((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))
          (Types.Limit.mk (homDiagram X 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))
                  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)
                ((hom (FC := TypeCat.Fun) (limit.π (homDiagram Y Y) j) :
                    (a : (fun (X : Type v) ↦ X) (limit (homDiagram Y Y))) →
                      (fun (X : Type v) ↦ X) ((homDiagram Y Y).obj j))
                  (Types.Limit.mk (homDiagram Y Y)
                    (fun (x : J) ↦
                      𝟙
                        ((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) ((homDiagram X Y).obj j))
      ((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 :
        (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))

Tactic:
simp [-homDiagram_obj]

Premises used: CategoryTheory.Cat.HasLimits.homDiagram_obj
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j : 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))
      ((hom (FC := TypeCat.Fun)
            (limit.lift (F ⋙ objects)
              { pt := (↑s.pt : Type v),
                π :=
                  { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                    NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                Cone (F ⋙ objects) }) :
          (a :
              (fun (X : Type v) ↦ X)
                { pt := (↑s.pt : Type v),
                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
            (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
        X) =
    (s.π.app j).toFunctor.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j : J
⊢ (s.π.app j).toFunctor.obj 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))
      ((hom (FC := TypeCat.Fun)
            (limit.lift (F ⋙ objects)
              { pt := (↑s.pt : Type v),
                π :=
                  { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                    NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                Cone (F ⋙ objects) }) :
          (a :
              (fun (X : Type v) ↦ X)
                { pt := (↑s.pt : Type v),
                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
            (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
        Y)

Tactic:
simp