[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
x : ((restrictedYoneda yoneda).obj P).obj X
⊢ (((restrictedYoneda yoneda).obj P).map f ≫ ((fun X => yonedaSectionsSmall X.unop P) Y).hom) x =
    (((fun X => yonedaSectionsSmall X.unop P) X).hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj P).map f) x
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
x : ((restrictedYoneda yoneda).obj P).obj X
⊢ NatTrans.app x { unop := Y.unop } (𝟙 Y.unop ≫ f.unop) = P.map f (NatTrans.app x { unop := X.unop } (𝟙 X.unop))
[PROOFSTEP]
have : x.app X (CategoryStruct.id (Opposite.unop X)) = (x.app X (𝟙 (Opposite.unop X))) := by rfl
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
x : ((restrictedYoneda yoneda).obj P).obj X
⊢ NatTrans.app x X (𝟙 X.unop) = NatTrans.app x X (𝟙 X.unop)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
x : ((restrictedYoneda yoneda).obj P).obj X
this : NatTrans.app x X (𝟙 X.unop) = NatTrans.app x X (𝟙 X.unop)
⊢ NatTrans.app x { unop := Y.unop } (𝟙 Y.unop ≫ f.unop) = P.map f (NatTrans.app x { unop := X.unop } (𝟙 X.unop))
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
x : ((restrictedYoneda yoneda).obj P).obj X
this : NatTrans.app x X (𝟙 X.unop) = NatTrans.app x X (𝟙 X.unop)
⊢ NatTrans.app x { unop := Y.unop } (𝟙 Y.unop ≫ f.unop) = P.map f (NatTrans.app x X (𝟙 X.unop))
[PROOFSTEP]
rw [← FunctorToTypes.naturality _ _ x f (𝟙 _)]
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
x : ((restrictedYoneda yoneda).obj P).obj X
this : NatTrans.app x X (𝟙 X.unop) = NatTrans.app x X (𝟙 X.unop)
⊢ NatTrans.app x { unop := Y.unop } (𝟙 Y.unop ≫ f.unop) = NatTrans.app x Y ((yoneda.op.obj X).unop.map f (𝟙 X.unop))
[PROOFSTEP]
simp only [id_comp, Functor.op_obj, Opposite.unop_op, yoneda_obj_map, comp_id]
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
τ : P ⟶ (restrictedYoneda A).obj E
p p' : (Functor.Elements P)ᵒᵖ
f : p ⟶ p'
⊢ ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
    (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p
[PROOFSTEP]
simp_rw [← f.unop.2]
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
τ : P ⟶ (restrictedYoneda A).obj E
p p' : (Functor.Elements P)ᵒᵖ
f : p ⟶ p'
⊢ ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ NatTrans.app τ p'.unop.fst p'.unop.snd =
    NatTrans.app τ p.unop.fst (P.map (↑f.unop) p'.unop.snd)
[PROOFSTEP]
apply (congr_fun (τ.naturality f.unop.1) p'.unop.2).symm
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
⊢ Function.LeftInverse
    (fun τ =>
      { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
        property :=
          (_ :
            ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
              ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
    fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })
[PROOFSTEP]
rintro ⟨k₁, k₂⟩
[GOAL]
case mk
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k₁ : (j : (Functor.Elements P)ᵒᵖ) → ((CategoryOfElements.π P).leftOp ⋙ A).obj j ⟶ E
k₂ : ∀ {j j' : (Functor.Elements P)ᵒᵖ} (f : j ⟶ j'), ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ k₁ j' = k₁ j
⊢ (fun τ =>
        { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
          property :=
            (_ :
              ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
                ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                  (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
      ((fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })) { val := k₁, property := k₂ }) =
    { val := k₁, property := k₂ }
[PROOFSTEP]
ext
[GOAL]
case mk.a.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k₁ : (j : (Functor.Elements P)ᵒᵖ) → ((CategoryOfElements.π P).leftOp ⋙ A).obj j ⟶ E
k₂ : ∀ {j j' : (Functor.Elements P)ᵒᵖ} (f : j ⟶ j'), ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ k₁ j' = k₁ j
x✝ : (Functor.Elements P)ᵒᵖ
⊢ ↑((fun τ =>
            { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
              property :=
                (_ :
                  ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
                    ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                      (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
          ((fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })) { val := k₁, property := k₂ }))
      x✝ =
    ↑{ val := k₁, property := k₂ } x✝
[PROOFSTEP]
dsimp
[GOAL]
case mk.a.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k₁ : (j : (Functor.Elements P)ᵒᵖ) → ((CategoryOfElements.π P).leftOp ⋙ A).obj j ⟶ E
k₂ : ∀ {j j' : (Functor.Elements P)ᵒᵖ} (f : j ⟶ j'), ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ k₁ j' = k₁ j
x✝ : (Functor.Elements P)ᵒᵖ
⊢ k₁ (Opposite.op { fst := x✝.unop.fst, snd := x✝.unop.snd }) = k₁ x✝
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
⊢ Function.RightInverse
    (fun τ =>
      { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
        property :=
          (_ :
            ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
              ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
    fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })
[PROOFSTEP]
rintro ⟨_, _⟩
[GOAL]
case mk
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E : ℰ
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
app✝ : (X : Cᵒᵖ) → P.obj X ⟶ ((restrictedYoneda A).obj E).obj X
naturality✝ : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), P.map f ≫ app✝ Y = app✝ X ≫ ((restrictedYoneda A).obj E).map f
⊢ (fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }))
      ((fun τ =>
          { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
            property :=
              (_ :
                ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
                  ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                    (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
        (NatTrans.mk app✝)) =
    NatTrans.mk app✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E₁ E₂ : ℰ
g : E₁ ⟶ E₂
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k : c.pt ⟶ E₁
⊢ ↑(restrictYonedaHomEquiv A P E₂ t) (k ≫ g) = ↑(restrictYonedaHomEquiv A P E₁ t) k ≫ (restrictedYoneda A).map g
[PROOFSTEP]
ext x X
[GOAL]
case w.h.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E₁ E₂ : ℰ
g : E₁ ⟶ E₂
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k : c.pt ⟶ E₁
x : Cᵒᵖ
X : P.obj x
⊢ NatTrans.app (↑(restrictYonedaHomEquiv A P E₂ t) (k ≫ g)) x X =
    NatTrans.app (↑(restrictYonedaHomEquiv A P E₁ t) k ≫ (restrictedYoneda A).map g) x X
[PROOFSTEP]
apply (assoc _ _ _).symm
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ (extendAlongYoneda A).map f = colimit.pre ((CategoryOfElements.π Y).leftOp ⋙ A) (CategoryOfElements.map f).op
[PROOFSTEP]
ext J
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
J : (Functor.Elements X)ᵒᵖ
⊢ colimit.ι ((CategoryOfElements.π X).leftOp ⋙ A) J ≫ (extendAlongYoneda A).map f =
    colimit.ι ((CategoryOfElements.π X).leftOp ⋙ A) J ≫
      colimit.pre ((CategoryOfElements.π Y).leftOp ⋙ A) (CategoryOfElements.map f).op
[PROOFSTEP]
erw [colimit.ι_pre ((CategoryOfElements.π Y).leftOp ⋙ A) (CategoryOfElements.map f).op]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
J : (Functor.Elements X)ᵒᵖ
⊢ colimit.ι ((CategoryOfElements.π X).leftOp ⋙ A) J ≫ (extendAlongYoneda A).map f =
    colimit.ι ((CategoryOfElements.π Y).leftOp ⋙ A) ((CategoryOfElements.map f).op.obj J)
[PROOFSTEP]
dsimp only [extendAlongYoneda, restrictYonedaHomEquiv, IsColimit.homIso', IsColimit.homIso, uliftTrivial]
  -- porting note: in mathlib3 the rest of the proof was `simp, refl`; this is squeezed
    -- and appropriately reordered, presumably because of a non-confluence issue.
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
J : (Functor.Elements X)ᵒᵖ
⊢ colimit.ι ((CategoryOfElements.π X).leftOp ⋙ A) J ≫
      (Adjunction.leftAdjointOfEquiv
            (fun P E =>
              ((Iso.mk (fun a => a.down) fun a => { down := a }).symm ≪≫
                    (Iso.mk (fun f => (Cocone.extend (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)) f.down).ι)
                        fun ι =>
                        {
                          down :=
                            IsColimit.desc (colimit.isColimit ((CategoryOfElements.π P).leftOp ⋙ A))
                              { pt := E, ι := ι } }) ≪≫
                      Iso.mk
                        (fun ι =>
                          { val := fun j => NatTrans.app ι j,
                            property :=
                              (_ :
                                ∀ {j j' : (Functor.Elements P)ᵒᵖ} (f : j ⟶ j'),
                                  ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ (fun j => NatTrans.app ι j) j' =
                                    (fun j => NatTrans.app ι j) j) })
                        fun p => NatTrans.mk fun j => ↑p j).trans
                { toFun := fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }),
                  invFun := fun τ =>
                    { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                      property :=
                        (_ :
                          ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
                            ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫
                                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                              (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) },
                  left_inv :=
                    (_ :
                      ∀
                        (x :
                          { p //
                            ∀ {j j' : (Functor.Elements P)ᵒᵖ} (f : j ⟶ j'),
                              ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫ p j' = p j }),
                        (fun τ =>
                              { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                property :=
                                  (_ :
                                    ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
                                      ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫
                                          (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                        (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                            ((fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })) x) =
                          x),
                  right_inv :=
                    (_ :
                      ∀ (x : P ⟶ (restrictedYoneda A).obj E),
                        (fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }))
                            ((fun τ =>
                                { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                  property :=
                                    (_ :
                                      ∀ (p p' : (Functor.Elements P)ᵒᵖ) (f : p ⟶ p'),
                                        ((CategoryOfElements.π P).leftOp ⋙ A).map f ≫
                                            (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                          (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                              x) =
                          x) })
            (_ :
              ∀ (P : Cᵒᵖ ⥤ Type u₁) (E E' : ℰ) (g : E ⟶ E')
                (k : (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt ⟶ E),
                ↑(restrictYonedaHomEquiv A P E' (colimit.isColimit ((CategoryOfElements.π P).leftOp ⋙ A))) (k ≫ g) =
                  ↑(restrictYonedaHomEquiv A P E (colimit.isColimit ((CategoryOfElements.π P).leftOp ⋙ A))) k ≫
                    (restrictedYoneda A).map g)).map
        f =
    colimit.ι ((CategoryOfElements.π Y).leftOp ⋙ A) ((CategoryOfElements.map f).op.obj J)
[PROOFSTEP]
simp only [Adjunction.leftAdjointOfEquiv_map, Iso.symm_mk, Iso.toEquiv_comp, Equiv.coe_trans, Equiv.coe_fn_mk,
  Iso.toEquiv_fun, Equiv.symm_trans_apply, Equiv.coe_fn_symm_mk, Iso.toEquiv_symm_fun, id.def, colimit.isColimit_desc,
  colimit.ι_desc, FunctorToTypes.comp, Cocone.extend_ι, Cocone.extensions_app, Functor.map_id, Category.comp_id,
  colimit.cocone_ι]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
J : (Functor.Elements X)ᵒᵖ
⊢ NatTrans.app
      (((fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })) ∘
          ((fun ι =>
                { val := fun j => NatTrans.app ι j,
                  property :=
                    (_ :
                      ∀ {j j' : (Functor.Elements Y)ᵒᵖ} (f : j ⟶ j'),
                        ((CategoryOfElements.π Y).leftOp ⋙ A).map f ≫ (fun j => NatTrans.app ι j) j' =
                          (fun j => NatTrans.app ι j) j) }) ∘
              fun f =>
              (colimit.cocone ((CategoryOfElements.π Y).leftOp ⋙ A)).ι ≫
                (Functor.const (Functor.Elements Y)ᵒᵖ).map f.down) ∘
            fun a => { down := a })
        (𝟙 (colimit.cocone ((CategoryOfElements.π Y).leftOp ⋙ A)).pt))
      J.unop.fst (NatTrans.app f J.unop.fst J.unop.snd) =
    colimit.ι ((CategoryOfElements.π Y).leftOp ⋙ A) ((CategoryOfElements.map f).op.obj J)
[PROOFSTEP]
simp only [Functor.comp_obj, Functor.leftOp_obj, CategoryOfElements.π_obj, colimit.cocone_x, Functor.comp_map,
  Functor.leftOp_map, CategoryOfElements.π_map, Opposite.unop_op, Adjunction.leftAdjointOfEquiv_obj,
  Function.comp_apply, Functor.map_id, comp_id, colimit.cocone_ι, Functor.op_obj]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
J : (Functor.Elements X)ᵒᵖ
⊢ colimit.ι ((CategoryOfElements.π Y).leftOp ⋙ A)
      (Opposite.op { fst := J.unop.fst, snd := NatTrans.app f J.unop.fst J.unop.snd }) =
    colimit.ι ((CategoryOfElements.π Y).leftOp ⋙ A) (Opposite.op ((CategoryOfElements.map f).obj J.unop))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A✝ : C ⥤ ℰ
inst✝ : HasColimits ℰ
A : C
⊢ ∀ (s : Cocone (Functor.empty (Functor.Elements (yoneda.obj A)))) (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (Elements.initial A)).ι j ≫
        (fun s =>
            { val := s.pt.snd.op,
              property :=
                (_ : s.pt.snd.op.unop ≫ 𝟙 (asEmptyCocone (Elements.initial A)).pt.fst.unop = s.pt.snd.op.unop) })
          s =
      NatTrans.app s.ι j
[PROOFSTEP]
rintro s ⟨⟨⟩⟩
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A✝ : C ⥤ ℰ
inst✝ : HasColimits ℰ
A : C
s : Cocone (Functor.empty (Functor.Elements (yoneda.obj A)))
m : (asEmptyCocone (Elements.initial A)).pt ⟶ s.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone (Elements.initial A)).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s =>
        { val := s.pt.snd.op,
          property := (_ : s.pt.snd.op.unop ≫ 𝟙 (asEmptyCocone (Elements.initial A)).pt.fst.unop = s.pt.snd.op.unop) })
      s
[PROOFSTEP]
simp_rw [← m.2]
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A✝ : C ⥤ ℰ
inst✝ : HasColimits ℰ
A : C
s : Cocone (Functor.empty (Functor.Elements (yoneda.obj A)))
m : (asEmptyCocone (Elements.initial A)).pt ⟶ s.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone (Elements.initial A)).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    { val := ((yoneda.obj A).map (↑m) (asEmptyCocone (Elements.initial A)).pt.snd).op,
      property :=
        (_ :
          (fun f => (yoneda.obj A).map f (asEmptyCocone (Elements.initial A)).pt.snd = s.pt.snd)
            ((yoneda.obj A).map (↑m) (asEmptyCocone (Elements.initial A)).pt.snd).op) }
[PROOFSTEP]
dsimp [Elements.initial]
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A✝ : C ⥤ ℰ
inst✝ : HasColimits ℰ
A : C
s : Cocone (Functor.empty (Functor.Elements (yoneda.obj A)))
m : (asEmptyCocone (Elements.initial A)).pt ⟶ s.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone (Elements.initial A)).ι j ≫ m = NatTrans.app s.ι j
⊢ m = { val := 𝟙 (Opposite.op A) ≫ ↑m, property := (_ : (𝟙 (Opposite.op A) ≫ ↑m).unop ≫ 𝟙 A = s.pt.snd) }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (yoneda ⋙ extendAlongYoneda A).map f ≫
        ((fun X =>
              IsColimit.coconePointUniqueUpToIso (colimit.isColimit ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A))
                (colimitOfDiagramTerminal (terminalOpOfInitial (isInitial X))
                  ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)))
            Y).hom =
      ((fun X =>
              IsColimit.coconePointUniqueUpToIso (colimit.isColimit ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A))
                (colimitOfDiagramTerminal (terminalOpOfInitial (isInitial X))
                  ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)))
            X).hom ≫
        A.map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
⊢ (yoneda ⋙ extendAlongYoneda A).map f ≫
      ((fun X =>
            IsColimit.coconePointUniqueUpToIso (colimit.isColimit ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A))
              (colimitOfDiagramTerminal (terminalOpOfInitial (isInitial X))
                ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)))
          Y).hom =
    ((fun X =>
            IsColimit.coconePointUniqueUpToIso (colimit.isColimit ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A))
              (colimitOfDiagramTerminal (terminalOpOfInitial (isInitial X))
                ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)))
          X).hom ≫
      A.map f
[PROOFSTEP]
change (colimit.desc _ _ ≫ _) = colimit.desc _ _ ≫ _
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
⊢ colimit.desc ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)
        { pt := (fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y),
          ι :=
            (Iso.mk
                  (fun ι =>
                    { val := fun j => NatTrans.app ι j,
                      property :=
                        (_ :
                          ∀ {j j' : (Functor.Elements (yoneda.obj X))ᵒᵖ} (f : j ⟶ j'),
                            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫ (fun j => NatTrans.app ι j) j' =
                              (fun j => NatTrans.app ι j) j) })
                  fun p => NatTrans.mk fun j => ↑p j).inv
              (↑{ toFun := fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }),
                      invFun := fun τ =>
                        { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                          property :=
                            (_ :
                              ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                    (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                  (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) },
                      left_inv :=
                        (_ :
                          ∀
                            (x :
                              { p //
                                ∀ {j j' : (Functor.Elements (yoneda.obj X))ᵒᵖ} (f : j ⟶ j'),
                                  ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫ p j' = p j }),
                            (fun τ =>
                                  { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                    property :=
                                      (_ :
                                        ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                          ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                              (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                            (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                                ((fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })) x) =
                              x),
                      right_inv :=
                        (_ :
                          ∀
                            (x :
                              yoneda.obj X ⟶
                                (restrictedYoneda A).obj
                                  ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt)
                                    (yoneda.obj Y))),
                            (fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }))
                                ((fun τ =>
                                    { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                      property :=
                                        (_ :
                                          ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                              (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                                  x) =
                              x) }.symm
                (yoneda.map f ≫
                  ↑((fun P E => restrictYonedaHomEquiv A P E (colimit.isColimit ((CategoryOfElements.π P).leftOp ⋙ A)))
                        (yoneda.obj Y)
                        ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y)))
                    (𝟙 ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y))))) } ≫
      ((fun X =>
            IsColimit.coconePointUniqueUpToIso (colimit.isColimit ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A))
              (colimitOfDiagramTerminal (terminalOpOfInitial (isInitial X))
                ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)))
          Y).hom =
    colimit.desc ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)
        (coconeOfDiagramTerminal (terminalOpOfInitial (isInitial X))
          ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)) ≫
      A.map f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
j✝ : (Functor.Elements (yoneda.obj X))ᵒᵖ
⊢ colimit.ι ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A) j✝ ≫
      colimit.desc ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)
          { pt := (fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y),
            ι :=
              (Iso.mk
                    (fun ι =>
                      { val := fun j => NatTrans.app ι j,
                        property :=
                          (_ :
                            ∀ {j j' : (Functor.Elements (yoneda.obj X))ᵒᵖ} (f : j ⟶ j'),
                              ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                  (fun j => NatTrans.app ι j) j' =
                                (fun j => NatTrans.app ι j) j) })
                    fun p => NatTrans.mk fun j => ↑p j).inv
                (↑{ toFun := fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }),
                        invFun := fun τ =>
                          { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                            property :=
                              (_ :
                                ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                  ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                      (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                    (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) },
                        left_inv :=
                          (_ :
                            ∀
                              (x :
                                { p //
                                  ∀ {j j' : (Functor.Elements (yoneda.obj X))ᵒᵖ} (f : j ⟶ j'),
                                    ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫ p j' = p j }),
                              (fun τ =>
                                    { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                      property :=
                                        (_ :
                                          ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                              (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                                  ((fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })) x) =
                                x),
                        right_inv :=
                          (_ :
                            ∀
                              (x :
                                yoneda.obj X ⟶
                                  (restrictedYoneda A).obj
                                    ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt)
                                      (yoneda.obj Y))),
                              (fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }))
                                  ((fun τ =>
                                      { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                        property :=
                                          (_ :
                                            ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                              ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                                  (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                                    x) =
                                x) }.symm
                  (yoneda.map f ≫
                    ↑((fun P E =>
                            restrictYonedaHomEquiv A P E (colimit.isColimit ((CategoryOfElements.π P).leftOp ⋙ A)))
                          (yoneda.obj Y)
                          ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y)))
                      (𝟙 ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y))))) } ≫
        ((fun X =>
              IsColimit.coconePointUniqueUpToIso (colimit.isColimit ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A))
                (colimitOfDiagramTerminal (terminalOpOfInitial (isInitial X))
                  ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)))
            Y).hom =
    colimit.ι ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A) j✝ ≫
      colimit.desc ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)
          (coconeOfDiagramTerminal (terminalOpOfInitial (isInitial X))
            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)) ≫
        A.map f
