adapt to rocq-prover/rocq#20707

theories/BGappendixC.v

@@ -485,7 +485,7 @@ have{Fp_w Dz} [n Dz]: exists n, sigma z = sigma ((s ^+ n) ^ u).
   by rewrite -{1}(natr_Zp n) scaler_nat mulr_natr conjXg !sigmaE ?in_PU.
 exists u^-1; last exists (u * v); rewrite ?groupV ?groupM //.
 exists (s ^+ n); rewrite ?groupX // mulgA; congr (_ * _).
-by apply: (injmP inj_sigma); rewrite -?mulgA ?in_PU.
+by apply: (injmP inj_sigma); rewrite // -?mulgA // -conjgE ?in_PU.
 Qed.
 
 (* This is B & G, Appendix C, Lemma C.3, Step 2. *)

theories/BGsection1.v

@@ -99,7 +99,7 @@
 End Definitions.
 
 (* This must be defined outside a Section to avoid spurrious delta-reduction *)
 Definition Puig_at := nosimpl Puig_rec.
 
 Definition Puig_inf (gT : finGroupType) (G : {set gT}) := Puig_at #|G|.*2 G.
 
@@ -596,7 +596,7 @@
   rewrite -quotientSK ?subsetIl // cosetpreK.
   by rewrite -coprime_norm_quotient_pgroup cent_sub.
 apply/eqP; rewrite eqEsubset subsetI -sub_quotient_pre ?subsetIr //.
-rewrite quotientInorm quotient_cents //= andbC subIset ?cent_sub //=.
+rewrite quotientInorm quotient_cents //= andbC /C subIset ?cent_sub //=.
 have nMC': 'N_Cq(T) \subset 'N(M) by rewrite subIset ?subsetIl.
 rewrite subsetI nMC' andbT (sameP commG1P trivgP) /=.
 rewrite -(coprime_TIg coMT) subsetI commg_subr subsetIr andbT.
@@ -789,7 +789,7 @@
 Variables (gT : finGroupType) (G S : {group gT}) (p : nat).
 Hypothesis sylS : p.-Sylow(G) S.
 
 Import finalg FiniteModule GRing.Theory.
 
 (* This is B & G, Theorem 1.17 ("Focal Subgroup Theorem", D. G. Higman), also *)
 (* Gorenstein Theorem 7.3.4 and Aschbacher (37.4).                            *)

theories/BGsection10.v

@@ -313,7 +313,7 @@ rewrite actM (orbit_transl _ (mem_orbit _ _ _)); last first.
 have [|w x nM0Pw cPx ->] := imset2P (_ : u \in 'N_M0(P) * 'C(P)).
   rewrite normC ?part_c ?IHX //; first by case/setIP: nLPu.
   by rewrite setIC subIset ?cent_norm.
-rewrite actM /= conjGid ?mem_orbit //; last by case/setIP: nM0Pw.
+rewrite actM /= (@conjGid _ M0) ?mem_orbit //; last by case/setIP: nM0Pw.
 by rewrite (subsetP (centS (subset_trans (proper_sub ltXX1) sX1P))).
 Qed.
 

theories/BGsection12.v

@@ -1917,7 +1917,7 @@ have t1q: q \in \tau1(M).
   by rewrite -subG1 quotient_sub1.
 have cycQ1: cyclic Q1.
   have [x _ sQ1E1x] := Hall_psubJ hallE1 t1q sQ1E qQ1.
-  by rewrite (cyclicS sQ1E1x) ?cyclicJ.
+  by rewrite (cyclicS sQ1E1x) // cyclicJ cycE1.
 have defQ1: Q :&: E = Q1.
   apply: (sub_pHall sylQ1) (subsetIr Q E); last by rewrite subsetI sQ1Q.
   by rewrite (pgroupS (subsetIl Q _)).

theories/BGsection14.v

