proposition: Theorem not_all_FTtype1 : ~~ all_FTtype1 gT.
proof: Proof. apply/negP=> allT1; pose k := #|'M^G|. have [partGpi coA1 _ [injA1 /(_ allT1)partG _]] := FT_Dade_support_partition gT. move/forall_inP in allT1. have [/subsetP maxMG _ injMG exMG] := mmax_transversalP gT. have{partGpi exMG} kge2: (k >= 2)%N. have [L MG_L]: exists L, L \in 'M^G. by have [L maxL] := any_mmax gT; have [x] := exMG L maxL; exists (L :^ x)%G. have maxL := maxMG L MG_L; have Ltype1 := allT1 L maxL. have /Frobenius_kerP[_ ltHL nsHL _] := FTtype1_Frobenius maxL Ltype1. rewrite ltnNge; apply: contra (proper_subn ltHL) => leK1. rewrite (sub_normal_Hall (Fcore_Hall L)) // (pgroupS (subsetT L)) //=. apply: sub_pgroup (pgroup_pi _) => p; rewrite partGpi => /exists_inP[M maxM]. have /eqP defMG: [set L] == 'M^G by rewrite eqEcard sub1set MG_L cards1. have [x] := exMG M maxM; rewrite -defMG => /set1P/(canRL (actK 'JG _))-> /=. by rewrite FTcoreJ cardJg FTcore_type1. pose L (i : 'I_k) : {group gT} := enum_val i; pose H i := (L i)`_\F%G. have MG_L i: L i \in 'M^G by apply: enum_valP. have maxL i: L i \in 'M by apply: maxMG. have defH i: (L i)`_\s = H i by rewrite FTcore_type1 ?allT1. pose frobL_P i E := [Frobenius L i = H i ><| gval E]. have /fin_all_exists[E frobHE] i: exists E, frobL_P i E. by apply/existsP/FTtype1_Frobenius; rewrite ?allT1. have frobL i: [/\ L i \subset G, solvable (L i) & frobL_P i (E i)]. by rewrite subsetT mmax_sol. have{coA1} coH_ i j: i != j -> coprime #|H i| #|H j|. move=> j'i; rewrite -!defH coA1 //; apply: contra j'i => /imsetP[x Gx defLj]. apply/eqP/enum_val_inj; rewrite -/(L i) -/(L j); apply: injMG => //. by rewrite defLj; apply/esym/orbit_act. have tiH i: normedTI (H i)^# G (L i). have ntA: (H i)^# != set0 by rewrite setD_eq0 subG1 mmax_Fcore_neq1. apply/normedTI_memJ_P=> //=; rewrite subsetT; split=> // x z H1x Gz. apply/idP/idP=> [H1xz | Lz]; last first. by rewrite memJ_norm // (subsetP _ z Lz) // normD1 gFnorm. have /subsetP sH1A0: (H i)^# \subset 'A0(L i) by apply: Fcore_sub_FTsupp0. have [/(sub_in2 sH1A0)wccH1 [_ maxN] Nfacts] := FTsupport_facts (maxL i). suffices{z Gz H1xz wccH1} sCxLi: 'C[x] \subset L i. have /imsetP[y Ly defxz] := wccH1 _ _ H1x H1xz (imset_f _ Gz). rewrite -[z](mulgKV y) groupMr // (subsetP sCxLi) // !inE conjg_set1. by rewrite conjgM defxz conjgK. apply/idPn=> not_sCxM; pose D := [set y in 'A0(L i) | ~~ ('C[y] \subset L i)]. have Dx: x \in D by rewrite inE sH1A0. have{maxN} /mem_uniq_mmax[maxN sCxN] := maxN x Dx. have Ntype1 := allT1 _ maxN. have [_ _ /setDP[/bigcupP[y NFy /setD1P[ntx cxy]] /negP[]]] := Nfacts x Dx. rewrite FTsupp1_type1 Ntype1 // in NFy cxy *. have /Frobenius_kerP[_ _ _ regFN] := FTtype1_Frobenius maxN Ntype1. by rewrite 2!inE ntx (subsetP (regFN y NFy)). have /negP[] := no_coherent_Frobenius_partition (mFT_odd _) kge2 frobL tiH coH_. rewrite eqEsubset sub1set !inE andbT; apply/andP; split; last first. apply/bigcupP=> [[i _ /imset2P[x y /setD1P[ntx _] _ Dxy]]]. by rewrite -(conjg_eq1 x y) -Dxy eqxx in ntx. rewrite subDset setUC -subDset -(cover_partition partG). apply/bigcupsP=> _ /imsetP[Li MG_Li ->]; pose i := enum_rank_in MG_Li Li. rewrite (bigcup_max i) //=; have ->: Li = L i by rewrite /L enum_rankK_in. rewrite -FT_Dade1_supportE //; apply/bigcupsP=> x A1x; apply: imset2S => //. move: (FT_Dade1_hyp _) (tiH i); rewrite -defH => _ /Dade_normedTI_P[_ -> //]. by rewrite mul1g sub1set -/(H i) -defH. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)