-- 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
x :
  (j : J) →
    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
h :
  ∀ (j j' : J) (f_1 : j ⟶ j'),
    Eq (α :=
      (fun (X : Type v) ↦ X)
        (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'))
      ((hom (FC := TypeCat.Fun)
              (Functor.map
                (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))
                f_1) :
            (a :
                (fun (X : Type v) ↦ X)
                  ((homDiagram
                        ((hom
                              (limit.lift (F ⋙ objects)
                                { pt := (↑s.pt : Type v),
                                  π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                            (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
                              (limit.lift (F ⋙ objects)
                                { pt := (↑s.pt : Type v),
                                  π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                            (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)).obj
                    j)) →
              (fun (X : Type v) ↦ X)
                ((homDiagram
                      ((hom
                            (limit.lift (F ⋙ objects)
                              { pt := (↑s.pt : Type v),
                                π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                          (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
                            (limit.lift (F ⋙ objects)
                              { pt := (↑s.pt : Type v),
                                π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                          (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)).obj
                  j'))
          (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) :
        (fun (X : Type v) ↦ X)
          (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'))
      (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯ :
        Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj 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) :
            (fun (X : Type v) ↦ X) ((F ⋙ objects).obj 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)))
                Y) :
            (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j')))
⊢ Quiver.Hom (V := limit (F ⋙ objects))
    ((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 :
      (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
    ((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 :
      (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))

Tactic:
fapply Types.Limit.mk.{v, v}