proposition: Proposition chief_stab_sub_Fitting : H' \subset 'F(G').
proof: Proof. without loss: / {K | [min K | K <| G & ~~ (K \subset 'F(G'))] & K \subset H'}. move=> IH; apply: wlog_neg => s'H'F; apply/IH/mingroup_exists=> {IH}/=. rewrite /normal subIset ?sG'G ?normsI ?norms_bigcap {s'H'F}//. apply/bigcapsP=> /= U /andP[/and3P[/maxgroupp/andP/=[_ nU2G] _ nU1G] _]. exact: subset_trans (actsQ nU2G nU1G) (astab_norm 'Q (U.1 / U.2)). case=> K /mingroupP[/andP[nsKG s'KF] minK] /subsetIP[sKG' nFK]. have [[Ks chiefKs defK] sKG]:= (chief_series_exists nsKG, normal_sub nsKG). suffices{nsKG s'KF} cKsK: (K.-central).-series 1%G Ks. by rewrite Fitting_max ?(normalS _ sG'G) ?(centrals_nil cKsK) in s'KF. move: chiefKs; rewrite -!(rev_path _ _ Ks) {}defK. case: {Ks}(rev _) => //= K1 Kr /andP[chiefK1 chiefKr]. have [/maxgroupp/andP[/andP[sK1K ltK1K] nK1G] _] := andP chiefK1. suffices{chiefK1} cKrK: [rel U V | central_factor K V U].-series K1 Kr. have cKK1: abelian (K / K1) := abelem_abelian (sol_chief_abelem solG chiefK1). by rewrite /central_factor subxx sK1K der1_min //= (subset_trans sKG). have{minK ltK1K nK1G} sK1F: K1 \subset 'F(G'). have nsK1G: K1 <| G by rewrite /normal (subset_trans sK1K). by apply: contraR ltK1K => s'K1F; rewrite (minK K1) ?nsK1G. elim: Kr K1 chiefKr => //= K2 Kr IHr K1 /andP[chiefK2 chiefKr] in sK1F sK1K *. have [/maxgroupp/andP[/andP[sK21 _] /(subset_trans sKG)nK2K] _] := andP chiefK2. rewrite /central_factor sK1K {}IHr ?(subset_trans sK21) {chiefKr}// !andbT. rewrite commGC -sub_astabQR ?(subset_trans _ nK2K) //. exact/(subset_trans nFK)/(bigcap_inf (K1, K2))/andP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)