∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] (j₀ : J), CategoryTheory.IsCardinalFiltered (CategoryTheory.Under j₀) κ