[PROOFSTEP]
rw [colimit.ι_desc_assoc, colimit.ι_desc_assoc]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
j✝ : (Functor.Elements (yoneda.obj X))ᵒᵖ
⊢ NatTrans.app
        { pt := (fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y),
            ι :=
              (Iso.mk
                    (fun ι =>
                      { val := fun j => NatTrans.app ι j,
                        property :=
                          (_ :
                            ∀ {j j' : (Functor.Elements (yoneda.obj X))ᵒᵖ} (f : j ⟶ j'),
                              ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                  (fun j => NatTrans.app ι j) j' =
                                (fun j => NatTrans.app ι j) j) })
                    fun p => NatTrans.mk fun j => ↑p j).inv
                (↑{ toFun := fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }),
                        invFun := fun τ =>
                          { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                            property :=
                              (_ :
                                ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                  ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                      (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                    (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) },
                        left_inv :=
                          (_ :
                            ∀
                              (x :
                                { p //
                                  ∀ {j j' : (Functor.Elements (yoneda.obj X))ᵒᵖ} (f : j ⟶ j'),
                                    ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫ p j' = p j }),
                              (fun τ =>
                                    { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                      property :=
                                        (_ :
                                          ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                              (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                                  ((fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p })) x) =
                                x),
                        right_inv :=
                          (_ :
                            ∀
                              (x :
                                yoneda.obj X ⟶
                                  (restrictedYoneda A).obj
                                    ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt)
                                      (yoneda.obj Y))),
                              (fun k => NatTrans.mk fun c p => ↑k (Opposite.op { fst := c, snd := p }))
                                  ((fun τ =>
                                      { val := fun p => NatTrans.app τ p.unop.fst p.unop.snd,
                                        property :=
                                          (_ :
                                            ∀ (p p' : (Functor.Elements (yoneda.obj X))ᵒᵖ) (f : p ⟶ p'),
                                              ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A).map f ≫
                                                  (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p' =
                                                (fun p => NatTrans.app τ p.unop.fst p.unop.snd) p) })
                                    x) =
                                x) }.symm
                  (yoneda.map f ≫
                    ↑((fun P E =>
                            restrictYonedaHomEquiv A P E (colimit.isColimit ((CategoryOfElements.π P).leftOp ⋙ A)))
                          (yoneda.obj Y)
                          ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y)))
                      (𝟙 ((fun P => (colimit.cocone ((CategoryOfElements.π P).leftOp ⋙ A)).pt) (yoneda.obj Y))))) }.ι
        j✝ ≫
      ((fun X =>
            IsColimit.coconePointUniqueUpToIso (colimit.isColimit ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A))
              (colimitOfDiagramTerminal (terminalOpOfInitial (isInitial X))
                ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)))
          Y).hom =
    NatTrans.app
        (coconeOfDiagramTerminal (terminalOpOfInitial (isInitial X))
            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)).ι
        j✝ ≫
      A.map f
