proposition: Theorem prTIres_irr_cases k (theta := 'chi_k) (phi := 'Ind theta) : {j | theta = chi_ j} + {phi \in irr L /\ (forall i j, phi != mu2_ i j)}.
proof: Proof. pose imIchi := [set Ichi j | j : Iirr W2]. have [/imsetP/sig2_eqW[j _] | imIchi'k] := boolP (k \in imIchi). by rewrite /theta => ->; left; exists j. suffices{phi} theta_inv: 'I_L[theta] = K. have irr_phi: phi \in irr L by apply: inertia_Ind_irr; rewrite ?theta_inv. right; split=> // i j; apply: contraNneq imIchi'k => Dphi; apply/imsetP. exists j => //; apply/eqP; rewrite -[k == _]constt_irr -(cfRes_prTIirr i). by rewrite -constt_Ind_Res -/phi Dphi irr_consttE cfnorm_irr oner_eq0. rewrite -(sdprodW (sdprod_modl defL (sub_inertia _))); apply/mulGidPl. apply/subsetP=> z /setIP[W1z Itheta_z]; apply: contraR imIchi'k => K'z. have{K'z} [Lz ntz] := (subsetP sW1L z W1z, group1_contra K'z : z != 1%g). have [p p_pr p_z]: {p | prime p & p %| #[z]} by apply/pdivP; rewrite order_gt1. have coKp := coprime_dvdr (dvdn_trans p_z (order_dvdG W1z)) coKW1. wlog{p_z} p_z: z W1z Lz Itheta_z ntz / p.-elt z. move/(_ z.`_p)->; rewrite ?groupX ?p_elt_constt //. by rewrite (sameP eqP constt1P) /p_elt p'natE ?negbK. have JirrP: is_action L (@conjg_Iirr gT K); last pose Jirr := Action JirrP. split=> [y k1 k2 eq_k12 | k1 y1 y2 Gy1 Gy2]; apply/irr_inj. by apply/(can_inj (cfConjgK y)); rewrite -!conjg_IirrE eq_k12. by rewrite !conjg_IirrE (cfConjgM _ nsKL). have [[_ nKL] [nKz _]] := (andP nsKL, setIdP Itheta_z). suffices{k theta Itheta_z} /eqP->: imIchi == 'Fix_Jirr[z]. by apply/afix1P/irr_inj; rewrite conjg_IirrE inertiaJ. rewrite eqEcard; apply/andP; split. apply/subsetP=> _ /imsetP[j _ ->]; apply/afix1P/irr_inj. by rewrite conjg_IirrE -(cfRes_prTIirr 0) (cfConjgRes _ _ nsKL) ?cfConjg_id. have ->: #|imIchi| = w2 by rewrite card_imset //; apply: prTIres_inj. have actsL_KK: [acts L, on classes K | 'Js \ subsetT L]. rewrite astabs_ract subsetIidl; apply/subsetP=> y Ly; rewrite !inE /=. apply/subsetP=> _ /imsetP[x Kx ->]; rewrite !inE /= -class_rcoset. by rewrite norm_rlcoset ?class_lcoset ?mem_classes ?memJ_norm ?(subsetP nKL). rewrite (card_afix_irr_classes Lz actsL_KK) => [|k x y Kx /=]; last first. by case/imsetP=> _ /imsetP[t Kt ->] ->; rewrite conjg_IirrE cfConjgEJ ?cfunJ. apply: leq_trans (subset_leq_card _) (leq_imset_card (class^~ K) _). apply/subsetP=> _ /setIP[/imsetP[x Kx ->] /afix1P/normP nxKz]. suffices{Kx} /pred0Pn[t /setIP[xKt czt]]: #|'C_(x ^: K)[z]| != 0%N. rewrite -(class_eqP xKt); apply: imset_f; have [y Ky Dt] := imsetP xKt. by rewrite -(@prKW1 z) ?(czt, inE) ?ntz // Dt groupJ. have{coKp}: ~~ (p %| #|K|) by rewrite -prime_coprime // coprime_sym. apply: contraNneq => /(congr1 (modn^~ p))/eqP; rewrite mod0n. rewrite -cent_cycle -afixJ -sylow.pgroup_fix_mod ?astabsJ ?cycle_subG //. by move/dvdn_trans; apply; rewrite -index_cent1 dvdn_indexg. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)