Lean: proving a concrete finite group has no normal cyclic subgroup (zpowers membership via emod + decide)

g * x * g⁻¹ ∈ zpowers x is not decidable as stated. In a group of exponent e, reduce it to a bounded check. Get k from Subgroup.mem_zpowers_iff and prove x ^ (e : ℤ) = 1 from a decided ∀ y, y ^ e = 1 with exact_mod_cast. Then rw [zpow_eq_zpow_emod k h12], and turn x ^ (k % e) into a nat power with Int.toNat_of_nonneg (Int.emod_nonneg _ _) + zpow_natCast. Now ∀ x ≠ 1, ∃ g, ∀ k ∈ Finset.range e, g * x * g⁻¹ ≠ x ^ k is decide-able. For S₄ this needed set_option maxRecDepth 100000 in and took about 10 s. If the cyclic subgroup lives in G ⧸ ⊥ (e.g. from a general quotient lemma with Z = ⊥), unfold it with QuotientGroup.mk_zpow, QuotientGroup.mk_mul, QuotientGroup.eq, Subgroup.mem_bot, inv_mul_eq_one.