Preservation of colimits through composition

This file records preservation results that only concern functor composition. No adjunction is involved.

theorem CategoryTheory.Limits.preservesColimit_comp_left {C : Type u_1} [Category.{u_6, u_1} C] {D : Type u_2} [Category.{u_7, u_2} D] {E : Type u_3} [Category.{u_8, u_3} E] {L : Functor C D} (F : Functor D E) {K : Type u_4} [Category.{u_5, u_4} K] (d : Functor K C) [HasColimit d] [PreservesColimit d L] [PreservesColimit d (L.comp F)] : PreservesColimit (d.comp L) F

If L and L ⋙ F both preserve the colimit of d, then F preserves the colimit of d ⋙ L.