proposition: Lemma charsimple_dprod G : charsimple G -> exists H : {group gT}, [/\ H \subset G, simple H & exists2 I : {set {perm gT}}, I \subset Aut G & \big[dprod/1]_(f in I) f @: H = G].
proof: Proof. case/charsimpleP=> ntG simG. have [H minH sHG]: {H : {group gT} | minnormal H G & H \subset G}. by apply: mingroup_exists; rewrite ntG normG. case/mingroupP: minH => /andP[ntH nHG] minH. pose Iok (I : {set {perm gT}}) := (I \subset Aut G) && [exists (M : {group gT} | M <| G), \big[dprod/1]_(f in I) f @: H == M]. have defH: (1 : {perm gT}) @: H = H. apply/eqP; rewrite eqEcard card_imset ?leqnn; last exact: perm_inj. by rewrite andbT; apply/subsetP=> _ /imsetP[x Hx ->]; rewrite perm1. have [|I] := @maxset_exists _ Iok 1. rewrite /Iok sub1G; apply/existsP; exists H. by rewrite /normal sHG nHG (big_pred1 1) => [|f]; rewrite ?defH /= ?inE. case/maxsetP=> /andP[Aut_I /exists_eq_inP[M /andP[sMG nMG] defM]] maxI. rewrite sub1set=> ntI; case/eqVproper: sMG => [defG | /andP[sMG not_sGM]]. exists H; split=> //; last by exists I; rewrite ?defM. apply/mingroupP; rewrite ntH normG; split=> // N /andP[ntN nNH] sNH. apply: minH => //; rewrite ntN /= -defG. move: defM; rewrite (bigD1 1) //= defH; case/dprodP=> [[_ K _ ->] <- cHK _]. by rewrite mul_subG // cents_norm // (subset_trans cHK) ?centS. have defG: <<\bigcup_(f in Aut G) f @: H>> = G. have sXG: \bigcup_(f in Aut G) f @: H \subset G. by apply/bigcupsP=> f Af; rewrite -(im_autm Af) morphimEdom imsetS. apply: simG. apply: contra ntH; rewrite -!subG1; apply: subset_trans. by rewrite sub_gen // (bigcup_max 1) ?group1 ?defH. rewrite /characteristic gen_subG sXG; apply/forall_inP=> f Af. rewrite -(autmE Af) -morphimEsub ?gen_subG ?morphim_gen // genS //. rewrite morphimEsub //= autmE. apply/subsetP=> _ /imsetP[_ /bigcupP[g Ag /imsetP[x Hx ->]] ->]. apply/bigcupP; exists (g * f); first exact: groupM. by apply/imsetP; exists x; rewrite // permM. have [f Af sfHM]: exists2 f, f \in Aut G & ~~ (f @: H \subset M). move: not_sGM; rewrite -{1}defG gen_subG; case/subsetPn=> x. by case/bigcupP=> f Af fHx Mx; exists f => //; apply/subsetPn; exists x. case If: (f \in I). by case/negP: sfHM; rewrite -(bigdprodWY defM) sub_gen // (bigcup_max f). case/idP: (If); rewrite -(maxI ([set f] :|: I)) ?subsetUr ?inE ?eqxx //. rewrite {maxI}/Iok subUset sub1set Af {}Aut_I; apply/existsP. have sfHG: autm Af @* H \subset G by rewrite -{4}(im_autm Af) morphimS. have{minH nHG} /mingroupP[/andP[ntfH nfHG] minfH]: minnormal (autm Af @* H) G. apply/mingroupP; rewrite andbC -{1}(im_autm Af) morphim_norms //=. rewrite -subG1 sub_morphim_pre // -kerE ker_autm subG1. split=> // N /andP[ntN nNG] sNfH. have sNG: N \subset G := subset_trans sNfH sfHG. apply/eqP; rewrite eqEsubset sNfH sub_morphim_pre //=. rewrite -(morphim_invmE (injm_autm Af)) [_ @* N]minH //=. rewrite -subG1 sub_morphim_pre /= ?im_autm // morphpre_invm morphim1 subG1. by rewrite ntN -{1}(im_invm (injm_autm Af)) /= {2}im_autm morphim_norms. by rewrite sub_morphim_pre /= ?im_autm // morphpre_invm. have{minfH sfHM} tifHM: autm Af @* H :&: M = 1. apply/eqP/idPn=> ntMfH; case/setIidPl: sfHM. rewrite -(autmE Af) -morphimEsub //. by apply: minfH; rewrite ?subsetIl // ntMfH normsI. have cfHM: M \subset 'C(autm Af @* H). rewrite centsC (sameP commG1P trivgP) -tifHM subsetI commg_subl commg_subr. by rewrite (subset_trans sMG) // (subset_trans sfHG). exists (autm Af @* H <*> M)%G; rewrite /normal /= join_subG sMG sfHG normsY //=. rewrite (bigD1 f) ?inE ?eqxx // (eq_bigl [in I]) /= => [|g]; last first. by rewrite /= !inE andbC; case: eqP => // ->. by rewrite defM -(autmE Af) -morphimEsub // dprodE // cent_joinEr ?eqxx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)