proposition: Theorem rank2_min_p'core_Hall gT (G : {group gT}) (p := pdiv #|G|) : odd #|G| -> solvable G -> 'r('F(G)) <= 2 -> p^'.-Hall(G) 'O_p^'(G).
proof: Proof. set F := 'F(G) => oddG solG Fle2. have nsFG: F <| G := Fitting_normal G; have [sFG nFG] := andP nsFG. have [H] := inv_quotientN nsFG (pcore_normal p^' _). rewrite /= -/F => defH sFH nsHG; have [sHG nHG] := andP nsHG. have [P sylP] := Sylow_exists p H; have [sPH pP _] := and3P sylP. have sPF: P \subset F. rewrite -quotient_sub1 ?(subset_trans (subset_trans sPH sHG)) //. rewrite -(setIidPl (quotientS _ sPH)) -defH coprime_TIg //. by rewrite coprime_morphl // (pnat_coprime pP (pcore_pgroup _ _)). have nilGq: nilpotent (G / F). by rewrite abelian_nil ?sub_der1_abelian ?rank2_der1_sub_Fitting. have pGq: p.-group (G / H). rewrite /pgroup -(card_isog (third_isog sFH nsFG nsHG)) /= -/F -/(pgroup _ _). rewrite -(dprodW (nilpotent_pcoreC p nilGq)) defH quotientMidr. by rewrite quotient_pgroup ?pcore_pgroup. rewrite pHallE pcore_sub -(Lagrange sHG) partnM // -card_quotient //=. have hallHp': p^'.-Hall(H) 'O_p^'(H). case p'H: (p^'.-group H). by rewrite pHallE /= pcore_pgroup_id ?subxx //= part_pnat_id. have def_p: p = pdiv #|H|. have [p_pr pH]: prime p /\ p %| #|H|. apply/andP; apply: contraFT p'H => p'H; apply/pgroupP=> q q_pr qH. by apply: contraNneq p'H => <-; rewrite q_pr qH. apply/eqP; rewrite eqn_leq ?pdiv_min_dvd ?prime_gt1 //. rewrite pdiv_prime // cardG_gt1. by case: eqP p'H => // ->; rewrite pgroup1. exact: dvdn_trans (pdiv_dvd _) (cardSg (normal_sub nsHG)). rewrite def_p rank2_min_p_complement ?(oddSg sHG) ?(solvableS sHG) -?def_p //. rewrite -(p_rank_Sylow sylP) (leq_trans (p_rank_le_rank _ _)) //. exact: leq_trans (rankS sPF) Fle2. rewrite -(card_Hall hallHp') part_p'nat ?pnatNK ?muln1 // subset_leqif_card. by rewrite pcore_max ?pcore_pgroup ?gFnormal_trans. rewrite pcore_max ?pcore_pgroup // (normalS _ _ (pcore_normal _ _)) //. rewrite -quotient_sub1 ?gFsub_trans //. rewrite -(setIidPr (quotientS _ (pcore_sub _ _))) coprime_TIg //. by rewrite coprime_morphr // (pnat_coprime pGq (pcore_pgroup _ _)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)