proposition: Corollary nilpotent_Hall_sigma H : nilpotent H -> Hall G H -> exists2 M, M \in 'M & H \subset M`_\sigma.
proof: Proof. move=> nilH /Hall_pi/=hallH; have [_ piH _] := and3P hallH. have [-> | ntH] := eqsVneq H 1. by have [M maxM] := any_mmax gT; exists M; rewrite ?sub1G. pose p := pdiv #|H|; have piHp: p \in \pi(H) by rewrite pi_pdiv cardG_gt1. pose S := 'O_p(H)%G; have sylS: p.-Sylow(H) S := nilpotent_pcore_Hall p nilH. have [sSH pS _] := and3P sylS. have ntS: S :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylS) p_rank_gt0. have [M maxNM] := mmax_exists (mFT_norm_proper ntS (mFT_pgroup_proper pS)). have [maxM sNM] := setIdP maxNM; exists M => //. have sSM: S \subset M := subset_trans (normG _) sNM. have sylS_G := subHall_Sylow hallH (pnatPpi piH piHp) sylS. have sylS_M := pHall_subl sSM (subsetT M) sylS_G. have sMp: p \in \sigma(M) by apply/exists_inP; exists S. have sSMs: S \subset M`_\sigma. by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup pS). rewrite -(nilpotent_Fitting nilH) FittingEgen gen_subG. apply/bigcupsP=> [[q /= _] piHq]; have [-> // | p'q] := eqVneq q p. have sylS_Ms := pHall_subl sSMs (pcore_sub _ _) sylS_M. have [X [_ cycX t2X defCS]] := cent_Hall_sigma_sdprod maxM sylS_Ms ntS. have{defCS} [nCMsCS _ defCS _ _] := sdprod_context defCS. have t2'CMs: \tau2(M)^'.-group 'C_(M`_\sigma)(S). apply: pgroupS (subsetIl _ _) (sub_pgroup _ (pcore_pgroup _ _)) => r. by apply: contraL => /andP[]. have [hallCMs hallX] := coprime_mulGp_Hall defCS t2'CMs t2X. have sHqCS: 'O_q(H) \subset 'C_M(S). rewrite (setIidPr (subset_trans (cent_sub _) sNM)). rewrite (sub_nilpotent_cent2 nilH) ?pcore_sub //. exact: pnat_coprime pS (pi_pgroup (pcore_pgroup _ _) _). have [t2q | t2'q] := boolP (q \in \tau2(M)); last first. apply: subset_trans (subsetIl _ 'C(S)). by rewrite (sub_normal_Hall hallCMs) // (pi_pgroup (pcore_pgroup _ _)). have sylHq := nilpotent_pcore_Hall q nilH. have sylHq_G := subHall_Sylow hallH (pnatPpi piH piHq) sylHq. have sylHq_CS := pHall_subl sHqCS (subsetT _) sylHq_G. have [Q sylQ] := Sylow_exists q X; have [sQX _] := andP sylQ. have sylQ_CS := subHall_Sylow hallX t2q sylQ. case/andP: t2q => _. rewrite eqn_leq andbC ltnNge (leq_trans (p_rankS q (subsetT _))) //. rewrite -(rank_Sylow sylHq_G) (rank_Sylow sylHq_CS) -(rank_Sylow sylQ_CS). by rewrite (leq_trans (rankS sQX)) // -abelian_rank1_cyclic ?cyclic_abelian. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14)