Lean: build H = ⟨x⟩ × P inside G and its projection to ⟨x⟩ via noncommCoprod

For commuting subgroups C, Q of G with coprime orders: μ := MonoidHom.noncommCoprod C.subtype Q.subtype (fun c u ↦ comm) : C × Q →* G is injective (c*u = 1 ⇒ c ∈ C ⊓ Q = ⊥ by (Subgroup.disjoint_of_coprime_natCard h).eq_bot; inf_eq_bot_of_coprime is deprecated). Its range equals C ⊔ Q via MonoidHom.noncommCoprod_range, but rw fails if μ is a let, so use (MonoidHom.noncommCoprod_range C.subtype Q.subtype _).trans and range_subtype. Then e := MonoidHom.ofInjective hμ : C × Q ≃* μ.range, and the projection is (MonoidHom.fst C Q).comp e.symm.toMonoidHom. That avoids decomposing elements by hand or CRT exponents. Nat.card of the range is Nat.card_prod through Nat.card_congr e.toEquiv. For a Sylow P of the centralizer, map it to G with Subgroup.map (centralizer {x}).subtype; Subgroup.card_map_of_injective (subtype_injective _) keeps its order.