proposition: Lemma ext_coprime_Hall_trans (H1 H2 : {group gT}) : pi.-Hall(G) H1 -> [acts A, on H1 | to] -> pi.-Hall(G) H2 -> [acts A, on H2 | to] -> exists2 x, x \in 'C_(G | to)(A) & H1 :=: H2 :^ x.
proof: Proof. move=> hallH1 nH1A hallH2 nH2A. have sH1G := pHall_sub hallH1; have sH2G := pHall_sub hallH2. rewrite !actsEsd // in nH1A nH2A. have hallH1': pi.-Hall(G') (inG @* H1) by rewrite morphim_pHall. have hallH2': pi.-Hall(G') (inG @* H2) by rewrite morphim_pHall. have [x'] := coprime_Hall_trans nGA' coGA' solG' hallH1' nH1A hallH2' nH2A. case/setIP=> /= Gx' cAx' /eqP defH1; pose x := invm injG x'. have Gx: x \in G by rewrite -(im_invm injG) mem_morphim. have def_x': x' = inG x by rewrite invmK. exists x; first by rewrite inE Gx gacentEsd mem_morphpre /= -?def_x'. apply/eqP; move: defH1; rewrite def_x' /= -morphimJ //=. by rewrite !eqEsubset !injmSK // conj_subG. 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)