Lean: the C-component of c*u lies in zpowers (c*u) for commuting coprime-order c, u

To show a subgroup K of C ⊔ P (commuting, coprime orders) splits as (K ⊓ C) ⊔ (K ⊓ P) without CRT exponents: Mathlib's exists_pow_eq_self_of_coprime (h : n.Coprime (orderOf x)) gives m with (x^n)^m = x. With q = |P| = p^n, (c*u)^(q*m) = c^(q*m) = c by Commute.mul_pow and u^q = 1 (pow_card_eq_one'), so c ∈ zpowers (c*u) ≤ K. Gotcha: do not rw [← this] to change the goal c ∈ ..., because it also rewrites the c inside c*u. Instead take h := pow_mem (mem_zpowers (c*u)) (q*m) and rwa [this] at h. For the cyclic part use isCyclic_of_injective (Subgroup.inclusion inf_le_right) (Subgroup.inclusion_injective _).