[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y) X✝
⊢ (fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y) Y✝
[PROOFSTEP]
refine' eqToHom _ ≫ (F.map f).map g ≫ eqToHom _
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y) X✝
⊢ limit.π (F ⋙ objects) Y✝ X = (F.map f).obj (limit.π (F ⋙ objects) X✝ X)
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y) X✝
⊢ (F.map f).obj (limit.π (F ⋙ objects) X✝ Y) = limit.π (F ⋙ objects) Y✝ Y
[PROOFSTEP]
exact (congr_fun (limit.w (F ⋙ Cat.objects) f) X).symm
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y) X✝
⊢ (F.map f).obj (limit.π (F ⋙ objects) X✝ Y) = limit.π (F ⋙ objects) Y✝ Y
[PROOFSTEP]
exact congr_fun (limit.w (F ⋙ Cat.objects) f) Y
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
⊢ { obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
          map := fun {X Y_1} f g =>
            eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
              (F.map f).map g ≫
                eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
            map := fun {X Y_1} f g =>
              eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
                (F.map f).map g ≫
                  eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.obj
        X)
[PROOFSTEP]
funext f
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
f :
  { obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
        map := fun {X Y_1} f g =>
          eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
            (F.map f).map g ≫
              eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.obj
    X
⊢ { obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
          map := fun {X Y_1} f g =>
            eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
              (F.map f).map g ≫
                eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
      (𝟙 X) f =
    𝟙
      ({ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
            map := fun {X Y_1} f g =>
              eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
                (F.map f).map g ≫
                  eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.obj
        X)
      f
[PROOFSTEP]
letI : Category (objects.obj (F.obj X)) := (inferInstance : Category (F.obj X))
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
f :
  { obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
        map := fun {X Y_1} f g =>
          eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
            (F.map f).map g ≫
              eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.obj
    X
this : Category.{v, v} (objects.obj (F.obj X)) := inferInstance
⊢ { obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
          map := fun {X Y_1} f g =>
            eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
              (F.map f).map g ≫
                eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
      (𝟙 X) f =
    𝟙
      ({ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y,
            map := fun {X Y_1} f g =>
              eqToHom (_ : limit.π (F ⋙ objects) Y_1 X✝ = (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) X✝) ≫
                (F.map f).map g ≫
                  eqToHom (_ : (limit.π (F ⋙ objects) X ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.obj
        X)
      f
[PROOFSTEP]
simp [Functor.congr_hom (F.map_id X) f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
⊢ { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
          map := fun {X_1 Y_1} f g =>
            eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
              (F.map f).map g ≫
                eqToHom (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
      (f ≫ g) =
    { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
            map := fun {X_1 Y_1} f g =>
              eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
                (F.map f).map g ≫
                  eqToHom (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
        f ≫
      { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
            map := fun {X_1 Y_1} f g =>
              eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
                (F.map f).map g ≫
                  eqToHom (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
        g
[PROOFSTEP]
funext h
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
h :
  { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
        map := fun {X_1 Y_1} f g =>
          eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
            (F.map f).map g ≫
              eqToHom (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.obj
    x✝¹
⊢ { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
          map := fun {X_1 Y_1} f g =>
            eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
              (F.map f).map g ≫
                eqToHom (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
      (f ≫ g) h =
    ({ obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
              map := fun {X_1 Y_1} f g =>
                eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
                  (F.map f).map g ≫
                    eqToHom
                      (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
          f ≫
        { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
              map := fun {X_1 Y_1} f g =>
                eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
                  (F.map f).map g ≫
                    eqToHom
                      (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
          g)
      h
[PROOFSTEP]
letI : Category (objects.obj (F.obj Z)) := (inferInstance : Category (F.obj Z))
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
h :
  { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
        map := fun {X_1 Y_1} f g =>
          eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
            (F.map f).map g ≫
              eqToHom (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.obj
    x✝¹
this : Category.{v, v} (objects.obj (F.obj Z)) := inferInstance
⊢ { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
          map := fun {X_1 Y_1} f g =>
            eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
              (F.map f).map g ≫
                eqToHom (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
      (f ≫ g) h =
    ({ obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
              map := fun {X_1 Y_1} f g =>
                eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
                  (F.map f).map g ≫
                    eqToHom
                      (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
          f ≫
        { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y,
              map := fun {X_1 Y_1} f g =>
                eqToHom (_ : limit.π (F ⋙ objects) Y_1 X = (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) X) ≫
                  (F.map f).map g ≫
                    eqToHom
                      (_ : (limit.π (F ⋙ objects) X_1 ≫ (F ⋙ objects).map f) Y = limit.π (F ⋙ objects) Y_1 Y) }.map
          g)
      h
[PROOFSTEP]
simp [Functor.congr_hom (F.map_comp f g) h, eqToHom_map]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j j' : J
f : j ⟶ j'
⊢ (homDiagram X X).map f ((fun j => 𝟙 (limit.π (F ⋙ objects) j X)) j) = (fun j => 𝟙 (limit.π (F ⋙ objects) j X)) j'
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y Z : limit (F ⋙ objects)
f : X ⟶ Y
g : Y ⟶ Z
j j' : J
h : j ⟶ j'
⊢ (homDiagram X Z).map h ((fun j => limit.π (homDiagram X Y) j f ≫ limit.π (homDiagram Y Z) j g) j) =
    (fun j => limit.π (homDiagram X Y) j f ≫ limit.π (homDiagram Y Z) j g) j'
[PROOFSTEP]
simp [← congr_fun (limit.w (homDiagram X Y) h) f, ← congr_fun (limit.w (homDiagram Y Z) h) g]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ x✝ = x✝
[PROOFSTEP]
apply Types.limit_ext.{v, v}
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : X✝ ⟶ Y✝
⊢ ∀ (j : J), limit.π (homDiagram X✝ Y✝) j (𝟙 X✝ ≫ x✝) = limit.π (homDiagram X✝ Y✝) j x✝
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : X✝ ⟶ Y✝
⊢ x✝ ≫ 𝟙 Y✝ = x✝
[PROOFSTEP]
apply Types.limit_ext.{v, v}
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : X✝ ⟶ Y✝
⊢ ∀ (j : J), limit.π (homDiagram X✝ Y✝) j (x✝ ≫ 𝟙 Y✝) = limit.π (homDiagram X✝ Y✝) j x✝
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
⊢ limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝ ⟶
    limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝
[PROOFSTEP]
fapply Types.Limit.mk.{v, v}
[GOAL]
case x
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
⊢ (j : J) →
    (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝)
          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)).obj
      j
[PROOFSTEP]
intro j
[GOAL]
case x
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j : J
⊢ (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝)
        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)).obj
    j
[PROOFSTEP]
refine' eqToHom _ ≫ (s.π.app j).map f ≫ eqToHom _
[GOAL]
case x.refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j : J
⊢ limit.π (F ⋙ objects) j
      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
    (NatTrans.app s.π j).obj X✝
[PROOFSTEP]
simp
[GOAL]
case x.refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j : J
⊢ (NatTrans.app s.π j).obj Y✝ =
    limit.π (F ⋙ objects) j
      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)
[PROOFSTEP]
simp
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
⊢ ∀ (j j' : J) (f_1 : j ⟶ j'),
    (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝)
            (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)).map
        f_1
        (eqToHom
            (_ :
              limit.π (F ⋙ objects) j
                  (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
                (NatTrans.app s.π j).obj X✝) ≫
          (NatTrans.app s.π j).map f ≫
            eqToHom
              (_ :
                (NatTrans.app s.π j).obj Y✝ =
                  limit.π (F ⋙ objects) j
                    (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                      Y✝))) =
      eqToHom
          (_ :
            limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
              (NatTrans.app s.π j').obj X✝) ≫
        (NatTrans.app s.π j').map f ≫
          eqToHom
            (_ :
              (NatTrans.app s.π j').obj Y✝ =
                limit.π (F ⋙ objects) j'
                  (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
intro j j' h
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
⊢ (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝)
          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)).map
      h
      (eqToHom
          (_ :
            limit.π (F ⋙ objects) j
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
              (NatTrans.app s.π j).obj X✝) ≫
        (NatTrans.app s.π j).map f ≫
          eqToHom
            (_ :
              (NatTrans.app s.π j).obj Y✝ =
                limit.π (F ⋙ objects) j
                  (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (NatTrans.app s.π j').obj X✝) ≫
      (NatTrans.app s.π j').map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j').obj Y✝ =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
dsimp
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
⊢ eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h)
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝)) ≫
      (F.map h).map
          (eqToHom
              (_ :
                limit.π (F ⋙ objects) j
                    (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
                  (NatTrans.app s.π j).obj X✝) ≫
            (NatTrans.app s.π j).map f ≫
              eqToHom
                (_ :
                  (NatTrans.app s.π j).obj Y✝ =
                    limit.π (F ⋙ objects) j
                      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                        Y✝))) ≫
        eqToHom
          (_ :
            (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h)
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝) =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (NatTrans.app s.π j').obj X✝) ≫
      (NatTrans.app s.π j').map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j').obj Y✝ =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
simp only [Category.assoc, Functor.map_comp, eqToHom_map, eqToHom_trans, eqToHom_trans_assoc, ← Functor.comp_map]
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
⊢ eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (F.map h).obj ((NatTrans.app s.π j).obj X✝)) ≫
      (NatTrans.app s.π j ⋙ F.map h).map f ≫
        eqToHom
          (_ :
            (F.map h).obj ((NatTrans.app s.π j).obj Y✝) =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (NatTrans.app s.π j').obj X✝) ≫
      (NatTrans.app s.π j').map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j').obj Y✝ =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
have := (s.π.naturality h).symm
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : NatTrans.app s.π j ≫ F.map h = ((Functor.const J).obj s.pt).map h ≫ NatTrans.app s.π j'
⊢ eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (F.map h).obj ((NatTrans.app s.π j).obj X✝)) ≫
      (NatTrans.app s.π j ⋙ F.map h).map f ≫
        eqToHom
          (_ :
            (F.map h).obj ((NatTrans.app s.π j).obj Y✝) =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (NatTrans.app s.π j').obj X✝) ≫
      (NatTrans.app s.π j').map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j').obj Y✝ =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
dsimp at this 
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : NatTrans.app s.π j ≫ F.map h = 𝟙 s.pt ≫ NatTrans.app s.π j'
⊢ eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (F.map h).obj ((NatTrans.app s.π j).obj X✝)) ≫
      (NatTrans.app s.π j ⋙ F.map h).map f ≫
        eqToHom
          (_ :
            (F.map h).obj ((NatTrans.app s.π j).obj Y✝) =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (NatTrans.app s.π j').obj X✝) ≫
      (NatTrans.app s.π j').map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j').obj Y✝ =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
rw [Category.id_comp] at this 
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : NatTrans.app s.π j ≫ F.map h = NatTrans.app s.π j'
⊢ eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (F.map h).obj ((NatTrans.app s.π j).obj X✝)) ≫
      (NatTrans.app s.π j ⋙ F.map h).map f ≫
        eqToHom
          (_ :
            (F.map h).obj ((NatTrans.app s.π j).obj Y✝) =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (NatTrans.app s.π j').obj X✝) ≫
      (NatTrans.app s.π j').map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j').obj Y✝ =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
erw [Functor.congr_hom this f]
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.pt
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : NatTrans.app s.π j ≫ F.map h = NatTrans.app s.π j'
⊢ eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (F.map h).obj ((NatTrans.app s.π j).obj X✝)) ≫
      (eqToHom (_ : (NatTrans.app s.π j ≫ F.map h).obj X✝ = (NatTrans.app s.π j').obj X✝) ≫
          (NatTrans.app s.π j').map f ≫
            eqToHom (_ : (NatTrans.app s.π j').obj Y✝ = (NatTrans.app s.π j ≫ F.map h).obj Y✝)) ≫
        eqToHom
          (_ :
            (F.map h).obj ((NatTrans.app s.π j).obj Y✝) =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝)) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j'
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X✝) =
            (NatTrans.app s.π j').obj X✝) ≫
      (NatTrans.app s.π j').map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j').obj Y✝ =
              limit.π (F ⋙ objects) j'
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y✝))
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
j : J
h : X = Y
⊢ limit.π (homDiagram X Y) j (eqToHom h) = eqToHom (_ : limit.π (F ⋙ objects) j X = limit.π (F ⋙ objects) j Y)
[PROOFSTEP]
subst h
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j : J
⊢ limit.π (homDiagram X X) j (eqToHom (_ : X = X)) = eqToHom (_ : limit.π (F ⋙ objects) j X = limit.π (F ⋙ objects) j X)
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
⊢ ∀ (X : ↑s.pt), (limitConeLift F s ≫ NatTrans.app (limitCone F).π j).obj X = (NatTrans.app s.π j).obj X
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : ↑s.pt
f : X ⟶ Y
⊢ (limitConeLift F s ≫ NatTrans.app (limitCone F).π j).map f =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X) =
            (NatTrans.app s.π j).obj X) ≫
      (NatTrans.app s.π j).map f ≫
        eqToHom (_ : (NatTrans.app s.π j).obj Y = (limitConeLift F s ≫ NatTrans.app (limitCone F).π j).obj Y)
[PROOFSTEP]
dsimp [limitConeLift]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : ↑s.pt
f : X ⟶ Y
⊢ limit.π
      (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
      j
      (Types.Limit.mk
        (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
        (fun j =>
          eqToHom
              (_ :
                limit.π (F ⋙ objects) j
                    (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X) =
                  (NatTrans.app s.π j).obj X) ≫
            (NatTrans.app s.π j).map f ≫
              eqToHom
                (_ :
                  (NatTrans.app s.π j).obj Y =
                    limit.π (F ⋙ objects) j
                      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)))
        (_ :
          ∀ (j j' : J) (h : j ⟶ j'),
            (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
                    (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                      Y)).map
                h
                (eqToHom
                    (_ :
                      limit.π (F ⋙ objects) j
                          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                            X) =
                        (NatTrans.app s.π j).obj X) ≫
                  (NatTrans.app s.π j).map f ≫
                    eqToHom
                      (_ :
                        (NatTrans.app s.π j).obj Y =
                          limit.π (F ⋙ objects) j
                            (limit.lift (F ⋙ objects)
                              { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))) =
              eqToHom
                  (_ :
                    limit.π (F ⋙ objects) j'
                        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                          X) =
                      (NatTrans.app s.π j').obj X) ≫
                (NatTrans.app s.π j').map f ≫
                  eqToHom
                    (_ :
                      (NatTrans.app s.π j').obj Y =
                        limit.π (F ⋙ objects) j'
                          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                            Y)))) =
    eqToHom
        (_ :
          limit.π (F ⋙ objects) j
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X) =
            (NatTrans.app s.π j).obj X) ≫
      (NatTrans.app s.π j).map f ≫
        eqToHom
          (_ :
            (NatTrans.app s.π j).obj Y =
              limit.π (F ⋙ objects) j
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
[PROOFSTEP]
exact Types.Limit.π_mk.{v, v} _ _ _ _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
⊢ m = limitConeLift F s
[PROOFSTEP]
symm
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
⊢ limitConeLift F s = m
[PROOFSTEP]
refine' CategoryTheory.Functor.ext _ _
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
⊢ ∀ (X : ↑s.pt), (limitConeLift F s).obj X = m.obj X
[PROOFSTEP]
intro X
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
X : ↑s.pt
⊢ (limitConeLift F s).obj X = m.obj X
[PROOFSTEP]
apply Types.limit_ext.{v, v}
[GOAL]
case refine'_1.w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
X : ↑s.pt
⊢ ∀ (j : J), limit.π (F ⋙ objects) j ((limitConeLift F s).obj X) = limit.π (F ⋙ objects) j (m.obj X)
[PROOFSTEP]
intro j
[GOAL]
case refine'_1.w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
X : ↑s.pt
j : J
⊢ limit.π (F ⋙ objects) j ((limitConeLift F s).obj X) = limit.π (F ⋙ objects) j (m.obj X)
[PROOFSTEP]
simp [Types.Limit.lift_π_apply', ← w j]
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
⊢ ∀ (X Y : ↑s.pt) (f : X ⟶ Y),
    (limitConeLift F s).map f =
      eqToHom (_ : (limitConeLift F s).obj X = m.obj X) ≫ m.map f ≫ eqToHom (_ : m.obj Y = (limitConeLift F s).obj Y)
[PROOFSTEP]
intro X Y f
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
X Y : ↑s.pt
f : X ⟶ Y
⊢ (limitConeLift F s).map f =
    eqToHom (_ : (limitConeLift F s).obj X = m.obj X) ≫ m.map f ≫ eqToHom (_ : m.obj Y = (limitConeLift F s).obj Y)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app s.π j
X Y : ↑s.pt
f : X ⟶ Y
⊢ Types.Limit.mk
      (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
      (fun j =>
        eqToHom
            (_ :
              limit.π (F ⋙ objects) j
                  (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X) =
                (NatTrans.app s.π j).obj X) ≫
          (NatTrans.app s.π j).map f ≫
            eqToHom
              (_ :
                (NatTrans.app s.π j).obj Y =
                  limit.π (F ⋙ objects) j
                    (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)))
      (_ :
        ∀ (j j' : J) (h : j ⟶ j'),
          (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
                  (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)).map
              h
              (eqToHom
                  (_ :
                    limit.π (F ⋙ objects) j
                        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                          X) =
                      (NatTrans.app s.π j).obj X) ≫
                (NatTrans.app s.π j).map f ≫
                  eqToHom
                    (_ :
                      (NatTrans.app s.π j).obj Y =
                        limit.π (F ⋙ objects) j
                          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                            Y))) =
            eqToHom
                (_ :
                  limit.π (F ⋙ objects) j'
                      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X) =
                    (NatTrans.app s.π j').obj X) ≫
              (NatTrans.app s.π j').map f ≫
                eqToHom
                  (_ :
                    (NatTrans.app s.π j').obj Y =
                      limit.π (F ⋙ objects) j'
                        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                          Y))) =
    Types.Limit.mk
      (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
      (fun j =>
        limit.π
            (homDiagram (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
              (m.obj X))
            j
            (eqToHom
              (_ :
                limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X =
                  m.obj X)) ≫
          limit.π
            (homDiagram (m.obj X)
              (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
            j
            (Types.Limit.mk
              (homDiagram (m.obj X)
                (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
              (fun j =>
                limit.π (homDiagram (m.obj X) (m.obj Y)) j (m.map f) ≫
                  limit.π
                    (homDiagram (m.obj Y)
                      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                    j
                    (eqToHom
                      (_ :
                        m.obj Y =
                          limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                            Y)))
              (_ :
                ∀ (j j' : J) (h : j ⟶ j'),
                  eqToHom
                        (_ :
                          limit.π (F ⋙ objects) j' (m.obj X) =
                            (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h) (m.obj X)) ≫
                      (F.map h).map
                          (limit.π (homDiagram (m.obj X) (m.obj Y)) j (m.map f) ≫
                            limit.π
                              (homDiagram (m.obj Y)
                                (limit.lift (F ⋙ objects)
                                  { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                              j
                              (eqToHom
                                (_ :
                                  m.obj Y =
                                    limit.lift (F ⋙ objects)
                                      { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))) ≫
                        eqToHom
                          (_ :
                            (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h)
                                (limit.lift (F ⋙ objects)
                                  { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y) =
                              limit.π (F ⋙ objects) j'
                                (limit.lift (F ⋙ objects)
                                  { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)) =
                    limit.π (homDiagram (m.obj X) (m.obj Y)) j' (m.map f) ≫
                      limit.π
                        (homDiagram (m.obj Y)
                          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                            Y))
                        j'
                        (eqToHom
                          (_ :
                            m.obj Y =
                              limit.lift (F ⋙ objects)
                                { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)))))
      (_ :
        ∀ (j j' : J) (h : j ⟶ j'),
          eqToHom
                (_ :
                  limit.π (F ⋙ objects) j'
                      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X) =
                    (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h)
                      (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                        X)) ≫
              (F.map h).map
                  (limit.π
                      (homDiagram
                        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
                        (m.obj X))
                      j
                      (eqToHom
                        (_ :
                          limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                              X =
                            m.obj X)) ≫
                    limit.π
                      (homDiagram (m.obj X)
                        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                          Y))
                      j
                      (Types.Limit.mk
                        (homDiagram (m.obj X)
                          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                            Y))
                        (fun j =>
                          limit.π (homDiagram (m.obj X) (m.obj Y)) j (m.map f) ≫
                            limit.π
                              (homDiagram (m.obj Y)
                                (limit.lift (F ⋙ objects)
                                  { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                              j
                              (eqToHom
                                (_ :
                                  m.obj Y =
                                    limit.lift (F ⋙ objects)
                                      { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)))
                        (_ :
                          ∀ (j j' : J) (h : j ⟶ j'),
                            eqToHom
                                  (_ :
                                    limit.π (F ⋙ objects) j' (m.obj X) =
                                      (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h) (m.obj X)) ≫
                                (F.map h).map
                                    (limit.π (homDiagram (m.obj X) (m.obj Y)) j (m.map f) ≫
                                      limit.π
                                        (homDiagram (m.obj Y)
                                          (limit.lift (F ⋙ objects)
                                            { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                                        j
                                        (eqToHom
                                          (_ :
                                            m.obj Y =
                                              limit.lift (F ⋙ objects)
                                                { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                                                Y))) ≫
                                  eqToHom
                                    (_ :
                                      (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h)
                                          (limit.lift (F ⋙ objects)
                                            { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y) =
                                        limit.π (F ⋙ objects) j'
                                          (limit.lift (F ⋙ objects)
                                            { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)) =
                              limit.π (homDiagram (m.obj X) (m.obj Y)) j' (m.map f) ≫
                                limit.π
                                  (homDiagram (m.obj Y)
                                    (limit.lift (F ⋙ objects)
                                      { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                                  j'
                                  (eqToHom
                                    (_ :
                                      m.obj Y =
                                        limit.lift (F ⋙ objects)
                                          { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))))) ≫
                eqToHom
                  (_ :
                    (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h)
                        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                          Y) =
                      limit.π (F ⋙ objects) j'
                        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                          Y)) =
            limit.π
                (homDiagram
                  (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X)
                  (m.obj X))
                j'
                (eqToHom
                  (_ :
                    limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } X =
                      m.obj X)) ≫
              limit.π
                (homDiagram (m.obj X)
                  (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                j'
                (Types.Limit.mk
                  (homDiagram (m.obj X)
                    (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                  (fun j =>
                    limit.π (homDiagram (m.obj X) (m.obj Y)) j (m.map f) ≫
                      limit.π
                        (homDiagram (m.obj Y)
                          (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj }
                            Y))
                        j
                        (eqToHom
                          (_ :
                            m.obj Y =
                              limit.lift (F ⋙ objects)
                                { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)))
                  (_ :
                    ∀ (j j' : J) (h : j ⟶ j'),
                      eqToHom
                            (_ :
                              limit.π (F ⋙ objects) j' (m.obj X) =
                                (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h) (m.obj X)) ≫
                          (F.map h).map
                              (limit.π (homDiagram (m.obj X) (m.obj Y)) j (m.map f) ≫
                                limit.π
                                  (homDiagram (m.obj Y)
                                    (limit.lift (F ⋙ objects)
                                      { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                                  j
                                  (eqToHom
                                    (_ :
                                      m.obj Y =
                                        limit.lift (F ⋙ objects)
                                          { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))) ≫
                            eqToHom
                              (_ :
                                (limit.π (F ⋙ objects) j ≫ (F ⋙ objects).map h)
                                    (limit.lift (F ⋙ objects)
                                      { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y) =
                                  limit.π (F ⋙ objects) j'
                                    (limit.lift (F ⋙ objects)
                                      { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)) =
                        limit.π (homDiagram (m.obj X) (m.obj Y)) j' (m.map f) ≫
                          limit.π
                            (homDiagram (m.obj Y)
                              (limit.lift (F ⋙ objects)
                                { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y))
                            j'
                            (eqToHom
                              (_ :
                                m.obj Y =
                                  limit.lift (F ⋙ objects)
                                    { pt := ↑s.pt, π := NatTrans.mk fun j => (NatTrans.app s.π j).obj } Y)))))
[PROOFSTEP]
simp [fun j => Functor.congr_hom (w j).symm f]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
J✝ : Type v
inst✝ : Category.{v, v} J✝
F : J✝ ⥤ Cat
⊢ (limit.cone (F ⋙ objects)).pt ≅ (objects.mapCone (HasLimits.limitCone F)).pt
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
J✝ : Type v
inst✝ : Category.{v, v} J✝
F : J✝ ⥤ Cat
⊢ ∀ (j : J✝),
    NatTrans.app (limit.cone (F ⋙ objects)).π j =
      (Iso.refl (limit.cone (F ⋙ objects)).pt).hom ≫ NatTrans.app (objects.mapCone (HasLimits.limitCone F)).π j
[PROOFSTEP]
aesop_cat
