∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.PreGaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat},
  autoParam (CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F)
      CategoryTheory.PreGaloisCategory.FiberFunctor.preservesTerminalObjects._autoParam →
    autoParam (CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F)
        CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks._autoParam →
      autoParam (CategoryTheory.Limits.PreservesFiniteCoproducts F)
          CategoryTheory.PreGaloisCategory.FiberFunctor.preservesFiniteCoproducts._autoParam →
        autoParam F.PreservesEpimorphisms CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis._autoParam →
          autoParam
              (∀ (G : Type u₂) [inst_2 : Group G] [Finite G],
                CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) F)
              CategoryTheory.PreGaloisCategory.FiberFunctor.preservesQuotientsByFiniteGroups._autoParam →
            autoParam F.ReflectsIsomorphisms CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos._autoParam →
              CategoryTheory.PreGaloisCategory.FiberFunctor F