path: root/mathcomp/odd_order/BGsection12.v

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq choice div fintype.
From mathcomp
Require Import path bigop finset prime fingroup morphism perm automorphism.
From mathcomp
Require Import quotient action gproduct gfunctor pgroup cyclic commutator.
From mathcomp
Require Import center gseries nilpotent sylow abelian maximal hall frobenius.
From mathcomp
Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
From mathcomp
Require Import BGsection7 BGsection9 BGsection10 BGsection11.

(******************************************************************************)
(*   This file covers B & G, section 12; it defines the prime sets for the    *)
(* complements of M`_\sigma in a maximal group M:                             *)
(*    \tau1(M) == the set of p not in \pi(M^`(1)) (thus not in \sigma(M)),    *)
(*                such that M has p-rank 1.                                   *)
(*    \tau2(M) == the set of p not in \sigma(M), such that M has p-rank 2.    *)
(*    \tau3(M) == the set of p not in \sigma(M), but in \pi(M^`(1)), such     *)
(*                that M has p-rank 1.                                        *)
(*   We also define the following helper predicate, which encapsulates the    *)
(* notation conventions defined at the beginning of B & G, Section 12:        *)
(*   sigma_complement M E E1 E2 E3 <=>                                        *)
(*                E is a Hall \sigma(M)^'-subgroup of M, the Ei are Hall      *)
(*                \tau_i(M)-subgroups of E, and E2 * E1 is a group.           *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope.
Section Definitions.

Variables (gT : finGroupType) (M : {set gT}).
Local Notation sigma' := \sigma(M)^'.

Definition tau1 := [pred p in sigma' | 'r_p(M) == 1%N & ~~ (p %| #|M^`(1)|)].
Definition tau2 := [pred p in sigma' | 'r_p(M) == 2].
Definition tau3 := [pred p in sigma' | 'r_p(M) == 1%N & p %| #|M^`(1)|].

Definition sigma_complement E E1 E2 E3 :=
  [/\ sigma'.-Hall(M) E, tau1.-Hall(E) E1, tau2.-Hall(E) E2, tau3.-Hall(E) E3
    & group_set (E2 * E1)].

End Definitions.

Notation "\tau1 ( M )" := (tau1 M)
  (at level 2, format "\tau1 ( M )") : group_scope.
Notation "\tau2 ( M )" := (tau2 M)
  (at level 2, format "\tau2 ( M )") : group_scope.
Notation "\tau3 ( M )" := (tau3 M)
  (at level 2, format "\tau3 ( M )") : group_scope.

Section Section12.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types p q r : nat.
Implicit Types A E H K M Mstar N P Q R S T U V W X Y Z : {group gT}.

Section Introduction.

Variables M E : {group gT}.
Hypotheses (maxM : M \in 'M) (hallE : \sigma(M)^'.-Hall(M) E).

Lemma tau1J x : \tau1(M :^ x) =i \tau1(M).
Proof. by move=> p; rewrite 3!inE sigmaJ p_rankJ derg1 -conjsRg cardJg. Qed.

Lemma tau2J x : \tau2(M :^ x) =i \tau2(M).
Proof. by move=> p; rewrite 3!inE sigmaJ p_rankJ. Qed.

Lemma tau3J x : \tau3(M :^ x) =i \tau3(M).
Proof. by move=> p; rewrite 3!inE sigmaJ p_rankJ derg1 -conjsRg cardJg. Qed.

Lemma tau2'1 : {subset \tau1(M) <= \tau2(M)^'}.
Proof. by move=> p; rewrite !inE; case/and3P=> ->; move/eqP->. Qed.

Lemma tau3'1 : {subset \tau1(M) <= \tau3(M)^'}.
Proof. by move=> p; rewrite !inE; case/and3P=> -> ->. Qed.

Lemma tau3'2 : {subset \tau2(M) <= \tau3(M)^'}.
Proof. by move=> p; rewrite !inE; case/andP=> ->; move/eqP->. Qed.

Lemma ex_sigma_compl : exists F : {group gT}, \sigma(M)^'.-Hall(M) F.
Proof. exact: Hall_exists (mmax_sol maxM). Qed.

Let s'E : \sigma(M)^'.-group E := pHall_pgroup hallE.
Let sEM : E \subset M := pHall_sub hallE.

