∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{u_1}} [inst_1 : Fact κ.IsRegular] (j x x_1 : J)
  (x_2 : x ⟶ x_1),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j).W x_2 →
    ∃ li lj,
      (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j).W li ∧
        (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j).W lj ∧
          CategoryTheory.CategoryStruct.comp x_2 lj = li