∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : CompactSpace G] (X : Action FintypeCat G) [inst_4 : TopologicalSpace X.V.carrier]
  [DiscreteTopology X.V.carrier] [ContinuousSMul G X.V.carrier],
  ∃ ι,
    ∃ (x : Finite ι),
      ∃ f,
        Nonempty
          ((∐ fun i =>
              Action.FintypeCat.ofMulAction G
                { carrier := G ⧸ ↑(f i), str := CategoryTheory.PreGaloisCategory.fintypeQuotient✝ (f i) }) ≅
            X)