[PROOFSTEP]
change (colimit.ι _ _ ≫ 𝟙 _) ≫ colimit.desc _ _ = _
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
j✝ : (Functor.Elements (yoneda.obj X))ᵒᵖ
⊢ (colimit.ι (Opposite.op ((CategoryOfElements.π (yoneda.obj Y)).leftOp ⋙ A)).unop
          (Opposite.op { fst := j✝.unop.fst, snd := NatTrans.app (yoneda.map f) j✝.unop.fst j✝.unop.snd }) ≫
        𝟙 (colimit (Opposite.op ((CategoryOfElements.π (yoneda.obj Y)).leftOp ⋙ A)).unop)) ≫
      colimit.desc (Opposite.op ((CategoryOfElements.π (yoneda.obj Y)).leftOp ⋙ A)).unop
        (coconeOfDiagramTerminal (terminalOpOfInitial (isInitial Y))
          ((CategoryOfElements.π (yoneda.obj Y)).leftOp ⋙ A)) =
    NatTrans.app
        (coconeOfDiagramTerminal (terminalOpOfInitial (isInitial X))
            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)).ι
        j✝ ≫
      A.map f
[PROOFSTEP]
rw [comp_id, colimit.ι_desc]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
j✝ : (Functor.Elements (yoneda.obj X))ᵒᵖ
⊢ NatTrans.app
      (coconeOfDiagramTerminal (terminalOpOfInitial (isInitial Y)) ((CategoryOfElements.π (yoneda.obj Y)).leftOp ⋙ A)).ι
      (Opposite.op { fst := j✝.unop.fst, snd := NatTrans.app (yoneda.map f) j✝.unop.fst j✝.unop.snd }) =
    NatTrans.app
        (coconeOfDiagramTerminal (terminalOpOfInitial (isInitial X))
            ((CategoryOfElements.π (yoneda.obj X)).leftOp ⋙ A)).ι
        j✝ ≫
      A.map f
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
j✝ : (Functor.Elements (yoneda.obj X))ᵒᵖ
⊢ A.map
      (↑(IsTerminal.from (terminalOpOfInitial (isInitial Y))
              (Opposite.op { fst := j✝.unop.fst, snd := j✝.unop.snd ≫ f })).unop).unop =
    A.map (↑(IsTerminal.from (terminalOpOfInitial (isInitial X)) j✝).unop).unop ≫ A.map f
