∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected X],
  CategoryTheory.PreGaloisCategory.IsGalois X ↔ MulAction.IsPretransitive (CategoryTheory.Aut X) (F.obj X).carrier