C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k ≫ (preservesColimitIso ((evaluation K C).obj k) F).hom =
    colimit.ι (F ⋙ (evaluation K C).obj k) j
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k ≫ (colimitObjIsoColimitCompEvaluation F k).hom = colimit.ι (F ⋙ (evaluation K C).obj k) j
dsimp [colimitObjIsoColimitCompEvaluation]
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k =
    colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k ≫ (preservesColimitIso ((evaluation K C).obj k) F).hom =
    colimit.ι (F ⋙ (evaluation K C).obj k) j
rw [← Iso.eq_comp_inv]
no goals
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k =
    colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv
simp