proposition: Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) : A \subset 'N(G) -> coprime #|G| #|A| -> solvable G -> X \subset G -> pi.-group X -> A \subset 'N(X) -> exists H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H].
proof: Proof. have [n] := ubnP #|G|. elim: n => // n IHn in gT A G X * => /ltnSE-leGn nGA coGA solG sXG piX nXA. have [G1 | ntG] := eqsVneq G 1. case: (coprime_Hall_exists pi nGA) => // H hallH nHA. by exists H; split; rewrite // (subset_trans sXG) // G1 sub1G. have sG_AG: G \subset A <*> G by rewrite joing_subr. have sA_AG: A \subset A <*> G by rewrite joing_subl. have nG_AG: A <*> G \subset 'N(G) by rewrite join_subG nGA normG. have nsG_AG: G <| A <*> G by apply/andP. case: (solvable_norm_abelem solG nsG_AG) => // M [sMG nsMAG ntM]. have{nsMAG} [nMA nMG]: A \subset 'N(M) /\ G \subset 'N(M). by apply/andP; rewrite -join_subG normal_norm. have nMX: X \subset 'N(M) by apply: subset_trans nMG. case/is_abelemP=> p pr_p; case/and3P=> pM cMM _. have: #|G / M| < n by rewrite (leq_trans (ltn_quotient _ _)). move/(IHn _ (A / M)%G _ (X / M)%G); rewrite !(quotient_norms, quotientS) //. rewrite !(coprime_morph, quotient_sol, morphim_pgroup) //. case=> //= Hq []; case/and3P=> sHGq piHq pi'Hq' nHAq sXHq. case/inv_quotientS: (sHGq) => [|HM defHM sMHM sHMG]; first exact/andP. have nMHM := subset_trans sHMG nMG. have{sXHq} sXHM: X \subset HM by rewrite -(quotientSGK nMX) -?defHM. have{pi'Hq' sHGq} pi'HM': pi^'.-nat #|G : HM|. move: pi'Hq'; rewrite -!divgS // defHM !card_quotient //. by rewrite -(divnMl (cardG_gt0 M)) !Lagrange. have{nHAq} nHMA: A \subset 'N(HM). by rewrite -(quotientSGK nMA) ?normsG ?quotient_normG -?defHM //; apply/andP. case/orP: (orbN (p \in pi)) => pi_p. exists HM; split=> //; apply/and3P; split; rewrite /pgroup //. by rewrite -(Lagrange sMHM) pnatM -card_quotient // -defHM (pi_pnat pM). case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}]. case: (IHn _ A HM X (leq_trans ltHG leGn)) => // [||H [hallH nHA sXH]]. - exact: coprimeSg coGA. - exact: solvableS solG. case/and3P: hallH => sHHM piH pi'H'. have sHG: H \subset G by apply: subset_trans sHMG. exists H; split=> //; apply/and3P; split=> //. rewrite -divgS // -(Lagrange sHMG) -(Lagrange sHHM) -mulnA mulKn //. by rewrite pnatM pi'H'. have{leGHM nHMA sHMG sMHM sXHM pi'HM'} eqHMG: HM = G. by apply/eqP; rewrite -val_eqE eqEcard sHMG. have pi'M: pi^'.-group M by rewrite /pgroup (pi_pnat pM). have{HM Hq nMHM defHM eqHMG piHq} hallM: pi^'.-Hall(G) M. apply/and3P; split; rewrite // /pgroup pnatNK. by rewrite -card_quotient // -eqHMG -defHM. case: (coprime_Hall_exists pi nGA) => // H hallH nHA. pose XM := (X <*> M)%G; pose Y := (H :&: XM)%G. case/and3P: (hallH) => sHG piH _. have sXXM: X \subset XM by rewrite joing_subl. have co_pi_M (B : {group gT}): pi.-group B -> coprime #|B| #|M|. by move=> piB; rewrite (pnat_coprime piB). have hallX: pi.-Hall(XM) X. rewrite /pHall piX sXXM -divgS //= norm_joinEl //. by rewrite coprime_cardMg ?co_pi_M // mulKn. have sXMG: XM \subset G by rewrite join_subG sXG. have hallY: pi.-Hall(XM) Y. have sYXM: Y \subset XM by rewrite subsetIr. have piY: pi.-group Y by apply: pgroupS piH; apply: subsetIl. rewrite /pHall sYXM piY -divgS // -(_ : Y * M = XM). by rewrite coprime_cardMg ?co_pi_M // mulKn //. rewrite /= setIC group_modr ?joing_subr //=; apply/setIidPl. rewrite ((H * M =P G) _) // eqEcard mul_subG //= coprime_cardMg ?co_pi_M //. by rewrite (card_Hall hallM) (card_Hall hallH) partnC. have nXMA: A \subset 'N(XM) by rewrite normsY. have:= coprime_Hall_trans nXMA _ _ hallX nXA hallY. rewrite !(coprimeSg sXMG, solvableS sXMG, normsI) //. case=> // x /setIP[XMx cAx] ->. exists (H :^ x)%G; split; first by rewrite pHallJ ?(subsetP sXMG). by rewrite norm_conj_cent. by rewrite conjSg subsetIl. 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)