Timings for PFsection9.v

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
From mathcomp
Require Import fintype tuple finfun bigop prime binomial ssralg poly finset.
From mathcomp
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
From mathcomp
Require Import gfunctor gproduct cyclic commutator center gseries nilpotent.
From mathcomp
Require Import pgroup sylow hall abelian maximal frobenius.
From mathcomp
Require Import matrix mxalgebra mxrepresentation mxabelem vector.
From mathcomp
Require Import BGsection1 BGsection3 BGsection7 BGsection15 BGsection16.
From mathcomp
Require Import algC classfun character inertia vcharacter.
From mathcomp
Require Import PFsection1 PFsection2 PFsection3 PFsection4.
From mathcomp
Require Import PFsection5 PFsection6 PFsection8.

(******************************************************************************)
(* This file covers Peterfalvi, Section 9: On the maximal subgroups of Types  *)
(* II, III and IV. For defW : W1 \x W2 = W, MtypeP : of_typeP M U defW, and   *)
(* H := M`_\F we define :                                                     *)
(*  Ptype_Fcore_kernel MtypeP == a maximal normal subgroup of M contained     *)
(*               (locally) H0    in H and containing 'C_H(U), provided M is   *)
(*                               not a maximal subgroup of type V.            *)
(*  Ptype_Fcore_kernel MtypeP == the stabiliser of Hbar := H / H0 in U; this  *)
(*   (locally to this file) C    is locked for performance reasons.           *)
(*        typeP_Galois MtypeP <=> U acts irreducibly on Hbar; this implies    *)
(*                               that M / H0C is isomorphic to a Galois group *)
(*                               acting on the semidirect product of the      *)
(*                               additive group of a finite field with a      *)
(*                               a subgroup of its multiplicative group.      *)
(* --> This predicate reflects alternative (b) in Peterfalvi (9.7).           *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope GRing.Theory FinRing.Theory.

Section Nine.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types (p q : nat) (x y z : gT).
Implicit Types H K L N P Q R S T U V W : {group gT}.

(* Peterfalvi (9.1) is covered by BGsection3.Frobenius_Wielandt_fixpoint. *)

(* These assumptions correspond to Peterfalvi, Hypothesis (9.2). *)

Variables M U W W1 W2 : {group gT}.
Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W) (MtypeP: of_typeP M U defW).
Hypothesis notMtype5 : FTtype M != 5.

Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
Local Notation H := `M`_\F%G.
Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope.
Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
Local Notation HU := M^`(1)%G.
Local Notation "` 'HU'" := `M^`(1) (at level 0) : group_scope.
Local Notation U' := U^`(1)%G.
Local Notation "` 'U''" := `U^`(1) (at level 0) : group_scope.

Let q := #|W1|.

Let defM : HU ><| W1 = M. Proof. by have [[]] := MtypeP. Qed.
Let defHU : H ><| U = HU. Proof. by have [_ []] := MtypeP. Qed.
Let nUW1 : W1 \subset 'N(U). Proof. by have [_ []] := MtypeP. Qed.
Let cHU' : U' \subset 'C(H). Proof. by have [_ []] := typeP_context MtypeP. Qed.

Let notMtype1 : FTtype M != 1%N. Proof. exact: FTtypeP_neq1 MtypeP. Qed.

Local Notation Mtype24 := (compl_of_typeII_IV maxM MtypeP notMtype5).
Let ntU : U :!=: 1. Proof. by have [] := Mtype24. Qed.
Let pr_q : prime q. Proof. by have [] := Mtype24. Qed.
Let ntW2 : W2 :!=: 1. Proof. by have [_ _ _ []] := MtypeP. Qed.
Let sW2H : W2 \subset H. Proof. by have [_ _ _ []] := MtypeP. Qed.
Let defW2 : 'C_H(W1) = W2. Proof. exact: typeP_cent_core_compl MtypeP. Qed.

Lemma Ptype_Fcore_sdprod : H ><| (U <*> W1) = M.
Proof.
have [_ /= sW1M mulHUW1 _ tiHUW1] := sdprod_context defM. 
have [/= /andP[sHHU _] sUHU mulHU nHU tiHU] := sdprod_context defHU.
rewrite sdprodE /= norm_joinEr // ?mulgA ?mulHU //.
  by rewrite mulG_subG nHU (subset_trans sW1M) ?gFnorm.
rewrite setIC -(setIidPr sHHU) setIA -group_modl //.
by rewrite (setIC W1) tiHUW1 mulg1 setIC tiHU.
Qed.
Local Notation defHUW1 := Ptype_Fcore_sdprod.

Lemma Ptype_Fcore_coprime : coprime #|H| #|U <*> W1|.
Proof.
by rewrite (coprime_sdprod_Hall_l defHUW1) ?(pHall_Hall (Fcore_Hall M)).
Qed.
Let coH_UW1 := Ptype_Fcore_coprime.
Let coHU : coprime #|H| #|U|.
Proof. exact: coprimegS (joing_subl U W1) coH_UW1. Qed.

Let not_cHU : ~~ (U \subset 'C(H)).
Proof. by have [_ [_ ->]] := typeP_context MtypeP. Qed.

Lemma Ptype_compl_Frobenius : [Frobenius U <*> W1 = U ><| W1].
Proof.
have [[_ _ ntW1 _] _ _ [_ _ _ _ prHU_W1] _] := MtypeP.
have [[_ _ _ tiHUW1] [_ sUHU _ _ tiHU]] := (sdprodP defM, sdprod_context defHU).
apply/Frobenius_semiregularP=> // [|x /prHU_W1 defCx].
  by rewrite sdprodEY //; apply/trivgP; rewrite -tiHUW1 setSI.
by apply/trivgP; rewrite -tiHU /= -{1}(setIidPr sUHU) setIAC defCx setSI.
Qed.
Local Notation frobUW1 := Ptype_compl_Frobenius.

Let nilH : nilpotent H. Proof. exact: Fcore_nil. Qed.
Let solH : solvable H. Proof. exact: nilpotent_sol. Qed.

(* This is Peterfalvi (9.3). *)
Lemma typeII_IV_core (p := #|W2|) :
  if FTtype M == 2 then 'C_H(U) = 1 /\ #|H| = (#|W2| ^ q)%N
  else [/\ prime p, 'C_H(U <*> W1) = 1 & #|H| = (p ^ q * #|'C_H(U)|)%N].
Proof.
have [_ _ nHUW1 _] := sdprodP defHUW1.
have /= [oH _ oH1] := Frobenius_Wielandt_fixpoint frobUW1 nHUW1 coH_UW1 solH.
have [Mtype2 {oH}| notMtype2 {oH1}] := boolP (FTtype M == 2).
  suffices regHU: 'C_H(U) = 1 by rewrite -defW2 oH1.
  have [_ _ _ HUtypeF defHUF] := compl_of_typeII maxM MtypeP Mtype2.
  have [_ _ [U0 [sU0U _]]] := HUtypeF; rewrite {}defHUF => frobHU0.
  have /set0Pn[x U0x]: U0^# != set0.
    by rewrite setD_eq0 subG1; case/Frobenius_context: frobHU0.
  apply/trivgP; rewrite -(Frobenius_reg_ker frobHU0 U0x) setIS // -cent_cycle.
  by rewrite centS // cycle_subG (subsetP sU0U) //; case/setD1P: U0x.
have p_pr: prime p.
  have [S pairMS [xdefW [U_S StypeP]]] := FTtypeP_pair_witness maxM MtypeP.
  have [[_ _ maxS] _] := pairMS; rewrite {1}(negPf notMtype2) /= => Stype2 _ _.
  by have [[]] := compl_of_typeII maxS StypeP Stype2.
rewrite -/q -/p centY setICA defW2 setIC in oH *.
suffices regW2U: 'C_W2(U) = 1 by rewrite -oH regW2U cards1 exp1n mul1n.
apply: prime_TIg => //=; apply: contra not_cHU => /setIidPl cUW2.
rewrite centsC (sameP setIidPl eqP) eqEcard subsetIl.
by rewrite -(@leq_pmul2l (p ^ q)) -?oH ?cUW2 //= expn_gt0 cardG_gt0.
Qed.

(* Existential witnesses for Peterfalvi (9.4). *)
Definition Ptype_Fcore_kernel of of_typeP M U defW :=
  odflt 1%G [pick H0 : {group gT} | chief_factor M H0 H & 'C_H(U) \subset H0].
Let H0 := (Ptype_Fcore_kernel MtypeP).
Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope.
Local Notation Hbar := (H / `H0)%G.
Local Notation "` 'Hbar'" := (`H / `H0)%g (at level 0) : group_scope.
Let p := pdiv #|Hbar|.

(* This corresponds to Peterfalvi (9.4). *)
Lemma Ptype_Fcore_kernel_exists : chief_factor M H0 H /\ 'C_H(U) \subset H0.
Proof.
pose S := <<class_support 'C_H(U) H>> .
suffices [H1 maxH sCH1]: {H1 : {group gT} | maxnormal H1 H M & S \subset H1}.
  apply/andP; rewrite /H0 /Ptype_Fcore_kernel; case: pickP => // /(_ H1)/idP[].
  rewrite /chief_factor maxH Fcore_normal (subset_trans _ sCH1) ?sub_gen //.
  exact: sub_class_support.
apply/maxgroup_exists/andP; split.
  have snCH: 'C_H(U) <|<| H by rewrite nilpotent_subnormal ?subsetIl.
  by have [/setIidPl/idPn[] | // ] := subnormalEsupport snCH; rewrite centsC.
have [_ {3}<- nHUW1 _] := (sdprodP defHUW1).
rewrite norms_gen // mulG_subG class_support_norm norms_class_support //.
by rewrite normsI ?norms_cent // join_subG normG.
Qed.

Let chiefH0 : chief_factor M H0 H.
Proof. by have [] := Ptype_Fcore_kernel_exists. Qed.
Let ltH0H : H0 \proper H.
Proof. by case/andP: chiefH0 => /maxgroupp/andP[]. Qed.
Let nH0M : M \subset 'N(H0).
Proof. by case/andP: chiefH0 => /maxgroupp/andP[]. Qed.
Let sH0H : H0 \subset H. Proof. exact: proper_sub ltH0H. Qed.
Let nsH0M : H0 <| M. Proof. by rewrite /normal (subset_trans sH0H) ?gFsub. Qed.
Let nsH0H : H0 <| H. Proof. by rewrite (normalS _ (Fcore_sub _)). Qed.
Let minHbar : minnormal Hbar (M / H0).
Proof. exact: chief_factor_minnormal. Qed.
Let ntHbar : Hbar :!=: 1. Proof. by case/mingroupp/andP: minHbar. Qed.
Let solHbar: solvable Hbar. Proof. by rewrite quotient_sol. Qed.
Let abelHbar : p.-abelem Hbar.
Proof. by have [] := minnormal_solvable minHbar _ solHbar. Qed.
Let p_pr : prime p. Proof. by have [/pgroup_pdiv[]] := and3P abelHbar. Qed.
Let abHbar : abelian Hbar. Proof. exact: abelem_abelian abelHbar. Qed.

(* This is Peterfalvi, Hypothesis (9.5). *)
Fact Ptype_Fcompl_kernel_key : unit. Proof. by []. Qed.
Definition Ptype_Fcompl_kernel :=
  locked_with Ptype_Fcompl_kernel_key 'C_U(Hbar | 'Q)%G.
Local Notation C := Ptype_Fcompl_kernel.
Local Notation "` 'C'" := (gval C) (at level 0, only parsing) : group_scope.
Local Notation Ubar := (U / `C)%G.
Local Notation "` 'Ubar'" := (`U / `C)%g (at level 0) : group_scope.
Local Notation W1bar := (W1 / `H0)%G.
Local Notation "` 'W1bar'" := (`W1 / `H0)%g (at level 0) : group_scope.
Local Notation W2bar := 'C_Hbar(`W1bar)%G.
Local Notation "` 'W2bar'" := 'C_`Hbar(`W1bar) (at level 0) : group_scope.
Let c := #|C|.
Let u := #|Ubar|.
Local Notation tau := (FT_Dade0 maxM).
Local Notation "chi ^\tau" := (tau chi).
Let calX := Iirr_kerD M^`(1) H 1.
Let calS := seqIndD M^`(1) M M`_\F 1.
Let X_ Y := Iirr_kerD M^`(1) H Y.
Let S_ Y := seqIndD M^`(1) M M`_\F Y.

Local Notation inMb := (coset (gval H0)).

Local Notation H0C := (`H0 <*> `C)%G.
Local Notation "` 'H0C'" := (`H0 <*> `C) (at level 0) : group_scope.
Local Notation HC := (`H <*> `C)%G.
Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope.
Local Notation H0U' := (`H0 <*> `U')%G.
Local Notation "` 'H0U''" := (gval H0 <*> `U')%G (at level 0) : group_scope.
Local Notation H0C' := (`H0 <*> `C^`(1)%g)%G.
Local Notation "` 'H0C''" := (`H0 <*> `C^`(1)) (at level 0) : group_scope.

Let defW2bar : W2bar :=: W2 / H0.
Proof.
rewrite -defW2 coprime_quotient_cent ?(subset_trans _ nH0M) //.
  by have [_ /mulG_sub[]] := sdprodP defM.
exact: coprimegS (joing_subr _ _) coH_UW1.
Qed.

Let sCU : C \subset U. Proof. by rewrite [C]unlock subsetIl. Qed.

Let nsCUW1 : C <| U <*> W1.
Proof.
have [_ sUW1M _ nHUW1 _] := sdprod_context defHUW1.
rewrite /normal [C]unlock subIset ?joing_subl // normsI //.
  by rewrite join_subG normG.
rewrite /= astabQ norm_quotient_pre ?norms_cent ?quotient_norms //.
exact: subset_trans sUW1M nH0M.
Qed.

Lemma Ptype_Fcore_extensions_normal :
  [/\ H0C <| M, HC <| M, H0U' <| M & H0C' <| M].
Proof.
have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM.
have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU.
have [sHM sUM] := (subset_trans sHHU sHUM, subset_trans sUHU sHUM).
have sCM: C \subset M := subset_trans sCU sUM.
have sH0C_M: H0C \subset M by rewrite /normal join_subG (subset_trans sH0H).
have [nH0C nH0_H0C] := (subset_trans sCM nH0M, subset_trans sH0C_M nH0M).
have nsH0C: H0C <| M.
  rewrite /normal sH0C_M -{1}defM sdprodEY //= -defHU sdprodEY //= -joingA.
  rewrite join_subG andbC normsY ?(normal_norm nsCUW1) //=; last first.
    by rewrite (subset_trans _ nH0M) // join_subG sUM.
  rewrite -quotientYK // -{1}(quotientGK nsH0H) morphpre_norms //= [C]unlock.
  by rewrite cents_norm // centsC -quotient_astabQ quotientS ?subsetIr.
split=> //; first by rewrite /= -{1}(joing_idPl sH0H) -joingA normalY ?gFnormal.
  rewrite normalY // /normal gFsub_trans //=.
  rewrite -defM sdprodEY //= -defHU sdprodEY //=.
  by rewrite !join_subG gFnorm cents_norm ?gFnorm_trans // centsC.
suffices ->: H0C' :=: H0 <*> H0C^`(1) by rewrite normalY ?gFnormal_trans.
by rewrite /= -!quotientYK ?gFsub_trans ?quotient_der ?subsetIl //= cosetpreK.
Qed.
Local Notation nsH0xx_M := Ptype_Fcore_extensions_normal.

Let Du : u = #|HU : HC|.
Proof.
have nCU := subset_trans (joing_subl U W1) (normal_norm nsCUW1).
by rewrite -(index_sdprodr defHU) -?card_quotient.
Qed.

(* This is Peterfalvi (9.6). *)
Lemma Ptype_Fcore_factor_facts :
  [/\ C :!=: U, #|W2bar| = p & #|Hbar| = p ^ q]%N.
Proof.
have [defUW1 _ ntW1 _ _] := Frobenius_context Ptype_compl_Frobenius.
have coHW1: coprime #|H| #|W1| := coprimegS (joing_subr U W1) coH_UW1.
have [_ sUW1M _ nHUW1 _] := sdprod_context defHUW1.
have nH0UW1 := subset_trans sUW1M nH0M; have [nH0U nH0W1] := joing_subP nH0UW1.
have regUHb: 'C_Hbar(U / H0) = 1.
  have [_ sCH0] := Ptype_Fcore_kernel_exists.
  by rewrite -coprime_quotient_cent ?(nilpotent_sol nilH) ?quotientS1.
have ->: C != U.
  apply: contraNneq ntHbar => defU; rewrite -subG1 -regUHb subsetIidl centsC.
  by rewrite -defU [C]unlock -quotient_astabQ quotientS ?subsetIr.
have frobUW1b: [Frobenius U <*> W1 / H0 = (U / H0) ><| W1bar].
  have tiH0UW1 := coprime_TIg (coprimeSg sH0H coH_UW1).
  have /isomP[inj_f im_f] := quotient_isom nH0UW1 tiH0UW1.
  have:= injm_Frobenius (subxx _) inj_f frobUW1.
  by rewrite im_f !morphim_restrm !(setIidPr _) ?joing_subl ?joing_subr.
have{frobUW1b} oHbar: #|Hbar| = (#|W2bar| ^ q)%N.
  have nHbUW1 : U <*> W1 / H0 \subset 'N(Hbar) := quotient_norms H0 nHUW1.
  have coHbUW1 : coprime #|Hbar| #|U <*> W1 / H0| by apply: coprime_morph.
  have [//|_ _ -> //] := Frobenius_Wielandt_fixpoint frobUW1b nHbUW1 coHbUW1 _.
  by rewrite -(card_isog (quotient_isog _ _)) // coprime_TIg ?(coprimeSg sH0H).
have abelW2bar: p.-abelem W2bar := abelemS (subsetIl _ _) abelHbar.
rewrite -(part_pnat_id (abelem_pgroup abelW2bar)) p_part in oHbar *.
suffices /eqP cycW2bar: logn p #|W2bar| == 1%N by rewrite oHbar cycW2bar.
have cycW2: cyclic W2 by have [_ _ _ []] := MtypeP.
rewrite eqn_leq -abelem_cyclic //= -/W2bar {1}defW2bar quotient_cyclic //=.
rewrite lt0n; apply: contraNneq ntHbar => W2bar1.
by rewrite trivg_card1 oHbar W2bar1 exp1n.
Qed.

Lemma def_Ptype_factor_prime : prime #|W2| -> p = #|W2|.
Proof.
move=> prW2; suffices: p \in \pi(W2) by rewrite !(primes_prime, inE) // => /eqP.
rewrite mem_primes p_pr cardG_gt0; have [_ <- _] := Ptype_Fcore_factor_facts.
by rewrite defW2bar dvdn_quotient.
Qed.

(* The first assertion of (9.4)(b) (the rest is subsumed by (9.6)). *)
Lemma typeIII_IV_core_prime : FTtype M != 2 -> p = #|W2|.
Proof.
by have:= typeII_IV_core => /=; case: ifP => // _ [/def_Ptype_factor_prime].
Qed.

Let frobUW1c : [Frobenius U <*> W1 / C = Ubar ><| W1 / C].
Proof.
apply: Frobenius_quotient frobUW1 _ nsCUW1 _.
  by apply: nilpotent_sol; have [_ []] := MtypeP.
by have [] := Ptype_Fcore_factor_facts; rewrite eqEsubset sCU.
Qed.  

Definition typeP_Galois := acts_irreducibly U Hbar 'Q.

(* This is Peterfalvi (9.7)(a). *)
Lemma typeP_Galois_Pn :
    ~~ typeP_Galois ->
  {H1 : {group coset_of H0} |
    [/\ #|H1| = p, U / H0 \subset 'N(H1), [acts U, on H1 | 'Q],
        \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar
      & let a := #|U : 'C_U(H1 | 'Q)| in
        [/\ a > 1, a %| p.-1, cyclic (U / 'C_U(H1 | 'Q))
          & exists V : {group 'rV['Z_a]_q.-1}, Ubar \isog V]]}.
Proof.
have [_ sUW1M defHUW1 nHUW1 _] := sdprod_context defHUW1.
have [nHU nHW1] := joing_subP nHUW1.
have nH0UW1 := subset_trans sUW1M nH0M; have [nH0U nH0W1] := joing_subP nH0UW1.
rewrite /typeP_Galois acts_irrQ //= => not_minHbarU.
have [H1 minH1 sH1Hb]: {H1 | minnormal (gval H1) (U / H0) & H1 \subset Hbar}.
  by apply: mingroup_exists; rewrite ntHbar quotient_norms.
exists H1; have [defH1 | ltH1H] := eqVproper sH1Hb.
  by rewrite -defH1 minH1 in not_minHbarU.
have [/andP[ntH1 nH1U] _] := mingroupP minH1.
have actsUH1: [acts U, on H1 | 'Q].
  by rewrite -(cosetpreK H1) actsQ ?norm_quotient_pre.
have [nH0H [neqCU _ oHbar]] := (normal_norm nsH0H, Ptype_Fcore_factor_facts).
have nUW1b: W1bar \subset 'N(U / H0) by apply: quotient_norms.
have oW1b: #|W1bar| = q.
  rewrite -(card_isog (quotient_isog _ _)) // coprime_TIg //.
  by rewrite (coprimeSg sH0H) // (coprimegS (joing_subr U W1)).
have [oH1 defHbar]: #|H1| = p /\ \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar.
  have nHbUW1: U <*> W1 / H0 \subset 'N(Hbar) by apply: quotient_norms.
  pose rUW1 := abelem_repr abelHbar ntHbar nHbUW1.
  have irrUW1: mx_irreducible rUW1.
    apply/abelem_mx_irrP/mingroupP; split=> [|H2]; first by rewrite ntHbar.
    case/andP=> ntH2 nH2UW1 sH2H; case/mingroupP: minHbar => _; apply=> //.
    by rewrite ntH2 -defHUW1 quotientMl // mulG_subG sub_abelian_norm.
  have nsUUW1: U / H0 <| U <*> W1 / H0 by rewrite quotient_normal // normalYl.
  pose rU := subg_repr rUW1 (normal_sub nsUUW1).
  pose V1 := rowg_mx (abelem_rV abelHbar ntHbar @* H1).
  have simV1: mxsimple rU V1 by apply/mxsimple_abelem_subg/mxsimple_abelemGP.
  have [W0 /subsetP sW01 [sumW0 dxW0]] := Clifford_basis irrUW1 simV1.
  have def_q: q = (#|W0| * \rank V1)%N.
    transitivity (\rank (\sum_(w in W0) V1 *m rUW1 w))%R.
      by rewrite sumW0 mxrank1 /= (dim_abelemE abelHbar) // oHbar pfactorK.
    rewrite (mxdirectP dxW0) -sum_nat_const; apply: eq_bigr => x /sW01/= Wx.
    by rewrite mxrankMfree ?row_free_unit ?repr_mx_unit.
  have oH1: #|H1| = (p ^ \rank V1)%N.
    by rewrite -{1}(card_Fp p_pr) -card_rowg rowg_mxK card_injm ?abelem_rV_injm.
  have oW0: #|W0| = q.
    apply/prime_nt_dvdP=> //; last by rewrite def_q dvdn_mulr.
    apply: contraTneq (proper_card ltH1H) => trivW0.
    by rewrite oHbar def_q trivW0 mul1n -oH1 ltnn.
  have q_gt0 := prime_gt0 pr_q.
  rewrite oH1 -(mulKn (\rank V1) q_gt0) -{1}oW0 -def_q divnn q_gt0.
  have defHbar: \big[dprod/1]_(w in W0) H1 :^ w = Hbar.
    have inj_rV_Hbar := rVabelem_injm abelHbar ntHbar.
    have/(injm_bigdprod _ inj_rV_Hbar)/= := bigdprod_rowg sumW0 dxW0.
    rewrite sub_im_abelem_rV rowg1 im_rVabelem => <- //=; apply: eq_bigr => w.
    by move/sW01=> Ww; rewrite abelem_rowgJ ?rowg_mxK ?abelem_rV_mK.
  have injW0: {in W0 &, injective (fun w => H1 :^ w)}.
    move=> x y Wx Wy /= eq_Hxy; apply: contraNeq ntH1 => neq_xy.
    rewrite -(conjsg_eq1 _ x) -[H1 :^ x]setIid {1}eq_Hxy; apply/eqP.
    rewrite (bigD1 y) // (bigD1 x) /= ?Wx // dprodA in defHbar.
    by case/dprodP: defHbar => [[_ _ /dprodP[_ _ _ ->] _]].
  have defH1W0: [set H1 :^ w | w in W0] = [set H1 :^ w | w in W1 / H0].
    apply/eqP; rewrite eqEcard (card_in_imset injW0) oW0 -oW1b leq_imset_card.
    rewrite andbT; apply/subsetP=> _ /imsetP[w /sW01/= Ww ->].
    move: Ww; rewrite norm_joinEr ?quotientMl // => /mulsgP[x w1 Ux Ww1 ->].
    by rewrite conjsgM (normsP nH1U) // mem_imset.
  have injW1: {in W1 / H0 &, injective (fun w => H1 :^ w)}.
    by apply/imset_injP; rewrite -defH1W0 (card_in_imset injW0) oW0 oW1b.
  by rewrite -(big_imset id injW1) -defH1W0 big_imset.
split=> //; set a := #|_ : _|; pose q1 := #|(W1 / H0)^#|.
have a_gt1: a > 1.
  rewrite indexg_gt1 subsetIidl /= astabQ -sub_quotient_pre //. 
  apply: contra neqCU => cH1U; rewrite [C]unlock (sameP eqP setIidPl) /= astabQ.
  rewrite -sub_quotient_pre // -(bigdprodWY defHbar) cent_gen centsC.
  by apply/bigcupsP=> w Ww; rewrite centsC centJ -(normsP nUW1b w) ?conjSg.
have Wb1: 1 \in W1bar := group1 _.
have ->: q.-1 = q1 by rewrite -oW1b (cardsD1 1) Wb1.
have /cyclicP[h defH1]: cyclic H1 by rewrite prime_cyclic ?oH1.
have o_h: #[h] = p by rewrite defH1 in oH1.
have inj_Zp_h w := injm_Zp_unitm (h ^ w).
pose phi w := invm (inj_Zp_h w) \o restr_perm <[h ^ w]> \o actperm 'Q.
have dU w: w \in W1bar -> {subset U <= 'dom (phi w)}.
  move=> Ww x Ux; have Qx := subsetP (acts_dom actsUH1) x Ux.
  rewrite inE Qx /= im_Zp_unitm inE mem_morphpre //=; last first.
    by apply: Aut_restr_perm (actperm_Aut 'Q _); rewrite //= quotientT.
  rewrite cycleJ -defH1 !inE /=; apply/subsetP=> z H1w_z; rewrite inE actpermK.
  rewrite qactJ (subsetP nH0U) ?memJ_norm // normJ mem_conjg.
  by rewrite (subsetP nH1U) // -mem_conjg (normsP nUW1b) ?mem_quotient.
have sUD := introT subsetP (dU _ _).
have Kphi w: 'ker (phi w) = 'C(H1 :^ w | 'Q).
  rewrite !ker_comp ker_invm -kerE ker_restr_perm defH1 -cycleJ.
  apply/setP=> x; rewrite !inE; congr (_ && _) => /=.
  by apply: eq_subset_r => h1; rewrite !inE actpermK.
have o_phiU w: w \in W1bar -> #|phi w @* U| = a.
  move=> Ww; have [w1 Nw1 Ww1 def_w] := morphimP Ww.
  rewrite card_morphim Kphi (setIidPr _) ?sUD // /a indexgI /= !astabQ.
  by rewrite centJ def_w morphpreJ // -{1}(normsP nUW1 w1 Ww1) indexJg.
have a_dv_p1: a %| p.-1.
  rewrite -(o_phiU 1) // (dvdn_trans (cardSg (subsetT _))) // card_units_Zp //.
  by rewrite conjg1 o_h (@totient_pfactor p 1) ?muln1.
have cycZhw w: cyclic (units_Zp #[h ^ w]).
  rewrite -(injm_cyclic (inj_Zp_h w)) // im_Zp_unitm Aut_prime_cyclic //=.
  by rewrite -orderE orderJ o_h.
have cyc_phi1U: cyclic (phi 1 @* U) := cyclicS (subsetT _) (cycZhw 1).
split=> //; last have{cyc_phi1U a_dv_p1} [z def_z] := cyclicP cyc_phi1U.
  by rewrite -(conjsg1 H1) -Kphi (isog_cyclic (first_isog_loc _ _)) ?sUD.
have o_hw w: #[h ^ w] = #[h ^ 1] by rewrite !orderJ.
pose phi1 w x := eq_rect _ (fun m => {unit 'Z_m}) (phi w x) _ (o_hw w).
have val_phi1 w x: val (phi1 w x) = val (phi w x) :> nat.
  by rewrite /phi1; case: _ / (o_hw _).
have mem_phi1 w x: w \in W1bar -> x \in U -> phi1 w x \in <[z]>%G.
  move=> Ww Ux; have: #|<[z]>%G| = a by rewrite /= -def_z o_phiU.
  rewrite /phi1; case: _ / (o_hw w) <[z]>%G => A oA /=.
  suffices <-: phi w @* U = A by rewrite mem_morphim // dU.
  by apply/eqP; rewrite (eq_subG_cyclic (cycZhw w)) ?subsetT // oA o_phiU.
have o_z: #[z] = a by rewrite orderE -def_z o_phiU.
pose phi0 w x := ecast m 'Z_m o_z (invm (injm_Zpm z) (phi1 w x)).
pose psi x := (\row_(i < q1) (phi0 (enum_val i) x * (phi0 1 x)^-1)%g)%R.
have psiM: {in U &, {morph psi: x y / x * y}}.
  have phi0M w: w \in W1bar -> {in U &, {morph phi0 w: x y / x * y}}.
    move=> Ww x y Ux Uy; rewrite /phi0; case: (a) / (o_z) => /=.
    rewrite -morphM; first 1 [congr (invm _ _)] || by rewrite im_Zpm mem_phi1.
    by rewrite /phi1; case: _ / (o_hw w); rewrite /= -morphM ?dU.
  move=> x y Ux Uy; apply/rowP=> i; have /setD1P[_ Ww] := enum_valP i.
  by rewrite !{1}mxE !{1}phi0M // addrCA -addrA -opprD addrCA addrA.
suffices Kpsi: 'ker (Morphism psiM) = C.
  by exists [group of Morphism psiM @* U]; rewrite /Ubar -Kpsi first_isog.
apply/esym/eqP; rewrite eqEsubset; apply/andP; split.
  rewrite [C]unlock -(bigdprodWY defHbar); apply/subsetP=> x /setIP[Ux cHx].
  suffices phi0x1 w: w \in W1bar -> phi0 w x = 1.
    rewrite !inE Ux; apply/eqP/rowP=> i; have /setD1P[_ Ww] := enum_valP i.
    by rewrite !mxE !phi0x1 ?mulgV.
  move=> Ww; apply: val_inj; rewrite /phi0; case: (a) / (o_z); congr (val _).
  suffices /eqP->: phi1 w x == 1 by rewrite morph1.
  rewrite -2!val_eqE [val _]val_phi1 -(o_hw w) [phi _ _]mker // Kphi.
  by apply: subsetP (astabS _ _) _ cHx; rewrite sub_gen // (bigcup_sup w).
have sKU: 'ker (Morphism psiM) \subset U by apply: subsetIl.
rewrite -quotient_sub1 -?(Frobenius_trivg_cent frobUW1c); last first.
  by apply: subset_trans (normal_norm nsCUW1); rewrite subIset ?joing_subl.
rewrite subsetI quotientS //= quotient_cents2r // [C]unlock subsetI.
rewrite (subset_trans (commSg W1 sKU)) ?commg_subl //= astabQ gen_subG /=.
apply/subsetP=> _ /imset2P[x w1 Kx Ww1 ->].
have:= Kx; rewrite -groupV 2!inE groupV => /andP[Ux /set1P/rowP psi_x'0].
have [nH0x Ux'] := (subsetP nH0U x Ux, groupVr Ux); pose x'b := (inMb x)^-1.
rewrite mem_morphpre ?groupR ?morphR //= ?(subsetP nH0W1) //.
have conj_x'b w: w \in W1bar -> (h ^ w) ^ x'b = (h ^ w) ^+ val (phi 1 x^-1).
  move=> Ww; transitivity (Zp_unitm (phi w x^-1) (h ^ w)).
    have /morphpreP[_ /morphpreP[Px' Rx']] := dU w Ww x^-1 Ux'.
    rewrite invmK ?restr_permE ?cycle_id //.
    by rewrite actpermE qactJ groupV nH0x morphV.
  have:= Ww; rewrite -(setD1K Wb1) autE ?cycle_id // => /setU1P[-> // | W'w].
  have /eqP := psi_x'0 (enum_rank_in W'w w); rewrite 2!mxE enum_rankK_in //.
  rewrite -eq_mulgV1 -val_eqE /phi0; case: (a) / (o_z); rewrite /= val_eqE.
  rewrite (inj_in_eq (injmP (injm_invm _))) /= ?im_Zpm ?mem_phi1 //.
  by rewrite -2!val_eqE /= !val_phi1 // => /eqP->.
rewrite -sub_cent1 -(bigdprodWY defHbar) gen_subG; apply/bigcupsP=> w2 Ww2.
rewrite defH1 -cycleJ cycle_subG cent1C inE conjg_set1 !conjgM // conj_x'b //.
rewrite conjXg -!conjgM -conj_x'b ?groupM ?groupV ?mem_quotient //.
by rewrite !conjgM !conjgKV.
Qed.

(* This is Peterfalvi (9.7)(b). *)
(* Note that part of this statement feeds directly into the final chapter of  *)
(* the proof (PFsection14 and BGappendixC) and is not used before; we have    *)
(* thus chosen to formulate the statement of (9.7)(b) accordingly.            *)
(*   For example, we supply separately the three component of the semi-direct *)
(* product isomorphism, because no use is made of the global isomorphism. We  *)
(* also state explicitly that the image of W2bar is Fp because this is the    *)
(* fact used in B & G, Appendix C, it is readily available during the proof,  *)
(* whereas it can only be derived from the original statement of (9.7)(b) by  *)
(* using Galois theory. Indeed the Galois part of the isomorphism is only     *)
(* needed for this -- so with the formulation below it will not be used.      *)
(*   In order to avoid the use of the Wedderburn theorem on finite division   *)
(* rings we build the field F from the enveloping algebra of the              *)
(* representation of U rather than its endomorphism ring: then the fact that  *)
(* Ubar is abelian yields commutativity directly.                              *)
Lemma typeP_Galois_P :
    typeP_Galois ->
  {F : finFieldType & {phi : {morphism Hbar >-> F}
     & {psi : {morphism U >-> {unit F}} & {eta : {morphism W1 >-> {perm F}}
   & forall alpha : {perm F}, reflect (rmorphism alpha) (alpha \in eta @* W1)
   & [/\ 'injm eta, {in Hbar & W1, morph_act 'Q 'P phi eta}
       & {in U & W1, forall x w, val (psi (x ^ w)) = eta w (val (psi x))}]}
   & 'ker psi = C /\ {in Hbar & U, morph_act 'Q 'U phi psi}}
   & [/\ #|F| = (p ^ q)%N, isom Hbar [set: F] phi & phi @* W2bar = <[1%R : F]>]}
   & [/\ cyclic Ubar, coprime u p.-1 & u %| (p ^ q).-1 %/ p.-1]}.
Proof.
move=> irrU; have [_ sUW1M _ /joing_subP[nHU nHW1] _] := sdprod_context defHUW1.
have [nHbU nHbW1] := (quotient_norms H0 nHU, quotient_norms H0 nHW1).
have{sUW1M} /joing_subP[nH0U nH0W1] := subset_trans sUW1M nH0M.
have [ltCU oW2b oHb] := Ptype_Fcore_factor_facts.
pose rU := abelem_repr abelHbar ntHbar nHbU.
pose inHb := rVabelem abelHbar ntHbar; pose outHb := abelem_rV abelHbar ntHbar.
have{irrU} irrU: mx_irreducible rU by apply/abelem_mx_irrP; rewrite -acts_irrQ.
pose E_U := [pred A | (A \in enveloping_algebra_mx rU)%MS].
have cEE A: A \in E_U -> centgmx rU A.
  case/envelop_mxP=> z_ ->{A}; rewrite -memmx_cent_envelop linear_sum.
  rewrite summx_sub // => x Ux; rewrite linearZ scalemx_sub {z_}//=.
  rewrite memmx_cent_envelop; apply/centgmxP=> y Uy.
  rewrite -repr_mxM // commgC 2?repr_mxM ?(groupR, groupM) // -/rU.
  apply/row_matrixP=> i; rewrite row_mul; move: (row i _) => h.
  have cHbH': (U / H0)^`(1) \subset 'C(Hbar).
    by rewrite -quotient_der ?quotient_cents.
  apply: rVabelem_inj; rewrite rVabelemJ ?groupR //.
  by apply: (canLR (mulKg _)); rewrite -(centsP cHbH') ?mem_commg ?mem_rVabelem.
have{cEE} [F [outF [inF outFK inFK] E_F]]:
  {F : finFieldType & {outF : {rmorphism F -> 'M(Hbar)%Mg}
   & {inF : {additive _} | cancel outF inF & {in E_U, cancel inF outF}}
   & forall a, outF a \in E_U}}%R.
- pose B := row_base (enveloping_algebra_mx rU).
  have freeB: row_free B by apply: row_base_free.
  pose outF := [additive of vec_mx \o mulmxr B].
  pose inF := [additive of mulmxr (pinvmx B) \o mxvec].
  have E_F a: outF a \in E_U by rewrite !inE vec_mxK mulmx_sub ?eq_row_base.
  have inK: {in E_U, cancel inF outF}.
    by move=> A E_A; rewrite /= mulmxKpV ?mxvecK ?eq_row_base.
  have outI: injective outF := inj_comp (can_inj vec_mxK) (row_free_inj freeB).
  have outK: cancel outF inF by move=> a; apply: outI; rewrite inK ?E_F.
  pose one := inF 1%R; pose mul a b := inF (outF a * outF b)%R.
  have outM: {morph outF: a b / mul a b >-> a * b}%R.
    by move=> a b; rewrite inK //; apply: envelop_mxM; apply: E_F.
  have out0: outF 0%R = 0%R by apply: raddf0.
  have out1: outF one = 1%R by rewrite inK //; apply: envelop_mx1.
  have nzFone: one != 0%R by rewrite -(inj_eq outI) out1 out0 oner_eq0.
  have mulA: associative mul by move=> *; apply: outI; rewrite !{1}outM mulrA.
  have mulC: commutative mul.
    move=> a b; apply: outI; rewrite !{1}outM.
    by apply: cent_mxP (E_F a); rewrite memmx_cent_envelop cEE ?E_F.
  have mul1F: left_id one mul by move=> a; apply: outI; rewrite outM out1 mul1r.
  have mulD: left_distributive mul +%R%R.
    by move=> a1 a2 b; apply: canLR outK _; rewrite !raddfD mulrDl -!{1}outM.
  pose Fring_NC := RingType 'rV__ (ComRingMixin mulA mulC mul1F mulD nzFone).
  pose Fring := ComRingType Fring_NC mulC.
  have outRM: multiplicative (outF : Fring -> _) by [].
  have mulI (nza : {a | a != 0%R :> Fring}): GRing.rreg (val nza).
    case: nza => a /=; rewrite -(inj_eq outI) out0 => nzA b1 b2 /(congr1 outF).
    rewrite !{1}outM => /row_free_inj eqB12; apply/outI/eqB12.
    by rewrite row_free_unit (mx_Schur irrU) ?cEE ?E_F.
  pose inv (a : Fring) := oapp (fun nza => invF (mulI nza) one) a (insub a).
  have inv0: (inv 0 = 0)%R by rewrite /inv insubF ?eqxx.
  have mulV: GRing.Field.axiom inv.
    by move=> a nz_a; rewrite /inv insubT /= (f_invF (mulI (exist _ _ _))).
  pose Funit := FieldUnitMixin mulV inv0.
  pose FringUcl := @GRing.ComUnitRing.Class _ (GRing.ComRing.class Fring) Funit.
  have Ffield := @FieldMixin (GRing.ComUnitRing.Pack FringUcl nat) _ mulV inv0.
  pose F := FieldType (IdomainType _ (FieldIdomainMixin Ffield)) Ffield.
  by exists [finFieldType of F], (AddRMorphism outRM); first exists inF.
pose in_uF (a : F) : {unit F} := insubd (1 : {unit F}) a.
have in_uF_E a: a != 1 -> val (in_uF a) = a.
  by move=> nt_a; rewrite insubdK /= ?unitfE.
have [psi psiK]: {psi : {morphism U >-> {unit F}}
                      | {in U, forall x, outF (val (psi x)) = rU (inMb x)}}.
- pose psi x := in_uF (inF (rU (inMb x))).
  have psiK x: x \in U -> outF (val (psi x)) = rU (inMb x).
    move/(mem_quotient H0)=> Ux; have EUx := envelop_mx_id rU Ux.
    rewrite in_uF_E ?inFK //; apply: contraTneq (repr_mx_unitr rU Ux).
    by move/(canRL_in inFK EUx)->; rewrite rmorph0 unitr0.
  suffices psiM: {in U &, {morph psi: x y / x * y}} by exists (Morphism psiM).
  move=> x y Ux Uy /=; apply/val_inj/(can_inj outFK); rewrite rmorphM //.
  by rewrite !{1}psiK ?groupM // morphM ?(subsetP nH0U) ?repr_mxM ?mem_quotient.
have /trivgPn/sig2W[s W2s nts]: W2bar != 1%G.
  by rewrite -cardG_gt1 oW2b prime_gt1.
pose sb := outHb s; have [Hs cW1s] := setIP W2s.
have nz_sb: sb != 0%R by rewrite morph_injm_eq1 ?abelem_rV_injm.
pose phi' a : coset_of H0 := inHb (sb *m outF a)%R.
have Hphi' a: phi' a \in Hbar by apply: mem_rVabelem.
have phi'D: {in setT &, {morph phi' : a b / a * b}}.
  by move=> a b _ _; rewrite /phi' !raddfD [inHb _]morphM ?mem_im_abelem_rV.
have inj_phi': injective phi'.
  move=> a b /rVabelem_inj eq_sab; apply: contraNeq nz_sb.
  rewrite -[sb]mulmx1 idmxE -(rmorph1 outF) -subr_eq0 => /divff <-.
  by rewrite rmorphM mulmxA !raddfB /= eq_sab subrr mul0mx.
have injm_phi': 'injm (Morphism phi'D) by apply/injmP; apply: in2W.
have Dphi: 'dom (invm injm_phi') = Hbar.
  apply/setP=> h; apply/morphimP/idP=> [[a _ _ ->] // | Hh].
  have /cyclic_mxP[A E_A def_h]: (outHb h <= cyclic_mx rU sb)%MS.
    by rewrite -(mxsimple_cyclic irrU) ?submx1.
  by exists (inF A); rewrite ?inE //= /phi' inFK // -def_h [inHb _]abelem_rV_K.
have [phi [def_phi Kphi _ im_phi]] := domP _ Dphi.
have{Kphi} inj_phi: 'injm phi by rewrite Kphi injm_invm.
have{im_phi} im_phi: phi @* Hbar = setT by rewrite im_phi -Dphi im_invm.
have phiK: {in Hbar, cancel phi phi'} by rewrite def_phi -Dphi; apply: invmK.
have{def_phi Dphi injm_phi'} phi'K: cancel phi' phi.
  by move=> a; rewrite def_phi /= invmE ?inE.
have phi'1: phi' 1%R = s by rewrite /phi' rmorph1 mulmx1 [inHb _]abelem_rV_K.
have phi_s: phi s = 1%R by rewrite -phi'1 phi'K.
have phiJ: {in Hbar & U, forall h x, phi (h ^ inMb x) = phi h * val (psi x)}%R.
  move=> h x Hh Ux; have Uxb := mem_quotient H0 Ux.
  apply: inj_phi'; rewrite phiK ?memJ_norm ?(subsetP nHbU) // /phi' rmorphM.
  by rewrite psiK // mulmxA [inHb _]rVabelemJ // -/inHb [inHb _]phiK.
have Kpsi: 'ker psi = C.
  apply/setP=> x; rewrite [C]unlock 2!in_setI /= astabQ; apply: andb_id2l => Ux.
  have Ubx := mem_quotient H0 Ux; rewrite 3!inE (subsetP nH0U) //= inE.
  apply/eqP/centP=> [psi_x1 h Hh | cHx]; last first.
    by apply/val_inj; rewrite -[val _]mul1r -phi_s -phiJ // conjgE -cHx ?mulKg.
  red; rewrite (conjgC h) -[h ^ _]phiK ?memJ_norm ?(subsetP nHbU) ?phiJ //.
  by rewrite psi_x1 mulr1 phiK.
have etaP (w : subg_of W1): injective (fun a => phi (phi' a ^ inMb (val w))).
  case: w => w /=/(mem_quotient H0)/(subsetP nHbW1) => nHw a b eq_ab.
  apply/inj_phi'/(conjg_inj (inMb w)).
  by apply: (injmP inj_phi) eq_ab; rewrite memJ_norm ?mem_rVabelem.
pose eta w : {perm F} := perm (etaP (subg W1 w)).
have etaK: {in Hbar & W1, forall h w, eta w (phi h) = phi (h ^ inMb w)}.
  by move=> h w Hh Ww; rewrite /= permE subgK ?phiK.
have eta1 w: w \in W1 -> eta w 1%R = 1%R.
  move=> Ww; rewrite -phi_s etaK //.
  by rewrite conjgE (centP cW1s) ?mulKg ?mem_quotient.
have etaM: {in W1 &, {morph eta: w1 w2 / w1 * w2}}.
  move=> w1 w2 Ww1 Ww2; apply/permP=> a; rewrite -[a]phi'K permM.
  rewrite !etaK ?memJ_norm ?groupM ?(subsetP nHbW1) ?mem_quotient //.
  by rewrite -conjgM -morphM ?(subsetP nH0W1).
have etaMpsi a: {in U & W1, forall x w, 
  eta w (a * val (psi x)) = eta w a * val (psi (x ^ w)%g)}%R.
- move=> x w Ux Ww; rewrite -[a]phi'K (etaK _ w (Hphi' a) Ww).
  rewrite -!phiJ // ?memJ_norm ?(subsetP nHbW1, subsetP nUW1) ?mem_quotient //.
  rewrite etaK ?memJ_norm ?(subsetP nHbU) ?mem_quotient // -!conjgM.
  by rewrite conjgC -morphJ ?(subsetP nH0U x Ux, subsetP nH0W1 w Ww).
have psiJ: {in U & W1, forall x w, val (psi (x ^ w)) = eta w (val (psi x))}.
  by move=> x w Ux Ww /=; rewrite -[val _]mul1r -(eta1 w Ww) -etaMpsi ?mul1r.
have etaRM w: w \in W1 -> rmorphism (eta w).
  move=> Ww; have nUw := subsetP nHbW1 _ (mem_quotient _ Ww).
  have etaD: additive (eta w).
    move=> a b; rewrite -[a]phi'K -[b]phi'K -!zmodMgE -!zmodVgE.
    rewrite -morphV // -morphM ?{1}etaK ?groupM ?groupV // conjMg conjVg.
    by rewrite morphM 1?morphV ?groupV // memJ_norm.
  do 2![split=> //] => [a b|]; last exact: eta1.
  rewrite -[a]outFK; have /envelop_mxP[d ->] := E_F a.
  rewrite raddf_sum mulr_suml ![eta w _](raddf_sum (Additive etaD)) mulr_suml.
  apply: eq_bigr => _ /morphimP[x Nx Ux ->]; move: {d}(d _) => dx.
  rewrite -[dx]natr_Zp scaler_nat !(mulrnAl, raddfMn); congr (_ *+ dx)%R.
  by rewrite -psiK //= outFK mulrC etaMpsi // mulrC psiJ.
have oF: #|F| = (p ^ q)%N by rewrite -cardsT -im_phi card_injm.
pose nF := <[1%R : F]>; have o_nF: #|nF| = p.
  by rewrite -orderE -phi_s (order_injm inj_phi) // (abelem_order_p abelHbar).
have cyc_uF := @field_unit_group_cyclic F.
exists F.
  exists phi; last first.
    split=> //; first exact/isomP; apply/esym/eqP; rewrite eqEcard o_nF -phi_s. 
    by rewrite (@cycle_subG F) mem_morphim //= card_injm ?subsetIl ?oW2b.
  exists psi => //; last first.
    by split=> // h x Hh Ux; rewrite qactJ (subsetP nH0U) ?phiJ.
  have inj_eta: 'injm (Morphism etaM).
    have /properP[_ [h Hh notW2h]]: W2bar \proper Hbar.
      by rewrite properEcard subsetIl oW2b oHb (ltn_exp2l 1) prime_gt1.
    apply/subsetP=> w /morphpreP[Ww /set1P/permP/(_ (phi h))].
    rewrite etaK // permE => /(injmP inj_phi) => chw.
    rewrite -(@prime_TIg _ W1 <[w]>) //; first by rewrite inE Ww cycle_id.
    rewrite proper_subn // properEneq cycle_subG Ww andbT.
    apply: contraNneq notW2h => defW1; rewrite inE Hh /= -defW1.
    rewrite quotient_cycle ?(subsetP nH0W1) // cent_cycle cent1C inE.
    by rewrite conjg_set1 chw ?memJ_norm // (subsetP nHbW1) ?mem_quotient.
  exists (Morphism etaM) => [alpha |]; last first.
    by split=> // h w Hh Ww /=; rewrite qactJ (subsetP nH0W1) -?etaK.
  pose autF (f : {perm F}) := rmorphism f. (* Bits of Galois theory... *)
  have [r prim_r]: {r : F | forall f g, autF f -> autF g -> f r = g r -> f = g}.
    have /cyclicP/sig_eqW[r def_uF] := cyc_uF [set: {unit F}]%G.
    exists (val r) => f g fRM gRM eq_fgr; apply/permP=> a.
    rewrite (_ : f =1 RMorphism fRM) // (_ : g =1 RMorphism gRM) //.
    have [-> | /in_uF_E <-] := eqVneq a 0%R; first by rewrite !rmorph0.
    have /cycleP[m ->]: in_uF a \in <[r]> by rewrite -def_uF inE.
    by rewrite val_unitX !rmorphX /= eq_fgr.
  have /sigW[P /and3P[Pr0 nP lePq]]:
    exists P: {poly F}, [&& root P r, all (mem nF) P & #|root P| <= q].
  - pose Mr := (\matrix_(i < q.+1) (sb *m outF (r ^+ i)))%R.
    have /rowV0Pn[v /sub_kermxP vMr0 nz_v]: kermx Mr != 0%R.
      rewrite kermx_eq0 neq_ltn ltnS (leq_trans (rank_leq_col Mr)) //.
      by rewrite (dim_abelemE abelHbar) // oHb pfactorK.
    pose P : {poly F} := (\poly_(i < q.+1) (v 0 (inord i))%:R)%R.
    have szP: size P <= q.+1 by apply: size_poly.
    exists P; apply/and3P; split.
    + apply/eqP/inj_phi'; congr (inHb _); rewrite rmorph0 mulmx0 -vMr0.
      rewrite horner_poly !raddf_sum mulmx_sum_row; apply: eq_bigr => i _.
      rewrite rowK inord_val //= mulr_natl rmorphMn -scaler_nat scalemxAr.
      by rewrite natr_Zp.
    + apply/(all_nthP 0%R)=> i /leq_trans/(_ szP) le_i_q.
      by rewrite coef_poly /= le_i_q mem_cycle.
    rewrite cardE -ltnS (leq_trans _ szP) //.
    rewrite max_poly_roots ?enum_uniq //; last first.
      by apply/allP=> r'; rewrite mem_enum.
    apply: contraNneq nz_v => /polyP P0; apply/eqP/rowP=> i; apply/eqP.
    have /eqP := P0 i; rewrite mxE coef0 coef_poly ltn_ord inord_val.
    have charF: p \in [char F]%R by rewrite !inE p_pr -order_dvdn -o_nF /=.
    by rewrite -(dvdn_charf charF) (dvdn_charf (char_Fp p_pr)) natr_Zp.
  have{Pr0 nP} fPr0 f: autF f -> root P (f r).
    move=> fRM; suff <-: map_poly (RMorphism fRM) P = P by apply: rmorph_root.
    apply/polyP=> i; rewrite coef_map.
    have [/(nth_default _)-> | lt_i_P] := leqP (size P) i; first exact: rmorph0.
    by have /cycleP[n ->] := all_nthP 0%R nP i lt_i_P; apply: rmorph_nat.
  apply: (iffP morphimP) => [[w _ Ww ->] | alphaRM]; first exact: etaRM.
  suffices /setP/(_ (alpha r)): [set (eta w) r | w in W1] = [set t | root P t].
    rewrite inE fPr0 // => /imsetP[w Ww def_wr]; exists w => //.
    by apply: prim_r => //; apply: etaRM.
  apply/eqP; rewrite eqEcard; apply/andP; split.
    by apply/subsetP=> _ /imsetP[w Ww ->]; rewrite inE fPr0 //; apply: etaRM.
  rewrite (@cardsE F) card_in_imset // => w1 w2 Ww1 Ww2 /= /prim_r eq_w12.
  by apply: (injmP inj_eta) => //; apply: eq_w12; apply: etaRM.
have isoUb: isog Ubar (psi @* U) by rewrite /Ubar -Kpsi first_isog.
pose unF := [set in_uF a | a in nF^#].
have unF_E: {in nF^#, cancel in_uF val} by move=> a /setD1P[/in_uF_E].
have unFg: group_set unF.
  apply/group_setP; split=> [|_ _ /imsetP[a nFa ->] /imsetP[b nFb ->]].
    have nF1: 1%R \in nF^# by rewrite !inE cycle_id oner_eq0.
    by apply/imsetP; exists 1%R => //; apply: val_inj; rewrite unF_E.
  have nFab: (a * b)%R \in nF^#.
    rewrite !inE mulf_eq0 negb_or.
    have [[-> /cycleP[m ->]] [-> /cycleP[n ->]]] := (setD1P nFa, setD1P nFb).
    by rewrite -natrM mem_cycle.
  by apply/imsetP; exists (a * b)%R => //; apply: val_inj; rewrite /= !unF_E.
have <-: #|Group unFg| = p.-1.
  by rewrite -o_nF (cardsD1 1 nF) group1 (card_in_imset (can_in_inj unF_E)).
have <-: #|[set: {unit F}]| = (p ^ q).-1.
  rewrite -oF -(cardC1 1) cardsT card_sub; apply: eq_card => a /=.
  by rewrite !inE unitfE.
rewrite /u (isog_cyclic isoUb) (card_isog isoUb) cyc_uF.
suffices co_u_p1: coprime #|psi @* U| #|Group unFg|.
  by rewrite -(Gauss_dvdr _ co_u_p1) mulnC divnK ?cardSg ?subsetT.
rewrite -(cyclic_dprod (dprodEY _ _)) ?cyc_uF //.
  by rewrite (sub_abelian_cent2 (cyclic_abelian (cyc_uF [set:_]%G))) ?subsetT.
apply/trivgP/subsetP=> _ /setIP[/morphimP[x Nx Ux ->] /imsetP[a nFa /eqP]].
have nCx: x \in 'N(C) by rewrite -Kpsi (subsetP (ker_norm _)).
rewrite -val_eqE (unF_E a) //; case/setD1P: nFa => _ /cycleP[n {a}->].
rewrite zmodXgE => /eqP def_psi_x; rewrite mker ?set11 // Kpsi coset_idr //.
apply/set1P; rewrite -set1gE -(Frobenius_trivg_cent frobUW1c) /= -/C.
rewrite inE mem_quotient //= -sub1set -quotient_set1 ?quotient_cents2r //.
rewrite gen_subG /= -/C -Kpsi; apply/subsetP=> _ /imset2P[_ w /set1P-> Ww ->].
have Uxw: x ^ w \in U by rewrite memJ_norm ?(subsetP nUW1).
apply/kerP; rewrite (morphM, groupM) ?morphV ?groupV //.
apply/(canLR (mulKg _))/val_inj; rewrite psiJ // mulg1 def_psi_x.
exact: (rmorph_nat (RMorphism (etaRM w Ww))).
Qed.

Local Open Scope ring_scope.

Let redM := [predC irr M].
Let mu_ := filter redM (S_ H0).

(* This subproof is shared between (9.8)(b) and (9.9)(b). *)
Let nb_redM_H0 : size mu_ = p.-1 /\ {subset mu_ <= S_ H0C}.
Proof.
have pddM := FT_prDade_hypF maxM MtypeP; pose ptiWM := prDade_prTI pddM.
have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM.
have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU.
have nb_redM K:
  K <| M -> K \subset HU -> K :&: H = H0 -> count redM (S_ K) = p.-1.
- move=> nsKM sKHU tiKHbar; have [sKM nKM] := andP nsKM; pose b L := (L / K)%G.
  have [nsKHU [_ [_ sW2HU cycW2 _] _]] := (normalS sKHU sHUM nsKM, ptiWM).
  have nKW2 := subset_trans sW2HU (normal_norm nsKHU).
  have oW2b: #|b W2| = p.
    have [_ <- _] := Ptype_Fcore_factor_facts; rewrite defW2bar.
    rewrite !card_quotient ?(subset_trans (subset_trans sW2HU sHUM)) //.
    by rewrite -indexgI -{2}(setIidPl sW2H) setIAC -setIA tiKHbar indexgI.
  have{cycW2} cycW2b: cyclic (b W2) by apply: quotient_cyclic.
  have ntW2b: (W2 / K != 1)%g by rewrite -cardG_gt1 oW2b prime_gt1.
  have{ntW2b} [defWb ptiWMb]:= primeTIhyp_quotient ptiWM ntW2b sKHU nsKM.
  pose muK j := (primeTIred ptiWMb j %% K)%CF.
  apply/eqP; have <-: size (image muK (predC1 0)) = p.-1.
    by rewrite size_map -cardE cardC1 card_Iirr_cyclic ?oW2b.
  rewrite -size_filter -uniq_size_uniq ?filter_uniq ?seqInd_uniq // => [|phi].
    by apply/dinjectiveP=> j1 j2 _ _ /(can_inj (cfModK nsKM))/prTIred_inj.
  rewrite mem_filter; apply/imageP/andP=> [[j nz_j ->] | [red_phi]]; last first.
    case/seqIndP=> s /setDP[kerK ker'H] Dphi; rewrite !inE in kerK ker'H.
    pose s1 := quo_Iirr K s; have Ds: s = mod_Iirr s1 by rewrite quo_IirrK.
    rewrite {phi}Dphi Ds mod_IirrE ?cfIndMod // in kerK ker'H red_phi *.
    have{red_phi} red_s1: 'Ind 'chi_s1 \notin irr (M / K) by rewrite -cfMod_irr.
    have [[j Ds1] | [/idPn//]] := prTIres_irr_cases ptiWMb s1.
    rewrite Ds1 cfInd_prTIres -/(muK j) in ker'H *; exists j => //.
    by apply: contraNneq ker'H => ->; rewrite prTIres0 rmorph1 cfker_cfun1.
  have red_j: redM (muK j) by rewrite /redM /= cfMod_irr // prTIred_not_irr.
  have [s DmuKj]: exists s, muK j = 'Ind[M, HU] 'chi_s.
    exists (mod_Iirr (primeTI_Ires ptiWMb j)).
    by rewrite mod_IirrE // cfIndMod // cfInd_prTIres.
  split=> //; apply/seqIndP; exists s; rewrite // !inE andbC.
  rewrite -(@sub_cfker_Ind_irr _ M) ?gFnorm // -DmuKj cfker_mod //=.
  have [[j1 Ds] | [/idPn]] := prTIres_irr_cases ptiWM s; last by rewrite -DmuKj.
  rewrite Ds cfker_prTIres //; apply: contraNneq nz_j => j1_0.
  apply/eqP/(prTIred_inj ptiWMb)/(can_inj (cfModK nsKM)); rewrite -{1}/(muK j).
  by rewrite DmuKj Ds j1_0 -cfInd_prTIres !prTIres0 -cfIndMod ?rmorph1.
have [sH0HU sH0M] := (subset_trans sH0H sHHU, subset_trans sH0H (gFsub _ _)).
have sz_mu: size mu_ = p.-1.
  by rewrite size_filter nb_redM ?(setIidPl sH0H) // /normal sH0M.
have s_muC_mu: {subset filter redM (S_ H0C) <= mu_}.
  move=> phi; rewrite /= !mem_filter => /andP[->]; apply: seqIndS.
  by rewrite setSD // Iirr_kerS ?joing_subl.
have UmuC: uniq (filter redM (S_ H0C)) by rewrite filter_uniq ?seqInd_uniq.
have [|Dmu _] := leq_size_perm UmuC s_muC_mu; last first.
  by split=> // phi; rewrite -Dmu mem_filter => /andP[].
have [nsH0C_M _ _ _] := nsH0xx_M.
have sCHU := subset_trans sCU sUHU; have sCM := subset_trans sCHU sHUM.
have sHOC_HU: H0C \subset HU by apply/joing_subP.
rewrite sz_mu size_filter nb_redM //= norm_joinEr ?(subset_trans sCM) //.
by rewrite -group_modl //= setIC [C]unlock setIA tiHU setI1g mulg1.
Qed.

Let isIndHC (zeta : 'CF(M)) :=
  [/\ zeta 1%g = (q * u)%:R, zeta \in S_ H0C
    & exists2 xi : 'CF(HC), xi \is a linear_char & zeta = 'Ind xi].

(* This is Peterfalvi (9.8). *)
Lemma typeP_nonGalois_characters (not_Galois : ~~ typeP_Galois) :
    let a := #|U : 'C_U(sval (typeP_Galois_Pn not_Galois) | 'Q)| in
  [/\ (*a*) {in X_ H0, forall s, (a %| 'chi_s 1%g)%C},
      (*b*) size mu_ = p.-1 /\ {in mu_, forall mu_j, isIndHC mu_j},
      (*c*) exists t, isIndHC 'chi_t
    & (*d*) let irr_qa := [pred zeta in irr M | zeta 1%g == (q * a)%:R] in
            let lb_n := (p.-1 * #|U|)%N in let lb_d := (a ^ 2 * #|U'|)%N in
            (lb_d %| lb_n /\ lb_n %/ lb_d <= count irr_qa (S_ H0U'))%N].
Proof.
case: (typeP_Galois_Pn _) => H1 [oH1 nH1U nH1Uq defHbar aP]; rewrite [sval _]/=.
move => a; case: aP; rewrite -/a => a_gt1 a_dv_p1 cycUb1 isoUb.
set part_a := ({in _, _}); pose HCbar := (HC / H0)%G.
have [_ /mulG_sub[sHUM sW1M] nHUW1 tiHUW1] := sdprodP defM.
have [nsHHU _ /mulG_sub[sHHU sUHU] nHU tiHU] := sdprod_context defHU.
have [nH0H nHHU] := (normal_norm nsH0H, normal_norm nsHHU).
have sHHC: H \subset HC by rewrite joing_subl.
have [nH0HU sCHU] := (subset_trans sHUM nH0M, subset_trans sCU sUHU).
have nsH0_HU: H0 <| HU by rewrite /normal (subset_trans sH0H).
have nH0C := subset_trans sCHU nH0HU.
have [nsH0C_M nsHC_M nsH0U'_M _] := nsH0xx_M; have [sHC_M _] := andP nsHC_M.
have nsH0HC: H0 <| HC := normalS (subset_trans sH0H sHHC) sHC_M nsH0M.
have defHCbar: Hbar \x (C / H0) = HCbar.
  rewrite /= quotientY // [C]unlock /= astabQ quotient_setIpre.
  by rewrite dprodEY ?subsetIr // setIA -quotientGI // tiHU quotient1 setI1g.
have sHC_HU: HC \subset HU by rewrite join_subG sHHU.
have nsHC_HU: HC <| HU := normalS sHC_HU sHUM nsHC_M.
have defHb1 := defHbar; rewrite (big_setD1 1%g) ?group1 ?conjsg1 //= in defHb1.
have [[_ H1c _ defH1c] _ _ _] := dprodP defHb1; rewrite defH1c in defHb1.
have [nsH1H _] := dprod_normal2 defHb1; have [sH1H nH1H] := andP nsH1H.
have nHW1: W1 \subset 'N(H) := subset_trans sW1M (gFnorm _ _).
have nHbW1: W1bar \subset 'N(Hbar) by rewrite quotient_norms.
have sH1wH w: w \in W1bar -> H1 :^ w \subset Hbar.
  by move/(normsP nHbW1) <-; rewrite conjSg.
have nsH1wHUb w: w \in W1bar -> H1 :^ w <| HU / H0.
  move=> W1w; rewrite -(normsP (quotient_norms _ nHUW1) w W1w) normalJ.
  rewrite /normal (subset_trans sH1H) ?quotientS //.
  by rewrite -defHU sdprodE // quotientMl // mulG_subG nH1H.
have nH1wHUb := normal_norm (nsH1wHUb _ _).
have Part_a: part_a.
  move=> s; rewrite !inE => /andP[kers'H kersH0].
  have [t sHt] := constt_cfRes_irr H s; pose theta := ('chi_t / H0)%CF.
  have{kers'H} t_neq0: t != 0.
    by rewrite -subGcfker (sub_cfker_constt_Res_irr sHt).
  have{kersH0} kertH0: H0 \subset cfker 'chi_t.
    by rewrite (sub_cfker_constt_Res_irr sHt).
  have Ltheta: theta \is a linear_char.
    by rewrite /theta -quo_IirrE // (char_abelianP _ _). 
  have Dtheta : _ = theta := cfBigdprod_Res_lin defHbar Ltheta.
  set T := 'I_HU['chi_t]; have sHT: H \subset T by rewrite sub_Inertia.
  have sTHU: T \subset HU by rewrite Inertia_sub.
  suffices{s sHt} a_dv_iTHU: a %| #|HU : T|.
    have [_ defInd_t _ imInd_t _] := cfInd_sum_Inertia t nsHHU.
    have /imsetP[r tTr ->]: s \in Ind_Iirr HU @: irr_constt ('Ind[T] 'chi_t).
      by rewrite imInd_t constt_Ind_Res.
    by rewrite defInd_t ?cfInd1 // dvdC_mulr ?dvdC_nat // Cint_Cnat ?Cnat_irr1.
  have /exists_inP[w W1w nt_t_w]: [exists w in W1bar, 'Res[H1 :^ w] theta != 1].
    rewrite -negb_forall_in; apply: contra t_neq0 => /forall_inP=> tH1w1.
    rewrite -irr_eq1 -(cfQuoK nsH0H kertH0) -/theta -Dtheta.
    rewrite [cfBigdprod _ _]big1 ?rmorph1 // => w /tH1w1/eqP->.
    by rewrite /cfBigdprodi rmorph1.
  have defT: H ><| (U :&: T) = T.
    by rewrite (sdprod_modl defHU) // (setIidPr sTHU).
  have /irrP[k Dk]: 'Res theta \in irr (H1 :^ w).
    by rewrite lin_char_irr ?cfRes_lin_char.
  rewrite -divgS // -(sdprod_card defHU) -(sdprod_card defT) divnMl // divgI.
  rewrite -indexgI; have ->: a = #|U : 'C_U(H1 :^ w | 'Q)|.
    have [w1 nH0w1 W1w1 ->] := morphimP W1w; rewrite astabQ centJ morphpreJ //.
    by rewrite -astabQ indexgI -(normsP nUW1 _ W1w1) indexJg -indexgI.
  rewrite indexgS ?setIS // sub_astabQ ?(subset_trans sTHU) //= -inertia_quo //.
  apply: subset_trans (sub_inertia_Res _ (nH1wHUb w W1w)) _.
  by rewrite Dk (inertia_irr_prime _ p_pr) ?subsetIr ?cardJg // -irr_eq1 -Dk.
pose isoJ := conj_isom H1; pose cfJ w i := 'chi_(isom_Iirr (isoJ w) i).
pose thetaH (f : {ffun _}) := cfBigdprod defHbar (fun w => cfJ w (f w)).
pose theta f := cfDprodl defHCbar (thetaH f).
have abH1: abelian H1 by rewrite cyclic_abelian ?prime_cyclic ?oH1.
have linH1 i: 'chi[H1]_i \is a linear_char by apply/char_abelianP.
have lin_thetaH f: thetaH f \is a linear_char.
  by apply: cfBigdprod_lin_char => w _; rewrite /cfJ isom_IirrE cfIsom_lin_char.
have nz_thetaH f: thetaH f 1%g != 0 by rewrite lin_char_neq0.
have Dtheta f: {in W1bar & H1, forall w xb, theta f (xb ^ w) = 'chi_(f w) xb}.
  move=> w xb W1w H1xb /=; have sHHCb := quotientS H0 sHHC.
  transitivity ('Res[H1 :^ w] ('Res[Hbar] (theta f)) (xb ^ w)); last first.
    by rewrite cfDprodlK cfBigdprodKabelian // isom_IirrE cfIsomE.
  by rewrite cfResRes ?sH1wH // cfResE ?memJ_conjg ?(subset_trans (sH1wH w _)).
have lin_theta f: theta f \is a linear_char by rewrite cfDprodl_lin_char.
pose Ftheta := pffun_on (0 : Iirr H1) W1bar (predC1 0).
have inj_theta: {in Ftheta &, injective theta}.
  move=> f1 f2 /pffun_onP[/supportP W1f1 _] /pffun_onP[/supportP W1f2 _] eq_f12.
  apply/ffunP=> w.
  have [W1w | W1'w] := boolP (w \in W1bar); last by rewrite W1f1 ?W1f2.
  by apply/irr_inj/cfun_inP=> x H1x; rewrite -!Dtheta ?eq_f12.
have irr_thetaH0 f: (theta f %% H0)%CF \in irr HC.
  by rewrite cfMod_irr ?lin_char_irr.
have def_Itheta f: f \in Ftheta -> 'I_HU[theta f %% H0]%CF = HC.
  case/pffun_onP=> _ nz_fW1; apply/eqP; rewrite eqEsubset sub_Inertia //.
  rewrite inertia_mod_pre //= -{1}(sdprodW defHU) -group_modl; last first.
    rewrite (subset_trans sHHC) // -sub_quotient_pre ?normal_norm //.
    by rewrite sub_Inertia ?quotientS.
  rewrite -gen_subG genM_join genS ?setUS //= {2}[C]unlock setIS //= astabQ.
  rewrite morphpreS // centsC -{1}(bigdprodWY defHbar) gen_subG.
  apply/bigcupsP=> w W1w; rewrite centsC.
  apply: subset_trans (sub_inertia_Res _ (quotient_norms _ nHHU)) _.
  rewrite cfDprodlK inertia_bigdprod_irr // subIset // orbC (bigcap_min w) //.
  rewrite (inertia_irr_prime _ p_pr) ?cardJg ?subsetIr // isom_Iirr_eq0.
  by apply: nz_fW1; apply: image_f.
have irrXtheta f: f \in Ftheta -> 'Ind (theta f %% H0)%CF \in irr HU.
  move/def_Itheta; rewrite -(cfIirrE (irr_thetaH0 f)) => I_f_HC.
  by rewrite inertia_Ind_irr ?I_f_HC //.
pose Mtheta := [set cfIirr (theta f %% H0)%CF | f in Ftheta].
pose Xtheta := [set cfIirr ('Ind[HU] 'chi_t) | t in Mtheta].
have oXtheta: (u * #|Xtheta| = p.-1 ^ q)%N.
  transitivity #|Ftheta|; last first.
    rewrite card_pffun_on cardC1 card_Iirr_abelian // oH1.
    rewrite -(card_isog (quotient_isog _ _)) ?oW1 ?(subset_trans sW1M) //.
    by apply/trivgP; rewrite -tiHUW1 setSI ?(subset_trans sH0H).
  rewrite Du -card_imset_Ind_irr ?card_in_imset //.
  - move=> f1 f2 Df1 Df2 /(congr1 (tnth (irr HC))); rewrite !{1}cfIirrE //.
    by move/(can_inj (cfModK nsH0HC)); apply: inj_theta.
  - by move=> _ /imsetP[f Df ->]; rewrite cfIirrE ?irrXtheta.
  move=> _ y /imsetP[f /familyP Ff ->] HUy; apply/imsetP.
  pose yb := inMb y; have HUyb: yb \in (HU / H0)%g by apply: mem_quotient.
  have nHb_y: inMb y \in 'N(Hbar) by rewrite (subsetP (quotient_norms _ nHHU)).
  have nH1b_y := subsetP (nH1wHUb _ _) yb HUyb.
  exists [ffun w => conjg_Iirr (f w) (inMb y ^ w^-1)].
    apply/familyP=> w; rewrite ffunE.
    by case: ifP (Ff w) => _; rewrite !inE conjg_Iirr_eq0.
  apply: irr_inj; rewrite !(cfIirrE, conjg_IirrE) // (cfConjgMod _ nsHC_HU) //.
  rewrite cfConjgDprodl //; first congr (cfDprodl _ _ %% H0)%CF; last first.
    rewrite /= -quotientYidl // (subsetP _ _ HUyb) ?quotient_norms //.
    by rewrite (subset_trans sHUM) ?normal_norm.
  rewrite cfConjgBigdprod //; apply: eq_bigr => w W1w; congr (cfBigdprodi _ _).
  rewrite ffunE /cfJ !isom_IirrE conjg_IirrE.
  apply/cfun_inP=> _ /imsetP[x Hx ->]; rewrite cfIsomE // cfConjgE ?nH1b_y //.
  rewrite -conjgM conjgCV conjVg conjgM cfIsomE //; last first.
    by rewrite -mem_conjg (normP _) // -mem_conjg -normJ ?nH1b_y.
  by rewrite cfConjgE // -mem_conjg -normJ ?nH1b_y.
have sXthXH0C: Xtheta \subset X_ H0C.
  apply/subsetP=> _ /imsetP[t Mt ->]; have{Mt} [f Ff Dt] := imsetP Mt.
  rewrite !inE cfIirrE; last by rewrite Dt cfIirrE ?irrXtheta.
  rewrite !sub_cfker_Ind_irr ?(subset_trans sHUM) ?normal_norm ?gFnormal //.
  rewrite {t}Dt cfIirrE // join_subG andbCA {1}cfker_mod //.
  rewrite !{1}sub_cfker_mod //= andbC {1}cfker_sdprod /=.
  apply: contraL (familyP Ff 1%g) => kerHb; rewrite group1 negbK.
  have:= sub_cfker_Res (subxx _) kerHb; rewrite cfDprodlK.
  move/(subset_trans (sH1wH _ (group1 _)))/(sub_cfker_Res (subxx _)).
  rewrite cfBigdprodKabelian // isom_IirrE cfker_isom morphim_conj /=.
  by rewrite !conjsg1 subsetIidl subGcfker.
pose mu_f (i : Iirr H1) := [ffun w => if w \in W1bar then i else 0].
have Fmu_f (i : Iirr H1): i != 0 -> mu_f i \in Ftheta.
  by move=> nz_i; apply/familyP=> w; rewrite ffunE; case: ifP; rewrite !inE.
pose mk_mu i := 'Ind[HU] (theta (mu_f i) %% H0)%CF.
have sW1_Imu i: W1 \subset 'I[theta (mu_f i) %% H0]%CF.
  apply/subsetP=> w W1w; have Mw := subsetP sW1M w W1w.
  have nHC_W1 := subset_trans sW1M (normal_norm nsHC_M).
  rewrite inE (subsetP nHC_W1) ?(cfConjgMod _ nsHC_M) //; apply/eqP.
  have W1wb: inMb w \in W1bar by rewrite mem_quotient.
  rewrite cfConjgDprodl ?(subsetP _ _ W1wb) ?quotient_norms //; last first.
    by rewrite (subset_trans (joing_subr U W1)) ?normal_norm.
  congr (cfDprodl _ _ %% H0)%CF.
  apply/cfun_inP=> _ /(mem_bigdprod defHbar)[x [H1x -> _]].
  have Hx w1: w1 \in W1bar -> x w1 \in Hbar.
    by move=> W1w1; rewrite (subsetP (sH1wH w1 _)) ?H1x.
  rewrite !lin_char_prod ?cfConjg_lin_char //; apply/eq_bigr=> w1 W1w1.
  rewrite cfConjgE ?(subsetP nHbW1) //.
  have W1w1w: (w1 * (inMb w)^-1)%g \in W1bar by rewrite !in_group.
  rewrite -(cfResE _ (sH1wH _ W1w1w)) -?mem_conjg -?conjsgM ?mulgKV ?H1x //.
  rewrite -(cfResE _ (sH1wH _ W1w1)) ?H1x ?cfBigdprodKabelian //.
  rewrite !ffunE W1w1 W1w1w -[x w1](conjgKV w1) -conjgM !isom_IirrE.
  by rewrite !cfIsomE -?mem_conjg ?H1x.
have inj_mu: {in predC1 0 &, injective (fun i => cfIirr (mk_mu i))}.
  move=> i1 i2 nz_i1 nz_i2 /(congr1 (tnth (irr HU))).
  rewrite !{1}cfIirrE ?irrXtheta ?Fmu_f // /mk_mu.
  do 2![move/esym; rewrite -{1}(cfIirrE (irr_thetaH0 _))].
  move/(cfclass_Ind_irrP _ _ nsHC_HU); rewrite !{1}cfIirrE //.
  case/cfclassP=> _ /(mem_sdprod defHU)[x [y [Hx Uy -> _]]].
  rewrite (cfConjgM _ nsHC_HU) ?(subsetP sHHU x) ?(subsetP sUHU) //.
  rewrite {x Hx}(cfConjg_id _ (subsetP sHHC x Hx)) => Dth1.
  suffices /setIP[_ /inertiaJ]: y \in 'I_HU[theta (mu_f i2) %% H0]%CF.
    rewrite -Dth1 => /(can_inj (cfModK nsH0HC))/inj_theta/ffunP/(_ 1%g).
    by rewrite !ffunE group1 => -> //; apply: Fmu_f.
  rewrite def_Itheta ?Fmu_f //= (subsetP (joing_subr _ _)) //.
  have nCy: y \in 'N(C).
    by rewrite (subsetP (normal_norm nsCUW1)) ?mem_gen ?inE ?Uy.
  have [_ _ /trivgPn[wb W1wb ntwb] _ _] := Frobenius_context frobUW1c.
  have /morphimP[w nCw W1w Dw] := W1wb; have Mw := subsetP sW1M w W1w.
  rewrite coset_idr //; apply/set1P; rewrite -set1gE; apply: wlog_neg => nty.
  rewrite -((Frobenius_reg_ker frobUW1c) wb); last by rewrite !inE ntwb.
  rewrite inE mem_quotient //=; apply/cent1P/commgP.
  rewrite Dw -morphR //= coset_id //.
  suffices: [~ y, w] \in U :&: HC.
    rewrite /= norm_joinEr ?(subset_trans sCU) // -group_modr ?subsetIl //=.
    by rewrite setIC tiHU mul1g.
  have Uyw: [~ y, w] \in U; last rewrite inE Uyw.
    by rewrite {1}commgEl groupMl ?groupV // memJ_norm ?(subsetP nUW1) // Uy.
  rewrite -(def_Itheta _ (Fmu_f _ nz_i1)) 2!inE /= andbA -in_setI.
  rewrite (setIidPl (normal_norm nsHC_HU)) (subsetP sUHU) //=.
  rewrite Dth1 -(cfConjgM _ nsHC_HU) ?(subsetP sUHU) //.
  have My: y \in M := subsetP (subset_trans sUHU sHUM) y Uy.
  rewrite mulKVg (cfConjgM _ nsHC_M) ?in_group //.
  have /inertiaJ-> := subsetP (sW1_Imu i2) _ (groupVr W1w).
  rewrite (cfConjgM _ nsHC_M) // -Dth1.
  by have /inertiaJ-> := subsetP (sW1_Imu i1) w W1w.
pose Xmu := [set cfIirr (mk_mu i) | i in predC1 0].
have def_IXmu: {in Xmu, forall s, 'I_M['chi_s] = M}.
  move=> _ /imsetP[i nz_i ->]; apply/setIidPl.
  rewrite -subsetIidl -{1}(sdprodW defM) mulG_subG sub_Inertia //.
  rewrite !cfIirrE ?irrXtheta ?Fmu_f //=.
  apply: subset_trans (sub_inertia_Ind _ (der_norm 1 M)).
  by rewrite subsetI sW1M /=.
pose Smu := [seq 'Ind[M] 'chi_s | s in Xmu].
have sSmu_mu: {subset Smu <= mu_}.
  move=> _ /imageP[s Xmu_s ->]; rewrite mem_filter /=.
  rewrite irrEchar cfnorm_Ind_irr ?gFnormal // def_IXmu //.
  rewrite -(index_sdprod defM) (eqC_nat _ 1) gtn_eqF ?prime_gt1 // andbF.
  rewrite mem_seqInd ?gFnormal /normal ?(subset_trans sH0H) ?gFsub //=.
  suffices /(subsetP sXthXH0C): s \in Xtheta.
    by apply: subsetP; rewrite setSD // Iirr_kerS ?joing_subl.
  have /imsetP[i nz_i ->] := Xmu_s; rewrite /Xtheta -imset_comp.
  by apply/imsetP; exists (mu_f i); rewrite /= ?cfIirrE ?Fmu_f.
have ResIndXmu: {in Xmu, forall s, 'Res ('Ind[M] 'chi_s) = q%:R *: 'chi_s}.
  move=> s /def_IXmu Imu_s; rewrite cfResInd_sum_cfclass ?gFnormal ?Imu_s //.
  by rewrite -(index_sdprod defM) -Imu_s cfclass_inertia big_seq1.
have uSmu: uniq Smu.
  apply/dinjectiveP=> s1 s2 Xs1 Xs2 /(congr1 'Res[HU]); rewrite !ResIndXmu //.
  by move/(can_inj (scalerK (neq0CG W1)))/irr_inj.
have sz_Smu: size Smu = p.-1.
  by rewrite size_map -cardE card_in_imset // cardC1 card_Iirr_abelian ?oH1.
have [sz_mu s_mu_H0C] := nb_redM_H0.
have Dmu: Smu =i mu_.
  by have [|//] := leq_size_perm uSmu sSmu_mu; rewrite sz_mu sz_Smu.
split=> {Part_a part_a}//.
- split=> // phi mu_phi; have S_HOC_phi := s_mu_H0C _ mu_phi.
  move: mu_phi; rewrite -Dmu => /imageP[_ /imsetP[i nz_i ->]].
  rewrite cfIirrE ?irrXtheta ?Fmu_f // => Dphi.
  split=> //; rewrite Dphi ?cfInd1 ?cfIndInd //.
    rewrite -(index_sdprod defM) -/q -Du mulrA -natrM.
    by rewrite lin_char1 1?cfMod_lin_char ?mulr1.
  by exists (theta (mu_f i) %% H0)%CF; rewrite 1?cfMod_lin_char.
- have /eqVproper: Xmu \subset Xtheta.
    apply/subsetP=> _ /imsetP[i nz_i ->]; rewrite -[Xtheta]imset_comp /=.
    by apply/imsetP; exists (mu_f i); rewrite /= ?cfIirrE ?Fmu_f.
  case=> [defXmu | /andP[_ /subsetPn[s theta_s Xmu'_s]]]; last first.
    have [_ /imsetP[f Dth_f ->] Ds] := imsetP theta_s; rewrite cfIirrE // in Ds.
    have /irrP[t Dt]: 'Ind 'chi_s \in irr M; last 1 [exists t; rewrite -{t}Dt].
      apply: contraR Xmu'_s => red_Ind_s.
      have: 'Ind 'chi_s \in mu_.
        rewrite mem_filter /= red_Ind_s mem_seqInd ?gFnormal //=.
        apply: subsetP theta_s; rewrite (subset_trans  sXthXH0C) ?setSD //.
        by rewrite Iirr_kerS ?joing_subl.
      rewrite -Dmu => /imageP[s1 Xmu_s1] /(congr1 (cfdot ('Ind 'chi_s1)))/eqP.
      rewrite cfnorm_Ind_irr ?gFnormal // eq_sym -cfdot_Res_l.
      rewrite ResIndXmu // cfdotZl cfdot_irr -natrM mulnC.
      by case: (s1 =P s) => [<- // | _] /idPn[]; apply: neq0CiG.
    split; first 2 [by rewrite mem_seqInd ?gFnormal ?(subsetP sXthXH0C)].
      rewrite Ds cfIirrE ?irrXtheta ?cfInd1 // -Du -(index_sdprod defM) -/q.
      by rewrite mulrA -natrM lin_char1 ?cfMod_lin_char ?mulr1.
    exists (theta f %% H0)%CF; first by rewrite cfMod_lin_char.
    by rewrite Ds  cfIirrE ?irrXtheta //= cfIndInd.
  suffices /(congr1 odd): u = (p.-1 ^ q.-1)%N.
    rewrite odd_exp -(subnKC (prime_gt1 pr_q)) /= -subn1 odd_sub ?prime_gt0 //.
    by rewrite -oH1 (oddSg sH1H) ?quotient_odd // mFT_odd.
  have p1_gt0: (0 < p.-1)%N by rewrite -(subnKC (prime_gt1 p_pr)).
  apply/eqP; rewrite -(eqn_pmul2r p1_gt0) -expnSr prednK ?prime_gt0 //. 
  by rewrite -oXtheta -defXmu card_in_imset // cardC1 card_Iirr_abelian ?oH1.
clear Xmu def_IXmu Smu sSmu_mu ResIndXmu uSmu sz_Smu sz_mu s_mu_H0C Dmu.
clear Mtheta Xtheta irrXtheta oXtheta sXthXH0C mu_f Fmu_f mk_mu sW1_Imu inj_mu.
clear nz_thetaH lin_thetaH lin_theta Ftheta inj_theta irr_thetaH0 def_Itheta. 
clear theta Dtheta => irr_qa lb_n lb_d.
have sU'U: U' \subset U := der_sub 1 U.
have nH0U := subset_trans sUHU nH0HU; have nH0U' := subset_trans sU'U nH0U.
have sU'CH1: U' \subset 'C_U(H1 | 'Q).
  by rewrite subsetI sU'U sub_astabQ nH0U' (centsS sH1H) ?quotient_cents.
have sCH1_U: 'C_U(H1 | 'Q) \subset U := subsetIl U _.
have dvd_lb: lb_d %| lb_n.
  rewrite -[lb_d]mulnA dvdn_mul // -(Lagrange sCH1_U).
  by rewrite mulnC dvdn_pmul2r ?cardSg ?indexg_gt0.
split; rewrite ?leq_divLR // /lb_n -(Lagrange sCH1_U) -/a -(Lagrange sU'CH1).
rewrite mulnCA -mulnA mulnC !mulnA !leq_pmul2r ?cardG_gt0 ?indexg_gt0 // mulnC.
pose H1CH1 := (H1 <*> 'C_(U / H0)(H1))%G; pose HCH1 := (H <*> 'C_U(H1 | 'Q))%G.
have defH1CH1: H1 \x 'C_(U / H0)(H1) = H1CH1.
  rewrite dprodEY ?subsetIr ?coprime_TIg ?(coprimeSg sH1H) //.
  by rewrite (coprimegS (subsetIl _ _)) ?coprime_morph.
have sHCH1_HU: HCH1 \subset HU by rewrite join_subG sHHU (subset_trans sCH1_U).
have nsHCH1_HU: HCH1 <| HU.
  rewrite /normal sHCH1_HU -(sdprodW defHU) mulG_subG normsG ?joing_subl //=.
  by rewrite normsY // sub_der1_norm.
have nsH0_HCH1: H0 <| HCH1.
  by rewrite (normalS _ sHCH1_HU) // (subset_trans sH0H) ?joing_subl.
have nsH1cHU: H1c <| HU / H0.
  rewrite -(bigdprodWY defH1c) /normal gen_subG norms_gen ?andbT //.
    by apply/bigcupsP=> w /setD1P[_ /nsH1wHUb/andP[]].
  by apply/norms_bigcup/bigcapsP=> w /setD1P[_ /nH1wHUb].
have defHCH1: H1c ><| H1CH1 = (HCH1 / H0)%G.
  have /sdprodP[_ /mulG_sub[sH1cH _] nH1cH1 tiH1cH1] := dprodWsdC defHb1.
  rewrite sdprodE /= -(dprodW defH1CH1).
  - rewrite mulgA (dprodWC defHb1) -morphim_setIpre -astabQ -quotientMl //.
    by rewrite norm_joinEr // (subset_trans sCH1_U).
  - rewrite mul_subG ?subIset // (subset_trans (quotientS _ sUHU)) //.
    exact: normal_norm nsH1cHU.
  rewrite -(setIidPl sH1cH) setIAC -setIA -group_modl // coprime_TIg ?mulg1 //.
  by rewrite coprime_sym (coprimegS (subsetIl _ _)) ?coprime_morph.
have [nsH1cHCH1 sH1CH1_HCH1 _ nH1cH1C _] := sdprod_context defHCH1.
pose Clam := ('C_(U / H0)(H1) / (U' / H0))%G.
pose lam (j : Iirr Clam) := 'chi_(mod_Iirr j).
pose theta i j := cfSdprod defHCH1 (cfDprod defH1CH1 'chi_i (lam j)).
have nsU'CH1: U' <| 'C_U(H1 | 'Q) by rewrite (normalS _ sCH1_U) ?gFnormal.
have nsU'CH1b: U' / H0 <| 'C_(U / H0)(H1).
  by rewrite -morphim_setIpre -astabQ quotient_normal.
have abClam: abelian Clam.
  by rewrite sub_der1_abelian //= quotient_der ?dergS ?subsetIl.
have lam_lin j: lam j \is a linear_char.
  by rewrite /lam mod_IirrE ?cfMod_lin_char //; apply/char_abelianP.
have theta_lin i j: theta i j \is a linear_char.
  by rewrite cfSdprod_lin_char ?cfDprod_lin_char.
have <-: #|Clam| = #|'C_U(H1 | 'Q) : U'|.
  rewrite -card_quotient ?normal_norm //= /= -morphim_setIpre -astabQ.
  have nsU'U : U' <| U by apply: der_normal.
  rewrite -(restrmEsub _ _ sCH1_U) -(restrm_quotientE _ sU'U) -morphim_quotm.
  rewrite card_injm ?quotientS ?injm_quotm ?(isom_inj (quotient_isom _ _)) //.
  by rewrite coprime_TIg ?(coprimeSg sH0H).
pose Mtheta := [set mod_Iirr (cfIirr (theta i j)) | i in [set~ 0], j in setT].
have ->: (p.-1 * #|Clam|)%N = #|Mtheta|.
  rewrite [Mtheta]curry_imset2X card_imset ?cardsX => [|[i1 j1] [i2 j2] /=/eqP].
    by rewrite cardsC1 cardsT !card_Iirr_abelian ?(abelianS sH1H) ?oH1.
  rewrite (can_eq (mod_IirrK _)) // -(inj_eq irr_inj) !cfIirrE ?lin_char_irr //.
  rewrite (can_eq (cfSdprodK _)) -!dprod_IirrE (inj_eq irr_inj).
  by rewrite (can_eq (dprod_IirrK _)) => /eqP[->] /(can_inj (mod_IirrK _))->.
have{lam_lin} thetaH1 i j: 'Res[H1] (theta i j) = 'chi_i.
  rewrite -(cfResRes _ _ sH1CH1_HCH1) ?joing_subl // cfSdprodK cfDprodKl //.
  exact: lin_char1.
have Itheta r: r \in Mtheta -> 'I_HU['chi_r]%CF = HCH1.
  case/imset2P=> i j; rewrite /= in_setC1 => nz_i _ Dr; apply/eqP.
  rewrite eqEsubset sub_Inertia //= Dr mod_IirrE // cfIirrE ?lin_char_irr //.
  rewrite andbT -(quotientSGK _ (normal_sub nsH0_HCH1)) ?subIset ?nH0HU //. 
  rewrite inertia_mod_quo //.
  apply: subset_trans (sub_inertia_Res _ (nH1wHUb _ (group1 _))) _.
  rewrite /= conjsg1 thetaH1 (inertia_irr_prime _ p_pr) //.
  rewrite -quotient_setIpre -astabQ quotientS // -{1}(sdprodW defHU).
  by rewrite -genM_join sub_gen // group_modl // sub_astabQ nH0H (centsS sH1H).
have irr_Xtheta: {in Mtheta, forall r, 'Ind[HU] 'chi_r \in irr HU}.
  by move=> r Mr; rewrite /= inertia_Ind_irr ?Itheta.
pose Xtheta := [set cfIirr ('Ind[HU] 'chi_r) | r in Mtheta].
have Da: a = #|HU : HCH1| by rewrite -(index_sdprodr defHU).
have Xtheta_1: {in Xtheta, forall s, 'chi_s 1%g = a%:R}.
  move=> _ /imsetP[r Mr ->]; have /imset2P[i j _ _ Dr] := Mr.
  rewrite cfIirrE ?irr_Xtheta ?cfInd1 //= -Da lin_char1 ?mulr1 //.
  by rewrite Dr mod_IirrE ?cfMod_lin_char // cfIirrE ?lin_char_irr.
have nsH0U'HU: H0U' <| HU.
  by apply: normalS nsH0U'_M; rewrite // -(sdprodWY defHU) genS ?setUSS.
have sXthetaXH0U': Xtheta \subset X_ H0U'.
  apply/subsetP=> _ /imsetP[r Mr ->]; have [i j nz_i _ Dr] := imset2P Mr.
  rewrite !inE cfIirrE ?irr_Xtheta ?sub_cfker_Ind_irr //= ?normal_norm //.
  rewrite Dr mod_IirrE // cfIirrE ?lin_char_irr // join_subG andbCA.
  rewrite {1}cfker_mod //= !{1}sub_cfker_mod //; apply/andP; split; last first.
    rewrite -(sdprodWY (sdprod_cfker _ _)) sub_gen ?subsetU // orbC.
    rewrite (subset_trans _ (cfker_dprod _ _ _)) // sub_gen ?subsetU // orbC.
    by rewrite /lam mod_IirrE ?cfker_mod.
  apply: contraL nz_i => /(subset_trans sH1H); rewrite !inE negbK.
  by move/(sub_cfker_Res (subxx _)); rewrite thetaH1 subGcfker.
have nsCH1_U: 'C_U(H1 | 'Q) <| U by rewrite sub_der1_normal.
have nH1cU: (U / H0)%g \subset 'N(H1c).
  rewrite -(bigdprodWY defH1c) norms_gen ?norms_bigcup //.
  apply/bigcapsP=> w /setD1P[_ W1w].
  by rewrite normJ -sub_conjgV (normsP (quotient_norms H0 nUW1)) ?groupV.
have ->: #|Mtheta| = (#|Xtheta| * a)%N.
  rewrite Da mulnC -card_imset_Ind_irr // => _ xy /imset2P[i j nz_i _ ->].
  case/(mem_sdprod defHU)=> x [y [Hx Uy -> _]]; have HUy := subsetP sUHU y Uy.
  pose yb := inMb y; have Uyb: yb \in (U / H0)%g by rewrite mem_quotient.
  pose iy := conjg_Iirr i yb; pose jy := conjg_Iirr j (coset (U' / H0)%g yb).
  apply/imset2P; exists iy jy; rewrite !inE ?conjg_Iirr_eq0 // in nz_i *.
  apply: irr_inj; have HCH1x: x \in HCH1 by rewrite mem_gen ?inE ?Hx.
  rewrite conjg_IirrE (cfConjgM _ nsHCH1_HU) ?(subsetP sHHU x) {Hx}//.
  rewrite {x HCH1x}(cfConjg_id _ HCH1x) !{1}mod_IirrE //.
  rewrite !{1}cfIirrE ?lin_char_irr //.
  rewrite cfConjgMod_norm ?(subsetP nH0U) ?(subsetP (normal_norm nsHCH1_HU)) //.
  have nCH1_Ub: (U / H0)%g \subset 'N('C_(U / H0)(H1)).
    by rewrite normsI ?normG ?norms_cent.
  rewrite cfConjgSdprod ?cfConjgDprod ?(subsetP _ _ Uyb) ?normsY //.
  rewrite /theta /lam !{1}mod_IirrE // !{1}conjg_IirrE.
  by rewrite cfConjgMod_norm ?(subsetP _ _ Uyb) // quotient_norms ?gFnorm.
rewrite leq_pmul2r ?indexg_gt0 // cardE -(size_map (fun s => 'Ind[M] 'chi_s)).
have kerH1c s: s \in Xtheta -> H1c \subset (cfker 'chi_s / H0)%g.
  case/imsetP=> r Mr {s}->; have [i j _ _ Dr] := imset2P Mr.
  rewrite -(setIidPr (normal_sub nsH1cHCH1)) -morphim_setIpre quotientS //.
  rewrite cfIirrE ?irr_Xtheta ?sub_cfker_Ind_irr //; last first.
    by rewrite normsI ?normal_norm // -(quotientGK nsH0_HU) cosetpre_normal.
  rewrite Dr mod_IirrE // cfker_morph ?normal_norm // cfIirrE ?lin_char_irr //.
  by rewrite setIS ?joing_subl ?morphpreS // cfker_sdprod.
have injXtheta:
  {in M & Xtheta &, forall w s1 s2, 'chi_s1 = 'chi_s2 ^ w -> w \in HU}%CF.
- move=> _ s1 s2 /(mem_sdprod defM)[y [w [HUy W1w -> _]]] Xs1 Xs2.
  rewrite groupMl // cfConjgMnorm ?(subsetP (normG _) y) ?(subsetP nHUW1) //.
  rewrite {y HUy}(cfConjg_id _ HUy) => Ds1.
  have nH0w: w \in 'N(H0) by rewrite ?(subsetP nH0M) ?(subsetP sW1M).
  rewrite (subsetP (normal_sub nsH0_HU)) // coset_idr //.
  have /setDP[]:= subsetP sXthetaXH0U' s1 Xs1; rewrite !inE join_subG /=.
  case/andP=> kerH0s1 _; apply: contraNeq; rewrite -eq_invg1 => ntw.
  rewrite -(quotientSGK nH0H) // -(dprodW defHb1) mul_subG ?kerH1c //=.
  rewrite Ds1 cfker_conjg ?(subsetP nHUW1) // quotientJ // -sub_conjgV.
  rewrite (subset_trans _ (kerH1c s2 Xs2)) // -(bigdprodWY defH1c) sub_gen //.
  by rewrite (bigcup_max (inMb w)^-1%g) // !inE ntw groupV mem_quotient.
rewrite -size_filter uniq_leq_size //.
  apply/dinjectiveP=> s1 s2 Xs1 Xs2.
  case/(cfclass_Ind_irrP _ _ (der_normal 1 M))/cfclassP=> y My Ds2.
  by apply: irr_inj; rewrite Ds2 cfConjg_id ?(injXtheta y s1 s2).
move=> _ /imageP[s Xs ->]; rewrite mem_filter /= cfInd1 // -(index_sdprod defM).
rewrite Xtheta_1 // -natrM eqxx mem_seqInd ?gFnormal //.
rewrite (subsetP sXthetaXH0U') // !andbT inertia_Ind_irr ?gFnormal //.
by apply/subsetP=> y /setIP[My /inertiaJ/esym/injXtheta->].
Qed.

Import ssrnum Num.Theory.

(* This is Peterfalvi (9.9); we have exported the fact that HU / H0 is a      *)
(* Frobenius group in case (c), as this is directly used in (9.10).           *)
Lemma typeP_Galois_characters (is_Galois : typeP_Galois) :
  [/\ (*a*) {in X_ H0, forall s, (u %| 'chi_s 1%g)%Cx},
            {in X_ H0C', forall s, 'chi_s 1%g = u%:R /\
             (exists2 xi : 'CF(HC), xi \is a linear_char & 'chi_s = 'Ind xi)},
      (*b*) size mu_ = p.-1 /\ {in mu_, forall mu_j, isIndHC mu_j}
    & (*c*) all redM (S_ H0C') ->
            [/\ C :=: 1%g, u = (p ^ q).-1 %/ p.-1
              & [Frobenius HU / H0 = Hbar ><| (U / H0)]]].
Proof.
have [F [phi [psi _ [Kpsi phiJ]]]] := typeP_Galois_P is_Galois.
case=> [oF /isomP[inj_phi im_phi] phiW2] [cycUbar co_u_p1 u_dv_pq1].
have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM.
have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU.
have [nsH0C_M nsHC_M _ nsH0C'_M] := nsH0xx_M; have nH0H := normal_norm nsH0H.
have nsH0HU: H0 <| HU := normalS (subset_trans sH0H sHHU) sHUM nsH0M.
have nH0U: U \subset 'N(H0) := subset_trans sUHU (normal_norm nsH0HU).
have nH0C := subset_trans sCU nH0U.
have sH0C_HU: H0C \subset HU by rewrite -(sdprodWY defHU) genS ?setUSS.
have nsH0C_HU: H0C <| HU := normalS sH0C_HU sHUM nsH0C_M.
have nH0C_HU := normal_norm nsH0C_HU.
have [coH0U coHC] := (coprimeSg sH0H coHU, coprimegS sCU coHU).
have [nH0C_H nH0C_U] := (subset_trans sHHU nH0C_HU, subset_trans sUHU nH0C_HU).
have tiHOC_H: H0C :&: H = H0.
  by rewrite /= norm_joinEr // -group_modl // setIC coprime_TIg ?mulg1.
have{coH0U} tiHOC_U: H0C :&: U = C.
  by rewrite /= norm_joinEr // setIC -group_modr // setIC coprime_TIg ?mul1g.
have isoHbar: Hbar \isog H / H0C.
  by have:= second_isog nH0C_H; rewrite tiHOC_H.
have isoUbar: Ubar \isog U / H0C.
  by have:= second_isog nH0C_U; rewrite tiHOC_U.
have frobHU: [Frobenius HU / H0C = (H / H0C) ><| (U / H0C)].
  have defHUbar: (H / H0C) ><| (U / H0C) = (HU / H0C)%g.
    exact: quotient_coprime_sdprod.
  apply/Frobenius_semiregularP=> //; first by rewrite -(isog_eq1 isoHbar).
    by rewrite -(isog_eq1 isoUbar); have [] := Frobenius_context frobUW1c.
  move=> yb /setD1P[ntyb /morphimP[y nH0Cy Uy] Dyb] /=; rewrite Dyb.
  apply/trivgP/subsetP=> _ /setIP[/morphimP[/= x nHOCx Hx ->] /cent1P/commgP].
  rewrite -morphR //; set xy := [~ x, y] => /eqP/coset_idr/=H0Cxy.
  have [nH0x nH0y] := (subsetP nH0H x Hx, subsetP nH0U y Uy).
  rewrite inE coset_id ?mem_gen // inE coset_idr //; apply: contraNeq ntyb.
  rewrite -(morph_injm_eq1 inj_phi) ?mem_quotient // => nz_x.
  rewrite {yb}Dyb /= coset_id ?mem_gen // -Kpsi !inE Uy orbC /= -val_eqE.
  rewrite -(inj_eq (mulfI nz_x)) mulr1 -[_ * _]phiJ ?mem_quotient // qactJ nH0y.
  rewrite -morphJ // conjg_mulR -/xy mkerr ?eqxx // ker_coset -tiHOC_H inE.
  by rewrite andbC groupM ?groupV ?memJ_norm ?(subsetP nHU) //= H0Cxy ?groupR.
have{coHC} tiHbC: (Hbar :&: C / H0 = 1)%g by rewrite coprime_TIg ?coprime_morph.
have{tiHbC} defHCbar: Hbar \x (C / H0) = (HC / H0)%g.
  by rewrite dprodEY ?quotientY // [C]unlock/= astabQ quotient_setIpre subsetIr.
have sHCHU: HC \subset HU by rewrite -(sdprodWY defHU) genS ?setUS.
have nsHCHU: HC <| HU := normalS sHCHU sHUM nsHC_M.
have sH0HC: H0 \subset HC := subset_trans sH0H (joing_subl H C).
have nsH0HC: H0 <| HC := normalS sH0HC sHCHU nsH0HU.
have nsHHUb: Hbar <| HU / H0 by rewrite quotient_normal.
have I_XH0_C i: i != 0 -> 'I_HU['chi[Hbar]_i %% H0]%CF = HC.
  move=> /= nz_i; apply/esym/eqP.
  have nsCHUb: C / H0 <| HU / H0 by rewrite -quotientYidl ?quotient_normal.
  have sH0C_HC: H0C \subset HC by rewrite genS ?setSU.
  have nsH0C_HC: H0C <| HC := normalS sH0C_HC sHCHU nsH0C_HU.
  have [j Dj]: exists j, 'chi_j = (cfDprodl defHCbar 'chi_i %% H0)%CF.
    by rewrite -dprodl_IirrE -mod_IirrE //; set j := mod_Iirr _; exists j.
  have kerH0Cj: H0C \subset cfker 'chi_j.
    by rewrite Dj sub_cfker_mod ?join_subG ?normG // quotientYidl ?cfker_sdprod.
  rewrite inertia_mod_pre // -(inertia_dprodl defHCbar) ?normal_norm //.
  rewrite -inertia_mod_pre // -Dj eqEsubset sub_Inertia //=.
  rewrite -(quotientSGK _ sH0C_HC) ?subIset ?nH0C_HU -?inertia_quo //.
  rewrite -(quotientYidr nH0C_H) joingA (joing_idPl sH0H) in frobHU.
  rewrite -?quo_IirrE ?(inertia_Frobenius_ker (FrobeniusWker frobHU)) //.
  by rewrite quo_Iirr_eq0 // -irr_eq1 Dj cfMod_eq1 // cfDprodl_eq1 irr_eq1.
have{I_XH0_C} irr_IndHC r: r \in Iirr_kerD HC H H0 -> 'Ind 'chi_r \in irr HU.
  rewrite !inE => /andP[ker'H kerH0]; apply: inertia_Ind_irr => //.
  apply: subset_trans (sub_inertia_Res _ (normal_norm nsHHU)) _.
  rewrite -{kerH0}(quo_IirrK _ kerH0) // mod_IirrE // in ker'H *.
  have /codomP[[i j] Dr] := dprod_Iirr_onto defHCbar (quo_Iirr H0 r).
  rewrite {r}Dr dprod_IirrE cfResMod ?joing_subl ?sub_cfker_mod //= in ker'H *.
  rewrite cfDprod_Resl linearZ inertia_scale_nz ?irr1_neq0 ?I_XH0_C //.
  by apply: contraNneq ker'H => ->; rewrite irr0 cfDprod_cfun1l cfker_sdprod.
have [nb_mu H0C_mu] := nb_redM_H0; set part_a' := ({in X_ H0C', _}).
have Part_a s: s \in X_ H0 -> exists r, 'chi_s = 'Ind[HU, HC] 'chi_r.
  rewrite !inE => /andP[Ks'H KsH0]; have [r sHCr] := constt_cfRes_irr HC s.
  have{KsH0} KrH0: H0 \subset cfker 'chi_r.
    by rewrite (sub_cfker_constt_Res_irr sHCr) // ?normal_norm.
  have{Ks'H} Kr'H: ~~ (H \subset cfker 'chi_r).
    by rewrite (sub_cfker_constt_Res_irr sHCr) ?joing_subl // ?normal_norm.
  have [|s1 Ds1] := irrP _ (irr_IndHC r _); first by rewrite !inE Kr'H.
  rewrite -constt_Ind_Res Ds1 constt_irr inE in sHCr.
  by rewrite (eqP sHCr) -Ds1; exists r.
have [nH0HC nH0C'] := (normal_norm nsH0HC, subset_trans (der_sub 1 _) nH0C).
have Part_a': part_a'.
  move=> s /setDP[KsH0C' Ks'H]; have [|r Ds] := Part_a s.
    by rewrite inE Ks'H (subsetP (Iirr_kerS _ _) _ KsH0C') ?joing_subl.
  suffices lin_r: 'chi_r \is a linear_char.
    by split; [rewrite Du Ds cfInd1 ?lin_char1 ?mulr1 | exists 'chi_r].
  have KrH0C': H0C' \subset cfker 'chi_r.
    rewrite inE Ds sub_cfker_Ind_irr // in KsH0C'.
    by rewrite (subset_trans sHUM) ?normal_norm.
  rewrite lin_irr_der1 (subset_trans _ KrH0C') //= (norm_joinEr nH0C').
  rewrite -quotientSK ?gFsub_trans ?quotient_der //= -/C.
  by rewrite -(der_dprod 1 defHCbar) (derG1P abHbar) dprod1g.
split=> // [s /Part_a[r ->] | | {Part_a' part_a'}red_H0C'].
- by rewrite Du cfInd1 // dvdC_mulr // Cint_Cnat ?Cnat_irr1.
- split=> // mu_j /H0C_mu H0C_mu_j; have [s XH0Cs Dmuj] := seqIndP H0C_mu_j.
  have [|s1u [xi lin_xi Ds]] := Part_a' s.
    by rewrite (subsetP _ _ XH0Cs) ?Iirr_kerDS // genS ?setUS ?der_sub.
  split=> //; first by rewrite Dmuj cfInd1 // s1u -natrM -(index_sdprod defM).
  by rewrite Dmuj Ds cfIndInd //; exists xi.
have C1: C :=: 1%g.
  apply: contraTeq red_H0C' => ntC; apply/allPn.
  have sCM: C \subset M := subset_trans sCU (subset_trans sUHU sHUM).
  have{sCM} solCbar: solvable (C / H0).
    by rewrite quotient_sol ?(solvableS sCM) ?mmax_sol.
  have [|{ntC solCbar} j lin_j nz_j] := solvable_has_lin_char _ solCbar.
    rewrite -(isog_eq1 (quotient_isog _ _)) ?(subset_trans sCU) //.
    by rewrite coprime_TIg ?(coprimegS sCU) ?(coprimeSg sH0H).
  have [i lin_i nz_i] := solvable_has_lin_char ntHbar solHbar.
  pose r := mod_Iirr (dprod_Iirr defHCbar (i, j)).
  have KrH0: H0 \subset cfker 'chi_r by rewrite mod_IirrE ?cfker_mod.
  have Kr'H: ~~ (H \subset cfker 'chi_r).
    rewrite -subsetIidl -cfker_Res ?joing_subl ?irr_char // mod_IirrE //.
    rewrite cfResMod ?joing_subl // sub_cfker_mod // dprod_IirrE.
    by rewrite cfDprodKl ?lin_char1 // subGcfker -irr_eq1.
  have [|s Ds] := irrP _ (irr_IndHC r _); first by rewrite !inE Kr'H.
  have Ks'H: s \notin Iirr_ker HU H.
    by rewrite inE -Ds sub_cfker_Ind_irr ?normal_norm.
  exists ('Ind 'chi_s).
    rewrite mem_seqInd ?gFnormal // inE Ks'H inE -Ds.
    rewrite sub_cfker_Ind_irr // ?(subset_trans sHUM) ?normal_norm //=.
    rewrite mod_IirrE // join_subG cfker_mod // sub_cfker_mod ?quotient_der //.
    apply: subset_trans (dergS 1 (quotientS H0 (joing_subr H C))) _.
    by rewrite -lin_irr_der1 dprod_IirrE cfDprod_lin_char.
  apply: contra nz_j => red_j; have /implyP := H0C_mu ('Ind 'chi_s).
  rewrite mem_filter red_j !mem_seqInd ?gFnormal // !in_setD Ks'H !inE -Ds.
  rewrite irr_eq1 !sub_cfker_Ind_irr ?(normal_norm nsH0HU) //.
  rewrite mod_IirrE // join_subG cfker_mod //= sub_cfker_mod // dprod_IirrE.
  by move/(sub_cfker_Res (subxx _)); rewrite cfDprodKr ?lin_char1 ?subGcfker.
rewrite /= -/C C1 joingG1 in frobHU; split=> //; move/FrobeniusWker in frobHU.
have nsHbHU: Hbar <| (HU / H0) by rewrite quotient_normal.
have ->: (p ^ q).-1 = (#|X_ H0| * u)%N.
  rewrite -oF -cardsT -im_phi card_injm // -(card_Iirr_abelian abHbar).
  rewrite -(cardsC1 0) (card_imset_Ind_irr nsHbHU) => [|i|i y]; last first.
  - by rewrite !inE conjg_Iirr_eq0.
  - by rewrite !inE => nz_i; rewrite inertia_Ind_irr ?inertia_Frobenius_ker.
  rewrite index_quotient_eq ?(subset_trans sHUM) ?subIset ?sH0H ?orbT //.
  apply/eqP; rewrite Du /= C1 joingG1 mulnC eqn_pmul2r //.
  rewrite -(card_imset _ (can_inj (mod_IirrK _))) // -imset_comp.
  apply/eqP/eq_card=> s; apply/imsetP/idP=> [[i nz_i -> /=] | Xs].
    rewrite !inE mod_IirrE 1?{1}cfker_mod // andbT in nz_i *.
    rewrite cfIirrE ?inertia_Ind_irr ?inertia_Frobenius_ker // sub_cfker_mod //.
    by rewrite sub_cfker_Ind_irr ?quotientS ?normal_norm // subGcfker.
  have [[]] := (Part_a s Xs, setDP Xs).
  rewrite /= C1 joingG1 !inE => r Ds [kerH0s].
  have:= kerH0s; rewrite Ds !sub_cfker_Ind_irr ?normal_norm // => kerH0 ker'H.
  exists (quo_Iirr H0 r).
    by rewrite !inE -subGcfker quo_IirrE // cfker_quo ?quotientSGK.
  by rewrite quo_IirrE // cfIndQuo // -Ds -quo_IirrE // irrK quo_IirrK.
suffices ->: #|X_ H0| = p.-1 by rewrite -(subnKC (prime_gt1 p_pr)) mulKn.
rewrite -nb_mu (size_red_subseq_seqInd_typeP MtypeP _ H0C_mu) //; last first.
- exact/allP/filter_all.
- by rewrite filter_uniq ?seqInd_uniq.
apply/esym/eq_card => i; rewrite inE mem_filter mem_seqInd ?gFnormal //.
rewrite andb_idl // => Xi; rewrite (allP red_H0C') //.
by rewrite mem_seqInd ?gFnormal //= C1 (trivgP (der_sub 1 _)) joingG1.
Qed.

(* This combination of (9.8)(b) and (9.9)(b) covers most uses of these lemmas *)
(* in sections 10-14.                                                         *)
Lemma typeP_reducible_core_Ind (ptiWM := FT_primeTI_hyp MtypeP) :
  [/\ size mu_ = p.-1, has predT mu_,
      {subset mu_ <= [seq primeTIred ptiWM j | j in predC1 0]}
    & {in mu_, forall mu_j, isIndHC mu_j}].
Proof.
have [[sz_mu _] /mulG_sub[sHHU _]] := (nb_redM_H0, sdprodW defHU).
rewrite has_predT sz_mu -subn1 subn_gt0 prime_gt1 //; split=> // [mu_j|].
  rewrite mem_filter => /andP[red_chi /seqIndP[s /setDP[_ kerH's] Dchi]].
  have [[j Ds] | [/idPn[]]] := prTIres_irr_cases ptiWM s; last by rewrite -Dchi.
  rewrite Dchi Ds cfInd_prTIres image_f ?inE //=.
  by apply: contraNneq kerH's => j0; rewrite inE Ds j0 prTIres0 cfker_cfun1.
have[/typeP_Galois_characters[_ _ []] // | Gal'M] := boolP typeP_Galois.
by have [_ []] := typeP_nonGalois_characters Gal'M.
Qed.

(* This is Peterfalvi (9.10), formulated as a constructive alternative. *)
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 -> [Frobenius HU = H ><| U]].
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.

Import ssrint.

(* This is Peterfalvi (9.11) *)
(* We had to cover a small gap in step (9.11.4) of the proof, which starts by *)
(* proving that U1 \subset {1} u A(M), then asserts this obviously implies    *)
(* HU1 \subset {1} u A(M). It is not, as while {1} u A(M) does contain H, it  *)
(* is not (necessarily) a subgroup. We had to use the solvability of HU1 in a *)
(* significant way (using Philip Hall's theorems) to bridge the gap; it's     *)
(* also possible to exploit lemma (2.1) (partition_cent_rcoset in PFsection1) *)
(* in a slightly different argument, but the inference is nontrivial in       *)
(* either case.                                                               *)
Lemma Ptype_core_coherence : coherent (S_ H0C') M^# tau.
Proof.
have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM.
have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU.
have nsCU: C <| U := normalS sCU (joing_subl _ _) nsCUW1.
have [_ nCU] := andP nsCU; have sC'C: C^`(1)%g \subset C := der_sub 1 _.
have coHC := coprimegS sCU coHU; have coH0C := coprimeSg sH0H coHC.
have [nsH0C_M nsHC_M nsH0U'_M nsH0C'_M] := nsH0xx_M; have [_ nH0H]:= andP nsH0H.
have nH0HU := subset_trans sHUM nH0M; have nH0U := subset_trans sUHU nH0HU.
have nH0C := subset_trans sCU nH0U; have nH0C' := subset_trans sC'C nH0C.
have sHCHU: HC \subset HU by rewrite join_subG sHHU (subset_trans sCU).
have [nsHCHU nHC] := (normalS sHCHU sHUM nsHC_M, subset_trans sCU nHU).
have tiHCbar: Hbar :&: (C / H0)%g = 1%g by rewrite coprime_TIg ?coprime_morph.
have defHCbar: Hbar \x (C / H0) = (HC / H0)%g.
  by rewrite dprodEY ?quotientY // [C]unlock/= astabQ quotient_setIpre subsetIr.
have{tiHCbar} defHC'bar: (HC / H0)^`(1)%g = (C^`(1) / H0)%g.
  by rewrite -(der_dprod 1 defHCbar) (derG1P abHbar) dprod1g quotient_der.
have sU'U := der_sub 1 U; have nH0U' := subset_trans sU'U nH0U.
have sU'C: U' \subset C.
  by rewrite [C]unlock subsetI sub_astabQ sU'U nH0U' quotient_cents.
have uS0: uniq (S_ H0C') by apply: seqInd_uniq.
have [rmR scohS0]: exists R : 'CF(M) -> seq 'CF(G), subcoherent (S_ H0C') tau R.
  move: (FTtypeP_coh_base _ _) (FTtypeP_subcoherent maxM MtypeP) => R scohR.
  exists R; apply: (subset_subcoherent scohR).
  split=> //; last exact: cfAut_seqInd.
  by apply: seqIndS; rewrite Iirr_kerDS ?sub1G ?Fcore_sub_FTcore.
have [GalM | Gal'M] := boolP typeP_Galois.
  have [_ XOC'u _ _] := typeP_Galois_characters GalM.
  apply: uniform_degree_coherence scohS0 _.
  apply: all_pred1_constant (#|M : HU| * u)%:R _ _; rewrite all_map.
  by apply/allP=> _ /seqIndP[s /XOC'u[s1u _] ->] /=; rewrite natrM cfInd1 ?s1u.
have:= typeP_nonGalois_characters Gal'M.
set U1 := 'C_U(_ | _); set a := #|_ : _|.
case: (_ Gal'M) => /= H1 [oH1 nH1U _ defHbar aP] in U1 a *.
rewrite -/U1 -/a in aP; case: aP => a_gt1 a_dv_p1 cycU1 _.
case=> [a_dv_XH0 [nb_mu IndHCmu] has_irrHC lb_Sqa]; rewrite -[S_ _]/(S_ H0C').
have defHb1 := defHbar; rewrite (big_setD1 1%g) ?group1 ?conjsg1 //= in defHb1.
have [[_ H1c _ defH1c] _ _ _] := dprodP defHb1; rewrite defH1c in defHb1.
have [nsH1H _] := dprod_normal2 defHb1; have [sH1H _] := andP nsH1H.
have nsU1U: U1 <| U; last have [sU1U nU1U] := andP nsU1U.
  by rewrite norm_normalI // astabQ norm_quotient_pre ?norms_cent.
have Da: a = #|HU : H <*> U1|.
  rewrite /a -!divgS /= ?join_subG ?sHHU ?norm_joinEr ?(subset_trans sU1U) //=.
  by rewrite -(sdprod_card defHU) coprime_cardMg ?(coprimegS sU1U) ?divnMl.
have sCU1: C \subset U1 by rewrite [C]unlock setIS ?astabS.
have a_dv_u: a %| u by rewrite Da Du indexgS ?genS ?setUS.
have [a_gt0 q_gt0 u_gt0 p1_gt0]: [/\ 0 < a, 0 < q, 0 < u & 0 < p.-1]%N.
  rewrite !cardG_gt0 ltnW // -subn1 subn_gt0 prime_gt1 //.
have [odd_p odd_q odd_a]: [/\ odd p, odd q & odd a].
  by rewrite mFT_odd -oH1 (oddSg sH1H) ?(dvdn_odd a_dv_u) ?mFT_quo_odd.
have Dp: p = (2 * p.-1./2 + 1)%N.
  by rewrite mul2n -[p]odd_double_half odd_p half_double addn1.
(* Start of main proof. *)
pose S1 := filter [pred zeta : 'CF(M) | zeta 1%g == (q * a)%:R] (S_ H0C').
have ntS1: (0 < size S1)%N.
  have [lb_dv lbS1] := lb_Sqa; apply: leq_trans (leq_trans lbS1 _).
    by rewrite ltn_divRL // mul0n muln_gt0 p1_gt0 cardG_gt0.
  rewrite -size_filter uniq_leq_size ?filter_uniq ?seqInd_uniq // => chi.
  rewrite !mem_filter -andbA /= => /and3P[_ ->].
  by apply: seqIndS; rewrite Iirr_kerDS // genS ?setUS ?dergS ?subsetIl.
have sS10: cfConjC_subset S1 (S_ H0C').
  split=> [||chi]; first by rewrite filter_uniq.
    by apply: mem_subseq; apply: filter_subseq.
  rewrite !mem_filter !inE cfunE => /andP[/eqP <- S0chi].
  by rewrite cfAut_seqInd // andbT conj_Cnat ?(Cnat_seqInd1 S0chi).
have cohS1: coherent S1 M^# tau.
  apply: uniform_degree_coherence (subset_subcoherent scohS0 sS10) _.
  by apply: all_pred1_constant (q * a)%:R _ _; rewrite all_map filter_all.
pose S3 := filter [predC S1] (S_ H0C'); move: {2}_.+1 (ltnSn (size S3)) => nS. 
move: @S3 (sS10) (cohS1); have: {subset S1 <= S1} by [].
elim: nS {-1}S1 => // nS IHnS S2 => sS12 S3 sS20 cohS2; rewrite ltnS => leS3nS.
have [ntS3|] := boolP (size S3 > 0)%N; last first.
  rewrite size_filter -has_count has_predC negbK => /allP sS02.
  exact: subset_coherent sS02 cohS2.
(* Ultimateley we'll contradict the maximality of S2 in (9.11.1) & (9.11.8). *)
suff [chi]: exists2 chi, chi \in S3 & coherent (chi :: chi^* :: S2)%CF M^# tau.
  rewrite mem_filter => /andP[/= S2'chi S0chi]; have [uS2 sS2S0 ccS2] := sS20.
  move/IHnS; apply=> [psi /sS12 S1psi||]; first by rewrite 2?mem_behead.
    split.
    - rewrite /= !inE negb_or S2'chi (contra (ccS2 _)) ?cfConjCK // eq_sym.
      by rewrite (seqInd_conjC_neq _ _ _ S0chi) ?mFT_odd.
    - by apply/allP; rewrite /= S0chi cfAut_seqInd //=; apply/allP.
    apply/allP; rewrite /= !inE cfConjCK !eqxx orbT /=.
    by apply/allP=> psi /ccS2; rewrite !inE orbA orbC => ->.
  apply: leq_trans leS3nS; rewrite ltnNge; apply: contra S2'chi.
  case/leq_size_perm=> [|psi|/(_ chi)]; first by rewrite filter_uniq.
    by rewrite !mem_filter !inE orbA negb_or -andbA => /andP[].
  by rewrite !mem_filter !inE eqxx S0chi !andbT => /esym/negbFE.
(* This is step (9.11.1). *) clear nS IHnS leS3nS.
without loss [[eqS12 irrS1 H0C_S1] [Da_p defC] [S3qu ne_qa_qu] [oS1 oS1ua]]:
  / [/\ [/\ S1 =i S2, {subset S1 <= irr M} & {subset S1 <= S_ H0C}],
        a = p.-1./2 /\ C :=: U',
        (forall chi, chi \in S3 -> chi 1%g == (q * u)%:R) /\ (q * u != q * a)%N
      & size S1 = (p.-1 * u %/ a ^ 2)%N /\ size S1 = (2 * u %/ a)%N].
- move=> IHwlog; have{sS20} [[uS2 sS20 ccS2] [uS1 _ _]] := (sS20, sS10).
  pose is_qu := [pred chi : 'CF(M) | chi 1%g == (q * u)%:R].
  pose isn't_qu := [pred chi | is_qu chi ==> all is_qu S3].
  have /hasP[chi S3chi qu'chi]: has isn't_qu S3.
    rewrite /isn't_qu; have [_|] := boolP (all _ _); last by rewrite has_predC. 
    by rewrite (eq_has (fun _ => implybT _)) has_predT.
  have [S2'chi S0chi]: chi \notin S2 /\ chi \in S_ H0C'.
    by apply/andP; rewrite mem_filter in S3chi.
  have [s X0C's Dchi] := seqIndP S0chi.
  have Dchi1: chi 1%g = q%:R * 'chi_s 1%g.
    by rewrite Dchi cfInd1 // -(index_sdprod defM).
  (* We'll show lb0 <= lb1 <= lb <= lb3 <= sumnS S1' <= sumnS S2 <= lb0,   *)
  (* with equality under conditions that imply the conclusion of (9.11.1). *)
  pose lb0 := (2 * q * a)%:R * chi 1%g.
  pose lb1 : algC := (2 * a * q ^ 2 * u)%:R.
  pose lb2 : algC := (p.-1 * q ^ 2 * u)%:R.
  pose lb3 : algC := (p.-1 * q ^ 2 * #|U : U'|)%:R.
  pose S1' := filter [predI irr M & S_ H0U'] S1.
  pose szS1' := ((p.-1 * #|U : U'|) %/ a ^ 2)%N; set lbS1' := _ %/ _ in lb_Sqa.
  pose Snorm (psi : 'CF(M)) := psi 1%g ^+ 2 / '[psi].
  pose sumnS Si := \sum_(psi <- Si) Snorm psi.
  have lb01: lb0 <= lb1 ?= iff (chi 1%g == (q * u)%:R).
    rewrite /lb1 mulnA -mulnA natrM /lb0 mulnAC mono_lerif; last first.
      by apply: ler_pmul2l; rewrite ltr0n !muln_gt0 a_gt0.
    apply: lerif_eq; rewrite Dchi1 natrM ler_pmul2l ?gt0CG //.
    have [KsH0C' _] := setDP X0C's; rewrite inE in KsH0C'.
    have [t sHCt] := constt_cfRes_irr HC s.
    have KtH0C': H0C' \subset cfker 'chi_t.
      apply: subset_trans (cfker_constt (cfRes_char _ (irr_char s)) sHCt).
      by rewrite cfker_Res ?irr_char // subsetI genS ?setUSS.
    rewrite -constt_Ind_Res in sHCt.
    apply: ler_trans (char1_ge_constt (cfInd_char _ (irr_char t)) sHCt) _.
    rewrite cfInd1 // -Du lin_char1 ?mulr1 // lin_irr_der1.
    apply: subset_trans KtH0C'; rewrite /= (norm_joinEr nH0C') /= -/C.
    rewrite -quotientSK ?(subset_trans (der_sub _ _)) ?(subset_trans sHCHU) //.
    by rewrite -defHC'bar quotient_der ?(subset_trans sHCHU).
  have lb12: lb1 <= lb2 ?= iff (a == p.-1./2).
    rewrite -(@eqn_pmul2l 2) // -(canLR (addnK 1) Dp) subn1 lerif_nat.
    rewrite !(mono_leqif (fun _ _ => leq_pmul2r _)) ?expn_gt0 ?q_gt0 //.
    apply: leqif_eq; rewrite dvdn_leq // Gauss_dvd //.
       by rewrite {1}Dp addn1 dvdn_mulr.
    by rewrite prime_coprime ?dvdn2 ?negbK.
  have lb23: lb2 <= lb3 ?= iff (C :==: U') :> algC.
    rewrite lerif_nat [u]card_quotient //.
    rewrite (mono_leqif (fun _ _ => leq_pmul2l _)) ?muln_gt0 ?p1_gt0 ?q_gt0 //.
    rewrite -(mono_leqif (fun _ _ => leq_pmul2l (cardG_gt0 C))) Lagrange //.
    rewrite -(Lagrange sU'U) (mono_leqif (fun _ _ => leq_pmul2r _)) //.
    by rewrite eq_sym; apply: subset_leqif_cards.
  have lb3S1': lb3 <= sumnS S1' ?= iff (size S1' == szS1').
    rewrite /szS1' -(divnMr (cardG_gt0 U')) mulnAC -mulnA Lagrange // -/lbS1'.
    have{lb_Sqa} [dv_lb lbSqa] := lb_Sqa; rewrite [sumnS S1']big_seq.
    rewrite (eq_bigr (fun _ => ((q * a) ^ 2)%:R)) => [|psi]; last first.
      rewrite !mem_filter -!andbA => /and4P[/irrP[r ->] _ /=/eqP r1qa _].
      by rewrite /Snorm cfnorm_irr divr1 r1qa natrX.
    rewrite -big_seq (big_nth 0) -natr_sum sum_nat_const_nat subn0.
    rewrite mulnC natrM [*%R]lock /lb3 natrM natf_indexg ?der_sub // mulrA.
    rewrite -natrM mulnAC -(divnK dv_lb) mulnAC mulnA natrM mulfK ?neq0CG //.
    rewrite -/lbS1' -mulnA -expnMn natrM mulrC -lock mono_lerif; last first.
      by apply: ler_pmul2l; rewrite ltr0n !muln_gt0 a_gt0 q_gt0.
    rewrite eq_sym lerif_nat; apply: leqif_eq; rewrite (leq_trans lbSqa) //.
    rewrite -size_filter uniq_leq_size ?filter_uniq ?seqInd_uniq // => psi.
    rewrite !mem_filter -!andbA /= => /and3P[-> -> S0psi]; rewrite S0psi.
    by apply: seqIndS S0psi; rewrite Iirr_kerDS //= genS ?setUS ?dergS.
  have lbS1'2: sumnS S1' <= sumnS S2 ?= iff ~~ has [predC S1'] S2.
    have Ds2: perm_eq S2 (S1' ++ filter [predC S1'] S2).
      rewrite -(perm_filterC (mem S1')) perm_cat2r.
      rewrite uniq_perm_eq ?filter_uniq // => psi.
      by rewrite mem_filter andb_idr //= mem_filter => /andP[_ /sS12].
    rewrite [sumnS S2](eq_big_perm _ Ds2) big_cat /= -/(sumnS S1') big_filter.
    rewrite -all_predC -big_all_cond !(big_tnth _ _ S2) big_andE.
    rewrite -{1}[_ S1']addr0 mono_lerif; last exact: ler_add2l.
    set sumS2' := \sum_(i | _) _; rewrite -[0]/(sumS2' *+ 0) -sumrMnl.
    apply: lerif_sum => i _; apply/lerifP; rewrite lt0r !mulf_eq0 invr_eq0.
    set psi := tnth _ i; have Spsi := sS20 psi (mem_tnth _ _).
    rewrite !negb_or (seqInd1_neq0 _ Spsi) //= (cfnorm_seqInd_neq0 _ Spsi) //=.
    by rewrite divr_ge0 ?exprn_ge0 ?cfnorm_ge0 ?Cnat_ge0 ?(Cnat_seqInd1 Spsi).
  have [lb0S2 | ] := boolP (lb0 < sumnS S2).
    exists chi => //; have /hasP[xi S1xi _]: has predT S1 by rewrite has_predT.
    have xi1: xi 1%g = (q * a)%:R.
      by rewrite mem_filter in S1xi; have [/eqP] := andP S1xi.
    apply: (extend_coherent scohS0 _ (sS12 _ S1xi)) => //.
    split=> //; last by rewrite mulrAC xi1 -natrM mulnA.
    rewrite xi1 Dchi1 irr1_degree -natrM dvdC_nat dvdn_pmul2l ?cardG_gt0 //.
    rewrite -dvdC_nat /= !nCdivE -irr1_degree a_dv_XH0 //.
    by rewrite (subsetP (Iirr_kerDS _ _ _) _ X0C's) ?joing_subl.
  have lb1S2 := lerif_trans lb12 (lerif_trans lb23 (lerif_trans lb3S1' lbS1'2)).
  rewrite ltr_neqAle !(lerif_trans lb01 lb1S2) andbT has_predC !negbK.
  case/and5P=> /eqP-chi1qu /eqP-Da_p /eqP-defC /eqP-sz_S1' /allP/=sS21'.
  have defS1': S1' = S1.
    apply/eqP; rewrite -(geq_leqif (size_subseq_leqif (filter_subseq _ S1))).
    by rewrite uniq_leq_size // => psi /sS12/sS21'.
  apply: IHwlog; split=> //.
  + split=> psi; do 1?[rewrite -defS1' mem_filter andbC => /and3P[_ _] //=].
      by apply/idP/idP=> [/sS12 | /sS21']; rewrite ?defS1'.
    by congr (_ \in S_ _); apply/group_inj; rewrite /= defC.
  + split; first by apply/allP; apply: contraLR qu'chi; rewrite /= chi1qu eqxx.
    rewrite -eqC_nat -chi1qu; apply: contra S2'chi => chi1qa.
    by rewrite sS12 // mem_filter /= chi1qa.
  rewrite -defS1' sz_S1' /szS1' -defC -card_quotient // -/u.
  by split=> //; rewrite -mulnn {1}Dp addn1 -Da_p mulnAC divnMr.
have nCW1: W1 \subset 'N(C).
  by rewrite (subset_trans (joing_subr U W1)) ?normal_norm.
(* This is step (9.11.2). *) clear sS20 cohS2 sS12 has_irrHC lb_Sqa sU'C.
have [tiU1 le_u_a2]: {in W1^#, forall w, U1 :&: U1 :^ w = C} /\ (u <= a ^ 2)%N.
  have tiU1 w: w \in W1^# -> U1 :&: U1 :^ w = C; last split => //.
    case/setD1P=> ntw W1w; have nH0w := subsetP (subset_trans sW1M nH0M) w W1w.
    pose wb := coset H0 w; have W1wb: wb \in W1bar^#.
      rewrite !inE mem_quotient ?(contraNneq _ ntw) // => /coset_idr H0w.
      rewrite -in_set1 -set1gE -tiHUW1 inE (subsetP sHHU) // (subsetP sH0H) //.
      by rewrite H0w.
    have ntH1 w1: H1 :^ w1 :!=: 1%g by rewrite -cardG_gt1 cardJg oH1 prime_gt1.
    pose t_ w1 :=
      if pred2 1%g wb w1 then sval (has_nonprincipal_irr (ntH1 w1)) else 0.
    pose theta :=
      cfDprodl defHCbar (cfBigdprod defHbar (fun w1 => 'chi_(t_ w1))).
    have lin_theta : theta \is a linear_char.
      rewrite cfDprodl_lin_char ?cfBigdprod_lin_char // => w1 _.
      by rewrite irr_prime_lin ?cardJg ?oH1.
    have nsH0HC: H0 <| HC.
      by rewrite /normal join_subG nH0H sub_gen ?subsetU ?sH0H.
    move defK: H0C => K. (* to avoid divergence in Coq kernel *)
    have kerK: K \subset cfker (theta %% H0).
      rewrite -defK sub_cfker_mod ?join_subG ?normG ?quotientYidl //.
      exact: cfker_sdprod.
    have sKHC: K \subset HC by rewrite -defK genS ?setSU.
    have nsKHC: K <| HC by rewrite (normalS sKHC (normal_sub nsHC_M)) -?defK.
    have sH0K: H0 \subset K by rewrite -defK joing_subl.
    have nsKHU: K <| HU.
      by rewrite (normalS (subset_trans sKHC sHCHU) sHUM) -?defK.
    have [t2 Dt2]: {t2 : Iirr (HC / K) | 'chi_t2 %% K = theta %% H0}%CF.
      exists (cfIirr ((theta %% H0) / K)).
      by rewrite cfIirrE ?cfQuoK ?cfQuo_irr ?cfMod_irr ?lin_char_irr.
    have nsHChatHU: HC / K <| HU / K by rewrite quotient_normal.
    have sHChatHU := normal_sub nsHChatHU.
    pose That := 'I_(HU / K)['chi_t2]%G.
    have sThatHU: That \subset (HU / K)%G := Inertia_sub _ _.
    have abThatHC: abelian (That / (HC / K)).
      rewrite (abelianS (quotientS _ sThatHU)) //.
      rewrite (isog_abelian (third_isog _ _ _)) // defC.
      rewrite -(isog_abelian (quotient_sdprodr_isog defHU _)) ?gFnormal //.
      by rewrite sub_der1_abelian.
    have hallHChat: Hall That (HC / K).
      rewrite /Hall -(card_isog (third_isog sH0K nsH0HC nsKHC)) /=.
      rewrite sub_Inertia // -[in #|_|]defK /= quotientYidl //.
      rewrite -(card_isog (sdprod_isog (dprodWsdC defHCbar))).
      apply: coprime_dvdr (indexSg (sub_Inertia _ sHChatHU) sThatHU) _.
      apply: coprime_dvdr (index_quotient _) _.
        by rewrite subIset // normal_norm.
      by rewrite -Du coprime_morphl // coprime_morphr.
    have [s t2HUs] := constt_cfInd_irr t2 sHChatHU.
    have s_1: ('chi_s %% K)%CF 1%g = #|U : U1 :&: U1 :^ w|%:R.
      rewrite cfMod1.
      have [||_ _ ->] // := cfInd_Hall_central_Inertia _ abThatHC.
      rewrite -cfMod1 Dt2 cfMod1 lin_char1 //= mulr1 -inertia_mod_quo // Dt2.
      rewrite index_quotient_eq ?normal_norm ?Inertia_sub ?setIS //; last first.
        by rewrite (subset_trans sKHC) ?sub_inertia.
      rewrite /= inertia_morph_pre //= -quotientE inertia_dprodl; first 1 last.
      - by rewrite quotient_norms ?normal_norm.
      - rewrite /= -(quotientYidl nH0C) quotient_norms ?normal_norm //.
        by rewrite -defK in nsKHU.
      have nH1wHU w1: w1 \in (W1 / H0)%g -> (HU / H0)%g \subset 'N(H1 :^ w1).
        move=> W1w1; rewrite -(normsP (quotient_norms H0 nHUW1) _ W1w1) normJ.
        rewrite conjSg /= -(sdprodW defHU) quotientMl ?mul_subG //.
        exact: normal_norm.
      rewrite indexgI /= inertia_bigdprod_irr // (big_setD1 1%g) ?group1 //=.
      rewrite 2!{1}setIA setIid (bigD1 wb) //= {1 2}/t_ /= !eqxx ?orbT /=.
      rewrite !(inertia_irr_prime _ p_pr) ?cardJg //=;
        try by case: (has_nonprincipal_irr _).
      rewrite conjsg1 centJ setIA -setIIr /=.
      elim/big_rec: _ => [|w1 Uk /andP[/setD1P[ntw1 Ww1] w'w1] IHk]; last first.
        rewrite /t_ -if_neg negb_or ntw1 w'w1 irr0 Inertia1 -?setIIr 1?setIA //.
        rewrite /normal nH1wHU //= -(normsP (quotient_norms H0 nHUW1) _ Ww1).
        by rewrite conjSg (subset_trans sH1H) ?quotientS.
      rewrite setIT !morphpreI morphpreJ ?(subsetP nH0W1) //= -astabQ.
      rewrite quotientGK //; last by rewrite /normal (subset_trans sH0H).
      rewrite -(sdprodWY (sdprod_modl defHU _)); last first.
        rewrite subsetI -sub_conjgV.
        rewrite (normsP (gFnorm _ _)) ?groupV ?(subsetP sW1M) //= andbb.
        by rewrite sub_astabQ nH0H sub_abelian_cent.
      rewrite -(index_sdprodr defHU) ?subsetIl // conjIg (normsP nUW1) //.
      by rewrite -setIIr.
    apply/esym/eqP; rewrite eqEcard subsetI -sub_conjgV.
    rewrite (normsP _ _ (groupVr W1w)) ?sCU1 /=; last first.
      by rewrite (subset_trans (joing_subr U W1)) ?normal_norm.
    have{s_1} : pred2 u a #|U : U1 :&: U1 :^ w|.
      rewrite /= -!eqC_nat -{}s_1 -mod_IirrE //.
      pose phi := 'Ind[M] 'chi_(mod_Iirr s).
      have Sphi: phi \in S_ H0C'.
        rewrite mem_seqInd ?gFnormal // !inE mod_IirrE //.
        rewrite andbC (subset_trans _ (cfker_mod _ _)) //=; last first.
          by rewrite -defK genS ?setUS ?der_sub.
        rewrite sub_cfker_mod ?(subset_trans sHHU) ?normal_norm //.
        have sHHC: H \subset HC by rewrite joing_subl.
        rewrite -(sub_cfker_constt_Ind_irr t2HUs) ?quotientS //; last first.
          by rewrite quotient_norms ?normal_norm.
        rewrite -sub_cfker_mod ?(subset_trans sHHU (normal_norm nsKHU)) //.
        rewrite Dt2 sub_cfker_mod //.
        apply: contra (valP (has_nonprincipal_irr (ntH1 1%g))).
        move/eq_cfker_Res; rewrite cfDprodlK => kerHbar.
        have:= sH1H; rewrite -{1}(conjsg1 H1) -kerHbar => /eq_cfker_Res.
        by rewrite cfBigdprodKabelian ?group1 // /t_ /= eqxx -subGcfker => ->.
      have [/S3qu | ] := boolP (phi \in S3).
        rewrite cfInd1 // natrM -(index_sdprod defM).
        by rewrite (inj_eq (mulfI (neq0CG _))) => ->.
      rewrite mem_filter Sphi andbT negbK /= -eqS12 mem_filter Sphi andbT /=.
      rewrite cfInd1 // natrM -(index_sdprod defM) (inj_eq (mulfI (neq0CG _))).
      by rewrite orbC => ->.
    case/pred2P=> [iUCu | iUCa].
      rewrite -(leq_pmul2r u_gt0) -{1}iUCu /u card_quotient ?Lagrange //.
      by rewrite /= -setIA subsetIl.
    rewrite subset_leq_card // subIset // [C]unlock subsetI subsetIl sub_astabQ.
    rewrite subIset ?nH0U //= centsC -(bigdprodWY defHbar) gen_subG.
    apply/orP; left; apply/bigcupsP=> w1 Ww1; rewrite centsC centJ -sub_conjgV.
    rewrite (normsP _ _ (groupVr Ww1)) ?quotient_norms //.
      by rewrite /U1 astabQ quotient_setIpre subsetIr.
    rewrite prime_meetG //; apply/trivgPn; exists w; rewrite // !inE W1w.
    rewrite (sameP setIidPr eqP) eqEcard subsetIr /= cardJg.
    by rewrite -(leq_pmul2r a_gt0) -{2}iUCa !Lagrange //= -setIA subsetIl.
  have /trivgPn[w W1w ntw]: W1 :!=: 1%g by rewrite -cardG_gt1 prime_gt1.
  rewrite -(leq_pmul2l u_gt0) mulnn.
  have nCU1 := subset_trans sU1U nCU.
  have {1}->: u = (#|(U1 / C)%g| * a)%N.
    by rewrite mulnC /u !card_quotient // Lagrange_index.
  rewrite expnMn leq_pmul2r ?expn_gt0 ?orbF // -mulnn.
  rewrite -{2}[U1](conjsgK w) quotientJ ?groupV ?(subsetP nCW1) //.
  rewrite cardJg -TI_cardMg /= -/U1 ?subset_leq_card //.
    rewrite mul_subG ?quotientS ?subsetIl //.
    by rewrite -(normsP nUW1 w W1w) conjSg subsetIl.
  by rewrite -quotientGI // tiU1 ?trivg_quotient // !inE ntw.
pose S4 := filter [predD S_ H0C & redM] S3.
have sS43: {subset S4 <= S3} by apply: mem_subseq; apply: filter_subseq.
(* This is step (9.11.3). *)
have nsHM: H <| M by apply: gFnormal.
have oS4: (q * u * size S4 + p.-1 * (q + u))%N = (p ^ q).-1.
  rewrite mulnAC {1}[q](index_sdprod defM) -[S4]filter_predI.
  rewrite (size_irr_subseq_seqInd _ (filter_subseq _ _)) //; last first.
    by move=> xi; rewrite mem_filter -!andbA negbK => /andP[].
  set Xn := finset _; pose sumH0C := \sum_(s in X_ H0C) 'chi_s 1%g ^+ 2.
  have /eqP: sumH0C = (q * size S1 * a ^ 2 + (#|Xn| + p.-1) * u ^ 2)%:R.
    rewrite [q](index_sdprod defM) natrD natrM natrX.
    rewrite (size_irr_subseq_seqInd _ (filter_subseq _ _)) //= -/S1.
    have sH0CC': {subset S_ H0C <= S_ H0C'}.
      by apply: seqIndS; rewrite Iirr_kerDS // genS ?setUS ?der_sub.
    rewrite [sumH0C](big_setID [set s | 'Ind 'chi_s \in S1]) /=; congr (_ + _).
      rewrite mulr_natl -[rhs in _ = rhs]sumr_const; apply: eq_big => s.
        by rewrite in_setI inE andb_idl // => /H0C_S1; rewrite mem_seqInd.
      rewrite 2!inE mem_filter andbCA /= cfInd1 //  -(index_sdprod defM) natrM.
      by case/andP=> /eqP/(mulfI (neq0CG _))->.
    rewrite (eq_bigr (fun _ => u%:R ^+ 2)) => [|s]; last first.
      rewrite 2!inE eqS12 => /andP[S2's H0Cs]; congr (_ ^+ 2).
      have /S3qu/eqP: 'Ind 'chi_s \in S3.
        by rewrite mem_filter /= S2's sH0CC' ?mem_seqInd.
      by rewrite natrM cfInd1 // -(index_sdprod defM) => /(mulfI (neq0CG _)).
    rewrite sumr_const -mulr_natl natrM natrX -nb_mu; congr (_%:R * _).
    have [_ s_mu_H0C] := nb_redM_H0.
    rewrite (size_red_subseq_seqInd_typeP MtypeP _ s_mu_H0C); last first.
    - by apply/allP; apply: filter_all.
    - by rewrite filter_uniq ?seqInd_uniq.
    rewrite -/mu_ -[#|_|](cardsID Xn) (setIidPr _); last first.
      apply/subsetP=> s; rewrite inE in_setD mem_filter /= -!andbA -eqS12.
      rewrite mem_seqInd ?gFnormal // => /and4P[_ -> S1'xi _].
      by rewrite inE S1'xi.
    congr (_ + _)%N; apply: eq_card => i; rewrite inE -/mu_ 2!inE.
    rewrite -[seqInd M _]/(S_ H0C') mem_filter /= andbC 2!inE eqS12 -!andbA.
    rewrite -(mem_seqInd nsHUM) // -/(S_ H0C); set xi := 'Ind _.
    apply/idP/idP=> [/and3P[-> H0Cxi] | mu_xi].
      rewrite H0Cxi sH0CC' //= andbT negbK mem_filter unfold_in => ->.
      by rewrite (seqIndS _ H0Cxi) // Iirr_kerDS ?joing_subl.
    have [xi1u H0Cxi _] := IndHCmu _ mu_xi.
    rewrite H0Cxi -eqS12 mem_filter sH0CC' //= !andbT xi1u eqC_nat ne_qa_qu.
    by rewrite andbT negbK mem_filter in mu_xi *; case/andP: mu_xi.
  rewrite oS1 -mulnA divnK ?dvdn_mul // !mulnA -mulnDl mulnC natrM {}/sumH0C.
  rewrite /X_ -Iirr_kerDY joingC joingA (joing_idPl sH0H) /=.
  rewrite sum_Iirr_kerD_square ?genS ?setSU //; last first.
    by apply: normalS nsH0C_M; rewrite // -(sdprodWY defHU) genS ?setUSS.
  rewrite -Du (inj_eq (mulfI (neq0CG _))) -(prednK (indexg_gt0 _ _)).
  rewrite mulrSr addrK eqC_nat addnC mulnDl addnAC (mulnC q) -addnA -mulnDr.
  move/eqP <-; congr _.-1.
  have nH0HC: HC \subset 'N(H0) by rewrite join_subG nH0H.
  rewrite -(index_quotient_eq _ _ nH0HC) ?genS ?setSU //; last first.
    by rewrite setIC subIset ?joing_subl.
  rewrite quotientYidl // -(index_sdprod (dprodWsdC defHCbar)).
  by case: Ptype_Fcore_factor_facts.
have /hasP[psi1 S1psi1 _]: has predT S1 by rewrite has_predT.
pose gamma := 'Ind[M, H <*> U1] 1; pose alpha := gamma - psi1.
(* This is step (9.11.4). *)
pose nm_alpha : algC := a%:R + 1 + (q.-1 * a ^ 2)%:R / u%:R.
have [Aalpha Nalpha]: alpha \in 'CF(M, 'A(M)) /\ '[alpha] = nm_alpha.
  have sHU1_HU: H <*> U1 \subset HU by rewrite -(sdprodWY defHU) genS ?setUS.
  have sHU1_M := subset_trans sHU1_HU sHUM.
  have sHU1_A1: H <*> U1 \subset 1%g |: 'A(M).
    pose pi := \pi(H); rewrite -subDset; apply/subsetP=> y /setD1P[nty HU1y].
    apply/bigcupP; rewrite notMtype1 /=; have sHMs := Fcore_sub_FTcore maxM.
    have defHU1: H ><| U1 = H <*> U1 := sdprod_subr defHU sU1U.
    have nsH_HU1: H <| H <*> U1 by have [] := sdprod_context defHU1.
    have [HUy [_ nH_HU1]] := (subsetP sHU1_HU y HU1y, normalP nsH_HU1).
    have hallH: pi.-Hall(H <*> U1) H.
      by rewrite Hall_pi // -(coprime_sdprod_Hall_l defHU1) (coprimegS sU1U).
    have hallU1: pi^'.-Hall(H <*> U1) U1.
      by rewrite -(compl_pHall _ hallH) sdprod_compl.
    have [pi'y | pi_y] := boolP (pi^'.-elt y); last first.
      exists y.`_pi; last by rewrite 3!inE nty HUy cent1C groupX ?cent1id.
      rewrite !inE (sameP eqP constt1P) pi_y (subsetP sHMs) //.
      by rewrite (mem_normal_Hall hallH) ?groupX ?p_elt_constt.
    have solHU1: solvable (H <*> U1) by rewrite (solvableS sHU1_M) ?mmax_sol.
    have [||z HU1z U1yz] := Hall_Jsub _ hallU1 _ pi'y; rewrite ?cycle_subG //.
    have /trivgPn[x /setIP[Hx cxyz] ntx]: 'C_H[y ^ z] != 1%g.
      apply: contraTneq (prime_gt1 p_pr) => regHy; rewrite -oH1 cardG_gt1 negbK.
      move: U1yz; rewrite -cycleJ subsetI sub_astabQ => /and3P[sYU nHY cH1Y].
      rewrite centsC in cH1Y; rewrite -(setIidPl cH1Y) -(setIidPl sH1H) -setIA.
      rewrite -coprime_quotient_cent ?(coprimegS sYU) // cent_cycle regHy.
      by rewrite quotient1 setIg1.
    exists (x ^ z^-1)%g; last by rewrite 3!inE nty HUy cent1J mem_conjgV cent1C.
    by rewrite 2!inE conjg_eq1 ntx (subsetP sHMs) // -mem_conjg nH_HU1.
  have{sHU1_A1} Aalpha: alpha \in 'CF(M, 'A(M)).
    have A'1: 1%g \notin 'A(M) by have /subsetD1P[] := FTsupp_sub M.
    rewrite -['A(M)](setU1K A'1) cfun_onD1 !cfunE subr_eq0 cfInd1 // cfun11.
    rewrite mulr1 -(Lagrange_index sHUM) // -(index_sdprod defM) -/q.
    rewrite -(index_sdprodr defHU) ?subsetIl // -/a eq_sym andbC.
    have:= S1psi1; rewrite mem_filter /= => /andP[-> _] /=.
    rewrite rpredB //.
      apply: cfun_onS (cfInd_on sHU1_M (cfun_onG _)).
      rewrite class_supportEr; apply/bigcupsP=> w Mw.
      by rewrite sub_conjg conjUg conjs1g (normsP (FTsupp_norm M)) ?groupV.
    have /seqIndP[s /setDP[_ ker'H ] ->] := H0C_S1 _ S1psi1.
    rewrite (prDade_Ind_irr_on (FT_prDade_hypF maxM MtypeP)) //.
    by rewrite inE in ker'H.
  have ->: '[alpha] = '[gamma] + 1.
    have /irrP[t Dt] := irrS1 _ S1psi1.
    rewrite cfnormBd; first by rewrite Dt cfnorm_irr.
    have /seqIndP[s /setDP[_ ker'H ] Dpsi1] := H0C_S1 _ S1psi1.
    apply: contraNeq ker'H; rewrite Dt /gamma -irr0 -irr_consttE => tHU1_0.
    rewrite inE -(sub_cfker_Ind_irr _ sHUM) ?gFnorm // -Dpsi1 Dt.
    rewrite -(sub_cfker_constt_Ind_irr tHU1_0) ?gFnorm ?joing_subl //.
    by rewrite irr0 cfker_cfun1 joing_subl.
  split=> //; rewrite /nm_alpha addrAC natrM mulrAC mulrC; congr (_ + 1).
  rewrite -{1}(mulnK a a_gt0) natf_div ?dvdn_mull // -mulrDr mulnn natrX.
  have /sdprod_isom[nH_UW1 isomMH]: H ><| (U <*> W1) = M.
    rewrite sdprodEY ?join_subG ?nHU ?(subset_trans sW1M) ?gFnorm //.
      by rewrite joingA (sdprodWY defHU) (sdprodWY defM).
    rewrite /= -(setIidPl sHHU) norm_joinEr // setIAC -setIA -group_modl //.
    by rewrite (setIC W1) tiHUW1 mulg1.
  have sU1_UW1: U1 \subset U <*> W1 by rewrite subIset ?joing_subl.
  rewrite /gamma -(cfMod_cfun1 _ H) cfIndMod ?joing_subl //.
  rewrite cfMod_iso //= quotientYidl ?(subset_trans sU1_UW1) //.
  rewrite -(restrm_quotientE _ sU1_UW1) -(cfIsom_cfun1 (restr_isom _ isomMH)).
  rewrite (cfIndIsom isomMH) // {nH_UW1 isomMH}cfIsom_iso.
  rewrite -(cfIndInd _ (joing_subl U W1)) // cfInd_cfun1 //= -/U1 -/a.
  rewrite linearZ cfnormZ normr_nat /=; congr (_ * _).
  have defUW1: U ><| W1 = U <*> W1.
    by rewrite sdprodEY // -(setIidPl sUHU) -setIA tiHUW1 setIg1.
  apply: canLR (mulKf (neq0CG _)) _; rewrite -(sdprod_card defUW1) natrM -/q.
  rewrite mulrAC mulrDr mulrCA -{1}(Lagrange sU1U) /= -/U1 -/a -(Lagrange sCU).
  rewrite -card_quotient // !natrM !mulfK ?neq0CiG ?neq0CG //.
  transitivity (\sum_(x in U <*> W1) \sum_(w1 in W1) \sum_(w2 in W1)
                  (x ^ w1 \in U1 :&: U1 :^ w2)%g%:R : algC).
  - apply: eq_bigr => x _; rewrite (cfIndEsdprod _ _ defUW1) mulr_suml.
    apply: eq_bigr => w1 W1w1; rewrite rmorph_sum mulr_sumr.
    rewrite (reindex_inj invg_inj) (eq_bigl _ _ (groupV W1)) /=.
    rewrite (reindex_acts 'R _ (groupVr W1w1)) ?astabsR //=.
    apply: eq_bigr => w2 _; rewrite inE !cfuniE // rmorph_nat -natrM mulnb.
    by congr (_ && _)%:R; rewrite invMg invgK conjgM -mem_conjg.
  rewrite exchange_big /= mulr_natr -sumr_const; apply: eq_bigr => w1 W1w1.
  transitivity (\sum_(w in W1) #|U1 :&: U1 :^ w|%:R : algC).
    rewrite exchange_big /=; apply: eq_bigr => w W1w.
    rewrite (reindex_acts 'J _ (groupVr W1w1)) ?astabsJ ?normsG ?joing_subr //=.
    symmetry; rewrite big_mkcond -sumr_const /= big_mkcond /=.
    apply: eq_bigr => x _; rewrite conjgKV.
    by case: setIP => [[/(subsetP sU1_UW1)-> //] | _]; rewrite if_same.
  rewrite (big_setD1 1%g) //= conjsg1 setIid; congr (_ + _).
  rewrite [q](cardsD1 1%g) group1 /= mulr_natl -sumr_const.
  by apply: eq_bigr => w W1w; rewrite tiU1.
(* This is step (9.11.5). *)
have [gtS4alpha s4gt0]: (size S4)%:R > '[alpha] /\ (size S4 > 0)%N.
  suffices gtS4alpha: (size S4)%:R > '[alpha].
    by split=> //; rewrite -ltC_nat (ler_lt_trans (cfnorm_ge0 alpha)).
  rewrite Nalpha -(@ltr_pmul2r _ u%:R) ?ltr0n // mulrDl divfK ?neq0CG //.
  rewrite -(ltr_pmul2l (gt0CG W1)) -/q -mulrSr -!(natrM, natrD) ltC_nat.
  rewrite mulnA mulnAC -(ltn_add2r (p.-1 * (q + u))) oS4 {1}Dp addn1 -Da_p /=.
  apply: leq_ltn_trans (_ : q.+2 * a ^ 3 + q ^ 2 * a ^ 2 + 2 * q * a < _)%N.
    rewrite (addnC q) 2!mulnDr addnA (mulnAC _ a q) leq_add2r.
    rewrite mulnA addnAC -mulnDl mulnS -addnA -mulnDl addn2 mulnCA -mulnA.
    rewrite -[q in (_ <= _ + q * _)%N](prednK q_gt0) (mulSn q.-1) addnA.
     by rewrite leq_add2r mulnA -mulnDl addnC leq_mul.
  have q_gt2: (2 < q)%N.
    by rewrite ltn_neqAle prime_gt1 ?(contraTneq _ odd_q) => // <-.
  apply: leq_trans (_ : a.*2 ^ q + 'C(q, 2) * a.*2 ^ 2 + q * a.*2 <= _)%N.
    rewrite -mul2n (mulnCA q) (mulnA 2) ltn_add2r !expnMn -addSn leq_add //.
      apply: leq_ltn_trans (_ : q.-1.*2.+1 * a ^ q < _)%N.
        rewrite leq_mul ?leq_pexp2l //.
        by rewrite -(subnKC q_gt2) -addnn !addnS !ltnS leq_addl.
      rewrite ltn_pmul2r ?expn_gt0 ?a_gt0 // -doubleS.
      by rewrite -(prednK q_gt0) expnS mul2n leq_double ltn_expl.
    rewrite mulnA leq_pmul2r ?expn_gt0 ?a_gt0 // -(subnKC q_gt2).
    rewrite mulnCA mulnA addSn -mul_Sm_binm bin1 -mulnA leq_pmul2l //.
    by rewrite mulnS -addSnnS leq_addr.
  rewrite Dp -Da_p mul2n (addnC a.*2) expnDn -(subnKC q_gt2) !addSn add0n.
  rewrite 3!big_ord_recl big_ord_recr /= !exp1n /= bin1 binn !mul1n /bump /=.
  by do 2!rewrite addnC leq_add2l; apply: leq_addl.
have{cohS1} [tau1 cohS1] := cohS1; have [[Itau1 Ztau1] Dtau1] := cohS1.
have sS30: cfConjC_subset S3 (S_ H0C').
  split=> [|chi|chi]; first by rewrite filter_uniq ?seqInd_uniq.
    by rewrite mem_filter => /andP[].
  rewrite !mem_filter /= -!eqS12 => /andP[S1'chi S_chi].
  rewrite cfAut_seqInd // (contra _ S1'chi) //.
  by have [_ _ ccS1] := sS10; move/ccS1; rewrite cfConjCK.
have scohS3: subcoherent S3 tau rmR := subset_subcoherent scohS0 sS30.
have [tau3 cohS3]: coherent S3 M^# tau.
  apply: uniform_degree_coherence scohS3 _.
  apply: all_pred1_constant (q * u)%:R _ _.
  by rewrite all_map; apply/allP=> chi /S3qu.
have [IZtau3 Dtau3] := cohS3; have [Itau3 Ztau3] := IZtau3.
have notA1: 1%g \notin 'A(M) by have /subsetD1P[] := FTsupp_sub M.
have sS0_1A: {subset S_ H0C' <= 'CF(M, 1%g |: 'A(M))}.
  move=> _ /seqIndP[s /setDP[_ ker'H] ->]; rewrite inE in ker'H.
  by rewrite (prDade_Ind_irr_on (FT_prDade_hypF maxM MtypeP)).
have sS0A: {subset 'Z[S_ H0C', M^#] <= 'Z[irr M, 'A(M)]}.
  move=> chi; rewrite (zcharD1_seqInd_Dade _ notA1) //.
  by apply: zchar_sub_irr; apply: seqInd_vcharW.
have Zalpha: alpha \in 'Z[irr M].
  rewrite rpredB ?char_vchar ?cfInd_char ?rpred1 //.
  exact: seqInd_char (H0C_S1 _ S1psi1).
have ZAalpha: alpha \in 'Z[irr M, 'A(M)] by rewrite zchar_split Zalpha.
have [Itau Ztau]: {in 'Z[irr M, 'A(M)], isometry tau, to 'Z[irr G]}.
  apply: sub_iso_to (Dade_Zisometry _); last exact: zcharW.
  by apply: zchar_onS; apply: FTsupp_sub0.
have oSgamma: {in S_ H0C', forall lam, '[gamma, lam] = 0}.
  move=> _ /seqIndP[s /setDP[_ ker'H ] ->].
  rewrite ['Ind _]cfun_sum_constt cfdot_sumr big1 // => t sMt.
  rewrite cfdotZr [gamma]cfun_sum_constt cfdot_suml big1 ?mulr0 // => t0 gMt0.
  rewrite cfdotZl cfdot_irr (negPf (contraNneq _ ker'H)) ?mulr0 // => Dt0.
  rewrite inE (sub_cfker_constt_Ind_irr sMt) ?gFnorm // -Dt0.
  rewrite /gamma -irr0 in gMt0.
  rewrite -(sub_cfker_constt_Ind_irr gMt0) ?gFnorm ?joing_subl //.
    by rewrite irr0 cfker_cfun1 joing_subl.
  by rewrite (subset_trans _ sHUM) // join_subG sHHU subIset ?sUHU.
(* This is step (9.11.6). *)
have [/eqP psi1qa Spsi1]: psi1 1%g == (q * a)%:R /\ psi1 \in S_ H0C'.
  by move: S1psi1; rewrite mem_filter => /andP[].
have o_alpha_S3: orthogonal alpha^\tau (map tau3 S3).
  rewrite /orthogonal /= andbT all_map.
  apply: contraFT (ltr_geF gtS4alpha) => /allPn[lam0 S3lam0 /= alpha_lam0].
  set ca := '[_, _] in alpha_lam0; pose al0 := (-1) ^+ (ca < 0)%R *: alpha.
  have{alpha_lam0} al0_lam0: '[al0^\tau, tau3 lam0] > 0.
    have Zca: ca \in Cint by rewrite Cint_cfdot_vchar ?Ztau // Ztau3 ?mem_zchar.
    by rewrite linearZ cfdotZl (canLR (signrMK _) (CintEsign Zca)) normr_gt0.
  rewrite -Itau // -(cfnorm_sign (ca < 0)%R) -linearZ /= -/al0.
  have S4_dIirrK: {in map tau3 S4, cancel (dirr_dIirr id) (@dchi _ _)}.
    apply: dirr_dIirrPE => _ /mapP[lam S4lam ->].
    rewrite mem_filter -andbA negbK in S4lam.
    have [/irrP[i Dlam] _ S3lam] := and3P S4lam.
    by rewrite dirrE Itau3 ?Ztau3 ?mem_zchar //= Dlam cfnorm_irr.
  rewrite -(size_map tau3) -(size_map (dirr_dIirr id)).
  rewrite -(card_uniqP _); last first.
    rewrite !map_inj_in_uniq ?filter_uniq ?seqInd_uniq //.
      apply: sub_in2 (Zisometry_inj Itau3) => lam.
      by rewrite mem_filter => /andP[_ /mem_zchar->].
    exact: can_in_inj S4_dIirrK.
  apply: ler_trans (_ : #|dirr_constt al0^\tau|%:R <= _); last first.
    have Zal0: al0^\tau \in 'Z[irr G] by rewrite Ztau ?rpredZsign.
    rewrite cnorm_dconstt // -sumr_const ler_sum // => i al0_i.
    by rewrite sqr_Cint_ge1 ?gtr_eqF -?dirr_consttE // Cint_Cnat ?Cnat_dirr.
  rewrite leC_nat subset_leq_card //; apply/subsetP=> _ /mapP[nu S4nu ->].
  rewrite dirr_consttE S4_dIirrK //; congr (_ > 0): al0_lam0.
  rewrite {al0}linearZ !cfdotZl /=; congr (_ * _) => {ca}; apply/eqP.
  have{nu S4nu} [lam S4lam ->] := mapP S4nu.
  rewrite mem_filter in S4lam; have{S4lam} [_ S3lam] := andP S4lam.
  have Zdlam: lam0 - lam \in 'Z[S3, M^#].
    rewrite zcharD1E rpredB ?mem_zchar //= !cfunE subr_eq0.
    by have [/eqP->] := (S3qu _ S3lam, S3qu _ S3lam0).
  rewrite -subr_eq0 -cfdotBr -raddfB Dtau3 //.
  rewrite Itau // ?sS0A //; last exact: zchar_filter Zdlam.
  suffices{lam S3lam Zdlam} oS3a: {in S3, forall lam, '[alpha, lam] = 0}.
    by rewrite cfdotBr subr_eq0 !oS3a.
  move=> lam; rewrite mem_filter /= -eqS12 => /andP[S1'lam H0C'lam].
  by rewrite cfdotBl oSgamma // (seqInd_ortho _ Spsi1) ?(memPn S1'lam) // subr0.
have{s4gt0 gtS4alpha} /hasP[lam1 S4lam1 _]: has predT S4 by rewrite has_predT.
have [/irrP[l1 Dl1] S3lam1]: lam1 \in irr M /\ lam1 \in S3.
  by move: S4lam1; rewrite mem_filter -andbA negbK => /and3P[].
have [S1'lam1 Slam1]: lam1 \notin S1 /\ lam1 \in S_ H0C'.
  by move: S3lam1; rewrite mem_filter eqS12 => /andP[].
have S3lam1s: lam1^*%CF \in S3 by have [[_ _ ->]] := scohS3.
have ZS3dlam1: lam1 - lam1^*%CF \in 'Z[S3, M^#].
  rewrite zcharD1E rpredB ?mem_zchar //.
  by have:= seqInd_sub_aut_zchar nsHUM conjC Slam1; rewrite zcharD1 => /andP[].
have ZAdlam1: lam1 - lam1^*%CF \in 'Z[irr M, 'A(M)].
  rewrite sS0A // zchar_split rpredB ?mem_zchar ?cfAut_seqInd //.
  by rewrite (zchar_on ZS3dlam1).
pose beta := lam1 - (u %/ a)%:R *: psi1.
have ZAbeta: beta \in 'Z[irr M, 'A(M)].
  apply: sS0A; rewrite zcharD1E rpredB ?scaler_nat ?rpredMn ?mem_zchar //=.
  by rewrite !cfunE subr_eq0 psi1qa -natrM mulnCA divnK // S3qu.
have [_ _ poSS _ _] := scohS0; have [_ oSS] := pairwise_orthogonalP poSS.
have o1S1: orthonormal S1.
  rewrite orthonormalE filter_pairwise_orthogonal // andbT.
  by apply/allP=> _ /irrS1/irrP[t ->]; rewrite /= cfnorm_irr.
have o1S4: orthonormal S4.
  rewrite orthonormalE !filter_pairwise_orthogonal // andbT.
  apply/allP=> nu; rewrite mem_filter /= -andbA negbK.
  by case/andP=> /irrP[t ->]; rewrite cfnorm_irr.
have n1psi1: '[psi1] = 1 by have [_ -> //] := orthonormalP o1S1; rewrite eqxx.
have n1lam1: '[lam1] = 1 by have [_ -> //] := orthonormalP o1S4; rewrite eqxx.
have oS14tau: orthogonal (map tau1 S1) (map tau3 S4).
  apply/orthogonalP=> psi _ S1psi /mapP[lam /sS43 S3lam ->].
  apply: {psi lam S3lam}orthogonalP S1psi (map_f tau3 S3lam).
  apply: (coherent_ortho scohS0 sS10 cohS1 sS30 cohS3) => psi /=.
  by rewrite mem_filter !inE eqS12 => /andP[-> _].
have [Gamma [S4_Gamma normGamma [b Dbeta]]]:
  exists Gamma, [/\ Gamma \in 'Z[map tau3 S4], '[Gamma] = 1
    & exists b : bool, beta^\tau
        = Gamma - (u %/ a)%:R *: tau1 psi1 + b%:R *: \sum_(psi <- S1) tau1 psi].
- have [G S4G [G' [Dbeta _ oG'4]]] := orthogonal_split (map tau3 S4) beta^\tau.
  have [B S1B [Delta [dG' _ oD1]]] := orthogonal_split (map tau1 S1) G'.
  have sZS43: {subset 'Z[S4] <= 'Z[S3]} := zchar_subset sS43.
  have [Itau34 Ztau34] := sub_iso_to sZS43 sub_refl IZtau3.
  have Z_G: G \in 'Z[map tau3 S4].
    have [_ -> ->] := orthonormal_span (map_orthonormal Itau34 o1S4) S4G.
    rewrite big_seq rpred_sum // => xi S4xi; rewrite rpredZ_Cint ?mem_zchar //.
    rewrite -(addrK G' G) -Dbeta cfdotBl (orthoPl oG'4) // subr0.
    rewrite Cint_cfdot_vchar ?Ztau //.
    by have{xi S4xi} [xi S4xi ->] := mapP S4xi; rewrite Ztau34 ?mem_zchar.
  have oD4: orthogonal Delta (map tau3 S4).
    apply/orthoPl=> xi S4xi; rewrite -(addKr B Delta) addrC -dG' cfdotBl.
    by rewrite (orthoPl oG'4) // (span_orthogonal oS14tau) ?subrr // memv_span.
  have [_ -> dB] := orthonormal_span (map_orthonormal Itau1 o1S1) S1B.
  pose b := (u %/ a)%:R + '[B, tau1 psi1].
  have betaS1_B: {in S1, forall psi, '[beta^\tau, tau1 psi] = '[B, tau1 psi]}.
    move=> psi S1psi; rewrite Dbeta dG' !cfdotDl (orthoPl oD1) ?map_f // addr0.
    rewrite cfdotC (span_orthogonal oS14tau) ?rmorph0 ?add0r //.
    by rewrite memv_span ?map_f.
  have Zb: b \in Cint.
    rewrite rpredD ?rpred_nat // -betaS1_B // Cint_cfdot_vchar ?Ztau //.
    by rewrite Ztau1 ?mem_zchar.
  have{dB} dB: B = - (u %/ a)%:R *: tau1 psi1 + b *: \sum_(psi <- S1) tau1 psi.
    rewrite dB big_map !(big_rem _ S1psi1) /= scalerDr addrA -scalerDl addKr.
    rewrite scaler_sumr; congr (_ + _); apply: eq_big_seq => psi.
    rewrite mem_rem_uniq ?filter_uniq ?seqInd_uniq // => /andP[/= psi_1' S1psi].
    apply/esym/eqP; rewrite -subr_eq0 -scalerBl -addrA -!betaS1_B // -cfdotBr.
    have [/eqP psi_qa Spsi]: psi 1%g == (q * a)%:R /\ psi \in S_ H0C'.
      by move: S1psi; rewrite mem_filter => /andP[].
    have Z1dpsi: psi1 - psi \in 'Z[S1, M^#].
      by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE psi1qa psi_qa subrr.
    rewrite -raddfB Dtau1 // Itau //; last first.
      by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi).
    rewrite cfdotC cfdotBr cfdotZr !cfdotBl 2?oSS ?(memPn S1'lam1) // subrr.
    by rewrite add0r n1psi1 oSS // subr0 mulr1 rmorphN conjCK subrr scale0r.
  have Gge1: 1 <= '[G] ?= iff ('[G] == 1).
    rewrite eq_sym; apply: lerif_eq.
    have N_G: '[G] \in Cnat.
      apply: Cnat_cfnorm_vchar; apply: zchar_sub_irr Z_G => _ /mapP[nu S4nu ->].
      by rewrite Ztau34 ?mem_zchar.
    rewrite -(truncCK N_G) ler1n lt0n -eqC_nat truncCK {N_G}// cfnorm_eq0.
    have: '[beta^\tau, (lam1 - lam1^*%CF)^\tau] != 0.
      rewrite Itau // cfdotBl cfdotZl !cfdotBr n1lam1.
      rewrite (seqInd_conjC_ortho _ _ _ Slam1) ?mFT_odd // subr0.
      rewrite !oSS ?cfAut_seqInd -?(inv_eq (@cfConjCK _ _)) ?(memPn S1'lam1) //.
        by rewrite !(subr0, mulr0) oner_eq0.
      by have [_ _ ->] := sS10.
    rewrite Dbeta -Dtau3 //; apply: contraNneq => ->.
    rewrite add0r raddfB cfdotBr !(orthoPl oG'4) ?map_f ?subr0 //.
    move: S4lam1; rewrite ![_ \in S4]mem_filter /= !negbK /= cfAut_irr S3lam1s.
    by case/andP=> /andP[-> /cfAut_seqInd->].
  have ubG: '[G] + (b ^+ 2 - b) * (u %/ a).*2%:R + '[Delta] = 1.
    apply: (addrI ((u %/ a) ^ 2)%:R); transitivity '[beta^\tau].
      rewrite -!addrA addrCA Dbeta cfnormDd; last first.
        by rewrite cfdotC (span_orthogonal oG'4) ?rmorph0 // memv_span ?inE.
      congr (_ + _); rewrite !addrA dG' cfnormDd; last first.
        by rewrite cfdotC (span_orthogonal oD1) ?rmorph0 // memv_span ?inE.
      congr (_ + _); rewrite dB scaleNr [- _ + _]addrC cfnormB !cfnormZ.
      rewrite normr_nat Cint_normK // scaler_sumr cfdotZr rmorph_nat.
      rewrite cfnorm_map_orthonormal // cfproj_sum_orthonormal //.
      rewrite Itau1 ?mem_zchar // n1psi1 mulr1 rmorphM rmorph_nat conj_Cint //.
      rewrite -mulr2n oS1ua -muln_divA // mul2n -addrA addrCA -natrX mulrBl.
      by congr (_ + (_ - _)); rewrite -mulrnAl -mulrnA muln2 mulrC.
    rewrite Itau // cfnormBd; last first.
      by rewrite cfdotZr oSS ?mulr0 // (memPnC S1'lam1).
    by rewrite cfnormZ normr_nat n1psi1 n1lam1 mulr1 addrC -natrX.
  have ubDelta: '[G] <= '[G] + '[Delta] ?= iff (Delta == 0).
    rewrite addrC -lerif_subLR subrr -cfnorm_eq0 eq_sym.
    by apply: lerif_eq; apply: cfnorm_ge0.
  have{ubG} ubDeltaG: '[G] + '[Delta] <= 1 ?= iff pred2 0 1 b.
    rewrite -{1}ubG addrAC [_ + _ + _] addrC -lerif_subLR subrr /=.
    set n := _%:R; rewrite mulrC -{1}(mulr0 n) mono_lerif; last first.
      by apply: ler_pmul2l; rewrite ltr0n double_gt0 divn_gt0 // dvdn_leq.
    rewrite /= -(subr_eq0 b 1) -mulf_eq0 mulrBr mulr1 eq_sym.
    apply: lerif_eq; rewrite subr_ge0.
    have [-> | nz_b] := eqVneq b 0; first by rewrite expr2 mul0r.
    rewrite (ler_trans (real_ler_norm _)) ?Creal_Cint // -[`|b|]mulr1.
    by rewrite -Cint_normK // ler_pmul2l ?normr_gt0 // norm_Cint_ge1.
  have [_ /esym] := lerif_trans Gge1 (lerif_trans ubDelta ubDeltaG).
  rewrite eqxx => /and3P[/eqP normG1 /eqP Delta0 /pred2P b01].
  exists G; split=> //; exists (b != 0).
  rewrite Dbeta dG' Delta0 addr0 dB scaleNr addrA; congr (_ + _ *: _).
  by case: b01 => ->; rewrite ?eqxx ?oner_eq0.
(* Final step (9.11.8). *)
have alpha_beta: '[alpha^\tau, beta^\tau] = (u %/ a)%:R.
  rewrite Itau // cfdotBr cfdotZr rmorph_nat !cfdotBl !oSgamma // !sub0r.
  by rewrite n1psi1 mulrN opprK mulr1 addrC oSS ?subr0 // (memPn S1'lam1).
have [X S1X [Delta [Dalpha _ oD1]]]:= orthogonal_split (map tau1 S1) alpha^\tau.
pose x := 1 + '[X, tau1 psi1].
have alphaS1_X: {in S1, forall psi, '[alpha^\tau, tau1 psi] = '[X, tau1 psi]}.
  by move=> psi S1psi; rewrite Dalpha cfdotDl (orthoPl oD1) ?map_f // addr0.
have Zx: x \in Cint.
  rewrite rpredD ?rpred1 // -alphaS1_X // Cint_cfdot_vchar ?Ztau //.
  by rewrite Ztau1 ?mem_zchar.
have{alphaS1_X S1X} defX: X = x *: (\sum_(psi <- S1) tau1 psi) - tau1 psi1.
  have [_ -> ->] := orthonormal_span (map_orthonormal Itau1 o1S1) S1X.
  rewrite addrC -scaleN1r big_map !(big_rem _ S1psi1) /= scalerDr addrA.
  rewrite -scalerDl addKr scaler_sumr; congr (_ + _); apply: eq_big_seq => psi.
  rewrite mem_rem_uniq ?filter_uniq ?seqInd_uniq // => /andP[/= psi_1' S1psi].
  apply/esym/eqP; rewrite -subr_eq0 -scalerBl -addrA -!alphaS1_X // -cfdotBr.
  have [/eqP psi_qa Spsi]: psi 1%g == (q * a)%:R /\ psi \in S_ H0C'.
    by move: S1psi; rewrite mem_filter => /andP[].
  have Z1dpsi: psi1 - psi \in 'Z[S1, M^#].
    by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE psi1qa psi_qa subrr.
  rewrite -raddfB Dtau1 // Itau //; last first.
    by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi).
  rewrite cfdotBr !cfdotBl !oSgamma // n1psi1 cfdotC oSS // rmorph0.
  by rewrite !subr0 add0r subrr scale0r.
have{x Zx X defX Delta Dalpha oD1} b_mod_ua: (b == 0 %[mod u %/ a])%C.
  rewrite -oppr0 -eqCmodN (eqCmod_trans _ (eqCmodm0 _)) // {2}nCdivE.
  rewrite -alpha_beta Dbeta -addrA cfdotDr.
  rewrite (span_orthogonal o_alpha_S3) ?add0r; first 1 last.
  - by rewrite memv_span ?inE.
  - apply: subvP (zchar_span S4_Gamma); apply: sub_span; apply: mem_subseq.
    by rewrite map_subseq ?filter_subseq.
  rewrite Dalpha addrC cfdotDl (span_orthogonal oD1); first 1 last.
  - by rewrite memv_span ?inE.
  - rewrite addrC rpredB ?rpredZ //; last by rewrite memv_span ?map_f.
    by rewrite big_seq rpred_sum // => psi S1psi; rewrite memv_span ?map_f.
  rewrite add0r addrC defX cfdotBr cfdotBl cfdotZl cfdotZr !scaler_sumr.
  rewrite cfdotZr !rmorph_nat cfdotBl Itau1 ?mem_zchar // n1psi1.
  rewrite cfnorm_map_orthonormal // cfdotC !cfproj_sum_orthonormal //.
  rewrite rmorph_nat oS1ua -muln_divA // natrM !mulrA addrC mulrC addrA.
  rewrite -mulNr -mulrDl eqCmod_sym eqCmod_addl_mul // addrC !rpredB ?rpred1 //.
  by rewrite !rpredM ?rpred_nat.
have{b_mod_ua alpha_beta} b0: b = 0%N :> nat.
  have:= b_mod_ua; rewrite /eqCmod subr0 dvdC_nat => /eqnP.
  rewrite modn_small // (leq_ltn_trans (leq_b1 b)) // ltn_divRL // mul1n.
  by rewrite ltn_neqAle -(eqn_pmul2l q_gt0) eq_sym ne_qa_qu dvdn_leq.
exists lam1 => //; suffices: coherent (lam1 :: lam1^* :: S1)%CF M^# tau.
  by apply: subset_coherent => phi; rewrite !inE eqS12.
move: Dbeta; rewrite b0 scale0r addr0.
apply: (extend_coherent_with scohS0 sS10 cohS1); first by [].
rewrite rpred_nat psi1qa -natrM mulnCA (eqP (S3qu _ S3lam1)) divnK //.
rewrite cfdotC (span_orthogonal oS14tau) ?(zchar_span S4_Gamma) ?conjC0 //.
by rewrite rpredZ ?memv_span ?map_f.
Qed.

End Nine.