[PROOFSTEP]
rw [← A.map_comp]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : C
f : X ⟶ Y
j✝ : (Functor.Elements (yoneda.obj X))ᵒᵖ
⊢ A.map
      (↑(IsTerminal.from (terminalOpOfInitial (isInitial Y))
              (Opposite.op { fst := j✝.unop.fst, snd := j✝.unop.snd ≫ f })).unop).unop =
    A.map ((↑(IsTerminal.from (terminalOpOfInitial (isInitial X)) j✝).unop).unop ≫ f)
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre (Lan.diagram yoneda A X) eq.functor ≫ colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) eq.inverse =
    𝟙 ((extendAlongYoneda A).obj X)
[PROOFSTEP]
erw [colimit.pre_pre ((CategoryOfElements.π X).leftOp ⋙ A) eq.inverse]
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) (eq.functor ⋙ eq.inverse) = 𝟙 ((extendAlongYoneda A).obj X)
[PROOFSTEP]
trans colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) (𝟭 _)
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) (eq.functor ⋙ eq.inverse) =
    colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) (𝟭 (Functor.Elements X)ᵒᵖ)
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) (𝟭 (Functor.Elements X)ᵒᵖ) = 𝟙 ((extendAlongYoneda A).obj X)
[PROOFSTEP]
congr
[GOAL]
case h.e_9.h
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ eq.functor ⋙ eq.inverse = 𝟭 (Functor.Elements X)ᵒᵖ
[PROOFSTEP]
exact congr_arg Functor.op (CategoryOfElements.from_toCostructuredArrow_eq X)
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) (𝟭 (Functor.Elements X)ᵒᵖ) = 𝟙 ((extendAlongYoneda A).obj X)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
j✝ : (Functor.Elements X)ᵒᵖ
⊢ colimit.ι (𝟭 (Functor.Elements X)ᵒᵖ ⋙ (CategoryOfElements.π X).leftOp ⋙ A) j✝ ≫
      colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) (𝟭 (Functor.Elements X)ᵒᵖ) =
    colimit.ι (𝟭 (Functor.Elements X)ᵒᵖ ⋙ (CategoryOfElements.π X).leftOp ⋙ A) j✝ ≫ 𝟙 ((extendAlongYoneda A).obj X)
