Lean4
/-- Naturally in `X`, we have `Hom(YX, colim_i Fi) ≅ colim_i Hom(YX, Fi)`. -/
noncomputable def yonedaYonedaColimit : yoneda.op ⋙ yoneda.obj (colimit F) ≅ yoneda.op ⋙ colimit (F ⋙ yoneda) :=
calc
yoneda.op ⋙ yoneda.obj (colimit F) ≅ colimit F ⋙ uliftFunctor.{u₁} := yonedaOpCompYonedaObj (colimit F)
_ ≅ F.flip ⋙ colim ⋙ uliftFunctor.{u₁} := (isoWhiskerRight (colimitIsoFlipCompColim F) uliftFunctor.{u₁})
_ ≅ F.flip ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ⋙ colim :=
(isoWhiskerLeft F.flip (preservesColimitNatIso uliftFunctor.{u₁}))
_ ≅ (yoneda.op ⋙ coyoneda ⋙ (whiskeringLeft _ _ _).obj F) ⋙ colim :=
(isoWhiskerRight (isoWhiskerRight largeCurriedYonedaLemma.symm ((whiskeringLeft _ _ _).obj F)) colim)
_ ≅ yoneda.op ⋙ colimit (F ⋙ yoneda) := isoWhiskerLeft yoneda.op (colimitIsoFlipCompColim (F ⋙ yoneda)).symm
