Lean4
/-- Computing ind-lims in `Ind C` is the same as computing them in `Cᵒᵖ ⥤ Type v`. -/
noncomputable def limCompInclusion {I : Type v} [SmallCategory I] [IsFiltered I] :
Ind.lim I ⋙ Ind.inclusion C ≅ (whiskeringRight _ _ _).obj yoneda ⋙ colim :=
calc
Ind.lim I ⋙ Ind.inclusion C ≅ (whiskeringRight _ _ _).obj Ind.yoneda ⋙ colim ⋙ Ind.inclusion C :=
Functor.associator _ _ _
_ ≅ (whiskeringRight _ _ _).obj Ind.yoneda ⋙ (whiskeringRight _ _ _).obj (Ind.inclusion C) ⋙ colim :=
(isoWhiskerLeft _ (preservesColimitNatIso _))
_ ≅ ((whiskeringRight _ _ _).obj Ind.yoneda ⋙ (whiskeringRight _ _ _).obj (Ind.inclusion C)) ⋙ colim :=
(Functor.associator _ _ _).symm
_ ≅ (whiskeringRight _ _ _).obj (Ind.yoneda ⋙ Ind.inclusion C) ⋙ colim :=
(isoWhiskerRight (whiskeringRightObjCompIso _ _) colim)
_ ≅ (whiskeringRight _ _ _).obj yoneda ⋙ colim :=
isoWhiskerRight ((whiskeringRight _ _ _).mapIso (Ind.yonedaCompInclusion)) colim