[PROOFSTEP]
simp only [colimit.ι_pre]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
j✝ : (Functor.Elements X)ᵒᵖ
⊢ colimit.ι ((CategoryOfElements.π X).leftOp ⋙ A) ((𝟭 (Functor.Elements X)ᵒᵖ).obj j✝) =
    colimit.ι (𝟭 (Functor.Elements X)ᵒᵖ ⋙ (CategoryOfElements.π X).leftOp ⋙ A) j✝ ≫ 𝟙 ((extendAlongYoneda A).obj X)
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
j✝ : (Functor.Elements X)ᵒᵖ
⊢ colimit.ι ((CategoryOfElements.π X).leftOp ⋙ A) ((𝟭 (Functor.Elements X)ᵒᵖ).obj j✝) =
    colimit.ι (𝟭 (Functor.Elements X)ᵒᵖ ⋙ (CategoryOfElements.π X).leftOp ⋙ A) j✝
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre ((CategoryOfElements.π X).leftOp ⋙ A) eq.inverse ≫ colimit.pre (Lan.diagram yoneda A X) eq.functor =
    𝟙 (((lan yoneda).obj A).obj X)
[PROOFSTEP]
erw [colimit.pre_pre (Lan.diagram (yoneda : C ⥤ _ ⥤ Type u₁) A X) eq.functor]
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre (Lan.diagram yoneda A X) (eq.inverse ⋙ eq.functor) = 𝟙 (((lan yoneda).obj A).obj X)
[PROOFSTEP]
trans colimit.pre (Lan.diagram (yoneda : C ⥤ _ ⥤ Type u₁) A X) (𝟭 _)
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre (Lan.diagram yoneda A X) (eq.inverse ⋙ eq.functor) =
    colimit.pre (Lan.diagram yoneda A X) (𝟭 (CostructuredArrow yoneda X))
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre (Lan.diagram yoneda A X) (𝟭 (CostructuredArrow yoneda X)) = 𝟙 (((lan yoneda).obj A).obj X)
[PROOFSTEP]
congr
[GOAL]
case h.e_9.h
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ eq.inverse ⋙ eq.functor = 𝟭 (CostructuredArrow yoneda X)
[PROOFSTEP]
exact CategoryOfElements.to_fromCostructuredArrow_eq X
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
⊢ colimit.pre (Lan.diagram yoneda A X) (𝟭 (CostructuredArrow yoneda X)) = 𝟙 (((lan yoneda).obj A).obj X)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
j✝ : CostructuredArrow yoneda X
⊢ colimit.ι (𝟭 (CostructuredArrow yoneda X) ⋙ Lan.diagram yoneda A X) j✝ ≫
      colimit.pre (Lan.diagram yoneda A X) (𝟭 (CostructuredArrow yoneda X)) =
    colimit.ι (𝟭 (CostructuredArrow yoneda X) ⋙ Lan.diagram yoneda A X) j✝ ≫ 𝟙 (((lan yoneda).obj A).obj X)
[PROOFSTEP]
simp only [colimit.ι_pre]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
j✝ : CostructuredArrow yoneda X
⊢ colimit.ι (Lan.diagram yoneda A X) ((𝟭 (CostructuredArrow yoneda X)).obj j✝) =
    colimit.ι (𝟭 (CostructuredArrow yoneda X) ⋙ Lan.diagram yoneda A X) j✝ ≫ 𝟙 (((lan yoneda).obj A).obj X)
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
case w
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X : Cᵒᵖ ⥤ Type u₁
eq : (Functor.Elements X)ᵒᵖ ≌ CostructuredArrow yoneda X := CategoryOfElements.costructuredArrowYonedaEquivalence X
j✝ : CostructuredArrow yoneda X
⊢ colimit.ι (Lan.diagram yoneda A X) ((𝟭 (CostructuredArrow yoneda X)).obj j✝) =
    colimit.ι (𝟭 (CostructuredArrow yoneda X) ⋙ Lan.diagram yoneda A X) j✝
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
⊢ ∀ {X Y : Cᵒᵖ ⥤ Type u₁} (f : X ⟶ Y),
    (extendAlongYoneda A).map f ≫ (extendAlongYonedaIsoKanApp A Y).hom =
      (extendAlongYonedaIsoKanApp A X).hom ≫ ((lan yoneda).obj A).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ (extendAlongYoneda A).map f ≫ (extendAlongYonedaIsoKanApp A Y).hom =
    (extendAlongYonedaIsoKanApp A X).hom ≫ ((lan yoneda).obj A).map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ (extendAlongYoneda A).map f ≫
      colimit.pre (Lan.diagram yoneda A Y) (CategoryOfElements.costructuredArrowYonedaEquivalence Y).functor =
    colimit.pre (Lan.diagram yoneda A X) (CategoryOfElements.costructuredArrowYonedaEquivalence X).functor ≫
      colimit.pre (Lan.diagram yoneda A Y) (CostructuredArrow.map f)
[PROOFSTEP]
rw [extendAlongYoneda_map]
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ colimit.pre ((CategoryOfElements.π Y).leftOp ⋙ A) (CategoryOfElements.map f).op ≫
      colimit.pre (Lan.diagram yoneda A Y) (CategoryOfElements.costructuredArrowYonedaEquivalence Y).functor =
    colimit.pre (Lan.diagram yoneda A X) (CategoryOfElements.costructuredArrowYonedaEquivalence X).functor ≫
      colimit.pre (Lan.diagram yoneda A Y) (CostructuredArrow.map f)
[PROOFSTEP]
erw [colimit.pre_pre (Lan.diagram (yoneda : C ⥤ _ ⥤ Type u₁) A Y) (CostructuredArrow.map f)]
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ colimit.pre ((CategoryOfElements.π Y).leftOp ⋙ A) (CategoryOfElements.map f).op ≫
      colimit.pre (Lan.diagram yoneda A Y) (CategoryOfElements.costructuredArrowYonedaEquivalence Y).functor =
    colimit.pre (Lan.diagram yoneda A Y)
      ((CategoryOfElements.costructuredArrowYonedaEquivalence X).functor ⋙ CostructuredArrow.map f)
[PROOFSTEP]
erw [colimit.pre_pre (Lan.diagram (yoneda : C ⥤ _ ⥤ Type u₁) A Y)
    (CategoryOfElements.costructuredArrowYonedaEquivalence Y).functor]
[GOAL]
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ colimit.pre (Lan.diagram yoneda A Y)
      ((CategoryOfElements.map f).op ⋙ (CategoryOfElements.costructuredArrowYonedaEquivalence Y).functor) =
    colimit.pre (Lan.diagram yoneda A Y)
      ((CategoryOfElements.costructuredArrowYonedaEquivalence X).functor ⋙ CostructuredArrow.map f)
