{C : Type u} →
  [hC : CategoryTheory.Category.{v, u} C] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        {motive : CategoryTheory.HasCardinalFilteredGenerator C κ → Sort u_1} →
          (t : CategoryTheory.HasCardinalFilteredGenerator C κ) →
            ([toLocallySmall : CategoryTheory.LocallySmall.{w, v, u} C] →
                (exists_generator :
                    ∃ P,
                      ∃ (_ : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P),
                        P.IsCardinalFilteredGenerator κ) →
                  motive ⋯) →
              motive t