{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        {G : Type u_1} →
          [inst_2 : Group G] →
            [inst_3 : (X : C) → MulAction G (F.obj X).obj] →
              [inst_4 : TopologicalSpace G] →
                [inst_5 : IsTopologicalGroup G] →
                  [inst_6 : CompactSpace G] →
                    {motive : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G → Sort u} →
                      ([toIsNaturalSMul : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] →
                          (transitive_of_isGalois :
                              ∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X],
                                MulAction.IsPretransitive G (F.obj X).obj) →
                            (continuous_smul : ∀ (X : C), ContinuousSMul G (F.obj X).obj) →
                              (non_trivial' : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1) →
                                motive ⋯) →
                        (t : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G) → motive t