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 J] (C : Type u₁) [Category C] [EssentiallySmall J] [HasLimitsOfSize C] : HasLimitsOfShape J C

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

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

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