From 739e83630b72914b16be3adf8695e1a3b1fdc673 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 11 Jun 2025 09:10:47 +0200
Subject: [PATCH 1/7] adapt to rocq-prover/rocq#20707

---
 theories/BGappendixC.v       |  2 +-
 theories/BGsection1.v        |  2 +-
 theories/BGsection10.v       |  2 +-
 theories/BGsection14.v       |  9 +++++----
 theories/BGsection3.v        |  2 +-
 theories/BGsection6.v        |  2 +-
 theories/BGsection7.v        |  4 ++--
 theories/PFsection10.v       |  2 +-
 theories/PFsection12.v       |  2 +-
 theories/PFsection13.v       |  8 ++++----
 theories/PFsection2.v        |  2 +-
 theories/PFsection5.v        |  2 +-
 theories/PFsection7.v        |  2 +-
 theories/PFsection9.v        | 14 +++++++-------
 theories/wielandt_fixpoint.v |  2 +-
 15 files changed, 29 insertions(+), 28 deletions(-)

diff --git a/theories/BGappendixC.v b/theories/BGappendixC.v
index efd960d..caa4733 100644
--- a/theories/BGappendixC.v
+++ b/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. *)
diff --git a/theories/BGsection1.v b/theories/BGsection1.v
index a098e23..971d3eb 100644
--- a/theories/BGsection1.v
+++ b/theories/BGsection1.v
@@ -596,7 +596,7 @@ suffices <-: 'N_Cq(T) = C.
   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.
diff --git a/theories/BGsection10.v b/theories/BGsection10.v
index e3101db..2771a3e 100644
--- a/theories/BGsection10.v
+++ b/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.
 
diff --git a/theories/BGsection14.v b/theories/BGsection14.v
index 516f0cc..61bb73b 100644
--- a/theories/BGsection14.v
+++ b/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}//=.
diff --git a/theories/BGsection3.v b/theories/BGsection3.v
index d471809..d073423 100644
--- a/theories/BGsection3.v
+++ b/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.
diff --git a/theories/BGsection6.v b/theories/BGsection6.v
index 8c07f60..410a5e9 100644
--- a/theories/BGsection6.v
+++ b/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.
diff --git a/theories/BGsection7.v b/theories/BGsection7.v
index f71d809..3c8d086 100644
--- a/theories/BGsection7.v
+++ b/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 _ _)).
diff --git a/theories/PFsection10.v b/theories/PFsection10.v
index bf75433..1a1c4b5 100644
--- a/theories/PFsection10.v
+++ b/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.
diff --git a/theories/PFsection12.v b/theories/PFsection12.v
index 3d5dcdd..b942ced 100644
--- a/theories/PFsection12.v
+++ b/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.
diff --git a/theories/PFsection13.v b/theories/PFsection13.v
index 05dbf3d..c765c2f 100644
--- a/theories/PFsection13.v
+++ b/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.
diff --git a/theories/PFsection2.v b/theories/PFsection2.v
index bed96f4..6193652 100644
--- a/theories/PFsection2.v
+++ b/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 (_ * _).
diff --git a/theories/PFsection5.v b/theories/PFsection5.v
index be2568f..baf5627 100644
--- a/theories/PFsection5.v
+++ b/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.
diff --git a/theories/PFsection7.v b/theories/PFsection7.v
index f02b6b6..5976f04 100644
--- a/theories/PFsection7.v
+++ b/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.
diff --git a/theories/PFsection9.v b/theories/PFsection9.v
index ab8c53e..54f3602 100644
--- a/theories/PFsection9.v
+++ b/theories/PFsection9.v
@@ -256,7 +256,7 @@ split=> //; first by rewrite /= -{1}(joing_idPl sH0H) -joingA normalY ?gFnormal.
   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.
+by rewrite /= -(quotientYK nH0C) -!(@quotientYK _ H0) ?gFsub_trans // ?quotient_der ?subsetIl // cosetpreK.
 Qed.
 Local Notation nsH0xx_M := Ptype_Fcore_extensions_normal.
 
@@ -284,7 +284,7 @@ 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.
+  by rewrite im_f !(morphim_restrm nH0UW1) !(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.
@@ -618,7 +618,7 @@ have phiJ: {in Hbar & U, forall h x, phi (h ^ inMb x) = phi h * val (psi x)}%R.
   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.
+  apply/setP=> x; rewrite [C]unlock. rewrite in_setI /= 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.
@@ -1164,7 +1164,7 @@ have <-: #|Clam| = #|'C_U(H1 | 'Q) : U'|.
   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].
