proposition: Lemma Msigma_setI_mmax_central p H : H \in 'M -> p \in \pi(E) -> p \in \pi(H) -> p \notin \tau1(H) -> [~: M`_\sigma :&: H, M :&: H] != 1 -> gval H \notin M :^: G -> [/\ forall P, P \subset M :&: H -> p.-group P -> P \subset 'C(M`_\sigma :&: H), p \notin \tau2(H) & p \in \tau1(M) -> p \in \beta(G)].
proof: Proof. move=> maxH piEp piHp t1H'p; set R := [~: _, _] => ntR notMGH. have [q sMq piH'q]: exists2 q, q \in \sigma(M) & q \in \pi(H^`(1)). pose q := pdiv #|R|; have q_pr: prime q by rewrite pdiv_prime ?cardG_gt1. have q_dv : q %| _ := dvdn_trans (pdiv_dvd _) (cardSg _). exists q; last by rewrite mem_primes q_pr cardG_gt0 q_dv ?commgSS ?subsetIr. rewrite (pgroupP (pcore_pgroup _ M)) ?q_dv //. have sR_MsM: R \subset [~: M`_\sigma, M] by rewrite commgSS ?subsetIl. by rewrite (subset_trans sR_MsM) // commg_subl gFnorm. have [Y sylY] := Sylow_exists q H^`(1); have [sYH' qY _] := and3P sylY. have nsHbH: H`_\beta <| H := pcore_normal _ _; have [_ nHbH] := andP nsHbH. have sYH := subset_trans sYH' (der_sub 1 H); have nHbY := subset_trans sYH nHbH. have nsHbY_H: H`_\beta <*> Y <| H. rewrite -{2}(quotientGK nsHbH) -quotientYK ?cosetpre_normal //. have ->: Y / H`_\beta = 'O_q(H^`(1) / H`_\beta). by apply: nilpotent_Hall_pcore; rewrite ?Mbeta_quo_nil ?quotient_pHall. by rewrite quotient_der ?gFnormal_trans. have sYNY: Y \subset 'N_H(Y) by rewrite subsetI sYH normG. have{nsHbY_H} defH: H`_\beta * 'N_H(Y) = H. rewrite -(mulSGid sYNY) mulgA -(norm_joinEr nHbY). rewrite (Frattini_arg _ (pHall_subl _ _ sylY)) ?joing_subr //. by rewrite join_subG Mbeta_der1. have ntY: Y :!=: 1 by rewrite -cardG_gt1 (card_Hall sylY) p_part_gt1. have{ntY} [_] := sigma_Jsub maxM (pi_pgroup qY sMq) ntY. have maxY_H: H \in 'M(Y) by apply/setIdP. move/(_ E p H hallE piEp _ maxY_H notMGH) => b'p_t3Hp. case t2Hp: (p \in \tau2(H)). have b'p: p \notin \beta(G) by case/tau2_not_beta: t2Hp. have rpH: 'r_p(H) = 2 by apply/eqP; case/andP: t2Hp. have p'Hb: p^'.-group H`_\beta. rewrite (pi_p'group (pcore_pgroup _ H)) // inE /=. by rewrite -predI_sigma_beta // negb_and b'p orbT. case: b'p_t3Hp; rewrite // -(p_rank_p'quotient p'Hb) ?subIset ?nHbH //=. by rewrite -quotientMidl defH p_rank_p'quotient ?rpH. have [S sylS] := Sylow_exists p H; have [sSH pS _] := and3P sylS. have sSH': S \subset H^`(1). have [sHp | sH'p] := boolP (p \in \sigma(H)). apply: subset_trans (Msigma_der1 maxH). by rewrite (sub_Hall_pcore (Msigma_Hall _)) // (pi_pgroup pS). have sH'_S: \sigma(H)^'.-group S by rewrite (pi_pgroup pS). have [F hallF sSF] := Hall_superset (mmax_sol maxH) sSH sH'_S. have t3Hp: p \in \tau3(H). have:= partition_pi_sigma_compl maxH hallF p. by rewrite (pi_sigma_compl hallF) inE /= sH'p piHp (negPf t1H'p) t2Hp. have [[F1 hallF1] [F3 hallF3]] := ex_tau13_compl hallF. have [F2 _ complFi] := ex_tau2_compl hallF hallF1 hallF3. have [[sF3F' nsF3F] _ _ _ _] := sigma_compl_context maxH complFi. apply: subset_trans (subset_trans sF3F' (dergS 1 (pHall_sub hallF))). by rewrite (sub_normal_Hall hallF3) ?(pi_pgroup pS). have sylS_H' := pHall_subl sSH' (der_sub 1 H) sylS. split=> // [P sPMH pP | t1Mp]; last first. apply/idPn=> b'p; have [_ /(_ t1Mp)/negP[]] := b'p_t3Hp b'p. have p'Hb: p^'.-group H`_\beta. rewrite (pi_p'group (pcore_pgroup _ H)) // inE /=. by rewrite -predI_sigma_beta // negb_and b'p orbT. rewrite -p_rank_gt0 -(p_rank_p'quotient p'Hb) ?comm_subG ?subIset ?nHbH //=. rewrite quotient_der ?subIset ?nHbH // -quotientMidl defH -quotient_der //=. rewrite p_rank_p'quotient ?comm_subG // -(rank_Sylow sylS_H'). by rewrite (rank_Sylow sylS) p_rank_gt0. have nsHaH: H`_\alpha <| H := pcore_normal _ _; have [_ nHaH] := andP nsHaH. have [sPM sPH] := subsetIP sPMH; have nHaS := subset_trans sSH nHaH. have nsHaS_H: H`_\alpha <*> S <| H. rewrite -[H in _ <| H](quotientGK nsHaH) -quotientYK ?cosetpre_normal //. have ->: S / H`_\alpha = 'O_p(H^`(1) / H`_\alpha). by apply: nilpotent_Hall_pcore; rewrite ?Malpha_quo_nil ?quotient_pHall. by rewrite quotient_der ?gFnormal_trans. have [sHaS_H nHaS_H] := andP nsHaS_H. have sP_HaS: P \subset H`_\alpha <*> S. have [x Hx sPSx] := Sylow_subJ sylS sPH pP; apply: subset_trans sPSx _. by rewrite sub_conjg (normsP nHaS_H) ?groupV ?joing_subr. have coHaS_Ms: coprime #|H`_\alpha <*> S| #|M`_\sigma|. rewrite (p'nat_coprime _ (pcore_pgroup _ _)) // -pgroupE norm_joinEr //. rewrite pgroupM andbC (pi_pgroup pS) ?(pnatPpi (pHall_pgroup hallE)) //=. apply: sub_pgroup (pcore_pgroup _ _) => r aHr. have [|_ ti_aH_sM _] := sigma_disjoint maxH maxM; first by rewrite orbit_sym. by apply: contraFN (ti_aH_sM r) => sMr; apply/andP. rewrite (sameP commG1P trivgP) -(coprime_TIg coHaS_Ms) commg_subI ?setIS //. by rewrite subsetI sP_HaS (subset_trans sPM) ?gFnorm. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12)