Lean4
/-- (implementation) Pulling out a colimit out of a hom functor is one half of the key lemma. Note
that all of the heavy lifting actually happens in `CostructuredArrow.toOverCompYonedaColimit`
and `yonedaYonedaColimit`. -/
noncomputable def compYonedaColimitIsoColimitCompYoneda :
𝒢 ⋙ yoneda.obj (colimit H) ≅ colimit (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢) :=
calc
𝒢 ⋙ yoneda.obj (colimit H) ≅ 𝒢 ⋙ colimit (H ⋙ yoneda) := isoWhiskerLeft G.op (toOverCompYonedaColimit H)
_ ≅ 𝒢 ⋙ (H ⋙ yoneda).flip ⋙ colim := (isoWhiskerLeft _ (colimitIsoFlipCompColim _))
_ ≅ (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢).flip ⋙ colim := (Iso.refl _)
_ ≅ colimit (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢) := (colimitIsoFlipCompColim _).symm