+  rewrite [Mtheta]curry_imset2X [RHS]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).
@@ -1400,7 +1400,7 @@ have ->: (p ^ q).-1 = (#|X_ H0| * u)%N.
   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 !inE mod_IirrE // (@cfker_mod _ _ H0) // 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).
@@ -1937,7 +1937,7 @@ have [Aalpha Nalpha]: alpha \in 'CF(M, 'A(M)) /\ '[alpha] = nm_alpha.
     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.
+  rewrite exchange_big /= mulr_natr -[RHS]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 //=.
@@ -1945,7 +1945,7 @@ have [Aalpha Nalpha]: alpha \in 'CF(M, 'A(M)) /\ '[alpha] = nm_alpha.
     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.
+  rewrite [q](cardsD1 1%g) group1 /= mulr_natl -[RHS]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.
diff --git a/theories/wielandt_fixpoint.v b/theories/wielandt_fixpoint.v
index 65877ac..21683e8 100644
--- a/theories/wielandt_fixpoint.v
+++ b/theories/wielandt_fixpoint.v
@@ -590,7 +590,7 @@ have{tiRCW} rCW : 'r('C_W(Ai1)) = rC i.
     by rewrite (subset_trans sAiG1) // gFnorm_trans.
   have ->: A i :=: fG @* Ai1.
     by rewrite /Ai1 morphim_invmE morphpreK // im_restrm imfG1.
-  rewrite -imfW morphim_restrm (setIidPr sAiG1).
+  rewrite -imfW [fG @* _]morphim_restrm (setIidPr sAiG1).
   have [f1 injf1 im_f1] := first_isom f.
   rewrite -!im_f1 -injm_subcent ?quotientS ?(subset_trans sAiG1) //.
   by rewrite -kerf isog_sym sub_isog // subIset ?quotientS.

From ece7eb58f185f839c3c296a8626013b152963251 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 18 Jun 2025 12:46:20 +0200
Subject: [PATCH 2/7] speedup

---
 theories/BGsection2.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/BGsection2.v b/theories/BGsection2.v
index 4df8456..92dfdeb 100644
--- a/theories/BGsection2.v
+++ b/theories/BGsection2.v
@@ -1104,9 +1104,10 @@ have lam_q Pi b:
   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 ->].

From 8fc3f4dc66e0fabc7478f21e8715dd8108b2c98a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 18 Jun 2025 18:51:38 +0200
Subject: [PATCH 3/7] speedup

---
 theories/PFsection3.v | 5 +++--
 theories/PFsection8.v | 3 ++-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/PFsection3.v b/theories/PFsection3.v
index e90c412..714a282 100644
--- a/theories/PFsection3.v
+++ b/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.
diff --git a/theories/PFsection8.v b/theories/PFsection8.v
index 6ddfe19..d327688 100644
--- a/theories/PFsection8.v
+++ b/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.

From ccf11a1ab0162f0775a5654bcab826577e222bfd Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 18 Jun 2025 18:59:31 +0200
Subject: [PATCH 4/7] speedup

---
 theories/PFsection11.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/PFsection11.v b/theories/PFsection11.v
index 4da48ac..a068af5 100644
--- a/theories/PFsection11.v
+++ b/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).

From 11a0066d3be81942040ab2136d45ced72ab5da94 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 18 Jun 2025 22:36:05 +0200
Subject: [PATCH 5/7] speedup

---
 theories/PFsection14.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/PFsection14.v b/theories/PFsection14.v
index 8e67051..b3651fb 100644
--- a/theories/PFsection14.v
+++ b/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)).

From 40526bece92a6f7cb8e90e73f13a96a0fa7085f4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 19 Jun 2025 10:03:56 +0200
Subject: [PATCH 6/7] speedup

---
 theories/BGsection15.v | 2 +-
 theories/BGsection4.v  | 2 +-
 theories/PFsection4.v  | 2 +-
 theories/PFsection6.v  | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/BGsection15.v b/theories/BGsection15.v
index b0ac5f0..6f84236 100644
--- a/theories/BGsection15.v
+++ b/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.
diff --git a/theories/BGsection4.v b/theories/BGsection4.v
index fa41486..8df24bf 100644
--- a/theories/BGsection4.v
+++ b/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').
diff --git a/theories/PFsection4.v b/theories/PFsection4.v
index 9b70202..50fa437 100644
--- a/theories/PFsection4.v
+++ b/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.
diff --git a/theories/PFsection6.v b/theories/PFsection6.v
index fa4eff4..9aaea66 100644
--- a/theories/PFsection6.v
+++ b/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.

From c49bbd1559646966237074e991a747a77f6ea891 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 19 Jun 2025 13:26:13 +0200
Subject: [PATCH 7/7] speedup

---
 theories/BGsection12.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/BGsection12.v b/theories/BGsection12.v
index 8bc4870..3f52131 100644
--- a/theories/BGsection12.v
+++ b/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 _)).