J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
⊢ { pt := Y, ι := h.hom.app Y { down := f } } = { pt := Y, ι := h.hom.app X { down := 𝟙 X } ≫ (const J).map f }
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
⊢ coconeOfHom h f = Cocone.extend (colimitCocone h) f
dsimp [coconeOfHom, colimitCocone, Cocone.extend]
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
⊢ { pt := Y, ι := h.hom.app Y { down := f } } = { pt := Y, ι := h.hom.app X { down := 𝟙 X } ≫ (const J).map f }
congr with j
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t :
  ((coyoneda.obj X.op ⋙ uliftFunctor).map f ≫ h.hom.app Y) { down := 𝟙 X } =
    (h.hom.app X ≫ (Functor.cocones F).map f) { down := 𝟙 X }
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
have t := congrFun (h.hom.naturality f) ⟨𝟙 X⟩
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := 𝟙 X ≫ f } = (Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t :
  ((coyoneda.obj X.op ⋙ uliftFunctor).map f ≫ h.hom.app Y) { down := 𝟙 X } =
    (h.hom.app X ≫ (Functor.cocones F).map f) { down := 𝟙 X }
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
dsimp at t
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = (Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := 𝟙 X ≫ f } = (Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
simp only [id_comp] at t
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = (Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })
⊢ ((Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })).app j =
    (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = (Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
rw [congrFun (congrArg NatTrans.app t) j]
no goals
case e_ι.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = (Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })
⊢ ((Functor.cocones F).map f (h.hom.app X { down := 𝟙 X })).app j =
    (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
rfl