@@ -411,7 +411,8 @@ Lemma sigma'_kappa'_facts M p S (A := 'Ohm_1(S)) (Ms := M`_\sigma) :
  [/\ M \in 'M_'F :|: 'M_'P2, logn p #|A| <= 2, 'C_Ms(A) = 1 & nilpotent Ms].
 Proof.
 move=> maxM sylS /and3P[piMp sM'p kM'p]; have [sSM pS _] := and3P sylS.
-rewrite 8!(maxM, inE) /= !andbT negb_and orb_andr orbN andbT negbK.
+rewrite 6!(maxM, inE) [M \in 'M_'F]inE maxM /=.
+rewrite !andbT negb_and orb_andr orbN andbT negbK.
 rewrite (contra (fun skM => pnatPpi skM piMp)) ?orbT; last exact/norP.
 rewrite partition_pi_mmax // (negPf sM'p) orbF orbCA in piMp.
 have{piMp} [t2p | t13p] := orP piMp.
@@ -1265,7 +1266,7 @@ have{sg_x} [ntx /imsetP[M maxM def_x]] := setD1P sg_x.
 wlog MSxM: M maxM def_x / M \in 'M_\sigma[x].
   have sMx: \sigma(M).-elt x by rewrite def_x p_elt_constt.
   have [|[z Ms_xz] _] := sigma_Jsub maxM sMx; first by rewrite cycle_eq1.
-  move/(_ (M :^ z^-1)%G)->; rewrite ?mmaxJ ?(eq_constt _ (sigmaJ M _)) //.
+  move/(_ (M :^ z^-1)%G)-> => //; [by rewrite mmaxJ | by rewrite (eq_constt _ (sigmaJ M _)) | ].
   by rewrite inE mmaxJ maxM MsigmaJ -sub_conjg.
 have ell1x: \ell_\sigma(x) == 1%N.
   by apply/ell_sigma1P; split=> //; apply/set0Pn; exists M.
@@ -1799,7 +1800,7 @@ have oTGgt_g2: (g / 2 < #|TG|%:R)%R.
   by rewrite ler_pM ?hm_inc ?hm_ge0 //= odd_geq ?(leq_trans _ ltpq).
 have defZhat: Z :\: (K :|: Ks) = T.
   rewrite /T cover_imset big_setU1 //= defMNX big_set1 defKs_star Ks0.
-  by rewrite -setDUl setDDl setUC setD1K // inE group1.
+  by rewrite -setDUl setDDl setUC setD1K // inE /Ks group1.
 rewrite defZhat {1}defKs; split; first 2 [by split].
 - by rewrite -defKs_star; case/Ptype_structure: hallKstar => // _ _ [].
 - split=> [|p]; first by rewrite -defKs_star defKs.
@@ -1963,7 +1964,7 @@ have tiPcover: trivIset Pcover.
   rewrite -!{1}sigma_supportJ setI_eq0 sigma_support_disjoint ?mmaxJ //.
   apply: contra notMGH; rewrite {a Ga}(orbit_transl _ (mem_orbit _ _ Ga)).
   rewrite {b Gb}(orbit_eqP (mem_orbit _ _ Gb))=> /imsetP[c Gc ->] /=.
-  by rewrite sigma_supportJ class_supportGidl.
+  by rewrite [in X in _ == X]sigma_supportJ class_supportGidl.
 have ntPcover: cover Pcover \subset G^#.
   apply/bigcupsP=> _ /imsetP[M maxM ->]; rewrite class_supportEr.
   apply/bigcupsP=> a _; rewrite subsetD1 subsetT mem_conjg conj1g {a}//=.

theories/BGsection15.v

@@ -400,7 +400,7 @@ have defQ: 'O_q(Ms) = Q by rewrite -(setIidPl sQMs) pcore_setI_normal.
 have sylQ: q.-Sylow(Ms) Q.
   have nsQMs: Q <| Ms by rewrite -defQ pcore_normal.
   rewrite -(pquotient_pHall qQ) // /= -/Q -{3}defQ.
-  by rewrite -(pquotient_pcore _ qQ) ?nilpotent_pcore_Hall.
+  by rewrite -(pquotient_pcore nsQMs qQ) //= nilpotent_pcore_Hall.
 have{sMq hallMs} sylQ_M := subHall_Sylow hallMs sMq sylQ.
 have sQ_MF: Q \subset M`_\F.
   by rewrite sub_gen ?(bigcup_max [group of Q]) ?(p_Sylow sylQ_M) ?pcore_normal.

theories/BGsection2.v

@@ -259,13 +259,13 @@
 have splitF: group_splitting_field F (Zp_group h).
   move: prim_eps (abelianS (subsetT (Zp h)) (Zp_abelian _)).
   by rewrite -{1}(card_Zp h_gt0); apply: primitive_root_splitting_abelian.
 have F'Zh: [char F]^'.-group (Zp h).
   apply/pgroupP=> p p_pr; rewrite card_Zp // => /dvdnP[d def_h].
   apply/negP=> /= charFp.
   have d_gt0: d > 0 by move: h_gt0; rewrite def_h; case d.
   have: eps ^+ d == 1.
     rewrite -(inj_eq (fmorph_inj (Frobenius_aut charFp))).
     by rewrite rmorph1 /= Frobenius_autE -exprM -def_h eps_h.
   by rewrite -(prim_order_dvd prim_eps) gtnNdvd // def_h ltn_Pmulr // prime_gt1.
 case: (ltngtP h 1) => [|h_gt1|h1]; last first; last by rewrite ltnNge h_gt0.
   rewrite /sumV mxdirectE /= h1 !big_ord1; split=> //.
@@ -1104,9 +1104,10 @@
   by rewrite !exprS mulmxA rQ_lam // -scalemxAl IHk scalerA.
 pose f b := (lam P1 b, lam P2 b).
 have inj_f: {in Q &, injective f}.
-  move=> b c Qb Qc /= [eq_bc1 eq_bc2]; apply: (mx_faithful_inj ffulQ) => //.
+  move=> b c Qb Qc; rewrite /f [lam]lock => [=]; rewrite -lock => eq_bc1 eq_bc2.
+  apply: (mx_faithful_inj ffulQ Qb Qc).
   rewrite -[rQ b]mul1mx -[rQ c]mul1mx {}def1 !mulmxDl -!mulmxA.
-  by rewrite !{1}rQ_lam ?eq_bc1 ?eq_bc2.
+  by rewrite ![P1 *m _]rQ_lam ?[P2 *m _]rQ_lam ?eq_bc1 ?eq_bc2.
 pose rs := [set x : 'F_p | x ^+ q == 1].
 have s_fQ_rs: f @: Q \subset setX rs rs.
   apply/subsetP=> _ /imsetP[b Qb ->].

theories/BGsection3.v

@@ -1004,7 +1004,7 @@ case cKK: (abelian K); last first.
     have Kx: x \in K by rewrite -cycle_subG -defCKR subsetIl.
     rewrite defCKR cycle_subG in not_sCKR_K' *.
     exact: nt_prime_order (exponentP eK x Kx) (group1_contra not_sCKR_K').
-  have tiCKR_K': 'C_K(R) :&: K' = 1 by rewrite prime_TIg ?oCKR.
+  have tiCKR_K': 'C_K(R) :&: K' = 1 by rewrite (@prime_TIg _ _ K') ?oCKR.
   have sKR_K: [~: K, R] \subset K by rewrite commg_subl nKR.
   have ziKRcR: 'C_K(R) :&: [~: K, R] \subset K'.
     rewrite -quotient_sub1 ?subIset ?nK'K // setIC.

theories/BGsection4.v

@@ -1384,7 +1384,7 @@ have hallGp'pi: pi.-Hall(Gp') 'O_pi(Gp').
   rewrite (pgroupP p'G) ?pdiv_dvd ?pdiv_prime // cardG_gt1.
   by apply: contra not_pi_G; move/eqP->; rewrite (trivgP (pcore_sub _ _)).
 have defGp'pi: 'O_pi(Gp') = 'O_pi(G).
-  rewrite -pcoreI; apply: eq_pcore => q; apply: andb_idr.
+  rewrite -[LHS]pcoreI; apply: eq_pcore => q; apply: andb_idr.
   by apply: contraL => /=; move/eqnP->.
 have hallGp': p^'.-Hall(G) Gp' by rewrite rank2_min_p'core_Hall.
 rewrite pHallE pcore_sub /= -defGp'pi (card_Hall hallGp'pi) (card_Hall hallGp').

theories/BGsection6.v

@@ -146,7 +146,7 @@ rewrite quotientGI ?subsetI ?sU'U ?dergS ?coprime_TIg //= -/G' -/U'.
 have sUG'_UKb: (U :&: G') / U' \subset (U :&: K) / U'.
   rewrite quotientSK // -normC ?group_modr ?setIS //.
   by rewrite -quotientSK ?comm_subG ?quotient_der // -defG quotientMidl.
-rewrite (coprimeSg sUG'_UKb) // -(card_isog (second_isog _)) //=.
+rewrite (coprimeSg sUG'_UKb) //= -(card_isog (second_isog _)) //=.
 rewrite setIA (setIidPl sU'U) coprime_morphl ?coprime_morphr //.
 exact: coprimeSg (subsetIr U K) coKH.
 Qed.

theories/BGsection7.v

@@ -749,7 +749,7 @@ exists (k * g); last first.
   by apply: val_inj; rewrite /= conjsgM -(normP nQ2g) defQ2.
 rewrite /KP -defK // (subsetP (subsetIl _ 'C(B))) //= setIAC defK // -/KB.
 rewrite -coprime_norm_cent 1?coprime_sym ?(pnat_coprime piP) //= -/KB.
-rewrite inE groupM //; apply/normP.
+rewrite inE /KB groupM //; apply/normP.
 by rewrite -{2}(conjsgK z P) (conjGid Pz) {2}defP /= !conjsgM conjsgK.
 Qed.
 
@@ -937,7 +937,7 @@ have cYKq: Y / K \subset 'C('O_p(X / K)).
   - by rewrite coprime_sym.
   - exact: pgroup_nil (pcore_pgroup _ _).
   apply: subset_trans (cYAq); rewrite -defCA -['C_P(A) / K](morphim_restrm nKP).
-  rewrite injm_cent ?ker_restrm ?ker_coset ?morphim_restrm -?quotientE //.
+  rewrite injm_cent ?ker_restrm ?ker_coset ?(morphim_restrm nKP) -?quotientE //.
     rewrite setIid (setIidPr sAP) setISS ?centS //.
     by rewrite pcore_sub_Hall ?morphim_pHall.
   by rewrite coprime_TIg ?(pnat_coprime _ (pcore_pgroup _ _)).

theories/PFsection10.v

@@ -782,7 +782,7 @@ apply: le_trans (_ : 1 - (3^-1 + 7^-1) <= _); last first.
   have frobUW2 := Ptype_compl_Frobenius maxS StypeP notStype5.
   apply: leq_ltn_trans (ltn_odd_Frobenius_ker frobUW2 (mFT_odd _)).
   by rewrite (leq_double 3).
-apply: le_trans (_ : 2^-1 <= _); last by rewrite -!CratrE; compute.
+apply: le_trans (_ : 2^-1 <= _); last by rewrite -11!CratrE; compute.
 rewrite mulrAC ler_pdivrMr 1?gt0CG // ler_pdivlMl ?ltr0n //.
 rewrite -!natrM ler_nat mulnA -(Lagrange (normal_sub nsM''M')) mulnC leq_mul //.
   by rewrite subset_leq_card //; have [_ _ _ []] := MtypeP.

theories/PFsection11.v

@@ -856,7 +856,7 @@ have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1.
   have{psi_phi} col0_beta: '[eta_col 0, beta] = a. (* Also part of (11.8.5). *)
     apply/(addIr (-1 + n))/(canRL (addNKr _)).
     rewrite addrCA addrA addrACA -{}psi_phi Dpsi cfdotBl; congr (_ + _).
-      rewrite -(betaE i j) // cfdotDr !cfdotBr -/phi cfdotZr -!addrA.
+      rewrite -(betaE i j) // cfdotDr 2!cfdotBr -/phi (cfdotZr n _ zeta1) -!addrA.
       apply/(canLR (addNKr _)); rewrite addNr !cfdot_suml.
       rewrite big1 ?add0r ?opprK => [|k _]; last first.
         by rewrite cfdot_cycTIiso andbC eq_sym (negPf nz_j1).

theories/PFsection12.v

@@ -1025,7 +1025,7 @@ have{ub_e} ub_a: p.-1.*2%:R * a ^+ 2 - 2 * a <= p.-1%:R / 2 :> algC.
 have a0: a = 0.
   apply: contraTeq ub_a => nz_a; rewrite lt_geF // ltr_pdivrMr ?ltr0n //.
   rewrite mulrC -{1}mulr_natl -muln2 natrM -mulrA mulrBr mulrCA ltrBrDl.
-  rewrite -ltrBrDr -mulrBr mulr_natl mulrA -expr2 -exprMn.
+  rewrite -ltrBrDr -mulrBr (mulr_natl a) mulrA -expr2 -exprMn.
   apply: lt_le_trans (_ : 2 * ((a *+ 2) ^+ 2 - 1) <= _); last first.
     rewrite (mulr_natl a 2) ler_wpM2r // ?subr_ge0.
       by rewrite sqr_intr_ge1 ?rpredMn // mulrn_eq0.

theories/PFsection13.v

@@ -1161,7 +1161,7 @@ have ->: #|V| = v by rewrite /v D_1 indexg1.
 rewrite mulnC !natrM invfM mulrA mulfK ?neq0CiG //.
 have [_ [_ oQ] _ _ _] := FTtypeP_facts maxT TtypeP; rewrite -/p -/q /= in oQ.
 rewrite Dv natf_div ?dvdn_pred_predX // oQ.
-rewrite invfM invrK -mulrA -subn1 mulVKf ?gt_eqF ?ltr0n //; last first.
+rewrite invfM invrK -(mulrA _ (q.-1)%:R) -subn1 mulVKf ?gt_eqF ?ltr0n //; last first.
   by rewrite subn_gt0 -(exp1n p) ltn_exp2r ltnW // ltnW.
 rewrite -oQ natrB ?cardG_gt0 // !mulrBl mul1r mulrC mulKf ?neq0CG // -invfM.
 by rewrite -natrM oQ opprD opprK addrA [LHS]addrAC.
@@ -1203,9 +1203,9 @@ pose d r : algC := (3 ^ r.-1)%:R^-1; pose f r := (r ^ 2)%:R * d r.
 have Dm: m = (1 - d p) / 2.
   rewrite mulrBl mul1r -mulrN mulrC /m q3 /= addrAC -addrA natrM invfM -mulrBl.
   rewrite -{1}(ltn_predK pgt2) expnS natrM invfM mulrA.
-  by congr (_ + _ / _); apply/eqP; rewrite -!CratrE; compute.
+    by congr (_ + _ / _); rewrite -!CratrE.
 split; last apply: le_lt_trans gen_lb_uc.
-  apply: lt_le_trans (_ : (1 - d 5%N) / 2 <= _).
+apply: lt_le_trans (_ : (1 - d 5%N) / 2 <= _).
     by rewrite /d -!CratrE; compute.
   rewrite Dm ler_pM2r ?invr_gt0 ?ltr0n // lerD2l lerN2.
   rewrite lef_pV2 ?qualifE/= ?ltr0n ?expn_gt0 // leC_nat leq_pexp2l //=.
@@ -1818,7 +1818,7 @@ have q_dv_u1: q %| u.-1 := Frobenius_dvd_ker1 frobUW1.
 have [nP_UW1 /isomP[/=]] := sdprod_isom defS_P; set h := restrm _ _ => injh hS.
 have /joing_sub[sUUW1 sW1UW1] := erefl (U <*> W1).
 have [hU hW1]: h @* U = Ubar /\ h @* W1 = W1bar.
-  by rewrite !morphim_restrm /= !(setIidPr _).
+  by rewrite /h !(morphim_restrm nP_UW1) /= !(setIidPr _).
 have{hS} frobSbar: [Frobenius Sbar = Ubar ><| W1bar].
   by rewrite -[Sbar]hS -hU -hW1 injm_Frobenius.
 have tiW1bar: normedTI W1bar^# Sbar W1bar by have /and3P[] := frobSbar.

theories/PFsection14.v

@@ -792,8 +792,8 @@ have nzT1_Ga zeta: zeta \in calT1 -> `|'[Gamma, tau1T zeta]| ^+ 2 >= 1.
   pose Delta := tauT betaT0 - 1 + tau1T zeta.
   have nz_i1: #1 != 0 := Iirr1_neq0 ntW2.
   rewrite -(canLR (addKr _) (erefl Delta)) opprB cfdotDr cfdotBr oGa1 add0r.
-  rewrite cfdotDl cfdotBl -/betaS o_eta0_betaT0 (negPf nz_i1) // addr0 opprB.
-  rewrite -(cycTIiso1 pddS) -(cycTIirr00 defW) {}o_eta0_betaT0 mulr1n.
+  rewrite cfdotDl cfdotBl -/betaS [X in _ - _ + X]o_eta0_betaT0 (negPf nz_i1) // addr0 opprB.
+  rewrite -(cycTIiso1 pddS) -(cycTIirr00 defW) {}[X in X + _ + _]o_eta0_betaT0 mulr1n.
   have QV'betaS: tauS betaS \in 'CF(G, ~: class_support QV^# G).
     have [_ [pP _] _ _ [_ ->]] := FTtypeP_facts _ StypeP; rewrite ?A0betaS //.
     apply: cfun_onS (cfInd_on (subsetT S) (PVbetaS _ nz_i1)).

theories/PFsection2.v

@@ -370,7 +370,7 @@ apply: eq_bigr => a /sTA=> {T sTA}Aa.
 have [La def_Ca] := (subsetP sAL a Aa, defCA Aa).
 rewrite (eq_bigr (fun _ => alpha a * (psi a)^*)) => [|ax]; last first.
   by case/imsetP=> x Lx ->{ax}; rewrite !cfunJ.
-rewrite sumr_const -index_cent1 mulrC -[_ *+ #|_|]mulr_natr -!mulrA.
+rewrite sumr_const -index_cent1 mulrC -[_ *+ #|L : _|]mulr_natr -!mulrA.
 rewrite (eq_bigr (fun xa => alpha a * (phi xa)^*)) => [|xa Fa_xa]; last first.
   by rewrite (DadeE _ Aa).
 rewrite -big_distrr /= -rmorph_sum; congr (_ * _).

theories/PFsection3.v

@@ -1514,7 +1514,7 @@ have Vphi: phi \in 'CF(W, V).
     by rewrite addrC -[g]mulg1 /w_ !dprod_IirrE !cfDprodE ?lin_char1 ?addKr.
   by rewrite -[g]mul1g /w_ !dprod_IirrE !cfDprodE ?lin_char1 ?addrK.
 suffices: '[psi, 'Ind[G] phi] == 0.
-  rewrite -!cycTIiso_Ind // !linearB !linearD !cfdotBr !cfdotDr.
+  rewrite -!cycTIiso_Ind // !linearB !linearD 2!cfdotBr !cfdotDr.
   by rewrite -addrA -opprD subr_eq0 => /eqP.
 rewrite (cfdotEr _ (cfInd_on sWG Vphi)) big1 ?mulr0 //.
 by move=> _ /imset2P[x y Vx Gy ->]; rewrite cfunJ ?psiV_0 ?mul0r.
@@ -1865,7 +1865,8 @@ Lemma cycTIiso_irrel defW defW' ctiW ctiW' :
   @sigma_ defW ctiW = @sigma_ defW' ctiW'.
 Proof.
 have xdefW: W2 \x W1 = W by rewrite dprodC.
-by rewrite !(cycTIiso_irrelC _ (cyclicTIhyp_sym ctiW xdefW)).
+have E := (cycTIiso_irrelC _ (cyclicTIhyp_sym ctiW xdefW)).
+by rewrite [LHS]E [RHS]E.
 Qed.
 
 End ThreeSymmetry.

theories/PFsection4.v

@@ -984,7 +984,7 @@ pose alpha := cfCyclicTIset defW i j; set beta := _ *: mu2_ i j - _ - _ + _.
 have Valpha: alpha \in 'CF(W, V) := cfCycTI_on ctiWL i j.
 have Dalpha: alpha = w_ i j - w_ 0 j - w_ i 0 + w_ 0 0.
   by rewrite addrC {1}cycTIirr00 addrA addrAC addrA addrAC -cfCycTI_E.
-rewrite -!(linearB sigma) -linearD -Dalpha cycTIiso_Ind //.
+rewrite -![in X in X + _](linearB sigma) -linearD -Dalpha cycTIiso_Ind //.
 suffices ->: beta = 'Ind[L] alpha by rewrite DtauV0 ?cfInd_on ?cfIndInd.
 rewrite Dalpha -addrA -[w_ 0 0]opprK -opprD linearB /= /beta -scalerBr.
 by rewrite !(cfInd_sub_prTIirr ptiWL) prTIsign0 scale1r opprD opprK addrA.

theories/PFsection5.v

@@ -673,7 +673,7 @@ apply: vchar_pairs_orthonormal 1 (-1) _ _ _ _.
 - by split; apply/allP; rewrite //= rpredN.
 - by rewrite o_cd andbT /orthonormal/= cfnormN /orthogonal /= cfdotNr !oppr_eq0.
 - by rewrite oppr_eq0 oner_eq0 rpredN rpred1.
-rewrite !(big_seq1, big_cons) in sum_ab sum_cd.
+rewrite !big_cons !big_nil !addr0 in sum_ab sum_cd.
 rewrite scale1r scaleN1r !opprK sum_ab sum_cd obpx eqxx /=.
 by rewrite !(cfun_on0 (zchar_on (Ztau _ _))) ?Zbeta ?inE ?eqxx.
 Qed.

theories/PFsection6.v

@@ -145,7 +145,7 @@ have sAbZH: (A / B \subset 'Z(H / B))%g.
     rewrite -(quotient_proper (normalS sBD sDL nsBL)) // -defDbar.
     by rewrite properEneq sDAbar neqDAbar.
   apply/setIidPl/minBbar; rewrite ?subsetIl {minBbar}//= andbC -/Abar -/Zbar.
-  rewrite normsI ?meet_center_nil ?quotient_normal ?(normalS sAH sHL) //=.
+  rewrite normsI // meet_center_nil // ?quotient_normal ?(normalS sAH sHL) //=.
   suffices /homgP[f /= <-]: (H / B)%g \homg (H / M)%g by rewrite morphim_nil.
   by apply: homg_quotientS; rewrite ?(subset_trans sHL) ?normal_norm.
 have ltAH: A \proper H.

theories/PFsection7.v

@@ -325,7 +325,7 @@ transitivity (\sum_(x in A) \sum_(xi <- S) \sum_(mu <- S) F xi mu x).
   apply: eq_bigr => xi _; rewrite mulrA -mulr_suml rmorph_sum; congr (_ * _).
   rewrite mulr_sumr; apply: eq_bigr => mu _; rewrite !cfunE (cfdotC mu).
   rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM/= conjCK -3!mulrA 2!(mulrCA _^-1).
-  by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) mulrA 2!(mulrA _^*).
+  by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) (mulrA (c mu)) 2!(mulrA _^*).
 rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=.
 apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu.
 rewrite /u eh (cfdotEr _ (seqInd_on nsHL Tmu)) (mulrC _^-1) -mulrBl mulrA.

theories/PFsection8.v

@@ -275,7 +275,8 @@ Remark conj_of_typeP x :
 Proof.
 have defWx: W1 :^ x \x W2 :^ x = W :^ x by rewrite -dprodJ defW.
 exists defWx; rewrite /of_typeP !derJ FcoreJ FittingJ centJ -conjIg normJ.
-rewrite !cyclicJ !conjsg_eq1 /Hall !conjSg indexJg cardJg -[_ && _]/(Hall M W1).
+rewrite (cyclicJ W1 x) (cyclicJ M`_\F x) (cyclicJ W2 x). 
+rewrite !conjsg_eq1 /Hall !conjSg indexJg cardJg -[_ && _]/(Hall M W1).
 rewrite -(isog_nil (conj_isog U x)) -!sdprodJ -conjsMg -conjD1g.
 rewrite -(conjGid (in_setT x)) -conjUg -conjDg normedTI_J.
 have [[-> -> -> ->] [-> -> -> ->] [-> -> -> ->] [-> -> -> -> prW1] ->]:= MtypeP.