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₂) [CategoryTheory.Category.{v₂, u₂} J] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EssentiallySmall.{w₁, v₂, u₂} J] [CategoryTheory.Limits.HasLimitsOfSize.{w₁, w₁, v₁, u₁} C] : CategoryTheory.Limits.HasLimitsOfShape J C

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

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

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