proposition: Proposition coprime_Hall_trans A G H1 H2 : A \subset 'N(G) -> coprime #|G| #|A| -> solvable G -> pi.-Hall(G) H1 -> A \subset 'N(H1) -> pi.-Hall(G) H2 -> A \subset 'N(H2) -> exists2 x, x \in 'C_G(A) & H1 :=: H2 :^ x.
proof: Proof. move: H1 => H nGA coGA solG hallH nHA hallH2. have{H2 hallH2} [x Gx -> nH1xA] := Hall_trans solG hallH2 hallH. have sG_AG: G \subset A <*> G by rewrite -{1}genGid genS ?subsetUr. have nG_AG: A <*> G \subset 'N(G) by rewrite gen_subG subUset nGA normG. pose N := 'N_(A <*> G)(H)%G. have nGN: N \subset 'N(G) by rewrite subIset ?nG_AG. have nGN_N: G :&: N <| N. apply/normalP; rewrite subsetIr; split=> // y Ny. by rewrite conjIg (normP _) // (subsetP nGN, conjGid). have NG_AG : G * N = A <*> G. by apply: Hall_Frattini_arg hallH => //; apply/andP. have iGN_A: #|N : G :&: N| = #|A|. rewrite -card_quotient //; last by case/andP: nGN_N. rewrite (card_isog (second_isog nGN)) /= -quotientMidr (normC nGN) NG_AG. rewrite card_quotient // -divgS //= joingC norm_joinEr //. by rewrite coprime_cardMg // mulnC mulnK. have solGN: solvable (G :&: N) by apply: solvableS solG; apply: subsetIl. have oAxA: #|A :^ x^-1| = #|A| by apply: cardJg. have sAN: A \subset N by rewrite subsetI -{1}genGid genS // subsetUl. have nGNA: A \subset 'N(G :&: N). by apply/normsP=> y ?; rewrite conjIg (normsP nGA) ?(conjGid, subsetP sAN). have coGNA: coprime #|G :&: N| #|A| := coprimeSg (subsetIl _ _) coGA. case: (SchurZassenhaus_trans_sol solGN nGNA _ coGNA oAxA) => [|y GNy defAx]. have ->: (G :&: N) * A = N. apply/eqP; rewrite eqEcard -{2}(mulGid N) mulgSS ?subsetIr //=. by rewrite coprime_cardMg // -iGN_A Lagrange ?subsetIr. rewrite sub_conjgV conjIg -normJ subsetI conjGid ?joing_subl //. by rewrite mem_gen // inE Gx orbT. case/setIP: GNy => Gy; case/setIP=> _; move/normP=> nHy. exists (y * x)^-1. rewrite -coprime_norm_cent // groupV inE groupM //=; apply/normP. by rewrite conjsgM -defAx conjsgKV. by apply: val_inj; rewrite /= -{2}nHy -(conjsgM _ y) conjsgK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)