proposition: Lemma typeP_reducible_core_cases : {t : Iirr M & 'chi_t \in S_ H0C' /\ 'chi_t 1%g = (q * u)%:R & {xi | xi \is a linear_char & 'chi_t = 'Ind[M, HC] xi}} + [/\ typeP_Galois, [Frobenius HU / H0 = Hbar ><| (U / H0)], cyclic U, #|U| = (p ^ q).-1 %/ p.-1 & FTtype M == 2%N -> [Frobenius HU = H ><| U]].
proof: Proof. have [GalM | Gal'M] := boolP typeP_Galois; last first. pose eqInHCb nu r := ('chi_r \is a linear_char) && (nu == 'Ind[M, HC] 'chi_r). pose isIndHCb (nu : 'CF(M)) := (nu 1%g == (q * u)%:R) && [exists r, eqInHCb nu r]. suffices /sig2W[t H0C't]: exists2 t, 'chi_t \in S_ H0C' & isIndHCb 'chi_t. case/andP=> /eqP t1qu /exists_inP/sig2W[r lin_r /eqP def_t]. by left; exists t => //; exists 'chi_r. have [_ _ [t [t1qu H0Ct IndHCt]] _] := typeP_nonGalois_characters Gal'M. exists t; first by rewrite (seqIndS _ H0Ct) ?Iirr_kerDS ?genS ?setUS ?der_sub. rewrite /isIndHCb t1qu eqxx; have [xi lin_xi ->] := IndHCt. by apply/exists_inP; exists (cfIirr xi); rewrite cfIirrE ?lin_char_irr. have [_ IndHC_SH0C' _] := typeP_Galois_characters GalM; rewrite all_predC. case: hasP => [/sig2W[eta H0C'eta /irrP/sig_eqW[t Dt]] _ | _ [//|C1 <- frobHU]]. have /sig2_eqW[s /IndHC_SH0C'[s1u IndHCs] Deta] := seqIndP H0C'eta. have [joinHU [xi lin_xi Ds]] := (sdprodWY defHU, sig2_eqW IndHCs). left; exists t; first split; rewrite -Dt // Deta. by rewrite cfInd1 ?der_sub // -(index_sdprod defM) s1u -natrM. by exists xi; rewrite ?Ds ?cfIndInd ?der_sub // -joinHU genS ?setUS ?subsetIl. have cycU: cyclic U. rewrite (isog_cyclic (quotient1_isog _)) -C1. by have [_ _ []] := typeP_Galois_P GalM. right; split=> //; first by rewrite /u /Ubar C1 -(card_isog (quotient1_isog _)). case/(compl_of_typeII maxM MtypeP) => /= _ _ _ UtypeF <-. have [_ -> _] := typeF_context UtypeF. by apply/forall_inP=> S /and3P[_ /cyclicS->]. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator center gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection8)