∀ {G : Type u_5} [inst : Group G] [inst_1 : Fintype G] (S : Set G) [inst_2 : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k]
  (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)