-- 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
x :
  (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
x₁ :
  (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)
⊢ Functor.obj
    (homDiagram (F := F)
      ((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)
      ((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))
    j

Tactic:
refine eqToHom ?_ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ?_

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.eqToHom, CategoryTheory.Functor.map, CategoryTheory.Cat.Hom.toFunctor, CategoryTheory.NatTrans.app