[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


[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ P = Q
[PROOFSTEP]
cases P
[GOAL]
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Q : Karoubi C
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝ p✝).X = Q.X
h_p : (mk X✝ p✝).p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ mk X✝ p✝ = Q
[PROOFSTEP]
cases Q
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : (mk X✝¹ p✝¹).X = (mk X✝ p✝).X
h_p : (mk X✝¹ p✝¹).p ≫ eqToHom h_X = eqToHom h_X ≫ (mk X✝ p✝).p
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
[PROOFSTEP]
dsimp at h_X h_p
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : X✝¹ = X✝
h_p : p✝¹ ≫ eqToHom h_X = eqToHom h_X ≫ p✝
⊢ mk X✝¹ p✝¹ = mk X✝ p✝
[PROOFSTEP]
subst h_X
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : C
p✝¹ : X✝ ⟶ X✝
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_p : p✝¹ ≫ eqToHom (_ : X✝ = X✝) = eqToHom (_ : X✝ = X✝) ≫ p✝
⊢ mk X✝ p✝¹ = mk X✝ p✝
[PROOFSTEP]
simpa only [mk.injEq, heq_eq_eq, true_and, eqToHom_refl, comp_id, id_comp] using h_p
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2814, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
⊢ 0 = P.p ≫ 0 ≫ Q.p
[PROOFSTEP]
rw [zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : Hom P Q
⊢ P.p ≫ f.f = f.f
[PROOFSTEP]
rw [f.comm, ← assoc, P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : Hom P Q
⊢ f.f ≫ Q.p = f.f
[PROOFSTEP]
rw [f.comm, assoc, assoc, Q.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : Hom P Q
⊢ P.p ≫ f.f = f.f ≫ Q.p
[PROOFSTEP]
rw [p_comp, comp_p]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q R : Karoubi C
g : Hom Q R
f : Hom P Q
⊢ f.f ≫ g.f = P.p ≫ (f.f ≫ g.f) ≫ R.p
[PROOFSTEP]
rw [assoc, comp_p, ← assoc, p_comp]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11320, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
repeat' rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11320, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11320, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g ↔ f.f = g.f
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g
[PROOFSTEP]
apply Hom.ext
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f.f = g.f
⊢ f = g
[PROOFSTEP]
simpa [hom_ext_iff] using h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q R : Karoubi C
f : P ⟶ Q
g : Q ⟶ R
⊢ (f ≫ g).f = f.f ≫ g.f
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15241, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
repeat' rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15241, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15241, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p
[PROOFSTEP]
rw [P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ 𝟙 P = Hom.mk P.p
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.15536, u_1} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
rw [comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ (mk X (𝟙 X)).X = X
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ (mk X (𝟙 X)).p = 𝟙 X
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
h : P = Q
⊢ (eqToHom h).f = P.p ≫ eqToHom (_ : P.X = Q.X)
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (eqToHom (_ : P = P)).f = P.p ≫ eqToHom (_ : P.X = P.X)
[PROOFSTEP]
simp only [eqToHom_refl, Karoubi.id_eq, comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.17980, u_1} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
rw [comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.17980, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ f = ((fun X => Karoubi.mk X (𝟙 X)) X✝).p ≫ f ≫ ((fun X => Karoubi.mk X (𝟙 X)) Y✝).p
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f + g.f = P.p ≫ (f.f + g.f) ≫ Q.p
[PROOFSTEP]
rw [add_comp, comp_add, ← f.comm, ← g.comm]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ f + g + h' = f + (g + h')
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ (f + g + h').f = (f + (g + h')).f
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
⊢ 0 = P.p ≫ 0 ≫ Q.p
[PROOFSTEP]
simp only [comp_zero, zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ 0 + f = f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (0 + f).f = f.f
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ f + 0 = f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (f + 0).f = f.f
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ -f.f = P.p ≫ (-f.f) ≫ Q.p
[PROOFSTEP]
simpa only [neg_comp, comp_neg, neg_inj] using f.comm
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ -f + f = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (-f + f).f = 0.f
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f + g = g + f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.24958, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ (f + g).f = (g + f).f
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35550, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
⊢ AddCommGroup (P ⟶ Q)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
⊢ IsIdempotentComplete (Karoubi C)
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
⊢ ∀ (X : Karoubi C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro P p hp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
simp only [hom_ext_iff, comp_f] at hp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
use⟨P.X, p.f, hp⟩
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ i e, i ≫ e = 𝟙 (Karoubi.mk P.X p.f) ∧ e ≫ i = p
[PROOFSTEP]
use⟨p.f, by rw [comp_p p, hp]⟩
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ p.f = (Karoubi.mk P.X p.f).p ≫ p.f ≫ P.p
[PROOFSTEP]
rw [comp_p p, hp]
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ e, Hom.mk p.f ≫ e = 𝟙 (Karoubi.mk P.X p.f) ∧ e ≫ Hom.mk p.f = p
[PROOFSTEP]
use⟨p.f, by rw [hp, p_comp p]⟩
[GOAL]
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ p.f = P.p ≫ p.f ≫ (Karoubi.mk P.X p.f).p
[PROOFSTEP]
rw [hp, p_comp p]
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.38941, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ Hom.mk p.f ≫ Hom.mk p.f = 𝟙 (Karoubi.mk P.X p.f) ∧ Hom.mk p.f ≫ Hom.mk p.f = p
[PROOFSTEP]
simp [hp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
⊢ P ∈ Functor.essImage (toKaroubi C)
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split P.X P.p P.idem with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ P ∈ Functor.essImage (toKaroubi C)
[PROOFSTEP]
use Y
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ Nonempty ((toKaroubi C).obj Y ≅ P)
[PROOFSTEP]
exact
  Nonempty.intro
    { hom := ⟨i, by erw [id_comp, ← h₂, ← assoc, h₁, id_comp]⟩
      inv := ⟨e, by erw [comp_id, ← h₂, assoc, h₁, comp_id]⟩ }
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ i = ((toKaroubi C).obj Y).p ≫ i ≫ P.p
[PROOFSTEP]
erw [id_comp, ← h₂, ← assoc, h₁, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.40282, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ e = P.p ≫ e ≫ ((toKaroubi C).obj Y).p
[PROOFSTEP]
erw [comp_id, ← h₂, assoc, h₁, comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.45540, u_1} C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ (mk P.X (𝟙 P.X)).p
[PROOFSTEP]
erw [coe_p, comp_id, P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.47113, u_1} C
P : Karoubi C
⊢ P.p = (mk P.X (𝟙 P.X)).p ≫ P.p ≫ P.p
[PROOFSTEP]
erw [coe_p, id_comp, P.idem]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ 𝟙 P = decompId_i P ≫ decompId_p P
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (𝟙 P).f = (decompId_i P ≫ decompId_p P).f
[PROOFSTEP]
simp only [comp_f, id_eq, P.idem, decompId_i, decompId_p]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (toKaroubi C).map P.p = decompId_p P ≫ decompId_i P
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (decompId_p P ≫ decompId_i P).f
[PROOFSTEP]
simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ decompId_i ((toKaroubi C).obj X) = 𝟙 ((toKaroubi C).obj X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ decompId_p ((toKaroubi C).obj X) = 𝟙 (mk ((toKaroubi C).obj X).X (𝟙 ((toKaroubi C).obj X).X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.50209, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ mk P.X (𝟙 P.X) ⟶ mk Q.X (𝟙 Q.X)
[PROOFSTEP]
exact Hom.mk f.f (by simp)
[GOAL]
C : Type u_1
inst✝ : Category.{?u.50209, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f.f = (mk P.X (𝟙 P.X)).p ≫ f.f ≫ (mk Q.X (𝟙 Q.X)).p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f ≫ decompId_i Q = decompId_i P ≫ Hom.mk f.f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.51254, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ mk P.X (𝟙 P.X) ⟶ mk Q.X (𝟙 Q.X)
[PROOFSTEP]
exact Hom.mk f.f (by simp)
[GOAL]
C : Type u_1
inst✝ : Category.{?u.51254, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f.f = (mk P.X (𝟙 P.X)).p ≫ f.f ≫ (mk Q.X (𝟙 Q.X)).p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ decompId_p P ≫ f = Hom.mk f.f ≫ decompId_p Q
[PROOFSTEP]
aesop_cat