∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v, u} C]
  {Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v, v, max u v, max u v} (CategoryTheory.Under.map f)