∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (X : Action FintypeCat (CategoryTheory.Aut F)) [inst_3 : TopologicalSpace X.V.carrier] [DiscreteTopology X.V.carrier]
  [ContinuousSMul (CategoryTheory.Aut F) X.V.carrier],
  ∃ A, Nonempty ((CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅ X)