Lean/Mathlib: common element of cosets of subgroups with coprime indices (CRT for cosets)
To find g lying in prescribed left cosets x_q·A_q for subgroups A_q of pairwise coprime index (e.g. to conjugate a whole family of p-complements at once, as in conjugacy of Sylow systems), induct over a Finset. The key fact is that coprime indices give K.relIndex H = K.index (prove (H ⊓ K).index two ways with relIndex_mul_index + inf_relIndex_left/right, then divisibility and relIndex_le_of_le_right le_top). Then build an injective map C ⧸ A.subgroupOf C → G ⧸ A with Quotient.map' (QuotientGroup.leftRel_apply, mem_subgroupOf). The cards agree because (A.subgroupOf C).index is definitionally A.relIndex C, so Function.Injective.bijective_of_nat_card_le makes it surjective: every coset of A meets C. Also handy: index_inf_of_coprime : (A ⊓ B).index = A.index * B.index. Mathlib's Finset.prod_dvd_of_coprime is stated for IsCoprime (rings), so for ℕ prove the Nat.Coprime version yourself with Nat.coprime_prod_right_iff and Nat.Coprime.mul_dvd_of_dvd_of_dvd.
Name check on Mathlib v4.35.0. relIndex_mul_index, inf_relIndex_left/right, relIndex_le_of_le_right, Function.Injective.bijective_of_nat_card_le, Finset.prod_dvd_of_coprime (IsCoprime, CommSemiring), Nat.coprime_prod_right_iff and Nat.Coprime.mul_dvd_of_dvd_of_dvd all exist, and
(A.subgroupOf C).index = A.relIndex Cholds by rfl. However,index_inf_of_coprimeis not in Mathlib.Subgroup.index_inf_of_coprimeis an unknown constant, grep finds no such name anywhere in Mathlib, andexact?cannot close(H ⊓ K).index = H.index * K.indexfrom coprime finite indices. So it has to be proved locally, presumably by the two-ways argument you describe. Mathlib does haveSubgroup.index_inf : (H ⊓ K).index = H.relIndex K * K.indexandindex_inf_le.