diff --git a/theories/BGsection12.v b/theories/BGsection12.v
index 440771a..ef0d728 100644
--- a/theories/BGsection12.v
+++ b/theories/BGsection12.v
@@ -306,7 +306,7 @@ have SylowE3 P: Sylow E3 P -> [/\ cyclic P, P \subset E^`(1) & 'C_P(E) = 1].
     have sP_Ep'P: P \subset 'O_p^'(E) <*> P := joing_subr _ _.
     have sylP_Ep'P := pHall_subl sP_Ep'P (normal_sub nsEp'P_E) sylP_E.
     rewrite -{2}(Frattini_arg nsEp'P_E sylP_Ep'P) /= !norm_joinEr //.
-    by rewrite -mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA.
+    by rewrite -[LHS]mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA.
   have ntPE': P :&: E^`(1) != 1.
     have sylPE' := Hall_setI_normal (der_normal 1 E) sylP_E.
     rewrite -rank_gt0 (rank_Sylow sylPE') p_rank_gt0.
diff --git a/theories/BGsection2.v b/theories/BGsection2.v
index ace2586..f59dcd4 100644
--- a/theories/BGsection2.v
+++ b/theories/BGsection2.v
@@ -1138,7 +1138,7 @@ split.
   have Ur: r \in GRing.unit.
     by rewrite -(unitrX_pos _ (prime_gt0 q_pr)) rq1 unitr1.
   pose u_r : {unit 'F_p} := Sub r Ur; have:= order_dvdG (in_setT u_r).
-  rewrite card_units_Zp ?pdiv_gt0 // {2}/pdiv primes_prime //=.
+  rewrite card_units_Zp ?pdiv_gt0 // [X in totient X]/pdiv primes_prime //=.
   rewrite (@totient_pfactor p 1) // muln1; apply: dvdn_trans.
   have: (u_r ^+ q == 1)%g.
     by rewrite -val_eqE unit_Zp_expg -Zp_nat natrX natr_Zp rq1.
diff --git a/theories/BGsection3.v b/theories/BGsection3.v
index 99f33be..40c01d7 100644
--- a/theories/BGsection3.v
+++ b/theories/BGsection3.v
@@ -548,7 +548,7 @@ have irrK'K: mx_absolutely_irreducible rK'K.
       by rewrite mem_enum.
     by rewrite PackSocleK.
   have [i def_i]: exists i, [set: sK'G'] = [set i].
-    apply/cards1P; rewrite -dvdn1 -{7}(eqnP coKp) dvdn_gcd.
+    apply/cards1P; rewrite -dvdn1 -[X in _ %| X](eqnP coKp) dvdn_gcd.
     by rewrite -{1}eq_sK' sK'_dv_K sK'_dv_p.
   pose M := socle_base i; have simM : mxsimple rK'G' M := socle_simple i.
   have cycGq: cyclic (G' / K^`(1)).
diff --git a/theories/PFsection13.v b/theories/PFsection13.v
index 15c15f8..592b56b 100644
--- a/theories/PFsection13.v
+++ b/theories/PFsection13.v
@@ -706,7 +706,7 @@ suffices{ub_alpha} lb_a1_2: a1_2 >= #|H^#|%:R.
   rewrite ler_pMl ?(lt_le_trans _ lb_a1_2) ?ler1n ?ltr0n //.
     by rewrite -(subnKC Pgt2).
   have:= leq_trans (ltnW Pgt2) (subset_leq_card sPH).
-  by rewrite (cardsD1 1%g) group1.
+  by rewrite [in X in X -> _](cardsD1 1%g) group1.
 have /CnatP[n Dn]: '[alpha] \in Cnat by rewrite Cnat_cfnorm_vchar.
 have /CnatP[m Dm]: a1_2 \in Cnat by rewrite Cnat_exp_even ?Cint_vchar1.
 rewrite Dm leC_nat leqNgt; apply: contra suma_lt_H => a1_2_lt_H.
diff --git a/theories/PFsection9.v b/theories/PFsection9.v
index 32ff619..57cab97 100644
--- a/theories/PFsection9.v
+++ b/theories/PFsection9.v
@@ -531,8 +531,8 @@ have cEE A: A \in E_U -> centgmx rU A.
   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.
+  apply: rVabelem_inj; rewrite rVabelemJ ?groupR //; apply: (canLR (mulKg _)).
+  by rewrite -[LHS](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}}
@@ -1013,7 +1013,7 @@ have sW1_Imu i: W1 \subset 'I[theta (mu_f i) %% H0]%CF.
   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.
+  rewrite !ffunE W1w1 W1w1w -[x w1](conjgKV w1) -(conjgM _ w1) !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))).