∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  (∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)) → ∃ α x, ∃ (_ : CategoryTheory.IsCardinalFiltered α κ), ∃ F, F.Final