proposition: 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: 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.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)