proposition: Lemma Hall_exists_subJ pi gT (G : {group gT}) : solvable G -> exists2 H : {group gT}, pi.-Hall(G) H & forall K : {group gT}, K \subset G -> pi.-group K -> exists2 x, x \in G & K \subset H :^ x.
proof: Proof. have [n] := ubnP #|G|; elim: n gT G => // n IHn gT G /ltnSE-leGn solG. have [-> | ntG] := eqsVneq G 1. exists 1%G => [|_ /trivGP-> _]; last by exists 1; rewrite ?set11 ?sub1G. by rewrite pHallE sub1G cards1 part_p'nat. case: (solvable_norm_abelem solG (normal_refl _)) => // M [sMG nsMG ntM]. case/is_abelemP=> p pr_p /and3P[pM cMM _]. pose Gb := (G / M)%G; case: (IHn _ Gb) => [||Hb]; try exact: quotient_sol. by rewrite (leq_trans (ltn_quotient _ _)). case/and3P=> [sHbGb piHb pi'Hb'] transHb. case: (inv_quotientS nsMG sHbGb) => H def_H sMH sHG. have nMG := normal_norm nsMG; have nMH := subset_trans sHG nMG. have{transHb} transH (K : {group gT}): K \subset G -> pi.-group K -> exists2 x, x \in G & K \subset H :^ x. - move=> sKG piK; have nMK := subset_trans sKG nMG. case: (transHb (K / M)%G) => [||xb Gxb sKHxb]; first exact: morphimS. exact: morphim_pgroup. case/morphimP: Gxb => x Nx Gx /= def_x; exists x => //. apply/subsetP=> y Ky. have: y \in coset M y by rewrite val_coset (subsetP nMK, rcoset_refl). have: coset M y \in (H :^ x) / M. rewrite /quotient morphimJ //=. by rewrite def_x def_H in sKHxb; apply/(subsetP sKHxb)/mem_quotient. case/morphimP=> z Nz Hxz ->. rewrite val_coset //; case/rcosetP=> t Mt ->; rewrite groupMl //. by rewrite mem_conjg (subsetP sMH) // -mem_conjg (normP Nx). have{pi'Hb'} pi'H': pi^'.-nat #|G : H|. move: pi'Hb'; rewrite -!divgS // def_H !card_quotient //. by rewrite -(divnMl (cardG_gt0 M)) !Lagrange. have [pi_p | pi'p] := boolP (p \in pi). exists H => //; apply/and3P; split=> //; rewrite /pgroup. by rewrite -(Lagrange sMH) -card_quotient // pnatM -def_H (pi_pnat pM). have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|. case: (IHn _ H (leq_trans ltHG leGn)) => [|H1]; first exact: solvableS solG. case/and3P=> sH1H piH1 pi'H1' transH1. have sH1G: H1 \subset G by apply: subset_trans sHG. exists H1 => [|K sKG piK]. apply/and3P; split => //. rewrite -divgS // -(Lagrange sHG) -(Lagrange sH1H) -mulnA. by rewrite mulKn // pnatM pi'H1'. case: (transH K sKG piK) => x Gx def_K. case: (transH1 (K :^ x^-1)%G) => [||y Hy def_K1]. - by rewrite sub_conjgV. - by rewrite /pgroup cardJg. exists (y * x); first by rewrite groupMr // (subsetP sHG). by rewrite -(conjsgKV x K) conjsgM conjSg. have{leGH Gb sHbGb sHG sMH pi'H'} eqHG: H = G. by apply/eqP; rewrite -val_eqE eqEcard sHG. have{H Hb def_H eqHG piHb nMH} hallM: pi^'.-Hall(G) M. rewrite /pHall /pgroup sMG pnatNK -card_quotient //=. by rewrite -eqHG -def_H (pi_pnat pM). case/splitsP: (SchurZassenhaus_split (pHall_Hall hallM) nsMG) => H. case/complP=> trMH defG. have sHG: H \subset G by rewrite -defG mulG_subr. exists H => [|K sKG piK]. apply: etrans hallM; rewrite /pHall sMG sHG /= -!divgS // -defG andbC. by rewrite (TI_cardMg trMH) mulKn ?mulnK // pnatNK. pose G1 := (K <*> M)%G; pose K1 := (H :&: G1)%G. have nMK: K \subset 'N(M) by apply: subset_trans sKG nMG. have defG1: M * K = G1 by rewrite -normC -?norm_joinEl. have sK1G1: K1 \subset M * K by rewrite defG1 subsetIr. have coMK: coprime #|M| #|K|. by rewrite coprime_sym (pnat_coprime piK) //; apply: (pHall_pgroup hallM). case: (SchurZassenhaus_trans_sol _ nMK sK1G1 coMK) => [||x Mx defK1]. - exact: solvableS solG. - apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 M)) -TI_cardMg //; last first. by apply/trivgP; rewrite -trMH /= setIA subsetIl. rewrite -coprime_cardMg // defG1; apply/eqP; congr #|(_ : {set _})|. rewrite group_modl; last by rewrite -defG1 mulG_subl. by apply/setIidPr; rewrite defG gen_subG subUset sKG. exists x^-1; first by rewrite groupV (subsetP sMG). by rewrite -(_ : K1 :^ x^-1 = K) ?(conjSg, subsetIl) // defK1 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)