-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : (↑s.pt : Type v)
f : X ⟶ Y
⊢ (hom (FC := TypeCat.Fun)
          (limit.π
            (homDiagram (F := F)
              ((@hom _ types 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 : (↑s.pt : Type v)) → limit (F ⋙ objects))
                X)
              ((@hom _ types 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 : (↑s.pt : Type v)) → limit (F ⋙ objects))
                Y))
            j) :
        (a :
            limit
              (homDiagram
                ((hom
                      (limit.lift (F ⋙ objects)
                        { pt := (↑s.pt : Type v),
                          π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                    (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
                  X)
                ((hom
                      (limit.lift (F ⋙ objects)
                        { pt := (↑s.pt : Type v),
                          π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                    (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
                  Y))) →
          (hom (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → objects.obj (F.obj j))
              ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := (↑s.pt : Type v),
                        π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                  (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
                X) ⟶
            (hom (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → objects.obj (F.obj j))
              ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := (↑s.pt : Type v),
                        π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                  (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
                Y))
      (Types.Limit.mk
        (homDiagram (F := F)
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                (limit.lift (F ⋙ objects)
                  { pt := (↑s.pt : Type v),
                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
              (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
            X)
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                (limit.lift (F ⋙ objects)
                  { pt := (↑s.pt : Type v),
                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
              (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
            Y))
        (fun (j : J) ↦ eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) ⋯) =
    eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯

Tactic:
Types.Limit.π_mk.{v, v} _ _ _ _

Premises used: CategoryTheory.Limits.Types.Limit.π_mk