[PROOFSTEP]
congr 1
[GOAL]
case h.e_9.h
C : Type u₁
inst✝² : SmallCategory C
ℰ : Type u₂
inst✝¹ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : HasColimits ℰ
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ (CategoryOfElements.map f).op ⋙ (CategoryOfElements.costructuredArrowYonedaEquivalence Y).functor =
    (CategoryOfElements.costructuredArrowYonedaEquivalence X).functor ⋙ CostructuredArrow.map f
[PROOFSTEP]
apply CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
α : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
⊢ NatTrans.app (coconeOfRepresentable P₁).ι j ≫ α =
    NatTrans.app (coconeOfRepresentable P₂).ι ((CategoryOfElements.map α).op.obj j)
[PROOFSTEP]
ext T f
[GOAL]
case w.h.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
α : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
T : Cᵒᵖ
f : ((functorToRepresentables P₁).obj j).obj T
⊢ NatTrans.app (NatTrans.app (coconeOfRepresentable P₁).ι j ≫ α) T f =
    NatTrans.app (NatTrans.app (coconeOfRepresentable P₂).ι ((CategoryOfElements.map α).op.obj j)) T f
[PROOFSTEP]
simpa [coconeOfRepresentable_ι_app] using FunctorToTypes.naturality _ _ α f.op _
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
⊢ IsColimit (coconeOfRepresentable P)
[PROOFSTEP]
suffices IsIso (IsColimit.desc (colimit.isColimit (functorToRepresentables P)) (coconeOfRepresentable P)) by
  apply IsColimit.ofPointIso (colimit.isColimit (functorToRepresentables P))
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
this : IsIso (IsColimit.desc (colimit.isColimit (functorToRepresentables P)) (coconeOfRepresentable P))
⊢ IsColimit (coconeOfRepresentable P)
[PROOFSTEP]
apply IsColimit.ofPointIso (colimit.isColimit (functorToRepresentables P))
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
⊢ IsIso (IsColimit.desc (colimit.isColimit (functorToRepresentables P)) (coconeOfRepresentable P))
[PROOFSTEP]
change IsIso (colimit.desc _ (Cocone.extend _ _))
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
⊢ IsIso
    (colimit.desc (functorToRepresentables P)
      (Cocone.extend (colimit.cocone (functorToRepresentables P)) (NatTrans.app extendAlongYonedaYoneda.hom P)))
[PROOFSTEP]
rw [colimit.desc_extend, colimit.desc_cocone]
[GOAL]
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
⊢ IsIso (𝟙 (colimit (functorToRepresentables P)) ≫ NatTrans.app extendAlongYonedaYoneda.hom P)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
⊢ L₁ ≅ L₂
[PROOFSTEP]
apply NatIso.ofComponents _ _
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
⊢ (X : Cᵒᵖ ⥤ Type u₁) → L₁.obj X ≅ L₂.obj X
[PROOFSTEP]
intro P
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P : Cᵒᵖ ⥤ Type u₁
⊢ L₁.obj P ≅ L₂.obj P
[PROOFSTEP]
refine'
  (isColimitOfPreserves L₁ (colimitOfRepresentable P)).coconePointsIsoOfNatIso
    (isColimitOfPreserves L₂ (colimitOfRepresentable P)) _
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P : Cᵒᵖ ⥤ Type u₁
⊢ functorToRepresentables P ⋙ L₁ ≅ functorToRepresentables P ⋙ L₂
[PROOFSTEP]
apply Functor.associator _ _ _ ≪≫ _
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P : Cᵒᵖ ⥤ Type u₁
⊢ (CategoryOfElements.π P).leftOp ⋙ yoneda ⋙ L₁ ≅ functorToRepresentables P ⋙ L₂
[PROOFSTEP]
exact isoWhiskerLeft (CategoryOfElements.π P).leftOp h
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
⊢ ∀ {X Y : Cᵒᵖ ⥤ Type u₁} (f : X ⟶ Y),
    L₁.map f ≫
        (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable Y))
            (isColimitOfPreserves L₂ (colimitOfRepresentable Y))
            (Functor.associator (CategoryOfElements.π Y).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π Y).leftOp h)).hom =
      (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable X))
            (isColimitOfPreserves L₂ (colimitOfRepresentable X))
            (Functor.associator (CategoryOfElements.π X).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π X).leftOp h)).hom ≫
        L₂.map f
[PROOFSTEP]
intro P₁ P₂ f
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
⊢ L₁.map f ≫
      (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₂))
          (isColimitOfPreserves L₂ (colimitOfRepresentable P₂))
          (Functor.associator (CategoryOfElements.π P₂).leftOp yoneda L₁ ≪≫
            isoWhiskerLeft (CategoryOfElements.π P₂).leftOp h)).hom =
    (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₁))
          (isColimitOfPreserves L₂ (colimitOfRepresentable P₁))
          (Functor.associator (CategoryOfElements.π P₁).leftOp yoneda L₁ ≪≫
            isoWhiskerLeft (CategoryOfElements.π P₁).leftOp h)).hom ≫
      L₂.map f
[PROOFSTEP]
apply (isColimitOfPreserves L₁ (colimitOfRepresentable P₁)).hom_ext
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
⊢ ∀ (j : (Functor.Elements P₁)ᵒᵖ),
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
        L₁.map f ≫
          (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₂))
              (isColimitOfPreserves L₂ (colimitOfRepresentable P₂))
              (Functor.associator (CategoryOfElements.π P₂).leftOp yoneda L₁ ≪≫
                isoWhiskerLeft (CategoryOfElements.π P₂).leftOp h)).hom =
      NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
        (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₁))
              (isColimitOfPreserves L₂ (colimitOfRepresentable P₁))
              (Functor.associator (CategoryOfElements.π P₁).leftOp yoneda L₁ ≪≫
                isoWhiskerLeft (CategoryOfElements.π P₁).leftOp h)).hom ≫
          L₂.map f
[PROOFSTEP]
intro j
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
⊢ NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
      L₁.map f ≫
        (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₂))
            (isColimitOfPreserves L₂ (colimitOfRepresentable P₂))
            (Functor.associator (CategoryOfElements.π P₂).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π P₂).leftOp h)).hom =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
      (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₁))
            (isColimitOfPreserves L₂ (colimitOfRepresentable P₁))
            (Functor.associator (CategoryOfElements.π P₁).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π P₁).leftOp h)).hom ≫
        L₂.map f
[PROOFSTEP]
dsimp only [id.def, IsColimit.comp_coconePointsIsoOfNatIso_hom, isoWhiskerLeft_hom]
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
⊢ NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
      L₁.map f ≫
        (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₂))
            (isColimitOfPreserves L₂ (colimitOfRepresentable P₂))
            (Functor.associator (CategoryOfElements.π P₂).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π P₂).leftOp h)).hom =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
      (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₁))
            (isColimitOfPreserves L₂ (colimitOfRepresentable P₁))
            (Functor.associator (CategoryOfElements.π P₁).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π P₁).leftOp h)).hom ≫
        L₂.map f
