proposition: Lemma P2type_signalizer M Mstar U K r R H : M \in 'M_'P2 -> kappa_complement M U K -> Mstar \in 'M('C(K)) -> r.-Sylow(U) R -> H \in 'M('N(R)) -> [/\ H \in 'M_'F, U \subset H`_\sigma, U <*> K = M :&: H & [/\ ~~ ('N_H(U) \subset M), K \subset 'F(H :&: Mstar) & \sigma(H)^'.-Hall(H) (H :&: Mstar)]].
proof: Proof. move=> P2maxM complU maxCMstar sylR maxNH; have [hallU hallK _] := complU. have [PmaxM notP1maxM] := setDP P2maxM; have [maxM notFmaxM] := setDP PmaxM. have [[sUM sk'M_U _] [sKM kK _]] := (and3P hallU, and3P hallK). have{notFmaxM} ntK: K :!=: 1 by rewrite (trivg_kappa maxM). have [hallE defM _ regK /(_ ntK)cUU] := kappa_compl_context maxM complU. case/sdprodP: defM => [[_ E _ defE] _ _ _]. have [nsUE sKE mulUK nUK tiUK] := sdprod_context defE. rewrite (norm_joinEr nUK) mulUK in hallE *. have [Mst [PmaxMst notMGMst] [uniqMst []]] := Ptype_embedding PmaxM hallK. set Ks := 'C_(_)(K) => hallKs; case/and3P=> sKsMst sM_Ks _ [defK _]. case=> cycZ ziMMst _ _ _ [_ _ defPmax _]. have [_ [defNK _] [ntKs _] _ [//|_ q_pr _ _]] := Ptype_structure PmaxM hallK. set q := #|K| in q_pr. have{} uniqMst: 'M('C(K)) = [set Mst]. by apply: uniqMst; apply/nElemP; exists q; rewrite p1ElemE // !inE subxx /=. have{maxCMstar} ->: Mstar = Mst by [apply/set1P; rewrite -uniqMst] => {Mstar}. have [maxH sNRH] := setIdP maxNH. have ntR: R :!=: 1. by apply: contraTneq sNRH => ->; rewrite norm1 proper_subn ?mmax_proper. have piUr: r \in \pi(U) by rewrite -p_rank_gt0 -(rank_Sylow sylR) rank_gt0. have r_pr: prime r by move: piUr; rewrite mem_primes; case/andP. have sylR_M := subHall_Sylow hallU (pnatPpi sk'M_U piUr) sylR. have [/= s'Mr k'Mr] := norP (pnatPpi sk'M_U piUr). have [sRH [sRM rR _]] := (subset_trans (normG R) sNRH, and3P sylR_M). have notMGH: gval H \notin M :^: G. apply: contra s'Mr; case/imsetP=> a _ defH. rewrite -(sigmaJ _ a) -defH; apply/exists_inP; exists R => //. by rewrite pHallE sRH /= (card_Hall sylR_M) defH cardJg. have sK_uniqMst a: K \subset Mst :^ a -> a \in Mst. move=> sKMa; apply: contraR ntK; rewrite -in_setC => Mst'a. have [_ _ _ [[tiK_MstG _] _ _] _] := Ptype_structure PmaxMst hallKs. by rewrite -(tiK_MstG a) // defK (setIidPl sKMa). have [_ _] := dprodP defNK; rewrite -/Ks => cKKs tiKKs. have snK_sMst L: K <|<| L -> L \subset Mst. elim: {L}_.+1 {-2}L (ltnSn #|L|) => // n IHn A leAn. case/subnormalEr=> [<- | [L [snKL nsLA ltLA]]]. by rewrite -defK subIset // pcore_sub. have [sKL sLMst]: K \subset L /\ L \subset Mst. by rewrite subnormal_sub // IHn // (leq_trans (proper_card ltLA)). apply/subsetP=> a Aa; rewrite -groupV sK_uniqMst // (subset_trans sKL) //. by rewrite -sub_conjg (normsP (normal_norm nsLA)). have sEH: E \subset H. have defR: R :=: 'O_r(U) := nilpotent_Hall_pcore (abelian_nil cUU) sylR. by apply: subset_trans sNRH; rewrite defR gFnorm_trans ?normal_norm. have [sUH sKH]: U \subset H /\ K \subset H by apply/mulGsubP; rewrite mulUK. have notMstGH: gval H \notin Mst :^: G. apply: contra ntR => /imsetP[a _ defH]. have{a} defH: H :=: Mst by rewrite -(conjGid (sK_uniqMst a _)) -?defH. rewrite -(setIidPl sRH) -(setIidPl sRM) -setIA defH ziMMst coprime_TIg //=. rewrite cent_joinEr // TI_cardMg //= coprimeMr -/Ks. rewrite (p'nat_coprime (pi_pnat rR _) kK) //=. exact: p'nat_coprime (pi_pnat rR _) sM_Ks. have FmaxH: H \in 'M_'F. suffices: H \notin 'M_'P by rewrite inE maxH andbT negbK. by apply: (contra (defPmax H)); rewrite inE; apply/norP. have sKMsts: K \subset Mst`_\sigma by rewrite -defK subsetIl. have s'H_K: \sigma(H)^'.-group K. apply/pgroupP=> p p_pr p_dv_K; have [maxMst _] := setDP PmaxMst. apply: contraFN (sigma_partition maxMst maxH notMstGH p) => /= sHp. by rewrite inE /= (pgroupP (pgroupS sKMsts _)) ?pcore_pgroup. have [D hallD sKD] := Hall_superset (mmax_sol maxH) sKH s'H_K. have piKq: q \in \pi(K) by rewrite pi_of_prime ?inE. have sK_FD: K \subset 'F(D). have EqK: K \in 'E_q^1(D) by rewrite p1ElemE // !inE sKD /=. have sMst_q: q \in \sigma(Mst). by rewrite (pnatPpi (pcore_pgroup _ _) (piSg sKMsts _)). apply: contraR notP1maxM => not_sKFD. have [L _ ] := primes_non_Fitting_Ftype FmaxH hallD EqK not_sKFD. case=> [[t2Lq ]|[kLq P1maxL]]. rewrite uniqMst => /set1_inj defL. by rewrite -defL inE /= inE /= sMst_q in t2Lq. have [PmaxL _] := setIdP P1maxL. case/setUP: (defPmax L PmaxL) => /imsetP[a _ defL]. by rewrite (group_inj defL) P1typeJ in P1maxL. move: kLq; rewrite defL kappaJ unlock 3!inE /=. by rewrite -andb_orr inE /= sMst_q. have sDMst: D \subset Mst. apply: snK_sMst (subnormal_trans _ (normal_subnormal (Fitting_normal D))). exact: nilpotent_subnormal (Fitting_nil D) sK_FD. have defUK: [~: U, K] = U. rewrite -{2}(coprime_cent_prod nUK) ?abelian_sol //; last first. by apply: p'nat_coprime (sub_pgroup _ sk'M_U) kK => ? /norP[]. by rewrite (cent_semiregular regK) ?mulg1. have qK: q.-group K := pnat_id q_pr. have sUHs: U \subset H`_\sigma. have [nsHsH _ mulHsD nHsD _] := sdprod_context (sdprod_sigma maxH hallD). have nHsDq: 'O_q(D) \subset 'N(H`_\sigma) by apply: gFsub_trans. pose HsDq := H`_\sigma <*> 'O_q(D). have defHsDq: H`_\sigma * 'O_q(D) = HsDq by rewrite -norm_joinEr. have hallHs_HsDq: q^'.-Hall(HsDq) H`_\sigma. have [|//] := coprime_mulGp_Hall defHsDq _ (pcore_pgroup _ _). rewrite p'groupEpi; apply: (contra (pnatPpi (pcore_pgroup _ _))). exact: pnatPpi s'H_K piKq. have sK_HsDq: K \subset HsDq. rewrite sub_gen ?subsetU // orbC -p_core_Fitting. by rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ (Fitting_nil _))) ?qK. have [|sHsDq_H nHsDq_H] := andP (_ : HsDq <| H). rewrite -(quotientGK nsHsH) -[HsDq]quotientYK //= cosetpre_normal //. by rewrite -{3}mulHsD quotientMidl quotient_normal // pcore_normal. have sU_HsDq: U \subset HsDq. by rewrite -defUK (subset_trans (commgSS sUH sK_HsDq)) // commg_subr. rewrite (sub_normal_Hall hallHs_HsDq) ?normalYl // p'groupEpi. by apply: contraL (pnatPpi sk'M_U) _; rewrite !inE /= orbC (pnatPpi kK). have defNMU: 'N_M(U) = E. have [_ mulHsE nHsE _] := sdprodP (sdprod_sigma maxM hallE). have [sUE nUE] := andP nsUE; rewrite -mulHsE -normC // -group_modl //=. rewrite coprime_norm_cent ?(subset_trans sUE) //; last first. exact: coprimegS sUE (coprime_sigma_compl hallE). have sR1U: 'Ohm_1(R) \subset U := gFsub_trans _ (pHall_sub sylR). rewrite (trivgP (subset_trans (setIS _ (centS sR1U)) _)) ?mulg1 //. have [|_ _ -> //] := sigma'_kappa'_facts maxM sylR_M. by rewrite s'Mr (piSg sUM). have sHsFH: H`_\sigma \subset 'F(H). rewrite Fitting_max ?pcore_normal //. have [S] := Sylow_exists q H; case/sigma'_kappa'_facts=> {S}//. have [_ k'H] := setIdP FmaxH. rewrite [~~ _](pnatPpi (pHall_pgroup hallD) (piSg sKD _)) //=. by rewrite [~~ _](pnatPpi k'H) (piSg sKH). suffices ->: H :&: Mst = D. set sk' := _^' in sk'M_U hallU; pose Fu := 'O_sk'('F(H)). have [sUFH nilFH] := (subset_trans sUHs sHsFH, Fitting_nil H). have hallFu: sk'.-Hall('F(H)) Fu := nilpotent_pcore_Hall sk' nilFH. have sUFu: U \subset Fu by rewrite (sub_Hall_pcore hallFu). have nsFuH: Fu <| H by rewrite !gFnormal_trans. have [[sFuFH sk'Fu _] [sFuH nFuH]] := (and3P hallFu, andP nsFuH). have defU: M :&: Fu = U. have sk'MFu: sk'.-group(M :&: Fu) := pgroupS (subsetIr M _) sk'Fu. by rewrite (sub_pHall hallU sk'MFu) ?subsetIl // subsetI sUM. do 2?split=> //. apply/eqP; rewrite eqEsubset subsetI (pHall_sub hallE) sEH /=. by rewrite -defNMU subsetI subsetIl -defU normsGI. apply: contra (contra_orbit _ _ notMGH) => sNHU_M. rewrite (eq_mmax maxH maxM (subset_trans _ sNHU_M)) // subsetIidl. rewrite -(nilpotent_sub_norm (nilpotentS sFuFH nilFH) sUFu) //= -/Fu. by rewrite -{2}defU subsetI subsetIl (subset_trans (setSI _ sFuH)). have [maxMst _] := setDP PmaxMst. have [_ <- _ _] := sdprodP (sdprod_sigma maxH hallD). rewrite -{2}(mul1g D) setIC -group_modr // setIC; congr (_ * _). apply/eqP; apply: wlog_neg => ntHsMst. have nregHsK: 'C_(H`_\sigma)(K) != 1. rewrite (subG1_contra _ ntHsMst) // subsetI subsetIl (sameP commG1P trivgP). have <-: H`_\sigma :&: Mst`_\sigma = 1. apply: card_le1_trivg; rewrite leqNgt -pi_pdiv; set p := pdiv _. apply: contraFN (sigma_partition maxMst maxH notMstGH p) => piIp. rewrite inE /= (pnatPpi (pcore_pgroup _ _) (piSg (subsetIl _ _) piIp)). by rewrite (pnatPpi (pcore_pgroup _ _) (piSg (subsetIr _ _) piIp)). rewrite commg_subI ?setIS ?gFnorm // subsetI sKMsts. by rewrite (subset_trans sKH) ?gFnorm. have t2Hq: q \in \tau2(H). have: q \in \pi(D) := piSg sKD piKq. rewrite (partition_pi_sigma_compl maxH hallD) orbCA; case/orP=> // t13Hq. case/FtypeP: FmaxH => _ /(_ q)/idP[]; rewrite unlock !(t13Hq, inE). by apply/exists_inP; exists K => //; rewrite p1ElemE // !inE sKH /=. have [A EqA_D EqA] := ex_tau2Elem hallD t2Hq. have [_ _ _ -> //] := tau2_context maxH t2Hq EqA. rewrite 3!inE -val_eqE /= eq_sym (contra_orbit _ _ notMstGH) maxMst. by have [sAD _ _] := pnElemP EqA_D; apply: subset_trans sAD sDMst. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)