(* For added convenience, this lemma does NOT depend on the maxM assumption. *)
Lemma sigma_compl_sol : solvable E.
Proof.
have [-> | [p p_pr pE]] := trivgVpdiv E; first exact: solvable1.
rewrite (solvableS sEM) // mFT_sol // properT.
apply: contraNneq (pgroupP s'E p p_pr pE) => ->.
have [P sylP] := Sylow_exists p [set: gT].
by apply/exists_inP; exists P; rewrite ?subsetT.
Qed. 
Let solE := sigma_compl_sol.

Let exHallE pi := exists Ei : {group gT}, pi.-Hall(E) Ei.
Lemma ex_tau13_compl : exHallE \tau1(M) /\ exHallE \tau3(M).
Proof. by split; apply: Hall_exists. Qed.

Lemma ex_tau2_compl E1 E3 :
    \tau1(M).-Hall(E) E1 -> \tau3(M).-Hall(E) E3 ->
  exists2 E2 : {group gT}, \tau2(M).-Hall(E) E2 & sigma_complement M E E1 E2 E3.
Proof.
move=> hallE1 hallE3; have [sE1E t1E1 _] := and3P hallE1.
pose tau12 := [predU \tau1(M) & \tau2(M)].
have t12E1: tau12.-group E1 by apply: sub_pgroup t1E1 => p t1p; apply/orP; left.
have [E21 hallE21 sE1E21] := Hall_superset solE sE1E t12E1.
have [sE21E t12E21 _] := and3P hallE21.
have [E2 hallE2] := Hall_exists \tau2(M) (solvableS sE21E solE).
have [sE2E21 t2E2 _] := and3P hallE2.
have hallE2_E: \tau2(M).-Hall(E) E2.
  by apply: subHall_Hall hallE21 _ hallE2 => p t2p; apply/orP; right.
exists E2 => //; split=> //.
suffices ->: E2 * E1 = E21 by apply: groupP.
have coE21: coprime #|E2| #|E1| := sub_pnat_coprime tau2'1 t2E2 t1E1.
apply/eqP; rewrite eqEcard mul_subG ?coprime_cardMg //=.
rewrite -(partnC \tau1(M) (cardG_gt0 E21)) (card_Hall hallE2) mulnC.
rewrite (card_Hall (pHall_subl sE1E21 sE21E hallE1)) leq_pmul2r //.
rewrite dvdn_leq // sub_in_partn // => p t12p t1'p.
by apply: contraLR (pnatPpi t12E21 t12p) => t2'p; apply/norP.
Qed.

Lemma coprime_sigma_compl : coprime #|M`_\sigma| #|E|.
Proof. exact: pnat_coprime (pcore_pgroup _ _) (pHall_pgroup hallE). Qed.
Let coMsE := coprime_sigma_compl.

Lemma pi_sigma_compl : \pi(E) =i [predD \pi(M) & \sigma(M)].
Proof. by move=> p; rewrite /= (card_Hall hallE) pi_of_part // !inE andbC. Qed.

Lemma sdprod_sigma : M`_\sigma ><| E = M.
Proof.
rewrite sdprodE ?coprime_TIg ?(subset_trans sEM) ?gFnorm //.
apply/eqP; rewrite eqEcard mul_subG ?pcore_sub ?coprime_cardMg //=.
by rewrite (card_Hall (Msigma_Hall maxM)) (card_Hall hallE) partnC.
Qed.

(* The preliminary remarks in the introduction of B & G, section 12. *)

Remark der1_sigma_compl : M^`(1) :&: E = E^`(1).
Proof.
have [nsMsM _ defM _ _] := sdprod_context sdprod_sigma.
by rewrite setIC (pprod_focal_coprime defM _ (subxx E)) ?(setIidPr _) ?der_sub.
Qed.

Remark partition_pi_mmax p :
  (p \in \pi(M)) =
     [|| p \in \tau1(M), p \in \tau2(M), p \in \tau3(M) | p \in \sigma(M)].
Proof.
symmetry; rewrite 2!orbA -!andb_orr orbAC -andb_orr orNb andbT.
rewrite orb_andl orNb /= -(orb_idl ((alpha_sub_sigma maxM) p)) orbA orbC -orbA.
rewrite !(eq_sym 'r_p(M)) -!leq_eqVlt p_rank_gt0 orb_idl //.
exact: sigma_sub_pi.
Qed.

Remark partition_pi_sigma_compl p :
  (p \in \pi(E)) = [|| p \in \tau1(M), p \in \tau2(M) | p \in \tau3(M)].
Proof.
rewrite pi_sigma_compl inE /= partition_pi_mmax !andb_orr /=.
by rewrite andNb orbF !(andbb, andbA) -2!andbA.
Qed.

Remark tau2E p : (p \in \tau2(M)) = (p \in \pi(E)) && ('r_p(E) == 2).
Proof.
have [P sylP] := Sylow_exists p E.
rewrite -(andb_idl (pnatPpi s'E)) -p_rank_gt0 -andbA; apply: andb_id2l => s'p.
have sylP_M := subHall_Sylow hallE s'p sylP.
by rewrite -(p_rank_Sylow sylP_M) (p_rank_Sylow sylP); case: posnP => // ->.
Qed.

Remark tau3E p : (p \in \tau3(M)) = (p \in \pi(E^`(1))) && ('r_p(E) == 1%N).
Proof.
have [P sylP] := Sylow_exists p E.
have hallE': \sigma(M)^'.-Hall(M^`(1)) E^`(1).
  by rewrite -der1_sigma_compl setIC (Hall_setI_normal _ hallE) ?der_normal.
rewrite 4!inE -(andb_idl (pnatPpi (pHall_pgroup hallE'))) -andbA.
apply: andb_id2l => s'p; have sylP_M := subHall_Sylow hallE s'p sylP.
rewrite -(p_rank_Sylow sylP_M) (p_rank_Sylow sylP) andbC; apply: andb_id2r.
rewrite eqn_leq p_rank_gt0 mem_primes => /and3P[_ p_pr _].
rewrite (card_Hall hallE') pi_of_part 3?inE ?mem_primes ?cardG_gt0 //=.
by rewrite p_pr inE /= s'p andbT.
Qed.

Remark tau1E p :
  (p \in \tau1(M)) = [&& p \in \pi(E), p \notin \pi(E^`(1)) & 'r_p(E) == 1%N].
Proof.
rewrite partition_pi_sigma_compl; apply/idP/idP=> [t1p|].
  have [s'p rpM _] := and3P t1p; have [P sylP] := Sylow_exists p E.
  have:= tau3'1 t1p; rewrite t1p /= inE /= tau3E -(p_rank_Sylow sylP).
  by rewrite (p_rank_Sylow (subHall_Sylow hallE s'p sylP)) rpM !andbT.
rewrite orbC andbC -andbA => /and3P[not_piE'p /eqP rpE].
by rewrite tau3E tau2E rpE (negPf not_piE'p) andbF.
Qed.

(* Generate a rank 2 elementary abelian tau2 subgroup in a given complement.  *)
Lemma ex_tau2Elem p :
  p \in \tau2(M) -> exists2 A, A \in 'E_p^2(E) & A \in 'E_p^2(M).
Proof.
move=> t2p; have [A Ep2A] := p_rank_witness p E.
have <-: 'r_p(E) = 2 by apply/eqP; move: t2p; rewrite tau2E; case/andP.
by exists A; rewrite // (subsetP (pnElemS p _ sEM)).
Qed.

(* A converse to the above Lemma: if E has an elementary abelian subgroup of  *)
(* order p^2, then p must be in tau2.                                         *)
Lemma sigma'2Elem_tau2 p A : A \in 'E_p^2(E) -> p \in \tau2(M).
Proof.
move=> Ep2A; have rE: 'r_p(E) > 1 by apply/p_rank_geP; exists A.
have: p \in \pi(E) by rewrite -p_rank_gt0 ltnW.
rewrite partition_pi_sigma_compl orbCA => /orP[] //.
by rewrite -!andb_orr eqn_leq leqNgt (leq_trans rE) ?andbF ?p_rankS.
Qed.

(* This is B & G, Lemma 12.1(a). *)
Lemma der1_sigma_compl_nil : nilpotent E^`(1).
Proof.
have sE'E := der_sub 1 E.
have nMaE: E \subset 'N(M`_\alpha) by rewrite (subset_trans sEM) ?gFnorm.
have tiMaE':  M`_\alpha :&: E^`(1) = 1.
  by apply/trivgP; rewrite -(coprime_TIg coMsE) setISS ?Malpha_sub_Msigma.
rewrite (isog_nil (quotient_isog (subset_trans sE'E nMaE) tiMaE')).
by rewrite (nilpotentS (quotientS _ (dergS 1 sEM))) ?Malpha_quo_nil.
Qed.

(* This is B & G, Lemma 12.1(g). *)
Lemma tau2_not_beta p :
  p \in \tau2(M) -> p \notin \beta(G) /\ {subset 'E_p^2(M) <= 'E*_p(G)}. 
Proof.
case/andP=> s'p /eqP rpM; split; first exact: sigma'_rank2_beta' rpM.
by apply/subsetP; apply: sigma'_rank2_max.
Qed.

End Introduction.

Implicit Arguments tau2'1 [[M] x].
Implicit Arguments tau3'1 [[M] x].
Implicit Arguments tau3'2 [[M] x].

(* This is the rest of B & G, Lemma 12.1 (parts b, c, d,e, and f). *)
Lemma sigma_compl_context M E E1 E2 E3 :
    M \in 'M -> sigma_complement M E E1 E2 E3 ->
  [/\ (*b*) E3 \subset E^`(1) /\ E3 <| E,
      (*c*) E2 :==: 1 -> E1 :!=: 1,
      (*d*) cyclic E1 /\ cyclic E3,
      (*e*) E3 ><| (E2 ><| E1) = E /\ E3 ><| E2 ><| E1 = E 
    & (*f*) 'C_E3(E) = 1].
Proof.
move=> maxM [hallE hallE1 hallE2 hallE3 groupE21].
have [sEM solM] := (pHall_sub hallE, mmax_sol maxM). 
have [[sE1E t1E1 _] [sE3E t3E3 _]] := (and3P hallE1, and3P hallE3).
have tiE'E1: E^`(1) :&: E1 = 1.
  rewrite coprime_TIg // coprime_pi' ?cardG_gt0 //.
  by apply: sub_pgroup t1E1 => p; rewrite (tau1E maxM hallE) => /and3P[].
have cycE1: cyclic E1.
  apply: nil_Zgroup_cyclic.
    rewrite odd_rank1_Zgroup ?mFT_odd //; apply: wlog_neg; rewrite -ltnNge.
    have [p p_pr ->]:= rank_witness E1; move/ltnW; rewrite p_rank_gt0.
    move/(pnatPpi t1E1); rewrite (tau1E maxM hallE) => /and3P[_ _ /eqP <-].
    by rewrite p_rankS.
  rewrite abelian_nil // /abelian (sameP commG1P trivgP) -tiE'E1.
  by rewrite subsetI (der_sub 1) (dergS 1).
have solE: solvable E := solvableS sEM solM.
have nilE': nilpotent E^`(1) := der1_sigma_compl_nil maxM hallE.
have nsE'piE pi: 'O_pi(E^`(1)) <| E by rewrite !gFnormal_trans.
have SylowE3 P: Sylow E3 P -> [/\ cyclic P, P \subset E^`(1) & 'C_P(E) = 1].
- case/SylowP=> p p_pr sylP; have [sPE3 pP _] := and3P sylP.
  have [-> | ntP] := eqsVneq P 1.
    by rewrite cyclic1 sub1G (setIidPl (sub1G _)).
  have t3p: p \in \tau3(M).
    rewrite (pnatPpi t3E3) // -p_rank_gt0 -(p_rank_Sylow sylP) -rank_pgroup //.
    by rewrite rank_gt0.
  have sPE: P \subset E := subset_trans sPE3 sE3E.
  have cycP: cyclic P.
    rewrite (odd_pgroup_rank1_cyclic pP) ?mFT_odd //.
    rewrite (tau3E maxM hallE) in t3p.
    by case/andP: t3p => _ /eqP <-; rewrite p_rankS.
  have nEp'E: E \subset 'N('O_p^'(E)) by apply: gFnorm.
  have nEp'P := subset_trans sPE nEp'E.
  have sylP_E := subHall_Sylow hallE3 t3p sylP.
  have nsEp'P_E: 'O_p^'(E) <*> P <| E.
    rewrite sub_der1_normal ?join_subG ?pcore_sub //=.
    rewrite norm_joinEr // -quotientSK ?gFsub_trans //=.
    have [_ /= <- _ _] := dprodP (nilpotent_pcoreC p nilE').
    rewrite -quotientMidr -mulgA (mulSGid (pcore_max _ _)) ?pcore_pgroup //=.
    rewrite quotientMidr quotientS //.
    apply: subset_trans (pcore_sub_Hall sylP_E).
    by rewrite pcore_max ?pcore_pgroup ?nsE'piE.
  have nEP_sol: solvable 'N_E(P) by rewrite (solvableS _ solE) ?subsetIl.
  have [K hallK] := Hall_exists p^' nEP_sol; have [sKNEP p'K _] := and3P hallK.
  have coPK: coprime #|P| #|K| := pnat_coprime pP p'K.
  have sP_NEP: P \subset 'N_E(P) by rewrite subsetI sPE normG.
  have mulPK: P * K = 'N_E(P).
    apply/eqP; rewrite eqEcard mul_subG //= coprime_cardMg // (card_Hall hallK).
    by rewrite (card_Hall (pHall_subl sP_NEP (subsetIl E _) sylP_E)) partnC.
  have{sKNEP} [sKE nPK] := subsetIP sKNEP; have nEp'K := subset_trans sKE nEp'E.
  have defE: 'O_p^'(E) <*> K * P = E.
    have sP_Ep'P: P \subset 'O_p^'(E) <*> P := joing_subr _ _.
    have sylP_Ep'P := pHall_subl sP_Ep'P (normal_sub nsEp'P_E) sylP_E.
    rewrite -{2}(Frattini_arg nsEp'P_E sylP_Ep'P) /= !norm_joinEr //.
    by rewrite -mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA.
  have ntPE': P :&: E^`(1) != 1.
    have sylPE' := Hall_setI_normal (der_normal 1 E) sylP_E. 
    rewrite -rank_gt0 (rank_Sylow sylPE') p_rank_gt0.
    by rewrite (tau3E maxM hallE) in t3p; case/andP: t3p.
  have defP := coprime_abelian_cent_dprod nPK coPK (cyclic_abelian cycP).
  have{defP} [[PK1 _]|[regKP defP]] := cyclic_pgroup_dprod_trivg pP cycP defP.
    have coP_Ep'K: coprime #|P| #|'O_p^'(E) <*> K|.
      rewrite (pnat_coprime pP) // -pgroupE norm_joinEr //.
      by rewrite pgroupM pcore_pgroup.
    rewrite -subG1 -(coprime_TIg coP_Ep'K) setIS ?der1_min // in ntPE'.
      rewrite -{1}defE mulG_subG normG normsY // cents_norm //.
      exact/commG1P.
    by rewrite -{2}defE quotientMidl quotient_abelian ?cyclic_abelian.
  split=> //; first by rewrite -defP commgSS.
  by apply/trivgP; rewrite -regKP setIS ?centS.
have sE3E': E3 \subset E^`(1).
  by rewrite -(Sylow_gen E3) gen_subG; apply/bigcupsP=> P; case/SylowE3.
have cycE3: cyclic E3.
  rewrite nil_Zgroup_cyclic ?(nilpotentS sE3E') //.
  by apply/forall_inP => P; case/SylowE3.
have regEE3: 'C_E3(E) = 1.
  have [// | [p p_pr]] := trivgVpdiv 'C_E3(E).
  case/Cauchy=> // x /setIP[]; rewrite -!cycle_subG => sXE3 cEX ox.
  have pX: p.-elt x by rewrite /p_elt ox pnat_id.
  have [P sylP sXP] := Sylow_superset sXE3 pX.
  suffices: <[x]> == 1 by case/idPn; rewrite cycle_eq1 -order_gt1 ox prime_gt1.
  rewrite -subG1; case/SylowE3: (p_Sylow sylP) => _ _ <-.
  by rewrite subsetI sXP.
have nsE3E: E3 <| E.
  have hallE3_E' := pHall_subl sE3E'  (der_sub 1 E) hallE3.
  by rewrite (nilpotent_Hall_pcore nilE' hallE3_E') /=.
have [sE2E t2E2 _] := and3P hallE2; have [_ nE3E] := andP nsE3E.
have coE21: coprime #|E2| #|E1| := sub_pnat_coprime tau2'1 t2E2 t1E1.
have coE31: coprime #|E3| #|E1| := sub_pnat_coprime tau3'1 t3E3 t1E1.
have coE32: coprime #|E3| #|E2| := sub_pnat_coprime tau3'2 t3E3 t2E2.
have{groupE21} defE: E3 ><| (E2 ><| E1) = E.
  have defE21: E2 * E1 = E2 <*> E1 by rewrite -genM_join gen_set_id.
  have sE21E: E2 <*> E1 \subset E by rewrite join_subG sE2E.
  have nE3E21 := subset_trans sE21E nE3E.
  have coE312: coprime #|E3| #|E2 <*> E1|.
    by rewrite -defE21 coprime_cardMg // coprime_mulr coE32.
  have nE21: E1 \subset 'N(E2).
    rewrite (subset_trans (joing_subr E2 E1)) ?sub_der1_norm ?joing_subl //.
    rewrite /= -{2}(mulg1 E2) -(setIidPr (der_sub 1 _)) /=.
    rewrite -(coprime_mulG_setI_norm defE21) ?gFnorm //.
    by rewrite mulgSS ?subsetIl // -tiE'E1 setIC setSI ?dergS.
  rewrite (sdprodEY nE21) ?sdprodE ?coprime_TIg //=.
  apply/eqP; rewrite eqEcard mul_subG // coprime_cardMg //= -defE21.
  rewrite -(partnC \tau3(M) (cardG_gt0 E)) (card_Hall hallE3) leq_mul //.
  rewrite coprime_cardMg // (card_Hall hallE1) (card_Hall hallE2).
  rewrite -[#|E|`__](partnC \tau2(M)) ?leq_mul ?(partn_part _ tau3'2) //.
  rewrite -partnI dvdn_leq // sub_in_partn // => p piEp; apply/implyP.
  rewrite inE /= -negb_or /= orbC implyNb orbC.
  by rewrite -(partition_pi_sigma_compl maxM hallE).
split=> // [/eqP E2_1|]; last split=> //.
  apply: contraTneq (sol_der1_proper solM (subxx _) (mmax_neq1 maxM)) => E1_1.
  case/sdprodP: (sdprod_sigma maxM hallE) => _ defM _ _.
  rewrite properE der_sub /= negbK -{1}defM mulG_subG Msigma_der1 //.
  by rewrite -defE E1_1 E2_1 !sdprodg1 (subset_trans sE3E') ?dergS //.
case/sdprodP: defE => [[_ E21 _ defE21]]; rewrite defE21 => defE nE321 tiE321.
have{defE21} [_ defE21 nE21 tiE21] := sdprodP defE21.
have [nE32 nE31] := (subset_trans sE2E nE3E, subset_trans sE1E nE3E).
rewrite [E3 ><| _]sdprodEY ? sdprodE ?coprime_TIg ?normsY //=.
  by rewrite norm_joinEr // -mulgA defE21.
by rewrite norm_joinEr // coprime_cardMg // coprime_mull coE31.
Qed.

(* This is B & G, Lemma 12.2(a). *)
Lemma prime_class_mmax_norm M p X :
     M \in 'M -> p.-group X -> 'N(X) \subset M ->
  (p \in \sigma(M)) || (p \in \tau2(M)).
Proof.
move=> maxM pX sNM; rewrite -implyNb; apply/implyP=> sM'p. 
by rewrite 3!inE /= sM'p (sigma'_norm_mmax_rank2 _ _ pX).
Qed.

(* This is B & G, Lemma 12.2(b). *)
Lemma mmax_norm_notJ M Mstar p X :
    M \in 'M -> Mstar \in 'M ->
    p.-group X -> X \subset M -> 'N(X) \subset Mstar ->
    [|| [&& p \in \sigma(M) & M :!=: Mstar], p \in \tau1(M) | p \in \tau3(M)] ->
  gval Mstar \notin M :^: G.
Proof.
move: Mstar => H maxM maxH pX sXM sNH; apply: contraL => MG_H.
have [x Gx defH] := imsetP MG_H.
have [sMp | sM'p] := boolP (p \in \sigma(M)); last first.
  have:= prime_class_mmax_norm maxH pX sNH.
  rewrite defH /= sigmaJ tau2J !negb_or (negPf sM'p) /= => t2Mp.
  by rewrite (contraL (@tau2'1 _ p)) // [~~ _]tau3'2.
rewrite 3!inE sMp 3!inE sMp orbF negbK.
have [_ transCX _] := sigma_group_trans maxM sMp pX.
set maxMX := finset _ in transCX.
have maxMX_H: gval H \in maxMX by rewrite inE MG_H (subset_trans (normG X)).
have maxMX_M: gval M \in maxMX by rewrite inE orbit_refl.
have [y cXy ->] := atransP2 transCX maxMX_H maxMX_M.
by rewrite /= conjGid // (subsetP sNH) // (subsetP (cent_sub X)).
Qed.

(* This is B & G, Lemma 12.3. *)
Lemma nonuniq_p2Elem_cent_sigma M Mstar p A A0 :
    M \in 'M -> Mstar \in 'M -> Mstar :!=: M -> A \in 'E_p^2(M) ->
    A0 \in 'E_p^1(A) -> 'N(A0) \subset Mstar ->
 [/\ (*a*) p \notin \sigma(M) -> A \subset 'C(M`_\sigma :&: Mstar)
   & (*b*) p \notin \alpha(M) -> A \subset 'C(M`_\alpha :&: Mstar)].
Proof.
move: Mstar => H maxM maxH neqMH Ep2A EpA0 sNH.
have p_pr := pnElem_prime Ep2A.
have [sAM abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have [sA0A _ _] := pnElemP EpA0; have pA0 := pgroupS sA0A pA.
have sAH: A \subset H.
  by apply: subset_trans (cents_norm _) sNH; apply: subset_trans (centS sA0A).
have nsHsH: H`_\sigma <| H by apply: pcore_normal.
have [sHsH nHsH] := andP nsHsH; have nHsA := subset_trans sAH nHsH.
have nsHsA_H: H`_\sigma <*> A <| H.
  have [sHp | sH'p] := boolP (p \in \sigma(H)).
    rewrite (joing_idPl _) ?pcore_normal //.
    by rewrite (sub_Hall_pcore (Msigma_Hall _)) // (pi_pgroup pA).
  have [P sylP sAP] := Sylow_superset sAH pA.
  have excH: exceptional_FTmaximal p H A0 A by split=> //; apply/pnElemP.
  exact: exceptional_mul_sigma_normal excH sylP sAP.
have cAp' K:
    p^'.-group K -> A \subset 'N(K) -> K \subset H ->
  [~: K, A] \subset K :&: H`_\sigma.
- move=> p'K nKA sKH; have nHsK := subset_trans sKH nHsH.
  rewrite subsetI commg_subl nKA /= -quotient_sub1 ?comm_subG // quotientR //=.
  have <-: K / H`_\sigma :&: A / H`_\sigma = 1.
    by rewrite setIC coprime_TIg ?coprime_morph ?(pnat_coprime pA p'K).
  rewrite subsetI commg_subl commg_subr /= -{2}(quotientYidr nHsA).
  by rewrite !quotient_norms //= joingC (subset_trans sKH) ?normal_norm.
have [sMp | sM'p] := boolP (p \in \sigma(M)).
  split=> // aM'p; have notMGH: gval H \notin M :^: G.
    apply: mmax_norm_notJ maxM maxH pA0 (subset_trans sA0A sAM) sNH _.
    by rewrite sMp eq_sym neqMH.
  rewrite centsC (sameP commG1P trivgP).
  apply: subset_trans (cAp' _ _ _ (subsetIr _ _)) _.
  - exact: pi_p'group (pgroupS (subsetIl _ _) (pcore_pgroup _ _)) aM'p.
  - by rewrite (normsI _ (normsG sAH)) // (subset_trans sAM) ?gFnorm.
  by rewrite setIAC; case/sigma_disjoint: notMGH => // -> _ _; apply: subsetIl.
suffices cMaA: A \subset 'C(M`_\sigma :&: H).
  by rewrite !{1}(subset_trans cMaA) ?centS ?setSI // Malpha_sub_Msigma.
have [sHp | sH'p] := boolP (p \in \sigma(H)); last first.
  apply/commG1P; apply: contraNeq neqMH => ntA_MsH.
  have [P sylP sAP] := Sylow_superset sAH pA.
  have excH: exceptional_FTmaximal p H A0 A by split=> //; apply/pnElemP.
  have maxAM: M \in 'M(A) by apply/setIdP.
  rewrite (exceptional_sigma_uniq maxH excH sylP sAP maxAM) //.
  apply: contraNneq ntA_MsH => tiMsHs; rewrite -subG1.
  have [sHsA_H nHsA_H] := andP nsHsA_H.
  have <-: H`_\sigma <*> A :&: M`_\sigma = 1.
    apply/trivgP; rewrite -tiMsHs subsetI subsetIr /=.
    rewrite -quotient_sub1 ?subIset ?(subset_trans sHsA_H) //.
    rewrite quotientGI ?joing_subl //= joingC quotientYidr //.
    rewrite setIC coprime_TIg ?coprime_morph //.
    rewrite (pnat_coprime (pcore_pgroup _ _)) // (card_pnElem Ep2A).
    by rewrite pnat_exp ?orbF ?pnatE.
  rewrite commg_subI // subsetI ?joing_subr ?subsetIl. 
    by rewrite (subset_trans sAM) ?gFnorm.
  by rewrite setIC subIset ?nHsA_H.
have sAHs: A \subset H`_\sigma.
  by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup pA).
have [S sylS sAS] := Sylow_superset sAHs pA; have [sSHs pS _] := and3P sylS.
have nsHaH: H`_\alpha <| H := pcore_normal _ _; have [_ nHaH] := andP nsHaH.
have nHaS := subset_trans (subset_trans sSHs sHsH) nHaH.
have nsHaS_H: H`_\alpha <*> S <| H.
  rewrite -{2}(quotientGK nsHaH) (norm_joinEr nHaS) -quotientK //.
  rewrite cosetpre_normal; apply: char_normal_trans (quotient_normal _ nsHsH).
  rewrite /= (nilpotent_Hall_pcore _ (quotient_pHall _ sylS)) ?pcore_char //.
  exact: nilpotentS (quotientS _ (Msigma_der1 maxH)) (Malpha_quo_nil maxH).
rewrite (sameP commG1P trivgP).
have <-: H`_\alpha <*> S :&: M`_\sigma = 1.
  have: gval M \notin H :^: G.
    by apply: contra sM'p; case/imsetP=> x _ ->; rewrite sigmaJ.
  case/sigma_disjoint=> // _ ti_aHsM _.
  rewrite setIC coprime_TIg ?(pnat_coprime (pcore_pgroup _ _)) //=.
  rewrite norm_joinEr // [pnat _ _]pgroupM (pi_pgroup pS) // andbT.
  apply: sub_pgroup (pcore_pgroup _ _) => q aHq.
  by apply: contraFN (ti_aHsM q) => sMq; rewrite inE /= aHq.
rewrite commg_subI // subsetI ?subsetIl.
  by rewrite (subset_trans sAS) ?joing_subr ?(subset_trans sAM) ?gFnorm.
by rewrite setIC subIset 1?normal_norm.
Qed.

(* This is B & G, Proposition 12.4. *)
Proposition p2Elem_mmax M p A :
      M \in 'M -> A \in 'E_p^2(M) ->
    (*a*) 'C(A) \subset M
 /\ (*b*) ([forall A0 in 'E_p^1(A), 'M('N(A0)) != [set M]] ->
           [/\ p \in \sigma(M), M`_\alpha = 1 & nilpotent M`_\sigma]).
Proof.
move=> maxM Ep2A; have p_pr := pnElem_prime Ep2A.
have [sAM abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have [EpAnonuniq |] := altP forall_inP; last first.
  rewrite negb_forall_in; case/exists_inP=> A0 EpA0; rewrite negbK.
  case/eqP/mem_uniq_mmax=> _ sNA0_M; rewrite (subset_trans _ sNA0_M) //.
  by have [sA0A _ _] := pnElemP EpA0; rewrite cents_norm // centS.
have{EpAnonuniq} sCMkApCA y: y \in A^# ->
  [/\ 'r('C_M(<[y]>)) <= 2,
      p \in \sigma(M)^' -> 'C_(M`_\sigma)[y] \subset 'C_M(A)
    & p \in \alpha(M)^' -> 'C_(M`_\alpha)[y] \subset 'C_M(A)].
- case/setD1P=> nty Ay; pose Y := <[y]>%G.
  rewrite -cent_cycle -[<[y]>]/(gval Y).
  have EpY: Y \in 'E_p^1(A).
    by rewrite p1ElemE // 2!inE cycle_subG Ay -orderE (abelem_order_p abelA) /=.
  have [sYA abelY dimY] := pnElemP EpY; have [pY _] := andP abelY.
  have [H maxNYH neqHM]: exists2 H, H \in 'M('N(Y)) & H \notin [set M].
    apply/subsetPn; rewrite subset1 negb_or EpAnonuniq //=.
    apply/set0Pn; have [|H] := (@mmax_exists _ 'N(Y)); last by exists H.
    rewrite mFT_norm_proper ?(mFT_pgroup_proper pY) //.
    by rewrite -rank_gt0 (rank_abelem abelY) dimY.
  have{maxNYH} [maxH sNYH] := setIdP maxNYH; rewrite inE -val_eqE /= in neqHM.
  have ->: 'r('C_M(Y)) <= 2.
    apply: contraR neqHM; rewrite -ltnNge => rCMYgt2.
    have uniqCMY: 'C_M(Y)%G \in 'U.
      by rewrite rank3_Uniqueness ?(sub_mmax_proper maxM) ?subsetIl.
    have defU: 'M('C_M(Y)) = [set M] by apply: def_uniq_mmax; rewrite ?subsetIl.
    rewrite (eq_uniq_mmax defU maxH) ?subIset //.
    by rewrite orbC (subset_trans (cent_sub Y)).
  have [cAMs cAMa] := nonuniq_p2Elem_cent_sigma maxM maxH neqHM Ep2A EpY sNYH.
  do 2!rewrite {1}subsetI {1}(subset_trans (subsetIl _ _) (pcore_sub _ _)).
  have sCYH: 'C(Y) \subset H := subset_trans (cent_sub Y) sNYH.
  by split=> // [/cAMs | /cAMa]; rewrite centsC; apply/subset_trans/setIS.
have ntA: A :!=: 1 by rewrite -rank_gt0 (rank_abelem abelA) dimA.
have ncycA: ~~ cyclic A by rewrite (abelem_cyclic abelA) dimA.
have rCMAle2: 'r('C_M(A)) <= 2.
  have [y Ay]: exists y, y \in A^# by apply/set0Pn; rewrite setD_eq0 subG1.
  have [rCMy _ _] := sCMkApCA y Ay; apply: leq_trans rCMy.
  by rewrite rankS // setIS // centS // cycle_subG; case/setIdP: Ay.
have sMp: p \in \sigma(M).
  apply: contraFT (ltnn 1) => sM'p; rewrite -dimA -(rank_abelem abelA).
  suffices cMsA: A \subset 'C(M`_\sigma).
    by rewrite -(setIidPl cMsA) sub'cent_sigma_rank1 // (pi_pgroup pA).
  have nMsA: A \subset 'N(M`_\sigma) by rewrite (subset_trans sAM) ?gFnorm.
  rewrite centsC /= -(coprime_abelian_gen_cent1 _ _ nMsA) //; last first.
    exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _).
  rewrite gen_subG; apply/bigcupsP=> y; case/sCMkApCA=> _ sCMsyCA _.
  by rewrite (subset_trans (sCMsyCA sM'p)) ?subsetIr.
have [P sylP sAP] := Sylow_superset sAM pA; have [sPM pP _] := and3P sylP.
pose Z := 'Ohm_1('Z(P)).
have sZA: Z \subset A.
  have maxA: A \in 'E*_p('C_M(A)).
    have sACMA: A \subset 'C_M(A) by rewrite subsetI sAM.
    rewrite (subsetP (p_rankElem_max _ _)) // !inE abelA sACMA.
    rewrite eqn_leq logn_le_p_rank /=; last by rewrite !inE sACMA abelA.
    by rewrite dimA (leq_trans (p_rank_le_rank _ _)).
  rewrite [Z](OhmE 1 (pgroupS (center_sub P) pP)) gen_subG.
  rewrite -(pmaxElem_LdivP p_pr maxA) -(setIA M) setIid setSI //=.
  by rewrite setISS // centS.
have{ntA} ntZ: Z != 1.
  by rewrite Ohm1_eq1 (center_nil_eq1 (pgroup_nil pP)) (subG1_contra sAP).
have rPle2: 'r(P) <= 2.
  have [z Zz ntz]: exists2 z, z \in Z & z \notin [1].
    by apply/subsetPn; rewrite subG1.
  have [|rCMz _ _] := sCMkApCA z; first by rewrite inE ntz (subsetP sZA).
  rewrite (leq_trans _ rCMz) ?rankS // subsetI sPM centsC cycle_subG.
  by rewrite (subsetP _ z Zz) // gFsub_trans ?subsetIr.
have aM'p: p \in \alpha(M)^'.
   by rewrite !inE -leqNgt -(p_rank_Sylow sylP) -rank_pgroup.
have sMaCMA: M`_\alpha \subset 'C_M(A).
have nMaA: A \subset 'N(M`_\alpha) by rewrite (subset_trans sAM) ?gFnorm.
  rewrite -(coprime_abelian_gen_cent1 _ _ nMaA) //; last first.
    exact: (pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _)).
  rewrite gen_subG; apply/bigcupsP=> y; case/sCMkApCA=> _ _ sCMayCA.
  by rewrite (subset_trans (sCMayCA aM'p)) ?subsetIr.
have Ma1: M`_\alpha = 1.
  have [q q_pr rMa]:= rank_witness M`_\alpha.
  apply: contraTeq rCMAle2; rewrite -ltnNge -rank_gt0 rMa p_rank_gt0 => piMa_q.
  have aMq: q \in \alpha(M) := pnatPpi (pcore_pgroup _ _) piMa_q.
  apply: leq_trans (rankS sMaCMA); rewrite rMa.
  have [Q sylQ] := Sylow_exists q M`_\alpha; rewrite -(p_rank_Sylow sylQ).
  by rewrite (p_rank_Sylow (subHall_Sylow (Malpha_Hall maxM) aMq sylQ)).
have nilMs: nilpotent M`_\sigma.
  rewrite (nilpotentS (Msigma_der1 maxM)) // (isog_nil (quotient1_isog _)).
  by rewrite -Ma1 Malpha_quo_nil.
rewrite (subset_trans (cents_norm (centS sZA))) ?(mmax_normal maxM) //=.
have{sylP} sylP: p.-Sylow(M`_\sigma) P.
  apply: pHall_subl _ (pcore_sub _ _) sylP.
  by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) // (pi_pgroup pP).
by rewrite (nilpotent_Hall_pcore _ sylP) ?gFnormal_trans.
Qed.

(* This is B & G, Theorem 12.5(a) -- this part does not mention a specific   *)
(* rank 2 elementary abelian \tau_2(M) subgroup of M.                        *)

Theorem tau2_Msigma_nil M p : M \in 'M -> p \in \tau2(M) -> nilpotent M`_\sigma.
Proof.
move=> maxM t2Mp; have [sM'p /eqP rpM] := andP t2Mp.
have [A Ep2A] := p_rank_witness p M; rewrite rpM in Ep2A.
have [_]:= p2Elem_mmax maxM Ep2A; rewrite -negb_exists_in [p \in _](negPf sM'p).
have [[A0 EpA0 /eqP/mem_uniq_mmax[_ sNA0M _]] | _ [] //] := exists_inP.
have{EpA0 sNA0M} excM: exceptional_FTmaximal p M A0 A by [].
have [sAM abelA _] := pnElemP Ep2A; have [pA _] := andP abelA.
have [P sylP sAP] := Sylow_superset sAM pA.
exact: exceptional_sigma_nil maxM excM sylP sAP.
Qed.

(* This is B & G, Theorem 12.5 (b-f) -- the bulk of the Theorem. *)
Theorem tau2_context M p A (Ms := M`_\sigma) :
    M \in 'M -> p \in \tau2(M) -> A \in 'E_p^2(M) ->
  [/\ (*b*) forall P, p.-Sylow(M) P ->
                abelian P
             /\ (A \subset P -> 'Ohm_1(P) = A /\ ~~ ('N(P) \subset M)),
      (*c*)  Ms <*> A <| M,
      (*d*) 'C_Ms(A) = 1,
      (*e*) forall Mstar, Mstar \in 'M(A) :\ M -> Ms :&: Mstar = 1
    & (*f*) exists2 A1, A1 \in 'E_p^1(A) & 'C_Ms(A1) = 1].
Proof.
move=> maxM t2Mp Ep2A; have [sM'p _] := andP t2Mp.
have [_]:= p2Elem_mmax maxM Ep2A; rewrite -negb_exists_in [p \in _](negPf sM'p).
have [[A0 EpA0 /eqP/mem_uniq_mmax[_ sNA0M _]] | _ [] //] := exists_inP.
have{EpA0 sNA0M} excM: exceptional_FTmaximal p M A0 A by [].
have strM := exceptional_structure maxM excM.
have [sAM abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have [P sylP sAP] := Sylow_superset sAM pA.
have nsMsA_M : Ms <*> A <| M := exceptional_mul_sigma_normal maxM excM sylP sAP.
have [_ regA [A1 EpA1 [_ _ [_ regA1 _]]]] := strM P sylP sAP.
split=> // [P1 sylP1 | {P sylP sAP A0 excM}H| ]; last by exists A1.
  split=> [|sAP1]; first exact: (exceptional_Sylow_abelian _ excM sylP).
  split; first by case/strM: sylP1.
  by apply: contra sM'p => sNP1M; apply/exists_inP; exists P1; rewrite // ?inE.
case/setD1P; rewrite -val_eqE /= => neqHM /setIdP[maxH sAH].
apply/trivgP; rewrite -regA subsetI subsetIl /=.
have Ep2A_H: A \in 'E_p^2(H) by apply/pnElemP.
have [_]:= p2Elem_mmax maxH Ep2A_H; rewrite -negb_exists_in.
have [[A0 EpA0 /eqP/mem_uniq_mmax[_ sNA0H _]]|_ [//|sHp _ nilHs]] := exists_inP.
  have [cMSH_A _]:= nonuniq_p2Elem_cent_sigma maxM maxH neqHM Ep2A EpA0 sNA0H.
  by rewrite centsC cMSH_A.
have [P sylP sAP] := Sylow_superset sAH pA; have [sPH pP _] := and3P sylP.
have sylP_Hs: p.-Sylow(H`_\sigma) P.
  rewrite (pHall_subl _ (pcore_sub _ _) sylP) //.
  by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup pP).
have nPH: H \subset 'N(P).
  by rewrite (nilpotent_Hall_pcore nilHs sylP_Hs) !gFnorm_trans ?normG.
have coMsP: coprime #|M`_\sigma| #|P|.
  exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat pP _).
rewrite (sameP commG1P trivgP) -(coprime_TIg coMsP) commg_subI ?setIS //.
by rewrite subsetI sAP (subset_trans sAM) ?gFnorm.
Qed.

(* This is B & G, Corollary 12.6 (a, b, c & f) -- i.e., the assertions that   *)
(* do not depend on the decomposition of the complement.                      *)
Corollary tau2_compl_context M E p A (Ms := M`_\sigma) :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) ->
  [/\ (*a*) A <| E /\ 'E_p^1(E) = 'E_p^1(A),
      (*b*) [/\ 'C(A) \subset E, 'N_M(A) = E & ~~ ('N(A) \subset M)],
      (*c*) forall X, X \in 'E_p^1(E) -> 'C_Ms(X) != 1 -> 'M('C(X)) = [set M]
    & (*f*) forall Mstar,
              Mstar \in 'M -> gval Mstar \notin M :^: G ->
            Ms :&: Mstar`_\sigma = 1
         /\ [predI \sigma(M) & \sigma(Mstar)] =i pred0].
Proof.
move=> maxM hallE t2Mp Ep2A; have [sEM sM'E _] := and3P hallE.
have [p_pr [sM'p _]] := (pnElem_prime Ep2A, andP t2Mp).
have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have [_ mulMsE nMsE tiMsE] := sdprodP (sdprod_sigma maxM hallE).
have Ep2A_M: A \in 'E_p^2(M) by rewrite (subsetP (pnElemS _ _ sEM)).
have [syl_p_M nsMsAM regA tiMsMA _] := tau2_context maxM t2Mp Ep2A_M.
have nMsA: A \subset 'N(Ms) := subset_trans sAE nMsE.
have nsAE: A <| E.
  rewrite /normal sAE -(mul1g A) -tiMsE setIC group_modr // normsI ?normG //.
  by rewrite (subset_trans sEM) // -(norm_joinEr nMsA) normal_norm.
have sAsylE P: p.-Sylow(E) P -> 'Ohm_1(P) = A /\ ~~ ('N(P) \subset M).
  move=> sylP; have sylP_M: p.-Sylow(M) P by apply: (subHall_Sylow hallE).
  have [_] := syl_p_M P sylP_M; apply.
  exact: subset_trans (pcore_max pA nsAE) (pcore_sub_Hall sylP).
have not_sNA_M: ~~ ('N(A) \subset M).
  have [P sylP] := Sylow_exists p E; have [<-]:= sAsylE P sylP.
  exact/contra/subset_trans/gFnorms.
have{sAsylE syl_p_M} defEpE: 'E_p^1(E) = 'E_p^1(A).
  apply/eqP; rewrite eqEsubset andbC pnElemS //.
  apply/subsetP=> X /pnElemP[sXE abelX dimX]; apply/pnElemP; split=> //.
  have [pX _ eX] := and3P abelX; have [P sylP sXP] := Sylow_superset sXE pX.
  have [<- _]:= sAsylE P sylP; have [_ pP _] := and3P sylP.
  by rewrite (OhmE 1 pP) sub_gen // subsetI sXP sub_LdivT.
have defNMA: 'N_M(A) = E.
  rewrite -mulMsE setIC -group_modr ?normal_norm //= setIC.
  rewrite coprime_norm_cent ?regA ?mul1g //.
  exact: (pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _)).
have [sCAM _]: 'C(A) \subset M /\ _  := p2Elem_mmax maxM Ep2A_M.
have sCAE: 'C(A) \subset E by rewrite -defNMA subsetI sCAM cent_sub.
split=> // [X EpX | H maxH not_MGH]; last first.
  by case/sigma_disjoint: not_MGH => // _ _; apply; apply: tau2_Msigma_nil t2Mp.
rewrite defEpE in EpX; have [sXA abelX dimX] := pnElemP EpX.
have ntX: X :!=: 1 by rewrite -rank_gt0 (rank_abelem abelX) dimX.
apply: contraNeq => neq_maxCX_M.
have{neq_maxCX_M} [H]: exists2 H, H \in 'M('C(X)) & H \notin [set M].
  apply/subsetPn; rewrite subset1 negb_or neq_maxCX_M.
  by have [H maxH]:= mmax_exists (mFT_cent_proper ntX); apply/set0Pn; exists H.
case/setIdP=> maxH sCXH neqHM.
rewrite -subG1 -(tiMsMA H) ?setIS // inE neqHM inE maxH.
exact: subset_trans (sub_abelian_cent cAA sXA) sCXH.
Qed.

(* This is B & G, Corollary 12.6 (d, e) -- the parts that apply to a          *)
(* particular decomposition of the complement. We included an easy consequece *)
(* of part (a), that A is a subgroup of E2, as this is used implicitly later  *)
(* in sections 12 and 13.                                                     *)
Corollary tau2_regular M E E1 E2 E3 p A (Ms := M`_\sigma) :
    M \in 'M -> sigma_complement M E E1 E2 E3 ->
    p \in \tau2(M) -> A \in 'E_p^2(E) ->
  [/\ (*d*) semiregular Ms E3,
      (*e*) semiregular Ms 'C_E1(A)
          & A \subset E2].
Proof.
move=> maxM complEi t2Mp Ep2A; have p_pr := pnElem_prime Ep2A.
have [hallE hallE1 hallE2 hallE3 _] := complEi.
have [sEM sM'E _] := and3P hallE; have [sM'p _] := andP t2Mp.
have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have Ep2A_M: A \in 'E_p^2(M) by rewrite (subsetP (pnElemS _ _ sEM)).
have [_ _ _ tiMsMA _] := tau2_context maxM t2Mp Ep2A_M.
have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2Mp Ep2A.
have [sCAM _]: 'C(A) \subset M /\ _  := p2Elem_mmax maxM Ep2A_M.
have sAE2: A \subset E2.
  exact: normal_sub_max_pgroup (Hall_max hallE2) (pi_pnat pA _) nsAE.
split=> // x /setD1P[ntx]; last first.
  case/setIP; rewrite -cent_cycle -!cycle_subG => sXE1 cAX.
  pose q := pdiv #[x]; have piXq: q \in \pi(#[x]) by rewrite pi_pdiv order_gt1.
  have [Q sylQ] := Sylow_exists q <[x]>; have [sQX qQ _] := and3P sylQ.
  have [sE1E t1E1 _] := and3P hallE1; have sQE1 := subset_trans sQX sXE1.
  have sQM := subset_trans sQE1 (subset_trans sE1E sEM).
  have [H /setIdP[maxH sNQH]]: {H | H \in 'M('N(Q))}.
    apply: mmax_exists; rewrite mFT_norm_proper ?(mFT_pgroup_proper qQ) //.
    by rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ) p_rank_gt0.
  apply/trivgP; rewrite -(tiMsMA H) ?setIS //.
    by rewrite (subset_trans _ sNQH) ?cents_norm ?centS.
  rewrite 3!inE maxH /=; apply/andP; split.
    apply: contra_orbit (mmax_norm_notJ maxM maxH qQ sQM sNQH _).
    by rewrite (pnatPpi (pgroupS sXE1 t1E1)) ?orbT.
  by rewrite (subset_trans _ sNQH) ?cents_norm // centsC (subset_trans sQX).
rewrite -cent_cycle -cycle_subG => sXE3.
pose q := pdiv #[x]; have piXq: q \in \pi(#[x]) by rewrite pi_pdiv order_gt1.
have [Q sylQ] := Sylow_exists q <[x]>; have [sQX qQ _] := and3P sylQ.
have [sE3E t3E3 _] := and3P hallE3; have sQE3 := subset_trans sQX sXE3.
have sQM := subset_trans sQE3 (subset_trans sE3E sEM).
have [H /setIdP[maxH sNQH]]: {H | H \in 'M('N(Q))}.
  apply: mmax_exists; rewrite mFT_norm_proper ?(mFT_pgroup_proper qQ) //.
  by rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ) p_rank_gt0.
apply/trivgP; rewrite -(tiMsMA H) ?setIS //.
  by rewrite (subset_trans _ sNQH) ?cents_norm ?centS.
rewrite 3!inE maxH /=; apply/andP; split.
  apply: contra_orbit (mmax_norm_notJ maxM maxH qQ sQM sNQH _).
  by rewrite (pnatPpi (pgroupS sXE3 t3E3)) ?orbT.
rewrite (subset_trans _ sNQH) ?cents_norm // (subset_trans _ (centS sQE3)) //.
have coE3A: coprime #|E3| #|A|.
  by rewrite (pnat_coprime t3E3 (pi_pnat pA _)) ?tau3'2.
rewrite (sameP commG1P trivgP) -(coprime_TIg coE3A) subsetI commg_subl.
have [[_ nsE3E] _ _ _ _] := sigma_compl_context maxM complEi.
by rewrite commg_subr (subset_trans sE3E) ?(subset_trans sAE) ?normal_norm.
Qed.

(* This is B & G, Theorem 12.7. *)
Theorem nonabelian_tau2 M E p A P0 (Ms := M`_\sigma) (A0 := 'C_A(Ms)%G) :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) ->
    p.-group P0 -> ~~ abelian P0 ->
 [/\ (*a*) \tau2(M) =i (p : nat_pred),
     (*b*) #|A0| = p /\ Ms \x A0 = 'F(M),
     (*c*) forall X,
             X \in 'E_p^1(E) :\ A0 -> 'C_Ms(X) = 1 /\ ~~ ('C(X) \subset M)
   & (*d*) exists2 E0 : {group gT}, A0 ><| E0 = E
   & (*e*) forall x, x \in Ms^# -> {subset \pi('C_E0[x]) <= \tau1(M)}].
Proof.
rewrite {}/A0 => maxM hallE t2Mp Ep2A pP0 not_cP0P0 /=.
have p_pr := pnElem_prime Ep2A.
have [sEM sM'E _] := and3P hallE; have [sM'p _] := andP t2Mp.
have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have Ep2A_M: A \in 'E_p^2(M) by rewrite (subsetP (pnElemS _ _ sEM)).
have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE.
have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3.
have [regE3 _ sAE2] := tau2_regular maxM complEi t2Mp Ep2A.
have [P sylP sAP] := Sylow_superset sAE2 pA; have [sPE2 pP _] := and3P sylP.
have [S /= sylS sPS] := Sylow_superset (subsetT P) pP.
have pS := pHall_pgroup sylS; have sAS := subset_trans sAP sPS.
have sylP_E: p.-Sylow(E) P := subHall_Sylow hallE2 t2Mp sylP.
have sylP_M: p.-Sylow(M) P := subHall_Sylow hallE sM'p sylP_E.
have [syl_p_M _ regA _ _] := tau2_context maxM t2Mp Ep2A_M.
have{syl_p_M} cPP: abelian P by case: (syl_p_M P).
have{P0 pP0 not_cP0P0} not_cSS: ~~ abelian S.
  have [x _ sP0Sx] := Sylow_subJ sylS (subsetT P0) pP0.
  by apply: contra not_cP0P0 => cSS; rewrite (abelianS sP0Sx) ?abelianJ.
have [defP | ltPS] := eqVproper sPS; first by rewrite -defP cPP in not_cSS.
have [[nsAE defEp] [sCAE _ _] nregA _] :=
  tau2_compl_context maxM hallE t2Mp Ep2A.
have defCSA: 'C_S(A) = P.
  apply: (sub_pHall sylP_E (pgroupS (subsetIl _ _) pS)).
    by rewrite subsetI sPS (sub_abelian_cent2 cPP).
  by rewrite subIset // sCAE orbT.
have max2A: A \in 'E_p^2(G) :&: 'E*_p(G).
  by rewrite 3!inE subsetT abelA dimA; case: (tau2_not_beta maxM t2Mp) => _ ->.
have def_t2: \tau2(M) =i (p : nat_pred).
  move=> q; apply/idP/idP=> [t2Mq |]; last by move/eqnP->.
  apply: contraLR (proper_card ltPS); rewrite !inE /= eq_sym -leqNgt => q'p.
  apply: wlog_neg => p'q; have [B EqB] := p_rank_witness q E.
  have{EqB} Eq2B: B \in 'E_q^2(E).
    by move: t2Mq; rewrite (tau2E hallE) => /andP[_ /eqP <-].
  have [sBE abelB dimB]:= pnElemP Eq2B; have [qB _] := andP abelB.
  have coBA: coprime #|B| #|A| by apply: pnat_coprime qB (pi_pnat pA _).
  have [[nsBE _] [sCBE _ _] _ _] := tau2_compl_context maxM hallE t2Mq Eq2B.
  have nBA: A \subset 'N(B) by rewrite (subset_trans sAE) ?normal_norm.
  have cAB: B \subset 'C(A).
    rewrite (sameP commG1P trivgP) -(coprime_TIg coBA) subsetI commg_subl nBA.
    by rewrite commg_subr (subset_trans sBE) ?normal_norm.
  have{cAB} qCA: q %| #|'C(A)|.
    by apply: dvdn_trans (cardSg cAB); rewrite (card_pnElem Eq2B) dvdn_mull.
  have [Q maxQ sBQ] := max_normed_exists qB nBA.
  have nnQ: q.-narrow Q.
    apply/implyP=> _; apply/set0Pn; exists B.
    rewrite 3!inE sBQ abelB dimB (subsetP (pmaxElemS q (subsetT Q))) //=.
    rewrite setIC 2!inE sBQ; case: (tau2_not_beta maxM t2Mq) => _ -> //.
    by rewrite (subsetP (pnElemS _ _ sEM)).
  have [P1 [sylP1 _] [_ _]] := max_normed_2Elem_signaliser q'p max2A maxQ qCA.
  move/(_ nnQ)=> cQP1; have sylP1_E: p.-Sylow(E) P1.
    apply: pHall_subl (subset_trans _ sCBE) (subsetT E) sylP1.
    exact: subset_trans (centS sBQ).
  rewrite (card_Hall sylS) -(card_Hall sylP1).
  by rewrite (card_Hall sylP_E) -(card_Hall sylP1_E).
have coMsA: coprime #|Ms| #|A|.
  by apply: pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _).
have defMs: <<\bigcup_(X in 'E_p^1(A)) 'C_Ms(X)>> = Ms.
  have ncycA: ~~ cyclic A by rewrite (abelem_cyclic abelA) dimA.
  have [sAM _ _] := pnElemP Ep2A_M.
  have{sAM} nMsA: A \subset 'N(Ms) by rewrite (subset_trans sAM) ?gFnorm.
  apply/eqP; rewrite eqEsubset andbC gen_subG.
  rewrite -{1}[Ms](coprime_abelian_gen_cent1 cAA ncycA nMsA coMsA).
  rewrite genS; apply/bigcupsP=> x; rewrite ?subsetIl //; case/setD1P=> ntx Ax.
  rewrite /= -cent_cycle (bigcup_max <[x]>%G) // p1ElemE // .
  by rewrite 2!inE cycle_subG Ax /= -orderE (abelem_order_p abelA).
have [A0 EpA0 nregA0]: exists2 A0, A0 \in 'E_p^1(A) & 'C_Ms(A0) != 1.
  apply/exists_inP; rewrite -negb_forall_in.
  apply: contra (Msigma_neq1 maxM); move/forall_inP => regAp.
  rewrite -/Ms -defMs -subG1 gen_subG; apply/bigcupsP=> X EpX.
  by rewrite subG1 regAp.
have uniqCA0: 'M('C(A0)) = [set M].
  by rewrite nregA // (subsetP (pnElemS _ _ sAE)).
have defSM: S :&: M = P.
  apply: sub_pHall (pgroupS (subsetIl S M) pS) _ (subsetIr S M) => //.
  by rewrite subsetI sPS (pHall_sub sylP_M).
have{ltPS} not_sSM: ~~ (S \subset M).
  by rewrite (sameP setIidPl eqP) defSM proper_neq.
have not_sA0Z: ~~ (A0 \subset 'Z(S)).
  apply: contra not_sSM; rewrite subsetI centsC; case/andP=> _ sS_CA0.
  by case/mem_uniq_mmax: uniqCA0 => _; apply: subset_trans sS_CA0.
have [EpZ0 dxCSA transNSA] := basic_p2maxElem_structure max2A pS sAS not_cSS.
do [set Z0 := 'Ohm_1('Z(S))%G; set EpA' := _ :\ Z0] in EpZ0 dxCSA transNSA.
have sZ0Z: Z0 \subset 'Z(S) := Ohm_sub 1 _.
have [sA0A _ _] := pnElemP EpA0; have sA0P := subset_trans sA0A sAP.
have EpA'_A0: A0 \in EpA'.
  by rewrite 2!inE EpA0 andbT; apply: contraNneq not_sA0Z => ->.
have{transNSA sAP not_sSM defSM} regA0' X:
  X \in 'E_p^1(E) :\ A0 -> 'C_Ms(X) = 1 /\ ~~ ('C(X) \subset M).
- case/setD1P=> neqXA0 EpX.
  suffices not_sCXM: ~~ ('C(X) \subset M).
    split=> //; apply: contraNeq not_sCXM => nregX.
    by case/mem_uniq_mmax: (nregA X EpX nregX).
  have [sXZ | not_sXZ] := boolP (X \subset 'Z(S)).
    apply: contra (subset_trans _) not_sSM.
    by rewrite centsC (subset_trans sXZ) ?subsetIr.
  have EpA'_X: X \in EpA'.
    by rewrite 2!inE -defEp EpX andbT; apply: contraNneq not_sXZ => ->.
  have [g NSAg /= defX] := atransP2 transNSA EpA'_A0 EpA'_X.
  have{NSAg} [Sg nAg] := setIP NSAg.
  have neqMgM: M :^ g != M.
    rewrite (sameP eqP normP) (norm_mmax maxM); apply: contra neqXA0 => Mg.
    rewrite defX [_ == _](sameP eqP normP) (subsetP (cent_sub A0)) //.
    by rewrite (subsetP (centSS (subxx _) sA0P cPP)) // -defSM inE Sg.
  apply: contra neqMgM; rewrite defX centJ sub_conjg.
  by move/(eq_uniq_mmax uniqCA0) => defM; rewrite -{1}defM ?mmaxJ ?actKV.
have{defMs} defA0: 'C_A(Ms) = A0.
  apply/eqP; rewrite eq_sym eqEcard subsetI sA0A (card_pnElem EpA0).
  have pCA: p.-group 'C_A(Ms) := pgroupS (subsetIl A _) pA.
  rewrite andbC (card_pgroup pCA) leq_exp2l ?prime_gt1 // -ltnS -dimA.
  rewrite properG_ltn_log //=; last first.
    rewrite properE subsetIl /= subsetI subxx centsC -(subxx Ms) -subsetI.
    by rewrite regA subG1 Msigma_neq1.
  rewrite centsC -defMs gen_subG (big_setD1 A0) //= subUset subsetIr /=.
  by apply/bigcupsP=> X; rewrite -defEp; case/regA0'=> -> _; rewrite sub1G.
rewrite defA0 (group_inj defA0) (card_pnElem EpA0).
have{dxCSA} [Y [cycY sZ0Y]] := dxCSA; move/(_ _ EpA'_A0)=> dxCSA.
have defCP_Ms: 'C_P(Ms) = A0.
  move: dxCSA; rewrite defCSA => /dprodP[_ mulA0Y cA0Y tiA0Y].
  rewrite -mulA0Y -group_modl /=; last by rewrite -defA0 subsetIr.
  rewrite setIC TI_Ohm1 ?mulg1 // setIC.
  have pY: p.-group Y by rewrite (pgroupS _ pP) // -mulA0Y mulG_subr.
  have cYY: abelian Y := cyclic_abelian cycY.
  have ->: 'Ohm_1(Y) = Z0.
    apply/eqP; rewrite eq_sym eqEcard (card_pnElem EpZ0) /= -['Ohm_1(_)]Ohm_id.
    rewrite OhmS // (card_pgroup (pgroupS (Ohm_sub 1 Y) pY)).
    rewrite leq_exp2l ?prime_gt1 -?p_rank_abelian // -rank_pgroup //.
    by rewrite -abelian_rank1_cyclic.
  rewrite prime_TIg ?(card_pnElem EpZ0) // centsC (sameP setIidPl eqP) eq_sym.
  case: (regA0' Z0) => [|-> _]; last exact: Msigma_neq1.
  by rewrite 2!inE defEp EpZ0 andbT; apply: contraNneq not_sA0Z => <-.
have [sPM pA0] := (pHall_sub sylP_M, pgroupS sA0A pA).
have cMsA0: A0 \subset 'C(Ms) by rewrite -defA0 subsetIr.
have nsA0M: A0 <| M.
  have [_ defM nMsE _] := sdprodP (sdprod_sigma maxM hallE).
  rewrite /normal (subset_trans sA0P) // -defM mulG_subG cents_norm 1?centsC //.
  by rewrite -defA0 normsI ?norms_cent // normal_norm.
have defFM: Ms \x A0 = 'F(M).
  have nilF := Fitting_nil M.
  rewrite dprodE ?(coprime_TIg (coprimegS sA0A coMsA)) //.
  have [_ /= defFM cFpp' _] := dprodP (nilpotent_pcoreC p nilF).
  have defFp': 'O_p^'('F(M)) = Ms.
    apply/eqP; rewrite eqEsubset.
    rewrite (sub_Hall_pcore (Msigma_Hall maxM)); last by rewrite !gFsub_trans.
    rewrite /pgroup (sub_in_pnat _ (pcore_pgroup _ _)) => [|q piFq]; last first.
      have [Q sylQ] := Sylow_exists q 'F(M); have [sQF qQ _] := and3P sylQ.
      have ntQ: Q :!=: 1.
        rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ) p_rank_gt0.
        by rewrite (piSg _ piFq) ?pcore_sub.
      have sNQM: 'N(Q) \subset M.
        rewrite (mmax_normal maxM) // (nilpotent_Hall_pcore nilF sylQ).
        by rewrite p_core_Fitting pcore_normal.
      apply/implyP; rewrite implyNb /= -def_t2 orbC. 
      by rewrite (prime_class_mmax_norm maxM qQ).
    rewrite pcore_max ?(pi_p'group (pcore_pgroup _ _)) //.
    rewrite [_ <| _]andbC gFsub_trans ?gFnorm //.
    rewrite Fitting_max ?gFnormal ?(tau2_Msigma_nil _ t2Mp) //.
  rewrite p_core_Fitting defFp' centsC in defFM cFpp'.
  rewrite -defFM (centC cFpp'); congr (Ms * _).
  apply/eqP; rewrite eqEsubset pcore_max //.
  by rewrite -defCP_Ms subsetI cFpp' pcore_sub_Hall.
split=> {defFM}//.
have [[sE1E t1E1 _] t2E2] := (and3P hallE1, pHall_pgroup hallE2).
have defE2: E2 :=: P by rewrite (sub_pHall sylP) // -(eq_pgroup _ def_t2) t2E2.
have [[_ nsE3E] _ _ [defEr _] _] := sigma_compl_context maxM complEi.
have [sE3E nE3E] := andP nsE3E; have{nE3E} nE3E := subset_trans _ nE3E.
have [[_ E21 _ defE21]] := sdprodP defEr; rewrite defE21 => defE nE321 tiE321.
rewrite defE2 in defE21; have{defE21} [_ defPE1 nPE1 tiPE1] := sdprodP defE21.
have [P0 defP nP0E1]: exists2 P0 : {group gT}, A0 \x P0 = P & E1 \subset 'N(P0).
  have p'E1b: p^'.-group (E1 / 'Phi(P)).
    rewrite quotient_pgroup //; apply: sub_pgroup t1E1 => q /tau2'1.
    by rewrite inE /= def_t2.
  have defPhiP: 'Phi(P) = 'Phi(Y).
    have [_ _ cA0Y tiA0Y] := dprodP dxCSA.
    rewrite defCSA dprodEcp // in dxCSA.
    have [_ abelA0 _] := pnElemP EpA0; rewrite -trivg_Phi // in abelA0.
    by rewrite -(Phi_cprod pP dxCSA) (eqP abelA0) cprod1g.
  have abelPb := Phi_quotient_abelem pP; have sA0Pb := quotientS 'Phi(P) sA0P.
  have [||P0b] := Maschke_abelem abelPb p'E1b sA0Pb; rewrite ?quotient_norms //.
    by rewrite (subset_trans (subset_trans sE1E sEM)) ?normal_norm.
  case/dprodP=> _ defPb _ tiAP0b nP0E1b.
  have sP0Pb: P0b \subset P / 'Phi(P) by rewrite -defPb mulG_subr.
  have [P0 defP0b sPhiP0 sP0P] := inv_quotientS (Phi_normal P) sP0Pb.
  exists P0; last first.
    rewrite -(quotientSGK (char_norm_trans (Phi_char P) nPE1)); last first.
      by rewrite cents_norm ?(sub_abelian_cent2 cPP (Phi_sub P) sP0P).
    by rewrite quotient_normG -?defP0b ?(normalS _ _ (Phi_normal P)).
  rewrite dprodEY ?(sub_abelian_cent2 cPP) //.
    apply/eqP; rewrite eqEsubset join_subG sA0P sP0P /=.
    rewrite -(quotientSGK (normal_norm (Phi_normal P))) //=; last first.
      by rewrite sub_gen // subsetU // sPhiP0 orbT.
    rewrite cent_joinEr ?(sub_abelian_cent2 cPP) //.
    rewrite quotientMr //; last by rewrite (subset_trans sP0P) ?gFnorm.
    by rewrite -defP0b defPb.
  apply/trivgP; case/dprodP: dxCSA => _ _ _ <-.
  rewrite subsetI subsetIl (subset_trans _ (Phi_sub Y)) // -defPhiP.
  rewrite -quotient_sub1 ?subIset ?(subset_trans sA0P) ?gFnorm //.
  by rewrite quotientIG // -defP0b tiAP0b.
have nA0E := subset_trans _ (subset_trans sEM (normal_norm nsA0M)).
have{defP} [_ defAP0 _ tiAP0] := dprodP defP.
have sP0P: P0 \subset P by rewrite -defAP0 mulG_subr.
have sP0E := subset_trans sP0P (pHall_sub sylP_E).
pose E0 := (E3 <*> (P0 <*> E1))%G.
have sP0E1_E: P0 <*> E1 \subset E by rewrite join_subG sP0E.
have sE0E:  E0 \subset E by rewrite join_subG sE3E.
have mulA0E0: A0 * E0 = E.
  rewrite /= (norm_joinEr (nE3E _ sP0E1_E)) mulgA -(normC (nA0E _ sE3E)).
  by rewrite /= -mulgA (norm_joinEr nP0E1) (mulgA A0) defAP0 defPE1.
have tiA0E0: A0 :&: E0 = 1.
  rewrite cardMg_TI // mulA0E0 -defE /= (norm_joinEr (nE3E _ sP0E1_E)).
  rewrite !TI_cardMg //; last first.
    by apply/trivgP; rewrite -tiE321 setIS //= ?norm_joinEr // -defPE1 mulSg.
  rewrite mulnCA /= leq_mul // norm_joinEr //= -defPE1.
  rewrite !TI_cardMg //; last by apply/trivgP; rewrite -tiPE1 setSI.
  by rewrite mulnA -(TI_cardMg tiAP0) defAP0.
have defAE0: A0 ><| E0 = E by rewrite sdprodE ?nA0E.
exists E0 => // x /setD1P[ntx Ms_x] q piCE0x_q.
have: q \in \pi(E) by apply: piSg piCE0x_q; rewrite subIset ?sE0E.
rewrite mem_primes in piCE0x_q; case/and3P: piCE0x_q => q_pr _.
case/Cauchy=> // z /setIP[E0z cxz] oz.
have ntz: z != 1 by rewrite -order_gt1 oz prime_gt1.
have ntCMs_z: 'C_Ms[z] != 1.
  apply: contraNneq ntx => reg_z; rewrite (sameP eqP set1gP) -reg_z inE Ms_x.
  by rewrite cent1C.
rewrite (partition_pi_sigma_compl maxM hallE) def_t2.
case/or3P => [-> // | pq | t3Mq].
  have EpA0'_z: <[z]>%G \in 'E_p^1(E) :\ A0.
    rewrite p1ElemE // !inE -orderE oz (eqnP pq) eqxx cycle_subG.
    rewrite (subsetP sE0E) // !andbT; apply: contraNneq ntz => eqA0z.
    by rewrite (sameP eqP set1gP) -tiA0E0 inE -eqA0z cycle_id E0z.
  have [reg_z _] := regA0' _ EpA0'_z.
  by rewrite -cent_cycle reg_z eqxx in ntCMs_z.
rewrite regE3 ?eqxx // !inE ntz /= in ntCMs_z.
by rewrite (mem_normal_Hall hallE3 nsE3E) ?(subsetP sE0E) // /p_elt oz pnatE.
Qed.

(* This is B & G, Theorem 12.8(c). This part does not use the decompotision   *)
(* of the complement, and needs to be proved ahead because it is used with    *)
(* different primes in \tau_2(M) in the main argument. We also include an     *)
(* auxiliary identity, which is needed in another part of the proof of 12.8.  *)
Theorem abelian_tau2_sub_Fitting M E p A S :
    M \in 'M -> \sigma(M)^'.-Hall(M) E ->
    p \in \tau2(M) -> A \in 'E_p^2(E) ->
    p.-Sylow(G) S -> A \subset S -> abelian S ->
  [/\        S \subset 'N(S)^`(1),
    'N(S)^`(1) \subset 'F(E),
         'F(E) \subset 'C(S),
         'C(S) \subset E
   &     'F('N(A)) = 'F(E)].
Proof.
move=> maxM hallE t2Mp Ep2A sylS sAS cSS.
have [sAE abelA dimA]:= pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have [sEM sM'E _] := and3P hallE.
have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A.
have eqFC H: A <| H -> 'C(A) \subset H -> 'F(H) = 'F('C(A)).
  move=> nsAH sCH; have [_ nAH] := andP nsAH.
  apply/eqP; rewrite eqEsubset !Fitting_max ?Fitting_nil //.
    by rewrite gFnormal_trans // /normal sCH norms_cent.
  apply: normalS sCH (Fitting_normal H).
  have [_ defF cFpFp' _] := dprodP (nilpotent_pcoreC p (Fitting_nil H)).
  have sAFp: A \subset 'O_p('F(H)) by rewrite p_core_Fitting pcore_max.
  have [x _ sFpSx] := Sylow_subJ sylS (subsetT _) (pcore_pgroup p 'F(H)).
  have cFpFp: abelian 'O_p('F(H)) by rewrite (abelianS sFpSx) ?abelianJ.
  by rewrite -defF mulG_subG (centSS _ _ cFpFp) // (centSS _ _ cFpFp').
have [[nsAE _] [sCAE _] _ _ _] := tau2_compl_context maxM hallE t2Mp Ep2A.
have eqFN_FE: 'F('N(A)) = 'F(E) by rewrite (eqFC E) // eqFC ?cent_sub ?normalG.
have sN'FN: 'N(A)^`(1) \subset 'F('N(A)).
  rewrite rank2_der1_sub_Fitting ?mFT_odd //.
    rewrite ?mFT_sol // mFT_norm_proper ?(mFT_pgroup_proper pA) //.
    by rewrite -rank_gt0 (rank_abelem abelA) dimA.
  rewrite eqFN_FE (leq_trans (rankS (Fitting_sub E))) //.
  have [q q_pr ->]:= rank_witness E; apply: wlog_neg; rewrite -ltnNge => rEgt2.
  rewrite (leq_trans (p_rankS q sEM)) // leqNgt.
  apply: contra ((alpha_sub_sigma maxM) q) (pnatPpi sM'E _).
  by rewrite -p_rank_gt0 (leq_trans _ rEgt2).
have sSE: S \subset E by rewrite (subset_trans _ sCAE) // (centSS _ _ cSS).
have nA_NS: 'N(S) \subset 'N(A).
  have [ ] := tau2_context maxM t2Mp Ep2A_M; have sSM := subset_trans sSE sEM.
  have sylS_M: p.-Sylow(M) S := pHall_subl sSM (subsetT M) sylS.
  by case/(_ S) => // _ [// |<- _] _ _ _ _; apply: char_norms (Ohm_char 1 _).
have sS_NS': S \subset 'N(S)^`(1) := mFT_Sylow_der1 sylS.
have sNS'_FE: 'N(S)^`(1) \subset 'F(E).
  by rewrite -eqFN_FE (subset_trans (dergS 1 nA_NS)).
split=> //; last by rewrite (subset_trans (centS sAS)).
have sSFE := subset_trans sS_NS' sNS'_FE; have nilFE := Fitting_nil E.
have sylS_FE := pHall_subl sSFE (subsetT 'F(E)) sylS.
suff sSZF: S \subset 'Z('F(E)) by rewrite centsC (subset_trans sSZF) ?subsetIr.
have [_ <- _ _] := dprodP (center_dprod (nilpotent_pcoreC p nilFE)).
by rewrite -(nilpotent_Hall_pcore nilFE sylS_FE) (center_idP cSS) mulG_subl.
Qed.

(* This is B & G, Theorem 12.8(a,b,d,e) -- the bulk of the Theorem. We prove  *)
(* part (f) separately below, as it does not depend on a decomposition of the *)
(* complement.                                                                *)
Theorem abelian_tau2 M E E1 E2 E3 p A S (Ms := M`_\sigma) :
    M \in 'M -> sigma_complement M E E1 E2 E3 ->
    p \in \tau2(M) -> A \in 'E_p^2(E) ->
    p.-Sylow(G) S -> A \subset S -> abelian S ->
  [/\ (*a*) E2 <| E /\ abelian E2,
      (*b*) \tau2(M).-Hall(G) E2,
      (*d*) [/\       'N(A) = 'N(S),
                      'N(S) = 'N(E2),
                     'N(E2) = 'N(E3 <*> E2)
            & 'N(E3 <*> E2) = 'N('F(E))]
    & (*e*) forall X, X \in 'E^1(E1) -> 'C_Ms(X) = 1 -> X \subset 'Z(E)].
Proof.
move=> maxM complEi t2Mp Ep2A sylS sAS cSS.
have [hallE hallE1 hallE2 hallE3 _] := complEi.
have [sEM sM'E _] := and3P hallE.
have [sE1E t1E1 _] := and3P hallE1.
have [sE2E t2E2 _] := and3P hallE2.
have [sE3E t3E3 _] := and3P hallE3.
have nilF: nilpotent 'F(E) := Fitting_nil E.
have sylE2_sylG_ZFE q Q:
  q.-Sylow(E2) Q -> Q :!=: 1 -> q.-Sylow(G) Q /\ Q \subset 'Z('F(E)).
- move=> sylQ ntQ; have [sQE2 qQ _] := and3P sylQ.
  have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 -rank_pgroup // rank_gt0.
  have t2Mq: q \in \tau2(M) by rewrite (pnatPpi t2E2) // (piSg sQE2).
  have sylQ_E: q.-Sylow(E) Q := subHall_Sylow hallE2 t2Mq sylQ.
  have rqQ: 'r_q(Q) = 2.
    rewrite (tau2E hallE) !inE -(p_rank_Sylow sylQ_E) in t2Mq.
    by case/andP: t2Mq => _ /eqP.
  have [B Eq2B sBQ]: exists2 B, B \in 'E_q^2(E) & B \subset Q.
    have [B Eq2B] := p_rank_witness q Q; have [sBQ abelB rBQ] := pnElemP Eq2B.
    exists B; rewrite // !inE rBQ rqQ abelB !andbT.
    exact: subset_trans sBQ (pHall_sub sylQ_E).
  have [T /= sylT sQT] := Sylow_superset (subsetT Q) qQ.
  have qT: q.-group T := pHall_pgroup sylT.
  have cTT: abelian T.
    apply: wlog_neg => not_cTT.
    have [def_t2 _ _ _] := nonabelian_tau2 maxM hallE t2Mq Eq2B qT not_cTT.
    rewrite def_t2 !inE in t2Mp; rewrite (eqP t2Mp) in sylS.
    by have [x _ ->] := Sylow_trans sylS sylT; rewrite abelianJ.
  have sTF: T \subset 'F(E).
    have subF := abelian_tau2_sub_Fitting maxM hallE t2Mq Eq2B sylT.
    have [sTN' sN'F _ _ _] := subF (subset_trans sBQ sQT) cTT.
    exact: subset_trans sTN' sN'F.
  have sTE: T \subset E := subset_trans sTF (Fitting_sub E).
  have <-: T :=: Q by apply: (sub_pHall sylQ_E).
  have sylT_F: q.-Sylow('F(E)) T := pHall_subl sTF (subsetT _) sylT.
  have [_ <- _ _] := dprodP (center_dprod (nilpotent_pcoreC q nilF)).
  by rewrite -(nilpotent_Hall_pcore nilF sylT_F) (center_idP cTT) mulG_subl.
have hallE2_G: \tau2(M).-Hall(G) E2.
  rewrite pHallE subsetT /= -(part_pnat_id t2E2); apply/eqnP.
  rewrite !(widen_partn _ (subset_leq_card (subsetT _))).
  apply: eq_bigr => q t2q; rewrite -!p_part.
  have [Q sylQ] := Sylow_exists q E2; have qQ := pHall_pgroup sylQ.
  have sylQ_E: q.-Sylow(E) Q := subHall_Sylow hallE2 t2q sylQ.
  have ntQ: Q :!=: 1.
    rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ_E) p_rank_gt0.
    by rewrite (tau2E hallE) in t2q; case/andP: t2q.
  have [sylQ_G _] := sylE2_sylG_ZFE q Q sylQ ntQ.
  by rewrite -(card_Hall sylQ) -(card_Hall sylQ_G).
have sE2_ZFE: E2 \subset 'Z('F(E)).
  rewrite -Sylow_gen gen_subG; apply/bigcupsP=> Q; case/SylowP=> q q_pr sylQ.
  have [-> | ntQ] := eqsVneq Q 1; first exact: sub1G.
  by have [_ ->] := sylE2_sylG_ZFE q Q sylQ ntQ.
have cE2E2: abelian E2 := abelianS sE2_ZFE (center_abelian _).
have sE2FE: E2 \subset 'F(E) := subset_trans sE2_ZFE (center_sub _).
have nsE2E: E2 <| E.
  have hallE2_F := pHall_subl sE2FE (Fitting_sub E) hallE2.
  by rewrite (nilpotent_Hall_pcore nilF hallE2_F) !gFnormal_trans.
have [_ _ [cycE1 cycE3] [_ defEl] _] := sigma_compl_context maxM complEi.
have [[K _ defK _] _ _ _] := sdprodP defEl; rewrite defK in defEl.
have [nsKE _ mulKE1 nKE1 _] := sdprod_context defEl; have [sKE _] := andP nsKE.
have [nsE3K sE2K _ nE32 tiE32] := sdprod_context defK.
rewrite -sdprodEY // defK.
have{defK} defK: E3 \x E2 = K.
  rewrite dprodEsd // (sameP commG1P trivgP) -tiE32 subsetI commg_subr nE32.
  by rewrite commg_subl (subset_trans sE3E) ?normal_norm.
have cKK: abelian K.
  by have [_ <- cE23 _] := dprodP defK; rewrite abelianM cE2E2 cyclic_abelian.
have [_ sNS'F _ sCS_E defFN] :=
  abelian_tau2_sub_Fitting maxM hallE t2Mp Ep2A sylS sAS cSS.
have{sCS_E} sSE2: S \subset E2.
  rewrite (sub_normal_Hall hallE2 nsE2E (subset_trans cSS sCS_E)).
  by rewrite (pi_pgroup (pHall_pgroup sylS)).
have charS: S \char E2.
  have sylS_E2: p.-Sylow(E2) S := pHall_subl sSE2 (subsetT E2) sylS.
  by rewrite (nilpotent_Hall_pcore (abelian_nil cE2E2) sylS_E2) pcore_char.
have nsSE: S <| E := char_normal_trans charS nsE2E; have [sSE nSE] := andP nsSE.
have charA: A \char S.
  have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A.
  have sylS_M := pHall_subl (subset_trans sSE sEM) (subsetT M) sylS.
  have [] := tau2_context maxM t2Mp Ep2A_M; case/(_ S sylS_M)=> _ [//|<- _].
  by rewrite Ohm_char.
have charE2: E2 \char K.
  have hallE2_K := pHall_subl sE2K sKE hallE2.
  by rewrite (nilpotent_Hall_pcore (abelian_nil cKK) hallE2_K) pcore_char.
have coKE1: coprime #|K| #|E1|.
  rewrite -(dprod_card defK) coprime_mull (sub_pnat_coprime tau3'1 t3E3 t1E1).
  by rewrite (sub_pnat_coprime tau2'1 t2E2 t1E1).
have hallK: Hall 'F(E) K.
  have hallK: Hall E K.
    by rewrite /Hall -divgS sKE //= -(sdprod_card defEl) mulKn.
  have sKFE: K \subset 'F(E) by rewrite Fitting_max ?abelian_nil.
  exact: pHall_Hall (pHall_subl sKFE (Fitting_sub E) (Hall_pi hallK)).
have charK: K \char 'F(E).
  by rewrite (nilpotent_Hall_pcore nilF (Hall_pi hallK)) pcore_char.
have{defFN} [eqNAS eqNSE2 eqNE2K eqNKF]:
  [/\ 'N(A) = 'N(S), 'N(S) = 'N(E2), 'N(E2) = 'N(K) & 'N(K) = 'N('F(E))].
  have: #|'N(A)| <= #|'N('F(E))|.
    by rewrite subset_leq_card // -defFN gFnorm.
  have leCN := subset_leqif_cards (@char_norms gT _ _ _).
  have trCN := leqif_trans (leCN _ _ _).
  have leq_KtoA := trCN _ _ _ _ charE2 (trCN _ _ _ _ charS (leCN _ _ charA)).
  rewrite (geq_leqif (trCN _ _ _ _ charK leq_KtoA)).
  by case/and4P; do 4!move/eqP->.
split=> // X E1_1_X regX.
have cK_NK': 'N(K)^`(1) \subset 'C(K).
  suffices sKZ: K \subset 'Z('F(E)).
    by rewrite -eqNE2K -eqNSE2 (centSS sNS'F sKZ) // centsC subsetIr.
  have{hallK} [pi hallK] := HallP hallK.
  have [_ <- _ _] := dprodP (center_dprod (nilpotent_pcoreC pi nilF)).
  by rewrite -(nilpotent_Hall_pcore nilF hallK) (center_idP cKK) mulG_subl.
have [q EqX] := nElemP E1_1_X; have [sXE1 abelX dimX] := pnElemP EqX.
have sXE := subset_trans sXE1 sE1E.
have nKX := subset_trans sXE (normal_norm nsKE).
have nCSX_NS: 'N(K) \subset 'N('C(K) * X).
  rewrite -(quotientGK (cent_normal _)) -quotientK ?norms_cent //.
  by rewrite morphpre_norms // sub_abelian_norm ?quotientS ?sub_der1_abelian.
have nKX_NS: 'N(S) \subset 'N([~: K, X]).
  have CK_K_1: [~: 'C(K), K] = 1 by apply/commG1P.
  rewrite eqNSE2 eqNE2K commGC -[[~: X, K]]mul1g -CK_K_1.
  by rewrite -commMG ?CK_K_1 ?norms1 ?normsR.
have not_sNKX_M: ~~ ('N([~: K, X]) \subset M).
  have [[sM'p _] sSM] := (andP t2Mp, subset_trans sSE sEM).
  apply: contra sM'p => sNKX_M; apply/existsP; exists S.
  by rewrite (pHall_subl sSM (subsetT _) sylS) // (subset_trans _ sNKX_M).
have cKX: K \subset 'C(X).
  apply: contraR not_sNKX_M; rewrite (sameP commG1P eqP) => ntKX.
  rewrite (mmax_normal maxM) //.
  have [sKM sM'K] := (subset_trans sKE sEM, pgroupS sKE sM'E).
  have piE1q: q \in \pi(E1).
    by rewrite -p_rank_gt0 -dimX logn_le_p_rank // inE sXE1.
  have sM'q: q \in \sigma(M)^' by rewrite (pnatPpi sM'E) // (piSg sE1E).
  have EpX_NK: X \in 'E_q^1('N_M(K)).
    by apply: subsetP EqX; rewrite pnElemS // subsetI (subset_trans sE1E).
  have q'K: q^'.-group K.
    by rewrite p'groupEpi ?coprime_pi' // in coKE1 *; apply: (pnatPpi coKE1).
  by have []:= commG_sigma'_1Elem_cyclic maxM sKM sM'K sM'q EpX_NK regX.
rewrite subsetI sXE /= -mulKE1 centM subsetI centsC cKX.
exact: subset_trans sXE1 (cyclic_abelian cycE1).
Qed.

(* This is B & G, Theorem 12.8(f). *)
Theorem abelian_tau2_norm_Sylow M E p A S :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) ->
    p.-Sylow(G) S -> A \subset S -> abelian S ->
  forall X, X \subset 'N(S) -> 'C_S(X) <| 'N(S) /\ [~: S, X] <| 'N(S).
Proof.
move=> maxM hallE t2Mp Ep2A sylS sAS cSS X nSX.
have [_ sNS'F sFCS _ _] :=
   abelian_tau2_sub_Fitting maxM hallE t2Mp Ep2A sylS sAS cSS.
have{sNS'F sFCS} sNS'CS: 'N(S)^`(1) \subset 'C(S) := subset_trans sNS'F sFCS.
have nCSX_NS: 'N(S) \subset 'N('C(S) * X).
  rewrite -quotientK ?norms_cent // -{1}(quotientGK (cent_normal S)).
  by rewrite morphpre_norms // sub_abelian_norm ?quotientS ?sub_der1_abelian.
rewrite /normal subIset ?comm_subG ?normG //=; split.
  have ->: 'C_S(X) = 'C_S('C(S) * X).
    by rewrite centM setIA; congr (_ :&: _); rewrite (setIidPl _) // centsC.
  by rewrite normsI ?norms_cent.
have CS_S_1: [~: 'C(S), S] = 1 by apply/commG1P.
by rewrite commGC -[[~: X, S]]mul1g -CS_S_1 -commMG ?CS_S_1 ?norms1 ?normsR.
Qed.

(* This is B & G, Corollary 12.9. *)
Corollary tau1_act_tau2 M E p A q Q (Ms := M`_\sigma) :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) ->
    q \in \tau1(M) -> Q \in 'E_q^1(E) -> 'C_Ms(Q) = 1 -> [~: A, Q] != 1 ->
 let A0 := [~: A, Q]%G in let A1 := ('C_A(Q))%G in
 [/\ (*a*) [/\ A0 \in 'E_p^1(A), 'C_A(Ms) = A0 & A0 <| M],
     (*b*) gval A0 \notin A1 :^: G
   & (*c*) A1 \in 'E_p^1(A) /\ ~~ ('C(A1) \subset M)].
Proof.
move=> maxM hallE t2Mp Ep2A t1Mq EqQ regQ ntA0 A0 A1.
have [sEM sM'E _] := and3P hallE.
have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have [sQE abelQ dimQ] := pnElemP EqQ; have [qQ _ _] := and3P abelQ.
have [p_pr q_pr] := (pnElem_prime Ep2A, pnElem_prime EqQ).
have p_gt1 := prime_gt1 p_pr.
have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A.
have [_ _ regA _ _] := tau2_context maxM t2Mp Ep2A_M.
have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2Mp Ep2A.
have [_ nAE] := andP nsAE; have nAQ := subset_trans sQE nAE.
have coAQ: coprime #|A| #|Q|.
  exact: sub_pnat_coprime tau2'1 (pi_pnat pA t2Mp) (pi_pnat qQ t1Mq).
have defA: A0 \x A1 = A := coprime_abelian_cent_dprod nAQ coAQ cAA.
have [_ _ _ tiA01] := dprodP defA.
have [sAM sM'A] := (subset_trans sAE sEM, pgroupS sAE sM'E).
have sM'q: q \in \sigma(M)^' by case/andP: t1Mq.
have EqQ_NA: Q \in 'E_q^1('N_M(A)).
  by apply: subsetP EqQ; rewrite pnElemS // subsetI sEM.
have q'A: q^'.-group A.
  rewrite p'groupEpi ?coprime_pi' // in coAQ *.
  by apply: (pnatPpi coAQ); rewrite -p_rank_gt0 (p_rank_abelem abelQ) dimQ.
have [] := commG_sigma'_1Elem_cyclic maxM sAM sM'A sM'q EqQ_NA regQ q'A cAA.
rewrite -[[~: A, Q]]/(gval A0) -/Ms => cMsA0 cycA0 nsA0M.
have sA0A: A0 \subset A by rewrite commg_subl.
have EpA0: A0 \in 'E_p^1(A).
  have abelA0 := abelemS sA0A abelA; have [pA0 _] := andP abelA0.
  rewrite p1ElemE // !inE sA0A -(Ohm1_id abelA0) /=.
  by rewrite (Ohm1_cyclic_pgroup_prime cycA0 pA0).
have defA0: 'C_A(Ms) = A0.
  apply/eqP; rewrite eq_sym eqEcard subsetI sA0A cMsA0 (card_pnElem EpA0).
  have pCAMs: p.-group 'C_A(Ms) := pgroupS (subsetIl A _) pA.
  rewrite (card_pgroup pCAMs) leq_exp2l //= leqNgt.
  apply: contra (Msigma_neq1 maxM) => dimCAMs.
  rewrite eq_sym -regA (sameP eqP setIidPl) centsC (sameP setIidPl eqP).
  by rewrite eqEcard subsetIl (card_pnElem Ep2A) (card_pgroup pCAMs) leq_exp2l.
have EpA1: A1 \in 'E_p^1(A).
  rewrite p1ElemE // !inE subsetIl -(eqn_pmul2l (ltnW p_gt1)).
  by rewrite -{1}[p](card_pnElem EpA0) (dprod_card defA) (card_pnElem Ep2A) /=.
have defNA0: 'N(A0) = M by apply: mmax_normal.
have not_cA0Q: ~~ (Q \subset 'C(A0)).
  apply: contra ntA0 => cA0Q.
  by rewrite -subG1 -tiA01 !subsetI subxx sA0A centsC cA0Q.
have rqM: 'r_q(M) = 1%N by apply/eqP; case/and3P: t1Mq.
have q'CA0: q^'.-group 'C(A0).
  have [S sylS sQS] := Sylow_superset (subset_trans sQE sEM) qQ.
  have qS := pHall_pgroup sylS; rewrite -(p_rank_Sylow sylS) in rqM.
  have cycS: cyclic S by rewrite (odd_pgroup_rank1_cyclic qS) ?mFT_odd ?rqM.
  have ntS: S :!=: 1 by rewrite -rank_gt0 (rank_pgroup qS) rqM.
  have defS1: 'Ohm_1(S) = Q.
    apply/eqP; rewrite eq_sym eqEcard -{1}(Ohm1_id abelQ) OhmS //=.
    by rewrite (card_pnElem EqQ) (Ohm1_cyclic_pgroup_prime cycS qS).
  have sylSC: q.-Sylow('C(A0)) 'C_S(A0).
    by rewrite (Hall_setI_normal _ sylS) // -defNA0 cent_normal.
  rewrite -partG_eq1 ?cardG_gt0 // -(card_Hall sylSC) -trivg_card1 /=.
  by rewrite setIC TI_Ohm1 // defS1 setIC prime_TIg ?(card_pnElem EqQ).
do 2?split=> //.
  have: ~~ q^'.-group Q by rewrite /pgroup (card_pnElem EqQ) pnatE ?inE ?negbK.
  apply: contra; case/imsetP=> x _ defA01.
  rewrite defA01 centJ pgroupJ in q'CA0.
  by apply: pgroupS q'CA0; rewrite centsC subsetIr.
have [S sylS sAS] := Sylow_superset (subsetT A) pA.
have [cSS | not_cSS] := boolP (abelian S).
  have solE := sigma_compl_sol hallE.
  have [E1 hallE1 sQE1] := Hall_superset solE sQE (pi_pnat qQ t1Mq).
  have [E3 hallE3] := Hall_exists \tau3(M) solE.
  have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3.
  have [_ _ _ reg1Z] := abelian_tau2 maxM complEi t2Mp Ep2A sylS sAS cSS.
  have E1Q: Q \in 'E^1(E1).
    by apply/nElemP; exists q; rewrite // !inE sQE1 abelQ dimQ.
  rewrite (subset_trans (reg1Z Q E1Q regQ)) ?subIset // in not_cA0Q.
  by rewrite centS ?orbT // (subset_trans sA0A).
have pS := pHall_pgroup sylS.
have [_ _ not_cent_reg _] := nonabelian_tau2 maxM hallE t2Mp Ep2A pS not_cSS.
case: (not_cent_reg A1); rewrite // 2!inE (subsetP (pnElemS p 1 sAE)) // andbT.
by rewrite -val_eqE /= defA0 eq_sym; apply/(TIp1ElemP EpA0 EpA1).
Qed.

(* This is B & G, Corollary 12.10(a). *)
Corollary sigma'_nil_abelian M N :
  M \in 'M -> N \subset M -> \sigma(M)^'.-group N -> nilpotent N -> abelian N.
Proof.
move=> maxM sNM sM'N /nilpotent_Fitting defN.
apply/center_idP; rewrite -{2}defN -{defN}(center_bigdprod defN).
apply: eq_bigr => p _; apply/center_idP; set P := 'O_p(N).
have [-> | ntP] := eqVneq P 1; first exact: abelian1.
have [pP sPN]: p.-group P /\ P \subset N by rewrite pcore_sub pcore_pgroup.
have{sPN sNM sM'N} [sPM sM'P] := (subset_trans sPN sNM, pgroupS sPN sM'N).
have{sPM sM'P} [E hallE sPE] := Hall_superset (mmax_sol maxM) sPM sM'P.
suffices [S sylS cSS]: exists2 S : {group gT}, p.-Sylow(E) S & abelian S.
  by have [x _ sPS] := Sylow_subJ sylS sPE pP; rewrite (abelianS sPS) ?abelianJ.
have{N P sPE pP ntP} piEp: p \in \pi(E).
  by rewrite (piSg sPE) // -p_rank_gt0 -rank_pgroup // rank_gt0.
rewrite (partition_pi_sigma_compl maxM hallE) orbCA orbC -orbA in piEp.
have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE.
have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3.
have{complEi} [_ _ [cycE1 cycE3] _ _] := sigma_compl_context maxM complEi.
have{piEp} [t1p | t3p | t2p] := or3P piEp.
- have [S sylS] := Sylow_exists p E1.
  exists S; first exact: subHall_Sylow hallE1 t1p sylS.
  exact: abelianS (pHall_sub sylS) (cyclic_abelian cycE1).
- have [S sylS] := Sylow_exists p E3.
  exists S; first exact: subHall_Sylow hallE3 t3p sylS.
  exact: abelianS (pHall_sub sylS) (cyclic_abelian cycE3).
have [s'p rpM] := andP t2p; have [S sylS] := Sylow_exists p E; exists S => //.
have sylS_M := subHall_Sylow hallE s'p sylS.
have [A _ Ep2A] := ex_tau2Elem hallE t2p.
by have [/(_ S sylS_M)[]] := tau2_context maxM t2p Ep2A.
Qed.

(* This is B & G, Corollary 12.10(b), first assertion. *)
Corollary der_mmax_compl_abelian M E :
  M \in 'M -> \sigma(M)^'.-Hall(M) E -> abelian E^`(1).
Proof.
move=> maxM hallE; have [sEM s'E _] := and3P hallE.
have sE'E := der_sub 1 E; have sE'M := subset_trans sE'E sEM.
exact: sigma'_nil_abelian (pgroupS _ s'E) (der1_sigma_compl_nil maxM hallE).
Qed.

(* This is B & G, Corollary 12.10(b), second assertion. *)
(* Note that we do not require the full decomposition of the complement. *)
Corollary tau2_compl_abelian M E E2 :
   M \in 'M -> \sigma(M)^'.-Hall(M) E -> \tau2(M).-Hall(E) E2 -> abelian E2.
Proof.
move: E2 => F2 maxM hallE hallF2; have [sEM s'E _] := and3P hallE.
have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE.
have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3.
have solE: solvable E := sigma_compl_sol hallE.
have{solE hallF2} [x _ ->{F2}] := Hall_trans solE hallF2 hallE2.
have [-> | ntE] := eqsVneq E2 1; rewrite {x}abelianJ ?abelian1 //.
have [[p p_pr rpE2] [sE2E t2E2 _]] := (rank_witness E2, and3P hallE2).
have piE2p: p \in \pi(E2) by rewrite -p_rank_gt0 -rpE2 rank_gt0.
have t2p := pnatPpi t2E2 piE2p; have [A Ep2A _] := ex_tau2Elem hallE t2p.
have [_ abelA _] := pnElemP Ep2A; have [pA _] := andP abelA.
have [S /= sylS sAS] := Sylow_superset (subsetT A) pA.
have [cSS | not_cSS] := boolP (abelian S).
  by have [[_ cE2E2] _ _ _] := abelian_tau2 maxM complEi t2p Ep2A sylS sAS cSS.
have pS := pHall_pgroup sylS.
have [def_t2 _ _ _] := nonabelian_tau2 maxM hallE t2p Ep2A pS not_cSS.
apply: sigma'_nil_abelian (subset_trans _ sEM) (pgroupS _ s'E) _ => //.
by rewrite (eq_pgroup _ def_t2) in t2E2; apply: pgroup_nil t2E2.
Qed.

(* This is B & G, Corollary 12.10(c). *)
(* We do not really need a full decomposition of the complement in the first  *)
(* part, but this reduces the number of assumptions.                          *)
Corollary tau1_cent_tau2Elem_factor M E p A :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) ->
  [/\ forall E1 E2 E3, sigma_complement M E E1 E2 E3 -> E3 * E2 \subset 'C_E(A),
      'C_E(A) <| E
    & \tau1(M).-group (E / 'C_E(A))].
Proof.
move=> maxM hallE t2p Ep2A; have sEM: E \subset M := pHall_sub hallE.
have nsAE: A <| E by case/(tau2_compl_context maxM): Ep2A => //; case.
have [sAE nAE]: A \subset E /\ E \subset 'N(A) := andP nsAE.
have nsCAE: 'C_E(A) <| E by rewrite norm_normalI ?norms_cent.
have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE.
have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3.
have{hallE1} [t1E1 sE3E] := (pHall_pgroup hallE1, pHall_sub hallE3).
have{nsAE} sAE2: A \subset E2.
  apply: subset_trans (pcore_max _ nsAE) (pcore_sub_Hall hallE2).
  by apply: pi_pnat t2p; case/pnElemP: Ep2A => _; case/andP.
have{complEi} defE: (E3 ><| E2) ><| E1 = E.
  by case/sigma_compl_context: complEi => // _ _ _ [_ ->].
have [[K _ defK _] _ _ _] := sdprodP defE; rewrite defK in defE.
have nsKE: K <| E by case/sdprod_context: defE.
have [[sKE nKE] [_ mulE32 nE32 tiE32]] := (andP nsKE, sdprodP defK).
have{sE3E} sK_CEA: K \subset 'C_E(A).
  have cE2E2: abelian E2 := tau2_compl_abelian maxM hallE hallE2.
  rewrite subsetI sKE -mulE32 mulG_subG (centsS sAE2 cE2E2) (sameP commG1P eqP).
  rewrite -subG1 -tiE32 subsetI commg_subl (subset_trans sAE2) //=.
  by rewrite (subset_trans _ sAE2) // commg_subr (subset_trans sE3E).
split=> // [_ F2 F3 [_ _ hallF2 hallF3 _] | ].
  have solE: solvable E := solvableS sEM (mmax_sol maxM).
  have [x2 Ex2 ->] := Hall_trans solE hallF2 hallE2. 
  have [x3 Ex3 ->] := Hall_trans solE hallF3 hallE3.
  rewrite mulG_subG !sub_conjg !(normsP (normal_norm nsCAE)) ?groupV //.
  by rewrite -mulG_subG mulE32.
have [f <-] := homgP (homg_quotientS nKE (normal_norm nsCAE) sK_CEA).
by rewrite morphim_pgroup // /pgroup -divg_normal // -(sdprod_card defE) mulKn.
Qed.

(* This is B & G, Corollary 12.10(d). *)
Corollary norm_noncyclic_sigma M p P :
    M \in 'M -> p \in \sigma(M) -> p.-group P -> P \subset M -> ~~ cyclic P ->
  'N(P) \subset M.
Proof.
move=> maxM sMp pP sPM ncycP.
have [A Ep2A]: exists A, A \in 'E_p^2(P).
  by apply/p_rank_geP; rewrite ltnNge -odd_pgroup_rank1_cyclic ?mFT_odd.
have [[sAP _ _] Ep2A_M] := (pnElemP Ep2A, subsetP (pnElemS p 2 sPM) A Ep2A).
have sCAM: 'C(A) \subset M by case/p2Elem_mmax: Ep2A_M.
have [_ _ <- //] := sigma_group_trans maxM sMp pP.
by rewrite mulG_subG subsetIl (subset_trans (centS sAP)).
Qed.

(* This is B & G, Corollary 12.10(e). *)
Corollary cent1_nreg_sigma_uniq M (Ms := M`_\sigma) x :
    M \in 'M -> x \in M^# -> \tau2(M).-elt x -> 'C_Ms[x] != 1 ->
 'M('C[x]) = [set M].
Proof.
move=> maxM /setD1P[ntx]; rewrite -cycle_subG => sMX t2x.
apply: contraNeq => MCx_neqM.
have{MCx_neqM} [H maxCxH neqHM]: exists2 H, H \in 'M('C[x]) & H \notin [set M].
  apply/subsetPn; have [H MCxH] := mmax_exists (mFT_cent1_proper ntx).
  by rewrite eqEcard cards1 (cardD1 H) MCxH andbT in MCx_neqM.
have sCxH: 'C[x] \subset H by case/setIdP: maxCxH.
have s'x: \sigma(M)^'.-elt x by apply: sub_pgroup t2x => p; case/andP.
have [E hallE sXE] := Hall_superset (mmax_sol maxM) sMX s'x.
have [sEM solE] := (pHall_sub hallE, sigma_compl_sol hallE).
have{sXE} [E2 hallE2 sXE2] := Hall_superset solE sXE t2x.
pose p := pdiv #[x].
have t2p: p \in \tau2(M) by rewrite (pnatPpi t2x) ?pi_pdiv ?order_gt1.
have [A Ep2A sAE2]: exists2 A, A \in 'E_p^2(M) & A \subset E2.
  have [A Ep2A_E EpA] := ex_tau2Elem hallE t2p.
  have [sAE abelA _] := pnElemP Ep2A_E; have [pA _] := andP abelA.
  have [z Ez sAzE2] := Hall_Jsub solE hallE2 sAE (pi_pnat pA t2p).
  by exists (A :^ z)%G; rewrite // -(normsP (normsG sEM) z Ez) pnElemJ.
have cE2E2: abelian E2 := tau2_compl_abelian maxM hallE hallE2.
have cxA: A \subset 'C[x] by rewrite -cent_cycle (sub_abelian_cent2 cE2E2).
have maxAH: H \in 'M(A) :\ M by rewrite inE neqHM (subsetP (mmax_ofS cxA)).
have [_ _ _ tiMsMA _] := tau2_context maxM t2p Ep2A.
by rewrite -subG1 -(tiMsMA H maxAH) setIS.
Qed.

(* This is B & G, Lemma 12.11. *)
Lemma primes_norm_tau2Elem M E p A Mstar :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) ->
    Mstar \in 'M('N(A)) ->
 [/\ (*a*) {subset \tau2(M) <= [predD \sigma(Mstar) & \beta(Mstar)]},
     (*b*) [predU \tau1(Mstar) & \tau2(Mstar)].-group (E / 'C_E(A))
   & (*c*) forall q, q \in \pi(E / 'C_E(A)) -> q \in \pi('C_E(A)) ->
           [/\ q \in \tau2(Mstar),
               exists2 P, P \in 'Syl_p(G) & P <| Mstar
             & exists Q, [/\ Q \in 'Syl_q(G), Q \subset Mstar & abelian Q]]].
Proof.
move=> maxM hallE t2Mp Ep2A; move: Mstar.
have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have ntA: A :!=: 1 by apply: (nt_pnElem Ep2A).
have [sEM solE] := (pHall_sub hallE, sigma_compl_sol hallE).
have [_ nsCA_E t1CEAb] := tau1_cent_tau2Elem_factor maxM hallE t2Mp Ep2A.
have [sAM nCA_E] := (subset_trans sAE sEM, normal_norm nsCA_E).
have part_a H:
  H \in 'M('N(A)) -> {subset \tau2(M) <= [predD \sigma(H) & \beta(H)]}.
- case/setIdP=> maxH sNA_H q t2Mq.
  have sCA_H: 'C(A) \subset H := subset_trans (cent_sub A) sNA_H.
  have sAH := subset_trans cAA sCA_H.
  have sHp: p \in \sigma(H).
    have [// | t2Hp] := orP (prime_class_mmax_norm maxH pA sNA_H).
    apply: contraLR sNA_H => sH'p.
    have sH'A: \sigma(H)^'.-group A by apply: pi_pnat pA _.
    have [F hallF sAF] := Hall_superset (mmax_sol maxH) sAH sH'A.
    have Ep2A_F: A \in 'E_p^2(F) by apply/pnElemP.
    by have [_ [_ _ ->]]:= tau2_compl_context maxH hallF t2Hp Ep2A_F.
  rewrite inE /= -predI_sigma_beta //= negb_and /= orbC.
  have [-> /= _] := tau2_not_beta maxM t2Mq.
  have [B Eq2B]: exists B, B \in 'E_q^2('C(A)).
    have [E2 hallE2 sAE2] := Hall_superset solE sAE (pi_pnat pA t2Mp).
    have cE2E2: abelian E2 := tau2_compl_abelian maxM hallE hallE2.
    have [Q sylQ] := Sylow_exists q E2; have sQE2 := pHall_sub sylQ.
    have sylQ_E := subHall_Sylow hallE2 t2Mq sylQ.
    apply/p_rank_geP; apply: leq_trans (p_rankS q (centsS sAE2 cE2E2)).
    rewrite -(p_rank_Sylow sylQ) (p_rank_Sylow sylQ_E).
    by move: t2Mq; rewrite (tau2E hallE) => /andP[_ /eqP->].
  have [cAB abelB dimB] := pnElemP Eq2B; have sBH := subset_trans cAB sCA_H.
  have{Eq2B} Eq2B: B \in 'E_q^2(H) by apply/pnElemP.
  have rqHgt1: 'r_q(H) > 1 by apply/p_rank_geP; exists B.
  have piHq: q \in \pi(H) by rewrite -p_rank_gt0 ltnW.
  rewrite partition_pi_mmax // in piHq.
  case/or4P: piHq rqHgt1 => // [|t2Hq _|]; try by case/and3P=> _ /eqP->.
  have [_ _ regB _ _] := tau2_context maxH t2Hq Eq2B.
  case/negP: ntA; rewrite -subG1 -regB subsetI centsC cAB andbT.
  by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup pA).
have part_b H:
  H \in 'M('N(A)) -> [predU \tau1(H) & \tau2(H)].-group (E / 'C_E(A)).
- move=> maxNA_H; have [maxH sNA_H] := setIdP maxNA_H.
  have [/= bH'p sHp] := andP (part_a H maxNA_H p t2Mp).
  have sCA_H: 'C(A) \subset H := subset_trans (cent_sub A) sNA_H.
  have sAH := subset_trans cAA sCA_H.
  apply/pgroupP=> q q_pr q_dv_CEAb; apply: contraR bH'p => t12H'q.
  have [Q sylQ] := Sylow_exists q E; have [sQE qQ _] := and3P sylQ.
  have nsAE: A <| E by case/(tau2_compl_context maxM): Ep2A => //; case.
  have nAE := normal_norm nsAE; have nAQ := subset_trans sQE nAE.
  have sAQ_A: [~: A, Q] \subset A by rewrite commg_subl.
  have ntAQ: [~: A, Q] != 1.
    apply: contraTneq q_dv_CEAb => /commG1P cAQ.
    have nCEA_Q := subset_trans sQE nCA_E.
    rewrite -p'natE // -partn_eq1 ?cardg_gt0 //.
    rewrite -(card_Hall (quotient_pHall nCEA_Q sylQ)) -trivg_card1 -subG1.
    by rewrite quotient_sub1 // subsetI sQE centsC.
  have sQH: Q \subset H := subset_trans nAQ sNA_H.
  have sHsubH' r X:
    r \in \sigma(H) -> X \subset H -> r.-group X -> X \subset H^`(1).
  + move=> sHr sXH rX; apply: subset_trans (Msigma_der1 maxH).
    by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup rX sHr).
  have sAH': A \subset H^`(1) by apply: sHsubH' pA.
  have{t12H'q} sQH': Q \subset H^`(1).
    have [sHq | sH'q] := boolP (q \in \sigma(H)); first exact: sHsubH' qQ.
    have{sH'q} sH'Q: \sigma(H)^'.-group Q by apply: (pi_pnat qQ).
    have{sH'Q} [F hallF sQF] := Hall_superset (mmax_sol maxH) sQH sH'Q.
    have [-> | ntQ] := eqsVneq Q 1; first exact: sub1G.
    have{t12H'q} t3Hq: q \in \tau3(H).
      apply: implyP t12H'q; rewrite implyNb -orbA.
      rewrite -(partition_pi_sigma_compl maxH hallF) -p_rank_gt0.
      by rewrite (leq_trans _ (p_rankS q sQF)) // -rank_pgroup // rank_gt0.
    have solF: solvable F := sigma_compl_sol hallF.
    have [F3 hallF3 sQF3] := Hall_superset solF sQF (pi_pnat qQ t3Hq).
    have [[F1 hallF1] _] := ex_tau13_compl hallF.
    have [F2 _ complFi] := ex_tau2_compl hallF hallF1 hallF3.
    have [[sF3H' _] _ _ _ _] := sigma_compl_context maxH complFi.
    exact: subset_trans sQF3 (subset_trans sF3H' (dergS 1 (pHall_sub hallF))).
  have hallHb: \beta(H).-Hall(H) H`_\beta := Mbeta_Hall maxH.
  have nilH'b: nilpotent (H^`(1) / H`_\beta) := Mbeta_quo_nil maxH.
  have{nilH'b} sAQ_Hb: [~: A, Q] \subset H`_\beta.
    rewrite commGC -quotient_cents2 ?gFnorm_trans ?normsG //=.
    rewrite (sub_nilpotent_cent2 nilH'b) ?quotientS ?coprime_morph //.
    rewrite (pnat_coprime (pi_pnat pA t2Mp) (pi_pnat qQ _)) ?tau2'1 //.
    by rewrite (pnatPpi t1CEAb) // mem_primes q_pr cardG_gt0.
  rewrite (pnatPpi (pHall_pgroup hallHb)) // (piSg sAQ_Hb) // -p_rank_gt0.
  by rewrite -(rank_pgroup (pgroupS sAQ_A pA)) rank_gt0.
move=> H maxNA_H; split; last 1 [move=> q piCEAb_q piCEAq] || by auto.
have [_ sHp]: _ /\ p \in \sigma(H) := andP (part_a H maxNA_H p t2Mp).
have{maxNA_H} [maxH sNA_H] := setIdP maxNA_H.
have{sNA_H} sCA_H: 'C(A) \subset H := subset_trans (cent_sub A) sNA_H.
have{piCEAq} [Q0 EqQ0]: exists Q0, Q0 \in 'E_q^1('C_E(A)).
  by apply/p_rank_geP; rewrite p_rank_gt0.
have [sQ0_CEA abelQ0 dimQ0]:= pnElemP EqQ0; have [qQ0 cQ0Q0 _] := and3P abelQ0.
have{sQ0_CEA} [sQ0E cAQ0]: Q0 \subset E /\ Q0 \subset 'C(A).
  by apply/andP; rewrite -subsetI.
have ntQ0: Q0 :!=: 1 by apply: (nt_pnElem EqQ0).
have{t1CEAb} t1Mq: q \in \tau1(M) := pnatPpi t1CEAb piCEAb_q.
have [Q sylQ sQ0Q] := Sylow_superset sQ0E qQ0; have [sQE qQ _] := and3P sylQ.
have [E1 hallE1 sQE1] := Hall_superset solE sQE (pi_pnat qQ t1Mq).
have rqE: 'r_q(E) = 1%N.
  by move: t1Mq; rewrite (tau1E maxM hallE) andbA andbC; case: eqP.
have cycQ: cyclic Q.
  by rewrite (odd_pgroup_rank1_cyclic qQ) ?mFT_odd // (p_rank_Sylow sylQ) rqE.
have sCAE: 'C(A) \subset E by case/(tau2_compl_context maxM): Ep2A => // _ [].
have{sCAE} sylCQA: q.-Sylow('C(A)) 'C_Q(A).
  by apply: Hall_setI_normal sylQ; rewrite /= -(setIidPr sCAE).
have{sylCQA} defNA: 'C(A) * 'N_('N(A))(Q0) = 'N(A).
  apply/eqP; rewrite eqEsubset mulG_subG cent_sub subsetIl /=.
  rewrite -{1}(Frattini_arg (cent_normal A) sylCQA) mulgS ?setIS ?char_norms //.
  by rewrite (sub_cyclic_char Q0 (cyclicS (subsetIl Q _) cycQ)) subsetI sQ0Q.
have [L maxNQ0_L]: {L | L \in 'M('N(Q0))}.
  by apply: mmax_exists; rewrite mFT_norm_proper ?(mFT_pgroup_proper qQ0).
have{maxNQ0_L} [maxL sNQ0_L] := setIdP maxNQ0_L.
have sCQ0_L: 'C(Q0) \subset L := subset_trans (cent_sub Q0) sNQ0_L.
have sAL: A \subset L by rewrite (subset_trans _ sCQ0_L) // centsC.
have sCA_L: 'C(A) \subset L.
  by have /p2Elem_mmax[]: A \in 'E_p^2(L) by apply/pnElemP.
have{sCA_L defNA} maxNA_L: L \in 'M('N(A)).
  by rewrite inE maxL -defNA setIC mul_subG // subIset ?sNQ0_L.
have t2Lq: q \in \tau2(L).
  have /orP[sLq | //] := prime_class_mmax_norm maxL qQ0 sNQ0_L.
  by have /orP[/andP[/negP] | ] := pnatPpi (part_b L maxNA_L) piCEAb_q.
have [cQQ [/= sL'q _]] := (cyclic_abelian cycQ, andP t2Lq).
have sQL: Q \subset L := subset_trans (centsS sQ0Q cQQ) sCQ0_L. 
have [F hallF sQF] := Hall_superset (mmax_sol maxL) sQL (pi_pnat qQ sL'q).
have [B Eq2B _] := ex_tau2Elem hallF t2Lq.
have [_ sLp]: _ /\ p \in \sigma(L) := andP (part_a L maxNA_L p t2Mp).
have{H sHp maxH sCA_H} <-: L :=: H.
  have sLHp: p \in [predI \sigma(L) & \sigma(H)] by apply/andP.
  have [_ transCA _] := sigma_group_trans maxH sHp pA.
  set S := finset _ in transCA; have sAH := subset_trans cAA sCA_H.
  suffices [SH SL]: gval H \in S /\ gval L \in S.
    have [c cAc -> /=]:= atransP2 transCA SH SL.
    by rewrite conjGid // (subsetP sCA_H).
  have [_ _ _ TIsL] := tau2_compl_context maxL hallF t2Lq Eq2B.
  apply/andP; rewrite !inE sAH sAL orbit_refl orbit_sym /= andbT.
  by apply: contraLR sLHp => /TIsL[] // _ ->.
split=> //.
  exists ('O_p(L`_\sigma))%G; last by rewrite /= -pcoreI pcore_normal.
  rewrite inE (subHall_Sylow (Msigma_Hall_G maxL) sLp) //.
  by rewrite nilpotent_pcore_Hall // (tau2_Msigma_nil maxL t2Lq).
have [Q1 sylQ1 sQQ1] := Sylow_superset (subsetT Q) qQ.
have [sQ0Q1 qQ1] := (subset_trans sQ0Q sQQ1, pHall_pgroup sylQ1).
have [cQ1Q1 | not_cQ1Q1] := boolP (abelian Q1).
  by exists Q1; rewrite inE (subset_trans (centsS sQ0Q1 cQ1Q1)).
have [_ _ regB [F0 /=]] := nonabelian_tau2 maxL hallF t2Lq Eq2B qQ1 not_cQ1Q1.
have{regB} ->: 'C_B(L`_\sigma) = Q0; last move=> defF _.
  apply: contraTeq sCQ0_L => neqQ0B; case: (regB Q0) => //.
  by rewrite 2!inE eq_sym neqQ0B; apply/pnElemP; rewrite (subset_trans sQ0Q).
have{defF} defQ: Q0 \x (F0 :&: Q) = Q.
  rewrite dprodEsd ?(centSS (subsetIr F0 Q) sQ0Q) //.
  by rewrite (sdprod_modl defF sQ0Q) (setIidPr sQF).
have [[/eqP/idPn//] | [_ eqQ0Q]] := cyclic_pgroup_dprod_trivg qQ cycQ defQ.
have nCEA_Q := subset_trans sQE nCA_E.
case/idPn: piCEAb_q; rewrite -p'natEpi -?partn_eq1 ?cardG_gt0 //.
rewrite -(card_Hall (quotient_pHall nCEA_Q sylQ)) -trivg_card1 -subG1.
by rewrite quotient_sub1 // subsetI sQE -eqQ0Q.
Qed.

(* This is a generalization of B & G, Theorem 12.12. *)
(* In the B & G text, Theorem 12.12 only establishes the type F structure     *)
(* for groups of type I, whereas it is required for the derived groups of     *)
(* groups of type II (in the sense of Peterfalvi). Indeed this is exactly     *)
(* what is stated in Lemma 15.15(e) and then Theorem B(3). The proof of       *)
(* 15.15(c) cites 12.12 in the type I case (K = 1) and then loosely invokes   *)
(* a "short and easy argument" inside the proof of 12.12 for the K != 1 case. *)
(* In fact, this involves copying roughly 25% of the proof, whereas the proof *)
(* remains essentially unchanged when Theorem 12.12 is generalized to a       *)
(* normal Hall subgroup of E as below.                                        *)
(*   Also, we simplify the argument for central tau2 Sylow subgroup S of U by *)
(* by replacing the considerations on the abelian structure of S by a         *)
(* comparison of Mho^n-1(S) and Ohm_1(S) (with exponent S = p ^ n), as the    *)
(* former is needed anyway to prove regularity when S is not homocyclic.      *)
Theorem FTtypeF_complement M (Ms := M`_\sigma) E U :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> Hall E U -> U <| E -> U :!=: 1 ->
  {in U^#, forall e, [predU \tau1(M) & \tau3(M)].-elt e -> 'C_Ms[e] = 1} ->
  [/\ (*a*) exists A0 : {group gT},
             [/\ A0 <| U, abelian A0 & {in Ms^#, forall x, 'C_U[x] \subset A0}]
    & (*b*) exists E0 : {group gT},
             [/\ E0 \subset U, exponent E0 = exponent U
               & [Frobenius Ms <*> E0 = Ms ><| E0]]].
Proof.
set p13 := predU _ _  => maxM hallE /Hall_pi hallU nsUE ntU regU13.
have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE.
have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3.
have [[sE1E _] [sE2E t2E2 _]] := (andP hallE1, and3P hallE2).
have [[_ nsE3E] _ [cycE1 _] [defE _] _] := sigma_compl_context maxM complEi.
have [[[sE3E t3E3 _][_ nE3E]] [sUE _]] := (and3P hallE3, andP nsE3E, andP nsUE).
have defM: Ms ><| E = M := sdprod_sigma maxM hallE.
have [nsMsM sEM mulMsE nMsE tiMsE] := sdprod_context defM.
have ntMs: Ms != 1 := Msigma_neq1 maxM.
have{defM} defMsU: Ms ><| U = Ms <*> U := sdprod_subr defM sUE.
pose U2 := (E2 :&: U)%G.
have hallU2: \tau2(M).-Hall(U) U2 := Hall_setI_normal nsUE hallE2.
have [U2_1 | ntU2] := eqsVneq U2 1.
  have frobMsU: [Frobenius Ms <*> U = Ms ><| U].
    apply/Frobenius_semiregularP=> // e Ue.
    apply: regU13 => //; case/setD1P: Ue => _; apply: mem_p_elt.
    have: \tau2(M)^'.-group U.
      by rewrite -partG_eq1 -(card_Hall hallU2) U2_1 cards1.
    apply: sub_in_pnat => p /(piSg sUE).
    by rewrite (partition_pi_sigma_compl maxM hallE) orbCA => /orP[] // /idPn.
  split; [exists 1%G; rewrite normal1 abelian1 | by exists U].
  by split=> //= x Ux; rewrite (Frobenius_reg_compl frobMsU).
have [[sU2U t2U2 _] [p p_pr rU2]] := (and3P hallU2, rank_witness U2).
have piU2p: p \in \pi(U2) by rewrite -p_rank_gt0 -rU2 rank_gt0.
have t2p: p \in \tau2(M) := pnatPpi t2U2 piU2p.
have [A Ep2A Ep2A_M] := ex_tau2Elem hallE t2p.
have [sAE abelA _] := pnElemP Ep2A; have{abelA} [pA cAA _] := and3P abelA.
have [S sylS sAS] := Sylow_superset (subsetT A) pA.
have [cSS | not_cSS] := boolP (abelian S); last first.
  have [_] := nonabelian_tau2 maxM hallE t2p Ep2A (pHall_pgroup sylS) not_cSS.
  set A0 := ('C_A(_))%G => [] [oA0 _] _ {defE} [E0 defE regE0].
  have [nsA0E sE0E mulAE0 nAE0 tiAE0] := sdprod_context defE.
  have [P sylP] := Sylow_exists p U; have [sPU _] := andP sylP.
  have sylP_E := subHall_Sylow hallU (piSg sU2U piU2p) sylP.
  have pA0: p.-group A0 by rewrite /pgroup oA0 pnat_id.
  have sA0P: A0 \subset P.
    by apply: subset_trans (pcore_sub_Hall sylP_E); apply: pcore_max.
  have sA0U: A0 \subset U := subset_trans sA0P sPU.
  pose U0 := (E0 :&: U)%G.
  have defU: A0 ><| U0 = U by rewrite (sdprod_modl defE) // (setIidPr sUE).
  have piU0p: p \in \pi(U0).
    have:= lognSg p sAE; rewrite (card_pnElem Ep2A) pfactorK //.
    rewrite -logn_part -(card_Hall sylP_E) (card_Hall sylP) logn_part.
    rewrite -(sdprod_card defU) oA0 lognM // ?prime_gt0 // logn_prime // eqxx.
    by rewrite ltnS logn_gt0.
  have defM0: Ms ><| U0 = Ms <*> U0 := sdprod_subr defMsU (subsetIr _ _).
  have frobM0: [Frobenius Ms <*> U0 = Ms ><| U0].
    apply/Frobenius_semiregularP=> // [|e /setD1P[nte /setIP[E0e Ue]]].      
      by rewrite -rank_gt0 (leq_trans _ (p_rank_le_rank p _)) ?p_rank_gt0.    
    have [ | ] := boolP (p13.-elt e); first by apply: regU13; rewrite !inE nte.
    apply: contraNeq => /trivgPn[x /setIP[Ms_x cex] ntx].
    apply/pgroupP=> q q_pr q_dv_x ; rewrite inE /= (regE0 x) ?inE ?ntx //.
    rewrite mem_primes q_pr cardG_gt0 (dvdn_trans q_dv_x) ?order_dvdG //.
    by rewrite inE E0e cent1C.
  have [nsA0U sU0U _ _ _] := sdprod_context defU.
  split; [exists A0 | exists U0].
    split=> // [|x Ms_x]; first by rewrite (abelianS (subsetIl A _) cAA).
    rewrite -(sdprodW defU) -group_modl ?(Frobenius_reg_compl frobM0) ?mulg1 //.
    by rewrite subIset //= orbC -cent_set1 centS // sub1set; case/setD1P: Ms_x.
  split=> //; apply/eqP; rewrite eqn_dvd exponentS //=.
  rewrite -(partnC p (exponent_gt0 U0)) -(partnC p (exponent_gt0 U)).
  apply: dvdn_mul; last first.
    rewrite (partn_exponentS sU0U) // -(sdprod_card defU) partnM ?cardG_gt0 //.
    by rewrite part_p'nat ?pnatNK // mul1n dvdn_part.
  have cPP: abelian P.
    have [/(_ P)[] //] := tau2_context maxM t2p Ep2A_M.
    by apply: subHall_Sylow hallE _ sylP_E; case/andP: t2p.
  have defP: A0 \x (U0 :&: P) = P.
    rewrite dprodEsd ?(sub_abelian_cent2 cPP) ?subsetIr //.
    by rewrite (sdprod_modl defU) // (setIidPr sPU).
  have sylP_U0: p.-Sylow(U0) (U0 :&: P).
    rewrite pHallE subsetIl /= -(eqn_pmul2l (cardG_gt0 A0)).
    rewrite (dprod_card defP) (card_Hall sylP) -(sdprod_card defU).
    by rewrite partnM // part_pnat_id.
  rewrite -(exponent_Hall sylP) -(dprod_exponent defP) (exponent_Hall sylP_U0).
  rewrite dvdn_lcm (dvdn_trans (exponent_dvdn A0)) //= oA0.
  apply: contraLR piU0p; rewrite -p'natE // -partn_eq1 // partn_part //.
  by rewrite partn_eq1 ?exponent_gt0 // pnat_exponent -p'groupEpi.
have{t2p Ep2A sylS sAS cSS} [[nsE2E cE2E2] hallE2_G _ _]
  := abelian_tau2 maxM complEi t2p Ep2A sylS sAS cSS.
clear p p_pr rU2 piU2p A S Ep2A_M sAE pA cAA.
have nsU2U: U2 <| U by rewrite (normalS sU2U sUE) ?normalI.
have cU2U2: abelian U2 := abelianS (subsetIl _ _) cE2E2.
split.
  exists U2; rewrite -set1gE; split=> // x /setDP[Ms_x ntx].
  rewrite (sub_normal_Hall hallU2) ?subsetIl //=.
  apply: sub_in_pnat (pgroup_pi _) => q /(piSg (subsetIl U _))/(piSg sUE).
  rewrite (partition_pi_sigma_compl maxM) // orbCA => /orP[] // t13q.
  rewrite mem_primes => /and3P[q_pr _ /Cauchy[] // y /setIP[Uy cxy] oy].
  case/negP: ntx; rewrite -(regU13 y); first by rewrite inE Ms_x cent1C.
    by rewrite !inE -order_gt1 oy prime_gt1.
  by rewrite /p_elt oy pnatE.
pose sylU2 S := (S :!=: 1) && Sylow U2 S.
pose cyclicRegular Z S :=
   [/\ Z <| U, cyclic Z, 'C_Ms('Ohm_1(Z)) = 1 & exponent Z = exponent S].
suffices /fin_all_exists[Z_ Z_P] S: exists Z, sylU2 S -> cyclicRegular Z S.
  pose Z2 := <<\bigcup_(S | sylU2 S) Z_ S>>.
  have sZU2: Z2 \subset U2.
    rewrite gen_subG; apply/bigcupsP=> S sylS.
    have [[/andP[sZE _] _ _ eq_expZS] [_ _ sSU2 _]] := (Z_P S sylS, and4P sylS).
    rewrite (sub_normal_Hall hallU2) // -pnat_exponent eq_expZS.
    by rewrite pnat_exponent (pgroupS sSU2 t2U2).
  have nZ2U: U \subset 'N(Z2).
    by rewrite norms_gen ?norms_bigcup //; apply/bigcapsP => S /Z_P[/andP[]].
  have solU: solvable U := solvableS sUE (sigma_compl_sol hallE).
  have [U31 hallU31] := Hall_exists \tau2(M)^' solU.
  have [[sU31U t2'U31 _] t2Z2] := (and3P hallU31, pgroupS sZU2 t2U2).
  pose U0 := (Z2 <*> U31)%G; have /joing_sub[sZ2U0 sU310] := erefl (gval U0).
  have sU0U: U0 \subset U by rewrite join_subG (subset_trans sZU2).
  have nsZ2U0: Z2 <| U0 by rewrite /normal sZ2U0 (subset_trans sU0U).
  have defU0: Z2 * U31 = U0 by rewrite -norm_joinEr // (subset_trans sU31U).
  have [hallZ2 hallU31_0] := coprime_mulpG_Hall defU0 t2Z2 t2'U31.
  have expU0U: exponent U0 = exponent U.
    have exp_t2c U' := partnC \tau2(M) (exponent_gt0 U').
    rewrite -(exp_t2c U) -(exponent_Hall hallU31) -(exponent_Hall hallU2).
    rewrite -{}exp_t2c -(exponent_Hall hallU31_0) -(exponent_Hall hallZ2).
    congr (_ * _)%N; apply/eqP; rewrite eqn_dvd exponentS //=.
    apply/dvdn_partP=> [|p]; first exact: exponent_gt0.
    have [S sylS] := Sylow_exists p U2; rewrite -(exponent_Hall sylS).
    rewrite pi_of_exponent -p_rank_gt0 -(rank_Sylow sylS) rank_gt0 => ntS.
    have{sylS} sylS: sylU2 S by rewrite /sylU2 ntS (p_Sylow sylS).
    by have /Z_P[_ _ _ <-] := sylS; rewrite exponentS ?sub_gen ?(bigcup_max S).
  exists U0; split=> //.
  have ntU0: U0 :!=: 1 by rewrite trivg_exponent expU0U -trivg_exponent.
  apply/Frobenius_semiregularP=> //; first by rewrite (sdprod_subr defMsU).
  apply: semiregular_sym => x /setD1P[ntx Ms_x]; apply: contraNeq ntx.
  rewrite -rank_gt0; have [p p_pr ->] := rank_witness [group of 'C_U0[x]].
  rewrite -in_set1 -set1gE p_rank_gt0 => piCp.
  have [e /setIP[U0e cxe] oe]: {e | e \in 'C_U0[x] & #[e] = p}.
    by move: piCp; rewrite mem_primes p_pr cardG_gt0; apply: Cauchy.
  have nte: e != 1 by rewrite -order_gt1 oe prime_gt1.
  have{piCp} piUp: p \in \pi(U).
    by rewrite -pi_of_exponent -expU0U pi_of_exponent (piSg _ piCp) ?subsetIl.
  have:= piSg sUE piUp; rewrite (partition_pi_sigma_compl maxM) // orbCA orbC.
  case/orP=> [t13p | t2p].
    rewrite -(regU13 e) 1?inE ?Ms_x 1?cent1C //.
      by rewrite inE nte (subsetP sU0U).
    by rewrite /p_elt oe pnatE.
  have Z2e: e \in Z2 by rewrite (mem_normal_Hall hallZ2) // /p_elt oe pnatE.
  have [S sylS] := Sylow_exists p U2; have [sSU2 pS _] := and3P sylS.
  have sylS_U: p.-Sylow(U) S := subHall_Sylow hallU2 t2p sylS.
  have ntS: S :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylS_U) p_rank_gt0.
  have sylS_U2: sylU2 S by rewrite /sylU2 ntS (p_Sylow sylS).
  have [nsZU cycZ regZ1 eqexpZS] := Z_P S sylS_U2.
  suffices defZ1: 'Ohm_1(Z_ S) == <[e]>.
    by rewrite -regZ1 (eqP defZ1) cent_cycle inE Ms_x cent1C.
  have pZ: p.-group (Z_ S) by rewrite -pnat_exponent eqexpZS pnat_exponent.
  have sylZ: p.-Sylow(Z2) (Z_ S).
    have:= sZU2; rewrite pHallE /Z2 /= -bigprodGE (bigD1 S) //=.
    set Z2' := (\prod_(T | _) _)%G => /joing_subP[sZ_U2 sZ2'_U2].
    rewrite joing_subl cent_joinEl ?(sub_abelian_cent2 cU2U2) //=.
    suffices p'Z2': p^'.-group Z2'.
      rewrite coprime_cardMg ?(pnat_coprime pZ) //.
      by rewrite partnM // part_pnat_id // part_p'nat // muln1.
    elim/big_ind: Z2' sZ2'_U2 => [_||T /andP[sylT neqTS]]; first exact: pgroup1.
      move=> X Y IHX IHY /joing_subP[sXU2 sYU2] /=.
      by rewrite cent_joinEl ?(sub_abelian_cent2 cU2U2) // pgroupM IHX ?IHY.
    have /Z_P[_ _ _ expYT _] := sylT.
    have{sylT} [_ /SylowP[q _ sylT]] := andP sylT.
    rewrite -pnat_exponent expYT pnat_exponent.
    apply: (pi_pnat (pHall_pgroup sylT)); apply: contraNneq neqTS => eq_qp.
    have defOE2 := nilpotent_Hall_pcore (abelian_nil cU2U2).
    by rewrite -val_eqE /= (defOE2 _ _ sylS) (defOE2 _ _ sylT) eq_qp.
  have nZZ2 := normalS (pHall_sub sylZ) (subset_trans sZU2 sU2U) nsZU.
  have Ze: e \in Z_ S by rewrite (mem_normal_Hall sylZ) // /p_elt oe pnat_id.
  rewrite (eq_subG_cyclic cycZ) ?Ohm_sub ?cycle_subG // -orderE oe.
  by rewrite (Ohm1_cyclic_pgroup_prime _ pZ) //; apply/trivgPn; exists e.
case: (sylU2 S) / andP => [[ntS /SylowP[p p_pr sylS_U2]]|]; last by exists E.
have [sSU2 pS _] := and3P sylS_U2; have [sSE2 sSU] := subsetIP sSU2.
have piSp: p \in \pi(S) by rewrite -p_rank_gt0 -rank_pgroup ?rank_gt0.
have t2p: p \in \tau2(M) := pnatPpi t2U2 (piSg sSU2 piSp).
have sylS_U: p.-Sylow(U) S := subHall_Sylow hallU2 t2p sylS_U2.
have sylS_E: p.-Sylow(E) S := subHall_Sylow hallU (piSg sSU piSp) sylS_U.
have sylS: p.-Sylow(E2) S := pHall_subl sSE2 sE2E sylS_E.
have sylS_G: p.-Sylow(G) S := subHall_Sylow hallE2_G t2p sylS.
have [cSS [/= s'p rpM]] := (abelianS sSU2 cU2U2, andP t2p).
have sylS_M: p.-Sylow(M) S := subHall_Sylow hallE s'p sylS_E.
have rpS: 'r_p(S) = 2 by apply/eqP; rewrite (p_rank_Sylow sylS_M).
have [A] := p_rank_witness p S; rewrite rpS -(setIidPr (pHall_sub sylS_E)).
rewrite pnElemI setIC 2!inE => /andP[sAS Ep2A].
have [[nsAE defEp] _ nregEp_uniq _] := tau2_compl_context maxM hallE t2p Ep2A.
have [_ sNS'FE _ sCSE _]
  := abelian_tau2_sub_Fitting maxM hallE t2p Ep2A sylS_G sAS cSS.
have [_ _ [defNS _ _ _] regE1subZ]
  := abelian_tau2 maxM complEi t2p Ep2A sylS_G sAS cSS.
have nSE: E \subset 'N(S) by rewrite -defNS normal_norm.
have [sSE nSU] := (subset_trans sSE2 sE2E, subset_trans sUE nSE).
have n_subNS := abelian_tau2_norm_Sylow maxM hallE t2p Ep2A sylS_G sAS cSS.
have not_sNS_M: ~~ ('N(S) \subset M).
  by apply: contra s'p => sNS_M; apply/exists_inP; exists S; rewrite // inE.
have regNNS Z (Z1 := 'Ohm_1(Z)%G):
  Z \subset S -> cyclic Z -> Z :!=: 1 -> 'N(S) \subset 'N(Z1) -> 'C_Ms(Z1) = 1.
- move=> sZS cycZ ntZ nZ1_NS; apply: contraNeq not_sNS_M => nregZ1.
  have sZ1S: Z1 \subset S by apply: gFsub_trans.
  have EpZ1: Z1 \in 'E_p^1(E).
    rewrite p1ElemE // !inE (subset_trans sZ1S) //=.
    by rewrite (Ohm1_cyclic_pgroup_prime _ (pgroupS sZS pS)).
  have /= uCZ1 := nregEp_uniq _ EpZ1 nregZ1.
  apply: (subset_trans nZ1_NS); apply: (sub_uniq_mmax uCZ1 (cent_sub _)).
  by rewrite mFT_norm_proper ?(mFT_pgroup_proper (pgroupS sZ1S pS)) ?Ohm1_eq1.
have [_ nsCEA t1CEAb] := tau1_cent_tau2Elem_factor maxM hallE t2p Ep2A.
have [cSU | not_cSU] := boolP (U \subset 'C(S)).
  pose n := logn p (exponent S); pose Sn := 'Mho^n.-1(S)%G.
  have n_gt0: 0 < n by rewrite -pi_of_exponent -logn_gt0 in piSp.
  have expS: (exponent S = p ^ n.-1 * p)%N.
    rewrite -expnSr prednK -?p_part //.
    by rewrite part_pnat_id ?pnat_exponent ?expg_exponent.
  have sSnS1: Sn \subset 'Ohm_1(S).
    rewrite (OhmE 1 pS) /= (MhoE _ pS); apply/genS/subsetP=> _ /imsetP[x Sx ->].
    by rewrite !inE groupX //= -expgM -expS expg_exponent.
  have sSZ: S \subset 'Z(U) by rewrite subsetI sSU centsC.
  have{sSZ} nsZU z: z \in S -> <[z]> <| U.
    by move=> Sz; rewrite sub_center_normal ?cycle_subG ?(subsetP sSZ).
  have [homoS | ltSnS1] := eqVproper sSnS1.
    have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A.
    have [_ _ _ _ [A1 EpA1 regA1]] := tau2_context maxM t2p Ep2A_M.
    have [sA1A _ oA1] := pnElemPcard EpA1.
    have /cyclicP[zn defA1]: cyclic A1 by rewrite prime_cyclic ?oA1.
    have [z Sz def_zn]: exists2 z, z \in S & zn = z ^+ (p ^ n.-1).
      apply/imsetP; rewrite -(MhoEabelian _ pS cSS) homoS (OhmE 1 pS).
      rewrite mem_gen // !inE -cycle_subG -defA1 (subset_trans sA1A) //=.
      by rewrite -oA1 defA1 expg_order.
    have oz: #[z] = exponent S.
      by rewrite expS; apply: orderXpfactor; rewrite // -def_zn orderE -defA1.
    exists <[z]>%G; split; rewrite ?cycle_cyclic ?exponent_cycle ?nsZU //.
    by rewrite (Ohm_p_cycle _ (mem_p_elt pS Sz)) subn1 oz -def_zn -defA1.
  have [z Sz /esym oz] := exponent_witness (abelian_nil cSS).
  exists <[z]>%G; split; rewrite ?cycle_cyclic ?exponent_cycle ?nsZU //.
  have ntz: <[z]> != 1 by rewrite trivg_card1 -orderE oz -dvdn1 -trivg_exponent.
  rewrite regNNS ?cycle_cyclic ?cycle_subG //=.
  suffices /eqP->: 'Ohm_1(<[z]>) == Sn by apply: char_norms; apply: gFchar.
  have [p_z pS1] := (mem_p_elt pS Sz, pgroupS (Ohm_sub 1 S) pS). 
  rewrite eqEcard (Ohm1_cyclic_pgroup_prime _ p_z) ?cycle_cyclic //.
  rewrite (Ohm_p_cycle _ p_z) oz -/n subn1 cycle_subG Mho_p_elt //=.
  rewrite (card_pgroup (pgroupS sSnS1 pS1)) (leq_exp2l _ 1) ?prime_gt1 //.
  by rewrite -ltnS -rpS p_rank_abelian ?properG_ltn_log.
have{not_cSU} [q q_pr piUq]: {q | prime q & q \in \pi(U / 'C(S))}.
  have [q q_pr rCE] := rank_witness (U / 'C(S)); exists q => //.
  by rewrite -p_rank_gt0 -rCE rank_gt0 -subG1 quotient_sub1 ?norms_cent.
have{piUq} [piCESbq piUq]: q \in \pi(E / 'C_E(S)) /\ q \in \pi(U).
  rewrite /= setIC (card_isog (second_isog (norms_cent nSE))).
  by rewrite (piSg _ piUq) ?quotientS // (pi_of_dvd _ _ piUq) ?dvdn_quotient.
have [Q1 sylQ1_U] := Sylow_exists q U; have [sQ1U qQ1 _] := and3P sylQ1_U.
have sylQ1: q.-Sylow(E) Q1 := subHall_Sylow hallU piUq sylQ1_U.
have sQ1E := subset_trans sQ1U sUE; have nSQ1 := subset_trans sQ1E nSE.
have [Q sylQ sQ1Q] := Sylow_superset nSQ1 qQ1; have [nSQ qQ _] := and3P sylQ.
have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A.
have ltCQ1_S: 'C_S(Q1) \proper S.
  rewrite properE subsetIl /= subsetI subxx centsC -sQ1E -subsetI.
  have nCES_Q1: Q1 \subset 'N('C_E(S)) by rewrite (setIidPr sCSE) norms_cent.
  rewrite -quotient_sub1 // subG1 -rank_gt0.
  by rewrite (rank_Sylow (quotient_pHall nCES_Q1 sylQ1)) p_rank_gt0.
have coSQ: coprime #|S| #|Q|.
  suffices p'q: q != p by rewrite (pnat_coprime pS) // (pi_pnat qQ).
  apply: contraNneq (proper_subn ltCQ1_S) => eq_qp; rewrite subsetI subxx.
  rewrite (sub_abelian_cent2 cE2E2) // (sub_normal_Hall hallE2) //.
  by rewrite (pi_pgroup qQ1) ?eq_qp.
have not_sQ1CEA: ~~ (Q1 \subset 'C_E(A)).
  rewrite subsetI sQ1E; apply: contra (proper_subn ltCQ1_S) => /= cAQ1.
  rewrite subsetIidl centsC coprime_abelian_faithful_Ohm1 ?(coprimegS sQ1Q) //.
  by case: (tau2_context maxM t2p Ep2A_M); case/(_ S sylS_M)=> _ [|->] //.
have t1q: q \in \tau1(M).
  rewrite (pnatPpi t1CEAb) // -p_rank_gt0.
  have nCEA_Q1: Q1 \subset 'N('C_E(A)) := subset_trans sQ1E (normal_norm nsCEA).
  rewrite -(rank_Sylow (quotient_pHall nCEA_Q1 sylQ1)) rank_gt0.
  by rewrite -subG1 quotient_sub1.
have cycQ1: cyclic Q1.
  have [x _ sQ1E1x] := Hall_psubJ hallE1 t1q sQ1E qQ1.
  by rewrite (cyclicS sQ1E1x) ?cyclicJ.
have defQ1: Q :&: E = Q1.
  apply: (sub_pHall sylQ1) (subsetIr Q E); last by rewrite subsetI sQ1Q.
  by rewrite (pgroupS (subsetIl Q _)).
pose Q0 := 'C_Q(S); have nsQ0Q: Q0 <| Q by rewrite norm_normalI ?norms_cent.
have [sQ0Q nQ0Q] := andP nsQ0Q; have nQ01 := subset_trans sQ1Q nQ0Q.
have coSQ0: coprime #|S| #|Q0| := coprimegS sQ0Q coSQ.
have ltQ01: Q0 \proper Q1.
  rewrite /proper -{1}defQ1 setIS //.
  apply: contra (proper_subn ltCQ1_S) => sQ10.
  by rewrite subsetIidl (centsS sQ10) // centsC subsetIr.
have [X]: exists2 X, X \in subgroups Q & ('C_S(X) != 1) && ([~: S, X] != 1).
  apply/exists_inP; apply: contraFT (ltnn 1); rewrite negb_exists_in => irrS.
  have [sQ01 not_sQ10] := andP ltQ01.
  have qQb: q.-group (Q / Q0) by apply: quotient_pgroup.
  have ntQ1b: Q1 / Q0 != 1 by rewrite -subG1 quotient_sub1.
  have ntQb: Q / Q0 != 1 := subG1_contra (quotientS _ sQ1Q) ntQ1b.
  have{irrS} regQ: semiregular (S / Q0) (Q / Q0).
    move=> Q0x; rewrite 2!inE -cycle_subG -cycle_eq1 -cent_cycle andbC.
    case/andP; case/(inv_quotientS nsQ0Q)=> X /= -> {Q0x} sQ0X sXQ ntXb.
    have [nSX nQ0X] := (subset_trans sXQ nSQ, subset_trans sXQ nQ0Q).
    rewrite -quotient_TI_subcent ?(coprime_TIg coSQ0) //.
    apply: contraTeq (forallP irrS X) => ntCSXb; rewrite inE sXQ negbK.
    apply/andP; split.
      by apply: contraNneq ntCSXb => ->; rewrite quotient1.
    apply: contraNneq ntXb; move/commG1P => cXS.
    by rewrite quotientS1 // subsetI sXQ centsC.
  have{regQ} cycQb: cyclic (Q / Q0).
    have nSQb: Q / Q0 \subset 'N(S / Q0) by apply: quotient_norms.
    apply: odd_regular_pgroup_cyclic qQb (mFT_quo_odd _ _) _ nSQb regQ.
    rewrite -(isog_eq1 (quotient_isog _ _)) ?coprime_TIg 1?coprime_sym //.
    by rewrite cents_norm // centsC subsetIr.
  have rQ1: 'r(Q1) = 1%N.
    apply/eqP; rewrite (rank_Sylow sylQ1).
    by rewrite (tau1E maxM hallE) in t1q; case/and3P: t1q.
  have: 'r(Q) <= 1; last apply: leq_trans.
    have nQ0_Ohm1Q: 'Ohm_1(Q) \subset 'N(Q0) by apply: gFsub_trans.
    rewrite -rQ1 -rank_Ohm1 rankS // -(quotientSGK _ sQ01) //.
    rewrite (subset_trans (morphim_Ohm _ _ nQ0Q)) //= -quotientE -/Q0.
    rewrite -(cardSg_cyclic cycQb) ?Ohm_sub ?quotientS //.
    have [_ q_dv_Q1b _] := pgroup_pdiv (pgroupS (quotientS _ sQ1Q) qQb) ntQ1b.
    by rewrite (Ohm1_cyclic_pgroup_prime cycQb qQb ntQb).
  have ltNA_G: 'N(A) \proper G.
    by rewrite defNS mFT_norm_proper // (mFT_pgroup_proper pS).
  have [H maxNA_H] := mmax_exists ltNA_G.
  have nCEA_Q1 := subset_trans sQ1E (normal_norm nsCEA). 
  have [_ _] := primes_norm_tau2Elem maxM hallE t2p Ep2A maxNA_H.
  case/(_ q)=> [||t2Hq [S2 sylS2 nsS2H] _].
  - rewrite -p_rank_gt0 -(rank_Sylow (quotient_pHall _ sylQ1)) //.
    by rewrite rank_gt0 -subG1 quotient_sub1.
  - rewrite -p_rank_gt0 -rQ1 (rank_pgroup qQ1) -p_rank_Ohm1 p_rankS //.
    have: 'Z(E) \subset 'C_E(A); last apply: subset_trans.
      by rewrite setIS ?centS // normal_sub.
    have [x Ex sQ1xE1] := Hall_pJsub hallE1 t1q sQ1E qQ1.
    rewrite -(conjSg _ _ x) ['Z(E) :^ x](normsP _ x Ex) ?gFnorm //.
    set Q11x := _ :^ x; have oQ11x: #|Q11x| = q.
      by rewrite cardJg (Ohm1_cyclic_pgroup_prime _ qQ1) // -rank_gt0 rQ1.
    apply: regE1subZ; rewrite /= -/Q11x.
      apply/nElemP; exists q; rewrite p1ElemE // !inE oQ11x.
      by rewrite (subset_trans _ sQ1xE1) //= conjSg Ohm_sub.
    have /cyclicP[y defQ11x]: cyclic Q11x by rewrite prime_cyclic ?oQ11x.
    rewrite defQ11x cent_cycle regU13 //.
      rewrite !inE -order_gt1 -cycle_subG /order -defQ11x oQ11x prime_gt1 //.
      by rewrite -(normsP (normal_norm nsUE) x Ex) conjSg gFsub_trans.
    by rewrite /p_elt /order -defQ11x oQ11x pnatE //; apply/orP; left.
  rewrite inE in sylS2; have [sS2H _]:= andP nsS2H.
  have sylS2_H := pHall_subl sS2H (subsetT H) sylS2.
  have [maxH sNS_H] := setIdP maxNA_H; rewrite /= defNS in sNS_H.
  have sylS_H := pHall_subl (subset_trans (normG S) sNS_H) (subsetT H) sylS_G.
  have defS2: S :=: S2 := uniq_normal_Hall sylS2_H nsS2H (Hall_max sylS_H).
  have sylQ_H: q.-Sylow(H) Q by rewrite -(mmax_normal maxH nsS2H) -defS2.
  by rewrite (rank_Sylow sylQ_H); case/andP: t2Hq => _ /eqP->.
rewrite inE => sXQ /=; have nSX := subset_trans sXQ nSQ.
set S1 := [~: S, X]; set S2 := 'C_S(X) => /andP[ntS2 ntS1].
have defS12: S1 \x S2 = S.
  by apply: coprime_abelian_cent_dprod; rewrite ?(coprimegS sXQ).
have /mulG_sub[sS1S sS2S] := dprodW defS12.
have [cycS1 cycS2]: cyclic S1 /\ cyclic S2.
  apply/andP; rewrite !(abelian_rank1_cyclic (abelianS _ cSS)) //.
  rewrite -(leqif_add (leqif_geq _) (leqif_geq _)) ?rank_gt0 // addn1 -rpS.
  rewrite !(rank_pgroup (pgroupS _ pS)) ?(p_rank_abelian p (abelianS _ cSS)) //.
  by rewrite -lognM ?cardG_gt0 // (dprod_card (Ohm_dprod 1 defS12)).
have [nsS2NS nsS1NS]: S2 <| 'N(S) /\ S1 <| 'N(S) := n_subNS X nSX.
pose Z := if #|S1| < #|S2| then [group of S2] else [group of S1].
have [ntZ sZS nsZN cycZ]: [/\ Z :!=: 1, Z \subset S, Z <| 'N(S) & cyclic Z].
  by rewrite /Z; case: ifP.
have nsZU: Z <| U := normalS (subset_trans sZS sSU) nSU nsZN.
exists Z; split=> //=.
  by rewrite regNNS // (char_norm_trans (Ohm_char 1 Z)) // normal_norm.
rewrite -(dprod_exponent defS12) /= (fun_if val) fun_if !exponent_cyclic //=.
rewrite (card_pgroup (pgroupS sS1S pS)) (card_pgroup (pgroupS sS2S pS)) //.
by rewrite /= -/S1 -/S2 ltn_exp2l ?prime_gt1 // -fun_if expn_max.
Qed.

(* This is B & G, Theorem 12.13. *)
Theorem nonabelian_Uniqueness p P : p.-group P -> ~~ abelian P -> P \in 'U.
Proof.
move=> pP not_cPP; have [M maxP_M] := mmax_exists (mFT_pgroup_proper pP).
have sigma_p L: L \in 'M(P) -> p \in \sigma(L).
  case/setIdP=> maxL sPL; apply: contraR not_cPP => sL'p.
  exact: sigma'_nil_abelian maxL sPL (pi_pnat pP _) (pgroup_nil pP).
have{maxP_M} [[maxM sPM] sMp] := (setIdP maxP_M, sigma_p M maxP_M).
rewrite (uniq_mmax_subset1 maxM sPM); apply/subsetP=> H maxP_H; rewrite inE.
have{sigma_p maxP_H} [[maxH sPH] sHp] := (setIdP maxP_H, sigma_p H maxP_H).
without loss{pP sPH sPM} sylP: P not_cPP / p.-Sylow(M :&: H) P.
  move=> IH; have sP_MH: P \subset M :&: H by rewrite subsetI sPM.
  have [S sylS sPS] := Sylow_superset sP_MH pP.
  exact: IH (contra (abelianS sPS) not_cPP) sylS.
have [sP_MH pP _] := and3P sylP; have [sPM sPH] := subsetIP sP_MH.
have ncycP := contra (@cyclic_abelian _ _) not_cPP.
have{sHp} sNMH: 'N(P) \subset M :&: H.
  by rewrite subsetI !(@norm_noncyclic_sigma _ p).
have{sylP} sylP_M: p.-Sylow(M) P.
  have [S sylS sPS] := Sylow_superset sPM pP; have pS := pHall_pgroup sylS.
  have [-> // | ltPS] := eqVproper sPS.
  have /andP[sNP] := nilpotent_proper_norm (pgroup_nil pS) ltPS.
  rewrite (sub_pHall sylP _ sNP) ?subxx ?(pgroupS (subsetIl _ _)) //.
  by rewrite subIset // orbC sNMH.
have{sMp} sylP_G: p.-Sylow(G) P := sigma_Sylow_G maxM sMp sylP_M.
have sylP_H: p.-Sylow(H) P := pHall_subl sPH (subsetT H) sylP_G.
have [rPgt2 | rPle2] := ltnP 2 'r(P).
  have uniqP: P \in 'U by rewrite rank3_Uniqueness ?(mFT_pgroup_proper pP).
  have defMP: 'M(P) = [set M] := def_uniq_mmax uniqP maxM sPM.
  by rewrite -val_eqE /= (eq_uniq_mmax defMP maxH).
have rpP: 'r_p(P) = 2.
  apply/eqP; rewrite eqn_leq -{1}rank_pgroup // rPle2 ltnNge.
  by rewrite -odd_pgroup_rank1_cyclic ?mFT_odd.
have:= mFT_rank2_Sylow_cprod sylP_G rPle2 not_cPP.
case=> Q [not_cQQ dimQ eQ] [R cycR [defP defR1]].
have sQP: Q \subset P by have /mulG_sub[] := cprodW defP.
have pQ: p.-group Q := pgroupS sQP pP.
have oQ: #|Q| = (p ^ 3)%N by rewrite (card_pgroup pQ) dimQ.
have esQ: extraspecial Q by apply: (p3group_extraspecial pQ); rewrite ?dimQ.
have p_pr := extraspecial_prime pQ esQ; have p_gt1 := prime_gt1 p_pr.
pose Z := 'Z(Q)%G; have oZ: #|Z| = p := card_center_extraspecial pQ esQ.
have nsZQ: Z <| Q := center_normal Q; have [sZQ nZQ] := andP nsZQ.
have [[defPhiQ defQ'] _]: ('Phi(Q) = Z /\ Q^`(1) = Z) /\ _ := esQ.
have defZ: 'Ohm_1 ('Z(P)) = Z.
  have [_ <- _] := cprodP (center_cprod defP).
  by rewrite (center_idP (cyclic_abelian cycR)) -defR1 mulSGid ?Ohm_sub.
have ncycQ: ~~ cyclic Q := contra (@cyclic_abelian _ Q) not_cQQ.
have rQgt1: 'r_p(Q) > 1.
  by rewrite ltnNge -(odd_pgroup_rank1_cyclic pQ) ?mFT_odd.
have [A Ep2A]: exists A, A \in 'E_p^2(Q) by apply/p_rank_geP.
wlog uniqNEpA: M H maxM maxH sP_MH sNMH sPM sPH sylP_M sylP_H /
    ~~ [exists A0 in 'E_p^1(A) :\ Z, 'M('N(A0)) == [set M]].
- move=> IH; case: exists_inP (IH M H) => [[A0 EpA0 defMA0] _ | _ -> //].
  case: exists_inP {IH}(IH H M) => [[A1 EpA1 defMA1] _ | _]; last first.
    by rewrite setIC eq_sym => ->.
  have [sAQ abelA dimA] := pnElemP Ep2A; have sAP := subset_trans sAQ sQP.
  have transNP: [transitive 'N_P(A), on 'E_p^1(A) :\ Z | 'JG].
    have [|_ _] :=  basic_p2maxElem_structure _ pP sAP not_cPP.
      have Ep2A_G := subsetP (pnElemS p 2 (subsetT Q)) A Ep2A.
      rewrite inE Ep2A_G (subsetP (p_rankElem_max p G)) //.
      by rewrite -(p_rank_Sylow sylP_G) rpP.
    by rewrite (group_inj defZ).
  have [x NPx defA1] := atransP2 transNP EpA0 EpA1.
  have Mx: x \in M by rewrite (subsetP sPM) //; case/setIP: NPx.
  rewrite eq_sym -in_set1 -(group_inj (conjGid Mx)).
  by rewrite -(eqP defMA1) defA1 /= normJ mmax_ofJ (eqP defMA0) set11.
apply: contraR uniqNEpA => neqHM; have sQM := subset_trans sQP sPM.
suffices{A Ep2A} [ntMa nonuniqNZ]: M`_\alpha != 1 /\ 'M('N(Z)) != [set M].
  have [A0 EpA0 defMNA0]: exists2 A0, A0 \in 'E_p^1(A) & 'M('N(A0)) == [set M].
    apply/exists_inP; apply: contraR ntMa; rewrite negb_exists_in => uniqNA1.
    have{Ep2A} Ep2A: A \in 'E_p^2(M) := subsetP (pnElemS p 2 sQM) A Ep2A.
    by have [_ [//|_ ->]] := p2Elem_mmax maxM Ep2A.
  apply/exists_inP; exists A0; rewrite // 2!inE EpA0 andbT.
  by apply: contraNneq nonuniqNZ => <-.
have coMaQ: coprime #|M`_\alpha| #|Q|.
  apply: pnat_coprime (pcore_pgroup _ _) (pi_pnat pQ _).
  by rewrite !inE -(p_rank_Sylow sylP_M) rpP.
have nMaQ: Q \subset 'N(M`_\alpha) by rewrite (subset_trans sQM) ?gFnorm.
have [coMaZ nMaZ] := (coprimegS sZQ coMaQ, subset_trans sZQ nMaQ).
pose K := 'N_(M`_\alpha)(Z).
have defKC: 'C_(M`_\alpha)(Z) = K by rewrite -coprime_norm_cent.
have coKQ: coprime #|K| #|Q| := coprimeSg (subsetIl _ _) coMaQ.
have nKQ: Q \subset 'N(K) by rewrite normsI ?norms_norm.
have [coKZ nKZ] := (coprimegS sZQ coKQ, subset_trans sZQ nKQ).
have sKH: K \subset H.
  have sZH := subset_trans sZQ (subset_trans sQP sPH).
  rewrite -(quotientSGK (subsetIr _ _) sZH) /= -/Z -/K.
  have cQQb: abelian (Q / Z) by rewrite -defQ' sub_der1_abelian.
  rewrite -(coprime_abelian_gen_cent cQQb) ?coprime_morph ?quotient_norms //.
  rewrite gen_subG /= -/K -/Z; apply/bigcupsP=> Ab; rewrite andbC; case/andP.
  case/(inv_quotientN nsZQ)=> A -> sZA nsAQ; have sAQ := normal_sub nsAQ.
  rewrite (isog_cyclic (third_isog _ _ _)) // -/Z => cycQA.
  have pA: p.-group A := pgroupS sAQ pQ.
  have rAgt1: 'r_p(A) > 1.
    have [-> // | ltAQ] := eqVproper sAQ.
    rewrite ltnNge -(odd_pgroup_rank1_cyclic pA) ?mFT_odd //.
    apply: contraL cycQA => cycA /=; have cAA := cyclic_abelian cycA.
    suff <-: Z :=: A by rewrite -defPhiQ (contra (@Phi_quotient_cyclic _ Q)).
    apply/eqP; rewrite eqEcard sZA /= oZ (card_pgroup pA) (leq_exp2l _ 1) //.
    by rewrite -abelem_cyclic // /abelem pA cAA (dvdn_trans (exponentS sAQ)).
  have [A1 EpA1] := p_rank_geP rAgt1.
  rewrite -(setIidPr (subset_trans sAQ (subset_trans sQP sPH))) pnElemI in EpA1.
  have{EpA1} [Ep2A1 sA1A]:= setIdP EpA1; rewrite inE in sA1A.
  have [sCA1_H _]: 'C(A1) \subset H /\ _ := p2Elem_mmax maxH Ep2A1.
  rewrite -quotient_TI_subcent ?(subset_trans sAQ) ?(coprime_TIg coKZ) //= -/K.
  by rewrite quotientS // subIset // orbC (subset_trans (centS sA1A)).
have defM: M`_\alpha * (M :&: H) = M.
  rewrite setIC in sNMH *.
  have [defM eq_aM_bM] := nonuniq_norm_Sylow_pprod maxM maxH neqHM sylP_G sNMH.
  by rewrite [M`_\alpha](eq_pcore M eq_aM_bM).
do [split; apply: contraNneq neqHM] => [Ma1 | uniqNZ].
  by rewrite -val_eqE /= (eq_mmax maxM maxH) // -defM Ma1 mul1g subsetIr.
have [_ sNZM]: _ /\ 'N(Z) \subset M := mem_uniq_mmax uniqNZ.
rewrite -val_eqE /= (eq_uniq_mmax uniqNZ maxH) //= -(setIidPr sNZM).
have sZ_MH: Z \subset M :&: H := subset_trans sZQ (subset_trans sQP sP_MH).
rewrite -(pprod_norm_coprime_prod defM) ?pcore_normal ?mmax_sol //.
by rewrite mulG_subG /= defKC sKH setIAC subsetIr.
Qed.

(* This is B & G, Corollary 12.14. We have removed the redundant assumption   *)
(* p \in \sigma(M), and restricted the quantification over P to the part of   *)
(* the conclusion where it is mentioned.                                      *)
(* Usage note: it might be more convenient to state that P is a Sylow         *)
(* subgroup of M rather than M`_\sigma; check later use.                      *)
Corollary cent_der_sigma_uniq M p X (Ms := M`_\sigma) :
    M \in 'M -> X \in 'E_p^1(M) -> (p \in \beta(M)) || (X \subset Ms^`(1)) ->
  'M('C(X)) = [set M] /\ (forall P, p.-Sylow(Ms) P -> 'M(P) = [set M]).
Proof.
move=> maxM EpX bMp_sXMs'; have p_pr := pnElem_prime EpX.
have [sXM abelX oX] := pnElemPcard EpX; have [pX _] := andP abelX.
have ntX: X :!=: 1 := nt_pnElem EpX isT; have ltCXG := mFT_cent_proper ntX.
have sMp: p \in \sigma(M).
  have [bMp | sXMs'] := orP bMp_sXMs'; first by rewrite beta_sub_sigma.
  rewrite -pnatE // -[p]oX; apply: pgroupS (subset_trans sXMs' (der_sub 1 _)) _.
  exact: pcore_pgroup.
have hallMs: \sigma(M).-Hall(M) Ms by apply: Msigma_Hall.
have sXMs: X \subset Ms by rewrite (sub_Hall_pcore hallMs) // /pgroup oX pnatE.
have [P sylP sXP]:= Sylow_superset sXMs pX.
have sylP_M: p.-Sylow(M) P := subHall_Sylow hallMs sMp sylP.
have sylP_G := sigma_Sylow_G maxM sMp sylP_M.
have [sPM pP _] := and3P sylP_M; have ltPG := mFT_pgroup_proper pP.
suffices [-> uniqP]: 'M('C(X)) = [set M] /\ 'M(P) = [set M].
  split=> // Py sylPy; have [y Ms_y ->] := Sylow_trans sylP sylPy.
  rewrite (def_uniq_mmaxJ _ uniqP) (group_inj (conjGid _)) //.
  exact: subsetP (pcore_sub _ _) y Ms_y.
have [rCPXgt2 | rCPXle2] := ltnP 2 'r_p('C_P(X)).
  have [sCPX_P sCPX_CX] := subsetIP (subxx 'C_P(X)).
  have [ltP ltCX] := (mFT_pgroup_proper pP, mFT_cent_proper ntX).
  have sCPX_M := subset_trans sCPX_P sPM.
  have ltCPX_G := sub_proper_trans sCPX_P ltPG.
  suff uniqCPX: 'M('C_P(X)) = [set M] by rewrite !(def_uniq_mmaxS _ _ uniqCPX).
  apply: (def_uniq_mmax (rank3_Uniqueness _ _)) => //.
  exact: leq_trans (p_rank_le_rank p _).
have nnP: p.-narrow P.
  apply: wlog_neg; rewrite negb_imply; case/andP=> rP _.
  by apply/narrow_centP; rewrite ?mFT_odd //; exists X.
have{bMp_sXMs'} [bM'p sXMs']: p \notin \beta(M) /\ X \subset Ms^`(1).
  move: bMp_sXMs'; rewrite !inE -negb_exists_in.
  by case: exists_inP => // [[]]; exists P.
have defMs: 'O_p^'(Ms) ><| P = Ms.
  by have [_ hallMp' _] := beta_max_pdiv maxM bM'p; apply/sdprod_Hall_p'coreP.
have{defMs} sXP': X \subset P^`(1).
  have{defMs} [_ defMs nMp'P tiMp'P] := sdprodP defMs.
  have [injMp'P imMp'P] := isomP (quotient_isom nMp'P tiMp'P).
  rewrite -(injmSK injMp'P) // morphim_der // {injMp'P}imMp'P morphim_restrm.
  rewrite (setIidPr sXP) /= -quotientMidl defMs -quotient_der ?quotientS //.
  by rewrite -defMs mul_subG ?normG.
have [rPgt2 | rPle2] := ltnP 2 'r_p(P).
  case/eqP: ntX; rewrite -(setIidPl sXP').
  by case/(narrow_cent_dprod pP (mFT_odd P)): rCPXle2.
have not_cPP: ~~ abelian P.
  by rewrite (sameP derG1P eqP) (subG1_contra sXP') ?ntX.
have sXZ: X \subset 'Z(P).
  rewrite -rank_pgroup // in rPle2.
  have := mFT_rank2_Sylow_cprod sylP_G rPle2 not_cPP.
  case=> Q [not_cQQ dimQ _] [R]; move/cyclic_abelian=> cRR [defP _].
  have [_ mulQR _] := cprodP defP; have [sQP _] := mulG_sub mulQR.
  rewrite (subset_trans sXP') // -(der_cprod 1 defP) (derG1P cRR) cprodg1.
  have{dimQ} dimQ: logn p #|Q| <= 3 by rewrite dimQ.
  have [[_ ->] _] := p3group_extraspecial (pgroupS sQP pP) not_cQQ dimQ.
  by case/cprodP: (center_cprod defP) => _ <- _; apply: mulG_subl.
have uniqP: 'M(P) = [set M].
  exact: def_uniq_mmax (nonabelian_Uniqueness pP not_cPP) maxM sPM.
rewrite (def_uniq_mmaxS _ ltCXG uniqP) //.
by rewrite centsC (subset_trans sXZ) // subsetIr.
Qed.

(* This is B & G, Proposition 12.15. *)
Proposition sigma_subgroup_embedding M q X Mstar :
    M \in 'M -> q \in \sigma(M) -> X \subset M -> q.-group X -> X :!=: 1 ->
    Mstar \in 'M('N(X)) :\ M -> 
 [/\ (*a*) gval Mstar \notin M :^: G,
           forall S, q.-Sylow(M :&: Mstar) S -> X \subset S ->
       (*b*) 'N(S) \subset M
    /\ (*c*) q.-Sylow(Mstar) S
    & if q \in \sigma(Mstar)
     (*d*) then 
     [/\ (*1*) Mstar`_\beta * (M :&: Mstar) = Mstar,
         (*2*) {subset \tau1(Mstar) <= [predU \tau1(M) & \alpha(M)]}
       & (*3*) M`_\beta = M`_\alpha /\ M`_\alpha != 1]
     (*e*) else
     [/\ (*1*) q \in \tau2(Mstar),
         (*2*) {subset [predI \pi(M) & \sigma(Mstar)] <= \beta(Mstar)}
       & (*3*) \sigma(Mstar)^'.-Hall(Mstar) (M :&: Mstar)]].
Proof.
move: Mstar => H maxM sMq sXM qX ntX /setD1P[neqHM maxNX_H].
have [q_pr _ _] := pgroup_pdiv qX ntX; have [maxH sNX_H] := setIdP maxNX_H.
have sXH := subset_trans (normG X) sNX_H.
have sX_MH: X \subset M :&: H by apply/subsetIP.
have parts_bc S:
  q.-Sylow(M :&: H) S -> X \subset S -> 'N(S) \subset M /\ q.-Sylow(H) S.
- move=> sylS sXS; have [sS_MH qS _] := and3P sylS.
  have [sSM sSH] := subsetIP sS_MH.
  have sNS_M: 'N(S) \subset M.
    have [cycS|] := boolP (cyclic S); last exact: norm_noncyclic_sigma qS _.
    have [T sylT sST] := Sylow_superset sSM qS; have [sTM qT _] := and3P sylT.
    rewrite -(nilpotent_sub_norm (pgroup_nil qT) sST).
      exact: norm_sigma_Sylow sylT.
    rewrite (sub_pHall sylS (pgroupS (subsetIl T _) qT)) //.
      by rewrite subsetI sST normG.
    by rewrite setISS // (subset_trans (char_norms _) sNX_H) // sub_cyclic_char.
  split=> //; have [T sylT sST] := Sylow_superset sSH qS.
  have [sTH qT _] := and3P sylT.
  rewrite -(nilpotent_sub_norm (pgroup_nil qT) sST) //.
  rewrite (sub_pHall sylS (pgroupS (subsetIl T _) qT)) //=.
    by rewrite subsetI sST normG.
  by rewrite /= setIC setISS.
have [S sylS sXS] := Sylow_superset sX_MH qX; have [sS_MH qS _] := and3P sylS.
have [sSM sSH] := subsetIP sS_MH; have [sNS_M sylS_H] := parts_bc S sylS sXS.
have notMGH: gval H \notin M :^: G.
  by apply: mmax_norm_notJ maxM maxH qX sXM sNX_H _; rewrite sMq eq_sym neqHM.
have /orP[sHq | t2Hq] := prime_class_mmax_norm maxH qX sNX_H; last first.
  have [/= sH'q rqH] := andP t2Hq; rewrite [q \in _](negPf sH'q); split=> //.
  have [A Eq2A] := p_rank_witness q S; have [sAS abelA dimA] := pnElemP Eq2A.
  rewrite (p_rank_Sylow sylS_H) (eqP rqH) in dimA; have [qA _] := andP abelA.
  have [sAH sAM] := (subset_trans sAS sSH, subset_trans sAS sSM).
  have [F hallF sAF] := Hall_superset (mmax_sol maxH) sAH (pi_pnat qA sH'q).
  have tiHsM: H`_\sigma :&: M = 1.
    have{Eq2A} Eq2A: A \in 'E_q^2(H) by apply/pnElemP.
    have [_ _ _ -> //] := tau2_context maxH t2Hq Eq2A.
    by rewrite 3!inE eq_sym neqHM maxM.
  have{Eq2A} Eq2A_F: A \in 'E_q^2(F) by apply/pnElemP.
  have [[nsAF _] [sCA_F _ _] _ TIsH]
    := tau2_compl_context maxH hallF t2Hq Eq2A_F.
  have sNA_M: 'N(A) \subset M.
    apply: norm_noncyclic_sigma maxM sMq qA sAM _.
    by rewrite (abelem_cyclic abelA) dimA.
  have ->: M :&: H = F.
    have [[_ <- _ _] [_ nAF]] := (sdprodP (sdprod_sigma maxH hallF), andP nsAF).
    by rewrite -(group_modr _ (subset_trans nAF sNA_M)) setIC tiHsM mul1g.
  split=> // p /andP[/= piMp sHp]; apply: wlog_neg => bH'p.
  have bM'q: q \notin \beta(M).
    by rewrite -predI_sigma_beta // inE /= sMq; case/tau2_not_beta: t2Hq.
  have sM'p: p \notin \sigma(M).
    rewrite orbit_sym in notMGH; have [_ TIsHM] := TIsH M maxM notMGH.
    by have:= TIsHM p; rewrite inE /= sHp /= => ->.
  have p'CA: p^'.-group 'C(A).
    by rewrite (pgroupS sCA_F) // (pi'_p'group (pHall_pgroup hallF)).
  have p_pr: prime p by rewrite mem_primes in piMp; case/andP: piMp.
  have [lt_pq | lt_qp | eq_pq] := ltngtP p q; last 1 first.
  - by rewrite eq_pq sMq in sM'p.
  - have bH'q: q \notin \beta(H) by apply: contra sH'q; apply: beta_sub_sigma.
    have [|[P sylP cPA] _ _] := beta'_cent_Sylow maxH bH'p bH'q qA.
      by rewrite lt_pq sAH orbT.
    have sylP_H := subHall_Sylow (Msigma_Hall maxH) sHp sylP.
    have piPp: p \in \pi(P).
      by rewrite -p_rank_gt0 (p_rank_Sylow sylP_H) p_rank_gt0 sigma_sub_pi.
    by rewrite centsC in cPA; case/eqnP: (pnatPpi (pgroupS cPA p'CA) piPp).
  have bM'p: p \notin \beta(M) by apply: contra sM'p; apply: beta_sub_sigma.
  have [P sylP] := Sylow_exists p M; have [sMP pP _] := and3P sylP.
  have [|[Q1 sylQ1 cQ1P] _ _] := beta'_cent_Sylow maxM bM'q bM'p pP.
    by rewrite lt_qp sMP orbT.
  have sylQ1_M := subHall_Sylow (Msigma_Hall maxM) sMq sylQ1.
  have [x Mx sAQ1x] := Sylow_subJ sylQ1_M sAM qA.
  have sPxCA: P :^ x \subset 'C(A) by rewrite (centsS sAQ1x) // centJ conjSg.
  have piPx_p: p \in \pi(P :^ x).
    by rewrite /= cardJg -p_rank_gt0 (p_rank_Sylow sylP) p_rank_gt0.
  by case/eqnP: (pnatPpi (pgroupS sPxCA p'CA) piPx_p).
rewrite sHq; split=> //.
have sNS_HM: 'N(S) \subset H :&: M by rewrite subsetI (norm_sigma_Sylow sHq).
have sylS_G: q.-Sylow(G) S := sigma_Sylow_G maxH sHq sylS_H.
have [defM eq_abM] := nonuniq_norm_Sylow_pprod maxM maxH neqHM sylS_G sNS_HM.
rewrite setIC eq_sym in sNS_HM neqHM defM.
have [defH eq_abH] := nonuniq_norm_Sylow_pprod maxH maxM neqHM sylS_G sNS_HM.
rewrite [M`_\alpha](eq_pcore M eq_abM) -/M`_\beta.
split=> // [r t1Hr|]; last first.
  split=> //; apply: contraNneq neqHM => Mb1.
  by rewrite -val_eqE /= (eq_mmax maxM maxH) // -defM Mb1 mul1g subsetIr.
have [R sylR] := Sylow_exists r (M :&: H); have [sR_MH rR _] := and3P sylR.
have [sRM sRH] := subsetIP sR_MH; have [sH'r rrH not_rH'] := and3P t1Hr.
have bH'r: r \notin \beta(H).
  by apply: contra sH'r; rewrite -eq_abH; apply: alpha_sub_sigma.
have sylR_H: r.-Sylow(H) R.
  rewrite pHallE sRH -defH -LagrangeMr partnM ?cardG_gt0 //.
  rewrite -(card_Hall sylR) part_p'nat ?mul1n ?(pnat_dvd (dvdn_indexg _ _)) //=.
  by rewrite (pi_p'nat (pcore_pgroup _ _)).
rewrite inE /= orbC -implyNb eq_abM; apply/implyP=> bM'r.
have sylR_M: r.-Sylow(M) R.
  rewrite pHallE sRM -defM -LagrangeMr partnM ?cardG_gt0 //.
  rewrite -(card_Hall sylR) part_p'nat ?mul1n ?(pnat_dvd (dvdn_indexg _ _)) //=.
  by rewrite (pi_p'nat (pcore_pgroup _ _)).
have rrR: 'r_r(R) = 1%N by rewrite (p_rank_Sylow sylR_H) (eqP rrH).
have piRr: r \in \pi(R) by rewrite -p_rank_gt0 rrR.
suffices not_piM'r: r \notin \pi(M^`(1)).
  rewrite inE /= -(p_rank_Sylow sylR_M) rrR /= -negb_or /=.
  apply: contra not_piM'r; case/orP=> [sMr | rM'].
    have sRMs: R \subset M`_\sigma.
      by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup rR).
    by rewrite (piSg (Msigma_der1 maxM)) // (piSg sRMs).
  by move: piRr; rewrite !mem_primes !cardG_gt0; case/andP=> ->.
have coMbR: coprime #|M`_\beta| #|R|.
  exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat rR _).
have sylRM': r.-Sylow(M^`(1)) _ := Hall_setI_normal (der_normal 1 M) sylR_M.
rewrite -p'groupEpi -partG_eq1 -(card_Hall sylRM') -trivg_card1 /=.
rewrite (pprod_focal_coprime defM (pcore_normal _ _)) //.
rewrite coprime_TIg ?(pnat_coprime rR (pgroupS (dergS 1 (subsetIr _ _)) _)) //.
by rewrite p'groupEpi mem_primes (negPf not_rH') !andbF.
Qed.

(* This is B & G, Corollary 12.16. *)
Corollary sigma_Jsub M Y :
    M \in 'M -> \sigma(M).-group Y -> Y :!=: 1 ->
  [/\ exists x, Y :^ x \subset M`_\sigma
    & forall E p H,
        \sigma(M)^'.-Hall(M) E -> p \in \pi(E) -> p \notin \beta(G) ->
        H \in 'M(Y) -> gval H \notin M :^: G ->
    [/\ (*a*) 'r_p('N_H(Y)) <= 1
      & (*b*) p \in \tau1(M) -> p \notin \pi(('N_H(Y))^`(1))]].
Proof.
move=> maxM sM_Y ntY.
have ltYG: Y \proper G.
  have ltMsG: M`_\sigma \proper G.
    exact: sub_proper_trans (pcore_sub _ _) (mmax_proper maxM).
  rewrite properEcard subsetT (leq_ltn_trans _ (proper_card ltMsG)) //.
  rewrite dvdn_leq ?cardG_gt0 // (card_Hall (Msigma_Hall_G maxM)).
  by rewrite -(part_pnat_id sM_Y) partn_dvd // cardSg ?subsetT.
have [q q_pr rFY] := rank_witness 'F(Y).
have [X [ntX qX charX]]: exists X, [/\ gval X :!=: 1, q.-group X & X \char Y].
  exists ('O_q(Y))%G; rewrite pcore_pgroup pcore_char //.
  rewrite -rank_gt0 /= -p_core_Fitting.
  rewrite (rank_Sylow (nilpotent_pcore_Hall q (Fitting_nil Y))) -rFY.
  by rewrite rank_gt0 (trivg_Fitting (mFT_sol ltYG)).
have sXY: X \subset Y := char_sub charX.
have sMq: q \in \sigma(M).
  apply: (pnatPpi (pgroupS sXY sM_Y)).
  by rewrite -p_rank_gt0 -(rank_pgroup qX) rank_gt0.
without loss sXMs: M maxM sM_Y sMq / X \subset M`_\sigma.
  move=> IH; have [Q sylQ] := Sylow_exists q M`_\sigma.
  have sQMs := pHall_sub sylQ.
  have sylQ_G := subHall_Sylow (Msigma_Hall_G maxM) sMq sylQ.
  have [x Gx sXQx] := Sylow_subJ sylQ_G (subsetT X) qX.
  have: X \subset M`_\sigma :^ x by rewrite (subset_trans sXQx) ?conjSg.
  rewrite -MsigmaJ => /IH; rewrite sigmaJ mmaxJ (eq_pgroup _ (sigmaJ _ _)).
  case => // [[y sYyMx] parts_ab].
  split=> [|E p H hallE piEp bG'p maxY_H notMGH].
    by exists (y * x^-1); rewrite conjsgM sub_conjgV -MsigmaJ.
  have:= parts_ab (E :^ x)%G p H; rewrite tau1J /= cardJg pHallJ2.
  rewrite (eq_pHall _ _ (eq_negn (sigmaJ _ _))).
  by rewrite 2!orbit_sym (orbit_eqP (mem_orbit _ _ _)) //; apply.
have pre_part_a E p H:
     \sigma(M)^'.-Hall(M) E -> p \in \pi(E) ->
  H \in 'M(Y) -> gval H \notin M :^: G -> 'r_p(H :&: M) <= 1.
- move=> hallE piEp /setIdP[maxH sYH] notMGH; rewrite leqNgt.
  apply: contra ntX => /p_rank_geP[A /pnElemP[/subsetIP[sAH sAM] abelA dimA]].
  have{abelA dimA} Ep2A: A \in 'E_p^2(M) by apply/pnElemP.
  have rpMgt1: 'r_p(M) > 1 by apply/p_rank_geP; exists A.
  have t2Mp: p \in \tau2(M).
    move: piEp; rewrite (partition_pi_sigma_compl maxM hallE) orbCA orbC.
    by rewrite -2!andb_orr orNb eqn_leq leqNgt rpMgt1 !andbF.
  have sM'p := pnatPpi (pHall_pgroup hallE) piEp.
  have [_ _ _ tiMsH _] := tau2_context maxM t2Mp Ep2A.
  rewrite -subG1 -(tiMsH H); first by rewrite subsetI sXMs (subset_trans sXY).
  by rewrite 3!inE maxH (contra_orbit _ _ notMGH).
have [sNX_M | not_sNX_M] := boolP ('N(X) \subset M).
  have sNY_M: 'N(Y) \subset M := subset_trans (char_norms charX) sNX_M.
  split=> [|E p H hallE piEp bG'p maxY_H notMGH]; last split.
  - exists 1; rewrite act1 (sub_Hall_pcore (Msigma_Hall maxM)) //.
    exact: subset_trans (normG Y) sNY_M.
  - rewrite (leq_trans (p_rankS p (setIS H sNY_M))) ?(pre_part_a E) //.
  case/and3P=> _ _; apply: contra; rewrite mem_primes => /and3P[_ _ pM'].
  by apply: dvdn_trans pM' (cardSg (dergS 1 _)); rewrite subIset ?sNY_M ?orbT.
have [L maxNX_L] := mmax_exists (mFT_norm_proper ntX (mFT_pgroup_proper qX)).
have [maxL sNX_L] := setIdP maxNX_L.
have{maxNX_L} maxNX_L: L \in 'M('N(X)) :\ M.
  by rewrite 2!inE maxNX_L andbT; apply: contraNneq not_sNX_M => <-.
have sXM := subset_trans sXMs (pcore_sub _ M).
have [notMGL _ embedL] := sigma_subgroup_embedding maxM sMq sXM qX ntX maxNX_L.
pose K := (if q \in \sigma(L) then L`_\beta else L`_\sigma)%G.
have sM'K: \sigma(M)^'.-group K.
  rewrite orbit_sym in notMGL.
  rewrite /K; case: (boolP (q \in _)) embedL => [sLq _ | sL'q [t2Lq _ _]].
    have [_ TIaLsM _] := sigma_disjoint maxL maxM notMGL.
    apply: sub_pgroup (pcore_pgroup _ _) => p bLp.
    by apply: contraFN (TIaLsM p) => /= sMp; rewrite inE /= beta_sub_alpha.
  have [F hallF] := ex_sigma_compl maxL.
  have [A Ep2A _] := ex_tau2Elem hallF t2Lq.
  have [_ _ _ TIsLs] := tau2_compl_context maxL hallF t2Lq Ep2A.
  have{TIsLs} [_ TIsLsM] := TIsLs M maxM notMGL.
  apply: sub_pgroup (pcore_pgroup _ _) => p sLp.
  by apply: contraFN (TIsLsM p) => /= sMp; rewrite inE /= sLp.
have defL: K * (M :&: L) = L.
  rewrite /K; case: (q \in _) embedL => [] [] // _ _.
  by move/(sdprod_Hall_pcoreP (Msigma_Hall maxL)); case/sdprodP.
have sYL := subset_trans (char_norm charX) sNX_L.
have [x sYxMs]: exists x, Y :^ x \subset M`_\sigma.
  have solML := solvableS (subsetIl M L) (mmax_sol maxM).
  have [H hallH] := Hall_exists \sigma(M) solML.
  have [sHM sHL] := subsetIP (pHall_sub hallH).
  have hallH_L: \sigma(M).-Hall(L) H.
    rewrite pHallE sHL -defL -LagrangeMr partnM ?cardG_gt0 //.
    rewrite -(card_Hall hallH) part_p'nat ?mul1n //=.
    exact: pnat_dvd (dvdn_indexg _ _) sM'K.
  have [x _ sYxH]:= Hall_Jsub (mmax_sol maxL) hallH_L sYL sM_Y.
  exists x; rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?pgroupJ //.
  exact: subset_trans sYxH sHM.
split=> [|E p H hallE piEp bG'p maxY_H notMGH]; first by exists x.
have p'K: p^'.-group K.
  have bL'p: p \notin \beta(L).
    by rewrite -predI_sigma_beta // negb_and bG'p orbT.
  rewrite /K; case: (q \in _) embedL => [_ | [_ bLp _]].
    by rewrite (pi_p'group (pcore_pgroup _ _)).
  rewrite (pi_p'group (pcore_pgroup _ _)) //; apply: contra bL'p => /= sLp.
  by rewrite bLp // inE /= (piSg (pHall_sub hallE)).
have sNHY_L: 'N_H(Y) \subset L.
  by rewrite subIset ?(subset_trans (char_norms charX)) ?orbT.
rewrite (leq_trans (p_rankS p sNHY_L)); last first.
  have [P sylP] := Sylow_exists p (M :&: L).
  have [_ sPL] := subsetIP (pHall_sub sylP).
  have{sPL} sylP_L: p.-Sylow(L) P.
    rewrite pHallE sPL -defL -LagrangeMr partnM ?cardG_gt0 //.
    rewrite -(card_Hall sylP) part_p'nat ?mul1n //=.
    exact: pnat_dvd (dvdn_indexg _ _) p'K.
  rewrite -(p_rank_Sylow sylP_L) {P sylP sylP_L}(p_rank_Sylow sylP).
  by rewrite /= setIC (pre_part_a E) // inE maxL.
split=> // t1Mp; rewrite (contra ((piSg (dergS 1 sNHY_L)) p)) // -p'groupEpi.
have nsKL: K <| L by rewrite /K; case: ifP => _; apply: pcore_normal.
have [sKL nKL] := andP nsKL; have nKML := subset_trans (subsetIr M L) nKL.
suffices: p^'.-group (K * (M :&: L)^`(1)).
  rewrite -norm_joinEr ?gFsub_trans //; apply: pgroupS => /=.
  rewrite norm_joinEr -?quotientSK ?gFsub_trans //= !quotient_der //.
  by rewrite -[in L / K]defL quotientMidl.
rewrite pgroupM p'K (pgroupS (dergS 1 (subsetIl M L))) // p'groupEpi.
by rewrite mem_primes andbA andbC negb_and; case/and3P: t1Mp => _ _ ->.
Qed.

(* This is B & G, Lemma 12.17. *)
Lemma sigma_compl_embedding M E (Ms := M`_\sigma) :
    M \in 'M -> \sigma(M)^'.-Hall(M) E ->
 [/\ 'C_Ms(E) \subset Ms^`(1), [~: Ms, E] = Ms
   & forall g (MsMg := Ms :&: M :^ g), g \notin M ->
     [/\ cyclic MsMg, \beta(M)^'.-group MsMg & MsMg :&: Ms^`(1) = 1]].
Proof.
move=> maxM hallE; have [sEM s'E _] := and3P hallE.
have solMs: solvable Ms := solvableS (pcore_sub _ _) (mmax_sol maxM).
have defM := coprime_der1_sdprod (sdprod_sigma maxM hallE).
have{s'E} coMsE: coprime #|Ms| #|E| := pnat_coprime (pcore_pgroup _ _) s'E.
have{defM coMsE} [-> ->] := defM coMsE solMs (Msigma_der1 maxM).
split=> // g MsMg notMg.
have sMsMg: \sigma(M).-group MsMg := pgroupS (subsetIl _ _) (pcore_pgroup _ _).
have EpMsMg p n X: X \in 'E_p^n(MsMg) -> n > 0 ->
  n = 1%N /\ ~~ ((p \in \beta(M)) || (X \subset Ms^`(1))).
- move=> EpX n_gt0; have [sXMsMg abelX dimX] := pnElemP EpX.
  have [[sXMs sXMg] [pX _]] := (subsetIP sXMsMg, andP abelX).
  have sXM := subset_trans sXMs (pcore_sub _ _).
  have piXp: p \in \pi(X) by rewrite -p_rank_gt0 p_rank_abelem ?dimX.
  have sMp: p \in \sigma(M) := pnatPpi (pgroupS sXMs (pcore_pgroup _ _)) piXp.
  have not_sCX_M: ~~ ('C(X) \subset M).
    apply: contra notMg => sCX_M; rewrite -groupV.
    have [transCX _ _] := sigma_group_trans maxM sMp pX.
    have [|c CXc [m Mm ->]] := transCX g^-1 sXM; rewrite ?sub_conjgV //.
    by rewrite groupM // (subsetP sCX_M).
  have cycX: cyclic X.
    apply: contraR not_sCX_M => ncycX; apply: subset_trans (cent_sub _) _.
    exact: norm_noncyclic_sigma maxM sMp pX sXM ncycX.
  have n1: n = 1%N by apply/eqP; rewrite eqn_leq -{1}dimX -abelem_cyclic ?cycX.
  rewrite n1 in dimX *; split=> //; apply: contra not_sCX_M.
  by case/cent_der_sigma_uniq=> //; [apply/pnElemP | case/mem_uniq_mmax].
have tiMsMg_Ms': MsMg :&: Ms^`(1) = 1.
  apply/eqP/idPn; rewrite -rank_gt0 => /rank_geP[X /nElemP[p]].
  case/pnElemP=> /subsetIP[sXMsMg sXMs'] abelX dimX.
  by case: (EpMsMg p 1%N X) => //; [apply/pnElemP | rewrite sXMs' orbT].
split=> //; last first.
  apply: sub_in_pnat sMsMg => p.
  by rewrite -p_rank_gt0 => /p_rank_geP[X /EpMsMg[] // _ /norP[]].
rewrite abelian_rank1_cyclic.
  by rewrite leqNgt; apply/rank_geP=> [[X /nElemP[p /EpMsMg[]]]].
by rewrite (sameP derG1P trivgP) -tiMsMg_Ms' subsetI der_sub dergS ?subsetIl.
Qed.

(* This is B & G, Lemma 12.18. *)
(* We corrected an omission in the text, which fails to quote Lemma 10.3 to   *)
(* justify the two p-rank inequalities (12.5) and (12.6), and indeed          *)
(* erroneously refers to 12.2(a) for (12.5). Note also that the loosely       *)
(* justified equalities of Ohm_1 subgroups are in fact unnecessary.           *)
Lemma cent_Malpha_reg_tau1 M p q P Q (Ma := M`_\alpha) :
    M \in 'M -> p \in \tau1(M) -> q \in p^' -> P \in 'E_p^1(M) -> Q :!=: 1 ->
    P \subset 'N(Q) -> 'C_Q(P) = 1 -> 'M('N(Q)) != [set M] ->
  [/\ (*a*) Ma != 1 -> q \notin \alpha(M) -> q.-group Q -> Q \subset M ->
            'C_Ma(P) != 1 /\ 'C_Ma(Q <*> P) = 1
    & (*b*) q.-Sylow(M) Q ->
            [/\ \alpha(M) =i \beta(M), Ma != 1, q \notin \alpha(M),
                'C_Ma(P) != 1 & 'C_Ma(Q <*> P) = 1]].
Proof.
move=> maxM t1p p'q EpP ntQ nQP regPQ nonuniqNQ.
set QP := Q <*> P; set CaQP := 'C_Ma(QP); set part_a := _ -> _.
have ssolM := solvableS _ (mmax_sol maxM).
have [sPM abelP oP] := pnElemPcard EpP; have{abelP} [pP _] := andP abelP.
have p_pr := pnElem_prime EpP; have [s'p _] := andP t1p.
have a'p: p \in \alpha(M)^' by apply: contra s'p; apply: alpha_sub_sigma.
have{a'p} [a'P t2'p] := (pi_pgroup pP a'p, tau2'1 t1p).
have uniqCMX: 'M('C_M(_)) = [set M] := def_uniq_mmax _ maxM (subsetIl _ _).
have nQ_CMQ: 'C_M(Q) \subset 'N(Q) by rewrite setIC subIset ?cent_sub.
have part_a_holds: part_a.
  move=> ntMa a'q qQ sQM; have{p'q} p'Q := pi_pgroup qQ p'q.
  have{p'Q} coQP: coprime #|Q| #|P| by rewrite coprime_sym (pnat_coprime pP).
  have{a'q} a'Q: \alpha(M)^'.-group Q by rewrite (pi_pgroup qQ).
  have rCMaQle1: 'r('C_Ma(Q)) <= 1.
    rewrite leqNgt; apply: contra nonuniqNQ => rCMaQgt1; apply/eqP.
    apply: def_uniq_mmaxS (uniqCMX Q _) => //; last exact: cent_alpha'_uniq.
    exact: mFT_norm_proper (mFT_pgroup_proper qQ).
  have rCMaPle1: 'r('C_Ma(P)) <= 1.
    have: ~~ ('N(P) \subset M).
      by apply: contra (prime_class_mmax_norm maxM pP) _; apply/norP.
    rewrite leqNgt; apply: contra => rCMaPgt1.
    apply: (sub_uniq_mmax (uniqCMX P _)); first exact: cent_alpha'_uniq.
      by rewrite /= setIC subIset ?cent_sub.
    exact: mFT_norm_proper (nt_pnElem EpP _) (mFT_pgroup_proper pP).
  have [sMaM nMaM] := andP (pcore_normal _ M : Ma <| M).
  have aMa: \alpha(M).-group Ma by rewrite pcore_pgroup.
  have nMaQP: QP \subset 'N(Ma) by rewrite join_subG !(subset_trans _ nMaM).
  have{nMaM} coMaQP: coprime #|Ma| #|QP|.
    by rewrite (pnat_coprime aMa) ?[QP]norm_joinEr // [pnat _ _]pgroupM ?a'Q.
  pose r := pdiv #|if CaQP == 1 then Ma else CaQP|.
  have{ntMa} piMar: r \in \pi(Ma).
    rewrite /r; case: ifPn => [_| ntCaQP]; first by rewrite pi_pdiv cardG_gt1.
    by rewrite (piSg (subsetIl Ma 'C(QP))) // pi_pdiv cardG_gt1.
  have{aMa} a_r: r \in \alpha(M) := pnatPpi aMa piMar.
  have [r'Q r'P] : r^'.-group Q /\ r^'.-group P by rewrite !(pi'_p'group _ a_r).
  have [Rc /= sylRc] := Sylow_exists r [group of CaQP].
  have [sRcCaQP rRc _] := and3P sylRc; have [sRcMa cQPRc] := subsetIP sRcCaQP.
  have nRcQP: QP \subset 'N(Rc) by rewrite cents_norm // centsC.
  have{nMaQP rRc coMaQP sRcCaQP sRcMa nRcQP} [R [sylR nR_QP sRcR]] :=
    coprime_Hall_subset nMaQP coMaQP (ssolM _ sMaM) sRcMa rRc nRcQP.
  have{nR_QP} [[sRMa rR _] [nRQ nRP]] := (and3P sylR, joing_subP nR_QP).
  have{piMar} ntR: R :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylR) p_rank_gt0.
  have [r_pr _ _] := pgroup_pdiv rR ntR.
  have sylR_M := subHall_Sylow (Malpha_Hall maxM) a_r sylR.
  have{rCMaQle1 a_r} not_cRQ: ~~ (Q \subset 'C(R)).
    apply: contraL rCMaQle1; rewrite centsC => cQR; rewrite -ltnNge ltnW //.
    by rewrite (leq_trans a_r) // -(rank_Sylow sylR_M) rankS // subsetI sRMa.
  have [R1 [charR1 _ _ expR1 rCR1_AutR]] := critical_odd rR (mFT_odd R) ntR.
  have [sR1R nR1R] := andP (char_normal charR1); have rR1 := pgroupS sR1R rR.
  have [nR1P nR1Q] := (char_norm_trans charR1 nRP, char_norm_trans charR1 nRQ).
  have [coR1Q coR1P] := (pnat_coprime rR1 r'Q, pnat_coprime rR1 r'P).
  have {rCR1_AutR not_cRQ} not_cR1Q: ~~ (Q \subset 'C(R1)).
    apply: contra not_cRQ => cR1Q; rewrite -subsetIidl.
    rewrite -quotient_sub1 ?normsI ?normG ?norms_cent // subG1 trivg_card1.
    rewrite (pnat_1 _ (quotient_pgroup _ r'Q)) //= -ker_conj_aut.
    rewrite (card_isog (first_isog_loc _ _)) //; apply: pgroupS rCR1_AutR.
    apply/subsetP=> za; case/morphimP=> z nRz Qz ->; rewrite inE Aut_aut inE.
    apply/subsetP=> x R1x; rewrite inE [_ x _]norm_conj_autE ?(subsetP sR1R) //.
    by rewrite /conjg -(centsP cR1Q z) ?mulKg.
  pose R0 := 'C_R1(Q); have sR0R1: R0 \subset R1 := subsetIl R1 'C(Q).
  have nR0P: P \subset 'N(R0) by rewrite normsI ?norms_cent.
  have nR0Q: Q \subset 'N(R0) by rewrite normsI ?norms_cent ?normG.
  pose R1Q := R1 <*> Q; have defR1Q: R1 * Q = R1Q by rewrite -norm_joinEr.
  have [[sR1_R1Q sQ_R1Q] tiR1Q] := (joing_sub (erefl R1Q), coprime_TIg coR1Q).
  have not_nilR1Q: ~~ nilpotent R1Q.
    by apply: contra not_cR1Q => /sub_nilpotent_cent2; apply.
  have not_nilR1Qb: ~~ nilpotent (R1Q / R0).
    apply: contra not_cR1Q => nilR1Qb.
    have [nilR1 solR1] := (pgroup_nil rR1, pgroup_sol rR1).
    rewrite centsC -subsetIidl -(nilpotent_sub_norm nilR1 sR0R1) //= -/R0.
    rewrite -(quotientSGK (subsetIr R1 _)) ?coprime_quotient_cent  //= -/R0.
    rewrite quotientInorm subsetIidl /= centsC -/R0.
    by rewrite (sub_nilpotent_cent2 nilR1Qb) ?quotientS ?coprime_morph.
  have coR1QP: coprime #|R1Q| #|P|.
    by rewrite -defR1Q TI_cardMg // coprime_mull coR1P.
  have defR1QP: R1Q ><| P = R1Q <*> P.
    by rewrite sdprodEY ?normsY ?coprime_TIg.
  have sR1Ma := subset_trans sR1R sRMa; have sR1M := subset_trans sR1Ma sMaM.
  have solR1Q: solvable R1Q by rewrite ssolM // !join_subG sR1M.
  have solR1QP: solvable (R1Q <*> P) by rewrite ssolM // !join_subG sR1M sQM.
  have defCR1QP: 'C_R1Q(P) = 'C_R1(P).
    by rewrite -defR1Q -subcent_TImulg ?regPQ ?mulg1 //; apply/subsetIP.
  have ntCR1P: 'C_R1(P) != 1.
    apply: contraNneq not_nilR1Q => regPR1.
    by rewrite (prime_Frobenius_sol_kernel_nil defR1QP) ?oP ?defCR1QP.
  split; first exact: subG1_contra (setSI _ sR1Ma) ntCR1P.
  have{rCMaPle1} cycCRP: cyclic 'C_R(P).
    have rCRP: r.-group 'C_R(P) := pgroupS (subsetIl R _) rR.
    rewrite (odd_pgroup_rank1_cyclic rCRP) ?mFT_odd -?rank_pgroup {rCRP}//.
    by rewrite (leq_trans (rankS _) rCMaPle1) ?setSI.
  have{ntCR1P} oCR1P: #|'C_R1(P)| = r.
    have cycCR1P: cyclic 'C_R1(P) by rewrite (cyclicS _ cycCRP) ?setSI.
    apply: cyclic_abelem_prime ntCR1P => //.
    by rewrite abelemE ?cyclic_abelian // -expR1 exponentS ?subsetIl.
  apply: contraNeq not_nilR1Qb => ntCaQP.
  have{Rc sRcR sylRc cQPRc ntCaQP} ntCRQP: 'C_R(QP) != 1.
    suffices: Rc :!=: 1 by apply: subG1_contra; apply/subsetIP.
    rewrite -rank_gt0 (rank_Sylow sylRc) p_rank_gt0.
    by rewrite /r (negPf ntCaQP) pi_pdiv cardG_gt1.
  have defR1QPb: (R1Q / R0) ><| (P / R0) = R1Q <*> P / R0.
    have [_ <- nR1QP _] := sdprodP defR1QP; rewrite quotientMr //.
    by rewrite sdprodE ?quotient_norms // coprime_TIg ?coprime_morph.
  have tiPR0: R0 :&: P = 1 by rewrite coprime_TIg // (coprimeSg sR0R1).
  have prPb: prime #|P / R0| by rewrite -(card_isog (quotient_isog _ _)) ?oP.
  rewrite (prime_Frobenius_sol_kernel_nil defR1QPb) ?quotient_sol //.
  rewrite -coprime_quotient_cent ?(subset_trans sR0R1) // quotientS1 //=.
  rewrite defCR1QP -{2}(setIidPl sR1R) -setIA subsetI subsetIl.
  apply: subset_trans (setIS R (centS (joing_subl Q P))).
  rewrite -(cardSg_cyclic cycCRP) ?setIS ?setSI ?centS ?joing_subr // oCR1P.
  by have [_ -> _] := pgroup_pdiv (pgroupS (subsetIl R _) rR) ntCRQP.
split=> // sylQ; have [sQM qQ _] := and3P sylQ.
have ltQG := mFT_pgroup_proper qQ; have ltNQG := mFT_norm_proper ntQ ltQG.
have{p'q} p'Q := pi_pgroup qQ p'q.
have{p'Q} coQP: coprime #|Q| #|P| by rewrite coprime_sym (pnat_coprime pP).
have sQM': Q \subset M^`(1).
  by rewrite -(coprime_cent_prod nQP) ?ssolM // regPQ mulg1 commgSS.
have ntMa: Ma != 1.
  apply: contraNneq nonuniqNQ => Ma1.
  rewrite (mmax_normal maxM _ ntQ) ?mmax_sup_id //.
  have sylQ_M': q.-Sylow(M^`(1)) Q := pHall_subl sQM' (der_sub 1 M) sylQ.
  rewrite (nilpotent_Hall_pcore _ sylQ_M') ?gFnormal_trans //.
  by rewrite (isog_nil (quotient1_isog _)) -Ma1 Malpha_quo_nil.
have a'q: q \notin \alpha(M).
  apply: contra nonuniqNQ => a_q.
  have uniqQ: Q \in 'U by rewrite rank3_Uniqueness ?(rank_Sylow sylQ).
  by rewrite (def_uniq_mmaxS _ _ (def_uniq_mmax _ _ sQM)) ?normG.
have b'q := contra (@beta_sub_alpha _ M _) a'q.
case: part_a_holds => // ntCaP regQP; split=> {ntCaP regQP}// r.
apply/idP/idP=> [a_r | ]; last exact: beta_sub_alpha.
apply: contraR nonuniqNQ => b'r; apply/eqP.
apply: def_uniq_mmaxS (uniqCMX Q _) => //.
have q'r: r != q by apply: contraNneq a'q => <-.
by have [|_ -> //] := beta'_cent_Sylow maxM b'r b'q qQ; rewrite q'r sQM'.
Qed.

(* This is B & G, Lemma 12.19. *)
(* We have used lemmas 10.8(b) and 10.2(c) rather than 10.9(a) as suggested   *)
(* in the text; this avoids a quantifier inversion!                           *)
Lemma der_compl_cent_beta' M E :
    M \in 'M -> \sigma(M)^'.-Hall(M) E -> 
  exists2 H : {group gT}, \beta(M)^'.-Hall(M`_\sigma) H & E^`(1) \subset 'C(H).
Proof.
move=> maxM hallE; have [sEM s'E _] := and3P hallE.
have s'E': \sigma(M)^'.-group E^`(1) := pgroupS (der_sub 1 E) s'E.
have b'E': \beta(M)^'.-group E^`(1).
  by apply: sub_pgroup s'E' => p; apply: contra; apply: beta_sub_sigma.
have solM': solvable M^`(1) := solvableS (der_sub 1 M) (mmax_sol maxM).
have [K hallK sE'K] := Hall_superset solM' (dergS 1 sEM) b'E'.
exists (K :&: M`_\sigma)%G.
  apply: Hall_setI_normal hallK.
  exact: normalS (Msigma_der1 maxM) (der_sub 1 M) (pcore_normal _ M).
have nilK: nilpotent K.
  by have [sKM' b'K _] := and3P hallK; apply: beta'_der1_nil sKM'.
rewrite (sub_nilpotent_cent2 nilK) ?subsetIl ?(coprimeSg (subsetIr _ _)) //.
exact: pnat_coprime (pcore_pgroup _ _) s'E'.
Qed.

End Section12.

Implicit Arguments tau2'1 [[gT] [M] x].
Implicit Arguments tau3'1 [[gT] [M] x].
Implicit Arguments tau3'2 [[gT] [M] x].