[PROOFSTEP]
have :
  (L₁.mapCocone (coconeOfRepresentable P₁)).ι.app j ≫ L₁.map f =
    (L₁.mapCocone (coconeOfRepresentable P₂)).ι.app ((CategoryOfElements.map f).op.obj j) :=
  by
  dsimp
  rw [← L₁.map_comp, coconeOfRepresentable_naturality]
  rfl
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
⊢ NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫ L₁.map f =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₂)).ι ((CategoryOfElements.map f).op.obj j)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
⊢ L₁.map (NatTrans.app (coconeOfRepresentable P₁).ι j) ≫ L₁.map f =
    L₁.map (NatTrans.app (coconeOfRepresentable P₂).ι (Opposite.op ((CategoryOfElements.map f).obj j.unop)))
[PROOFSTEP]
rw [← L₁.map_comp, coconeOfRepresentable_naturality]
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
⊢ L₁.map (NatTrans.app (coconeOfRepresentable P₂).ι ((CategoryOfElements.map f).op.obj j)) =
    L₁.map (NatTrans.app (coconeOfRepresentable P₂).ι (Opposite.op ((CategoryOfElements.map f).obj j.unop)))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
this :
  NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫ L₁.map f =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₂)).ι ((CategoryOfElements.map f).op.obj j)
⊢ NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
      L₁.map f ≫
        (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₂))
            (isColimitOfPreserves L₂ (colimitOfRepresentable P₂))
            (Functor.associator (CategoryOfElements.π P₂).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π P₂).leftOp h)).hom =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫
      (IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves L₁ (colimitOfRepresentable P₁))
            (isColimitOfPreserves L₂ (colimitOfRepresentable P₁))
            (Functor.associator (CategoryOfElements.π P₁).leftOp yoneda L₁ ≪≫
              isoWhiskerLeft (CategoryOfElements.π P₁).leftOp h)).hom ≫
        L₂.map f
[PROOFSTEP]
erw [reassoc_of% this, IsColimit.ι_map_assoc, IsColimit.ι_map]
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
this :
  NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫ L₁.map f =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₂)).ι ((CategoryOfElements.map f).op.obj j)
⊢ NatTrans.app
        (Functor.associator (CategoryOfElements.π P₂).leftOp yoneda L₁ ≪≫
            isoWhiskerLeft (CategoryOfElements.π P₂).leftOp h).hom
        ((CategoryOfElements.map f).op.obj j) ≫
      NatTrans.app (L₂.mapCocone (coconeOfRepresentable P₂)).ι ((CategoryOfElements.map f).op.obj j) =
    NatTrans.app
        (Functor.associator (CategoryOfElements.π P₁).leftOp yoneda L₁ ≪≫
            isoWhiskerLeft (CategoryOfElements.π P₁).leftOp h).hom
        j ≫
      NatTrans.app (L₂.mapCocone (coconeOfRepresentable P₁)).ι j ≫ L₂.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
this :
  NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫ L₁.map f =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₂)).ι ((CategoryOfElements.map f).op.obj j)
⊢ (𝟙 (L₁.obj (yoneda.obj j.unop.fst.unop)) ≫ NatTrans.app h.hom j.unop.fst.unop) ≫
      L₂.map (NatTrans.app (coconeOfRepresentable P₂).ι (Opposite.op ((CategoryOfElements.map f).obj j.unop))) =
    (𝟙 (L₁.obj (yoneda.obj j.unop.fst.unop)) ≫ NatTrans.app h.hom j.unop.fst.unop) ≫
      L₂.map (NatTrans.app (coconeOfRepresentable P₁).ι j) ≫ L₂.map f
[PROOFSTEP]
rw [← L₂.map_comp, coconeOfRepresentable_naturality]
[GOAL]
C : Type u₁
inst✝³ : SmallCategory C
ℰ : Type u₂
inst✝² : Category.{u₁, u₂} ℰ
A : C ⥤ ℰ
L₁ L₂ : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ
inst✝¹ : PreservesColimits L₁
inst✝ : PreservesColimits L₂
h : yoneda ⋙ L₁ ≅ yoneda ⋙ L₂
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
f : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
this :
  NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₁)).ι j ≫ L₁.map f =
    NatTrans.app (L₁.mapCocone (coconeOfRepresentable P₂)).ι ((CategoryOfElements.map f).op.obj j)
⊢ (𝟙 (L₁.obj (yoneda.obj j.unop.fst.unop)) ≫ NatTrans.app h.hom j.unop.fst.unop) ≫
      L₂.map (NatTrans.app (coconeOfRepresentable P₂).ι (Opposite.op ((CategoryOfElements.map f).obj j.unop))) =
    (𝟙 (L₁.obj (yoneda.obj j.unop.fst.unop)) ≫ NatTrans.app h.hom j.unop.fst.unop) ≫
      L₂.map (NatTrans.app (coconeOfRepresentable P₂).ι ((CategoryOfElements.map f).op.obj j))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
⊢ (tautologicalCocone P).pt ⟶ s.pt
[PROOFSTEP]
refine' ⟨fun X t => yonedaEquiv (s.ι.app (CostructuredArrow.mk (yonedaEquiv.symm t))), _⟩
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    (tautologicalCocone P).pt.map f ≫
        (fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) Y =
      (fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) X ≫ s.pt.map f
[PROOFSTEP]
intros X Y f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (tautologicalCocone P).pt.map f ≫
      (fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) Y =
    (fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) X ≫ s.pt.map f
[PROOFSTEP]
ext t
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
X Y : Cᵒᵖ
f : X ⟶ Y
t : (tautologicalCocone P).pt.obj X
⊢ ((tautologicalCocone P).pt.map f ≫
        (fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) Y)
      t =
    ((fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) X ≫ s.pt.map f) t
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
X Y : Cᵒᵖ
f : X ⟶ Y
t : (tautologicalCocone P).pt.obj X
⊢ ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm (P.map f t)))) =
    s.pt.map f (↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t))))
[PROOFSTEP]
rw [yonedaEquiv_naturality', yonedaEquiv_symm_map]
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
X Y : Cᵒᵖ
f : X ⟶ Y
t : (tautologicalCocone P).pt.obj X
⊢ ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (yoneda.map f.unop ≫ ↑yonedaEquiv.symm t))) =
    ↑yonedaEquiv (yoneda.map f.unop ≫ NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))
[PROOFSTEP]
simpa using (s.ι.naturality (CostructuredArrow.homMk' (CostructuredArrow.mk (yonedaEquiv.symm t)) f.unop)).symm
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)) (j : CostructuredArrow yoneda P),
    NatTrans.app (tautologicalCocone P).ι j ≫
        (fun s => NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t))))
          s =
      NatTrans.app s.ι j
[PROOFSTEP]
intro s t
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
t : CostructuredArrow yoneda P
⊢ NatTrans.app (tautologicalCocone P).ι t ≫
      (fun s => NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) s =
    NatTrans.app s.ι t
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
t : CostructuredArrow yoneda P
⊢ (t.hom ≫ NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) =
    NatTrans.app s.ι t
