Refactoring and linting especially polydiv

- Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`:
  The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and
  introduces a hypothesis in the form of `x != y` in the second case. Thus,
  `case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms
  can be replaced with `case: eqVneq`, `case: (eqVneq x)` and
  `case: (eqVneq x y)` respectively. This replacement slightly simplifies and
  reduces proof scripts.
- use `have [] :=` rather than `case` if it is better.
- `by apply:` -> `exact:`.
- `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`.
- `move/lem1; move/lem2` -> `move/lem1/lem2`.
- Remove `GRing.` prefix if applicable.
- `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`.

1 files changed, 4 insertions, 5 deletions

diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index aff51bd..51d28f8 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -1592,7 +1592,7 @@ Lemma mxsimple_exists m (U : 'M_(m, n)) :
 Proof.
 move=> modU nzU [] // simU; move: {2}_.+1 (ltnSn (\rank U)) => r leUr.
 elim: r => // r IHr in m U leUr modU nzU simU.
-have genU := genmxE U; apply simU; exists <<U>>%MS; last by rewrite genU.
+have genU := genmxE U; apply: (simU); exists <<U>>%MS; last by rewrite genU.
 apply/mxsimpleP; split; rewrite ?(eqmx_eq0 genU) ?(eqmx_module genU) //.
 case=> V; rewrite !genU=> /and4P[modV sVU nzV ltVU]; case: notF.
 apply: IHr nzV _ => // [|[W simW sWV]]; first exact: leq_trans ltVU _.
@@ -1891,7 +1891,7 @@ move=> modV redV [] // nssimV; have [r leVr] := ubnP (\rank V).
 elim: r => // r IHr in V leVr modV redV nssimV.
 have [V0 | nzV] := eqVneq V 0.
   by rewrite nssimV ?V0 //; apply: mxsemisimple0.
-apply (mxsimple_exists modV nzV) => [[U simU sUV]]; have [modU nzU _] := simU.
+apply: (mxsimple_exists modV nzV) => [[U simU sUV]]; have [modU nzU _] := simU.
 have [W modW defUW dxUW] := redV U modU sUV.
 have sWV: (W <= V)%MS by rewrite -defUW addsmxSr.
 apply: IHr (mx_reducibleS modW sWV redV) _ => // [|ssimW].
@@ -3492,8 +3492,7 @@ rewrite -defW; apply/sumsmx_subP=> j _; set x := x_ W j.
 have{Gx_} Gx: x \in G by rewrite Gx_.
 apply: submx_trans (submxMr _ sMU) _; apply: (mxmoduleP modU).
 rewrite inE -val_Clifford_act Gx //; set Wx := 'Cl%act W x.
-have [-> //= | neWxW] := eqVneq Wx W.
-case: (simM) => _ /negP[]; rewrite -submx0.
+case: (eqVneq Wx W) (simM) => [-> //=|] neWxW [_ /negP[]]; rewrite -submx0.
 rewrite (canF_eq (actKin 'Cl Gx)) in neWxW.
 rewrite -(component_mx_disjoint _ _ neWxW); try exact: socle_simple.
 rewrite sub_capmx {1}(submx_trans sMU sUW) val_Clifford_act ?groupV //.
@@ -5838,7 +5837,7 @@ have: mx_subseries (aG F) U /\ path ltmx 0 U by [].
 pose f : {rmorphism F0 -> F} := [rmorphism of idfun].
 elim: m F U f => [|m IHm] F U f [modU ltU].
   by rewrite addn0 (leq_trans (max_size_mx_series ltU)) ?rank_leq_row.
-rewrite addnS ltnNge -implybF; apply/implyP=> le_nG_Um; apply nosplit.
+rewrite addnS ltnNge -implybF; apply/implyP=> le_nG_Um; apply: nosplit.
 exists F => //; case=> [|n] rG irrG; first by case/mx_irrP: irrG.
 apply/idPn=> nabsG; pose cG := ('C(enveloping_algebra_mx rG))%MS.
 have{nabsG} [A]: exists2 A, (A \in cG)%MS & ~~ is_scalar_mx A.