Limits over essentially small indexing categories

If C has limits of size w and J is w-essentially small, then C has limits of shape J.

See also the file FinallySmall.lean for more general results.

theorem CategoryTheory.Limits.hasLimitsOfShape_of_essentiallySmall (J : Type u₂) [Category.{v₂, u₂} J] (C : Type u₁) [Category.{v₁, u₁} C] [EssentiallySmall.{w₁, v₂, u₂} J] [HasLimitsOfSize.{w₁, w₁, v₁, u₁} C] : HasLimitsOfShape J C

theorem CategoryTheory.Limits.hasColimitsOfShape_of_essentiallySmall (J : Type u₂) [Category.{v₂, u₂} J] (C : Type u₁) [Category.{v₁, u₁} C] [EssentiallySmall.{w₁, v₂, u₂} J] [HasColimitsOfSize.{w₁, w₁, v₁, u₁} C] : HasColimitsOfShape J C

theorem CategoryTheory.Limits.hasProductsOfShape_of_small (C : Type u₁) [Category.{v₁, u₁} C] (β : Type w₂) [Small.{w₁, w₂} β] [HasProducts C] : HasProductsOfShape β C

theorem CategoryTheory.Limits.hasCoproductsOfShape_of_small (C : Type u₁) [Category.{v₁, u₁} C] (β : Type w₂) [Small.{w₁, w₂} β] [HasCoproducts C] : HasCoproductsOfShape β C