[PROOFSTEP]
apply yonedaEquiv.injective
[GOAL]
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
t : CostructuredArrow yoneda P
⊢ ↑yonedaEquiv
      (t.hom ≫ NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) =
    ↑yonedaEquiv (NatTrans.app s.ι t)
[PROOFSTEP]
rw [yonedaEquiv_comp]
[GOAL]
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
t : CostructuredArrow yoneda P
⊢ NatTrans.app (NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t))))
      (Opposite.op t.left) (↑yonedaEquiv t.hom) =
    ↑yonedaEquiv (NatTrans.app s.ι t)
[PROOFSTEP]
dsimp only
[GOAL]
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
t : CostructuredArrow yoneda P
⊢ ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm (↑yonedaEquiv t.hom)))) =
    ↑yonedaEquiv (NatTrans.app s.ι t)
[PROOFSTEP]
rw [Equiv.symm_apply_apply]
[GOAL]
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
t : CostructuredArrow yoneda P
⊢ ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk t.hom)) = ↑yonedaEquiv (NatTrans.app s.ι t)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)) (m : (tautologicalCocone P).pt ⟶ s.pt),
    (∀ (j : CostructuredArrow yoneda P), NatTrans.app (tautologicalCocone P).ι j ≫ m = NatTrans.app s.ι j) →
      m =
        (fun s => NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) s
[PROOFSTEP]
intro s j h
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
j : (tautologicalCocone P).pt ⟶ s.pt
h : ∀ (j_1 : CostructuredArrow yoneda P), NatTrans.app (tautologicalCocone P).ι j_1 ≫ j = NatTrans.app s.ι j_1
⊢ j = (fun s => NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) s
[PROOFSTEP]
ext V x
[GOAL]
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
j : (tautologicalCocone P).pt ⟶ s.pt
h : ∀ (j_1 : CostructuredArrow yoneda P), NatTrans.app (tautologicalCocone P).ι j_1 ≫ j = NatTrans.app s.ι j_1
V : Cᵒᵖ
x : (tautologicalCocone P).pt.obj V
⊢ NatTrans.app j V x =
    NatTrans.app
      ((fun s => NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) s)
      V x
[PROOFSTEP]
obtain ⟨t, rfl⟩ := yonedaEquiv.surjective x
[GOAL]
case w.h.h.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
j : (tautologicalCocone P).pt ⟶ s.pt
h : ∀ (j_1 : CostructuredArrow yoneda P), NatTrans.app (tautologicalCocone P).ι j_1 ≫ j = NatTrans.app s.ι j_1
V : Cᵒᵖ
t : yoneda.obj V.unop ⟶ (tautologicalCocone P).pt
⊢ NatTrans.app j V (↑yonedaEquiv t) =
    NatTrans.app
      ((fun s => NatTrans.mk fun X t => ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm t)))) s)
      V (↑yonedaEquiv t)
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
j : (tautologicalCocone P).pt ⟶ s.pt
h : ∀ (j_1 : CostructuredArrow yoneda P), NatTrans.app (tautologicalCocone P).ι j_1 ≫ j = NatTrans.app s.ι j_1
V : Cᵒᵖ
t : yoneda.obj V.unop ⟶ (tautologicalCocone P).pt
⊢ NatTrans.app j V (↑yonedaEquiv t) =
    ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk (↑yonedaEquiv.symm (↑yonedaEquiv t))))
[PROOFSTEP]
rw [Equiv.symm_apply_apply, ← yonedaEquiv_comp']
[GOAL]
case w.h.h.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type v₁
s : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
j : (tautologicalCocone P).pt ⟶ s.pt
h : ∀ (j_1 : CostructuredArrow yoneda P), NatTrans.app (tautologicalCocone P).ι j_1 ≫ j = NatTrans.app s.ι j_1
V : Cᵒᵖ
t : yoneda.obj V.unop ⟶ (tautologicalCocone P).pt
⊢ ↑yonedaEquiv (t ≫ j) = ↑yonedaEquiv (NatTrans.app s.ι (CostructuredArrow.mk t))
[PROOFSTEP]
exact congr_arg _ (h (CostructuredArrow.mk t))


[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
J✝ : Type w
inst✝³ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝² : PreservesFiniteLimits F
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
apply preservesLimitsOfShapeOfEquiv (FinCategory.equivAsType J)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
haveI := preservesSmallestLimitsOfPreservesLimits F
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
exact preservesLimitsOfShapeOfEquiv (FinCategory.equivAsType J) F
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
letI : Category (ULiftHom (ULift J)) := ULiftHom.category
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : Category.{?u.3382, ?u.3380} (ULiftHom (ULift J)) := ULiftHom.category
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this✝ : Category.{?u.3382, ?u.3380} (ULiftHom (ULift J)) := ULiftHom.category
this : PreservesLimitsOfShape (ULiftHom (ULift J)) F
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
exact preservesLimitsOfShapeOfEquiv (ULiftHomULiftCategory.equiv J).symm F
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
⊢ PreservesLimitsOfShape x✝² (𝟭 C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J : Type w
inst✝² : SmallCategory J
K : J ⥤ C
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteLimits G
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
⊢ PreservesLimitsOfShape x✝² (F ⋙ G)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
J✝ : Type w
inst✝³ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝² : PreservesFiniteColimits F
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
apply preservesColimitsOfShapeOfEquiv (FinCategory.equivAsType J)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
haveI := preservesSmallestColimitsOfPreservesColimits F
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
exact preservesColimitsOfShapeOfEquiv (FinCategory.equivAsType J) F
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
letI : Category (ULiftHom (ULift J)) := ULiftHom.category
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : Category.{?u.13228, ?u.13226} (ULiftHom (ULift J)) := ULiftHom.category
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this✝ : Category.{?u.13228, ?u.13226} (ULiftHom (ULift J)) := ULiftHom.category
this : PreservesColimitsOfShape (ULiftHom (ULift J)) F
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
exact preservesColimitsOfShapeOfEquiv (ULiftHomULiftCategory.equiv J).symm F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J : Type w
inst✝² : SmallCategory J
K : J ⥤ C
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesFiniteColimits F
inst✝ : PreservesFiniteColimits G
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
⊢ PreservesColimitsOfShape x✝² (F ⋙ G)
[PROOFSTEP]
infer_instance


[GOAL]
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : {X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PreservesLimit (cospan f g) L
inst✝ : {X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ L.map (factorThruImage f) ≫ L.map (image.ι f) = L.map f
[PROOFSTEP]
rw [← L.map_comp, Limits.image.fac]
[GOAL]
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : {X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PreservesLimit (cospan f g) L
inst✝ : {X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ factorThruImage (L.map f) ≫ (iso L f).hom = L.map (factorThruImage f)
[PROOFSTEP]
simp
[GOAL]
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : {X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PreservesLimit (cospan f g) L
inst✝ : {X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ (iso L f).hom ≫ L.map (image.ι f) = image.ι (L.map f)
[PROOFSTEP]
rw [iso_hom, image.lift_fac]
[GOAL]
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : {X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PreservesLimit (cospan f g) L
inst✝ : {X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ (iso L f).inv ≫ image.ι (L.map f) = L.map (image.ι f)
[PROOFSTEP]
simp