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`.

5 files changed, 21 insertions, 23 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 78c5295..113ef8b 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -491,7 +491,7 @@ Proof. by rewrite cfunE cfuniE ?normal1 // inE mulr_natr. Qed.
 Lemma cfReprReg : cfRepr (regular_repr algCF G) = cfReg G.
 Proof.
 apply/cfun_inP=> x Gx; rewrite cfRegE.
-have [-> | ntx] := altP (x =P 1%g); first by rewrite cfRepr1.
+have [-> | ntx] := eqVneq x 1%g; first by rewrite cfRepr1.
 rewrite cfunE Gx [\tr _]big1 // => i _; rewrite 2!mxE /=.
 rewrite -(inj_eq enum_val_inj) gring_indexK ?groupM ?enum_valP //.
 by rewrite eq_mulVg1 mulKg (negbTE ntx).
@@ -714,7 +714,7 @@ Qed.
 
 Lemma xcfun_id i j : ('chi_i).['e_j]%CF = 'chi_i 1%g *+ (i == j).
 Proof.
-have [<-{j} | /xcfun_annihilate->//] := altP eqP; last exact: Wedderburn_id_mem.
+have [<-{j} | /xcfun_annihilate->//] := eqVneq; last exact: Wedderburn_id_mem.
 by rewrite -xcfunG // repr_mx1 -(xcfun_mul_id _ (envelop_mx1 _)) mulmx1.
 Qed.
 
@@ -1204,7 +1204,7 @@ transitivity (('chi_i).[e j *m aG y]%CF / 'chi_j 1%g).
   rewrite mulmx_suml raddf_sum big_distrl; apply: eq_bigr => x Gx /=.
   rewrite -scalemxAl xcfunZr -repr_mxM // xcfunG ?groupM // mulrAC mulrC.
   by congr (_ * _); rewrite mulrC mulKf ?irr1_neq0.
-rewrite mulr_natl mulrb; have [<-{j} | neq_ij] := altP eqP.
+rewrite mulr_natl mulrb; have [<-{j} | neq_ij] := eqVneq.
   by congr (_ / _); rewrite xcfun_mul_id ?envelop_mx_id ?xcfunG.
 rewrite (xcfun_annihilate neq_ij) ?mul0r //.
 case/andP: (Wedderburn_ideal (W j)) => _; apply: submx_trans.
@@ -1284,7 +1284,7 @@ transitivity ((#|'C_G[repr (y ^: G)]|%:R *: (X' *m X)) i_y i_x).
 rewrite mulmx1C // !mxE -!divg_index !(index_cent1, =^~ indexgI).
 rewrite (class_eqP (mem_repr y _)) ?class_refl // mulr_natr.
 rewrite (can_in_eq class_IirrK) ?mem_classes //.
-have [-> | not_yGx] := altP eqP; first by rewrite class_refl.
+have [-> | not_yGx] := eqVneq; first by rewrite class_refl.
 by rewrite [x \in _](contraNF _ not_yGx) // => /class_eqP->.
 Qed.
 
@@ -1450,7 +1450,7 @@ rewrite -!eq_scale_irr; apply/eqP/idP; last first.
   case/orP; first by case/andP=> /eqP-> /eqP->.
   case/orP=> /and3P[/eqP-> /eqP-> /eqP->]; first by rewrite addrC.
   by rewrite !scaleNr !addNr.
-have [-> /addrI/eqP-> // | /= ] := altP eqP.
+have [-> /addrI/eqP-> // | /=] := eqVneq.
 rewrite eq_scale_irr => /norP[/negP nz_a /negPf neq_ir].
 move/(congr1 (cfdotr 'chi__))/esym/eqP => /= eq_cfdot.
 move: {eq_cfdot}(eq_cfdot i) (eq_cfdot r); rewrite eq_sym !cfdotDl !cfdotZl.
@@ -2412,7 +2412,7 @@ Implicit Types G H : {group gT}.
 Lemma lin_irr_der1 G i :
    ('chi_i \is a linear_char) = (G^`(1)%g \subset cfker 'chi[G]_i).
 Proof.
-apply/idP/idP=> [|sG'K]; first by apply: lin_char_der1.
+apply/idP/idP=> [|sG'K]; first exact: lin_char_der1.
 have nsG'G: G^`(1) <| G := der_normal 1 G.
 rewrite qualifE irr_char -[i](quo_IirrK nsG'G) // mod_IirrE //=.
 by rewrite cfModE // morph1 lin_char1 //; apply/char_abelianP/der_abelian.
@@ -2832,8 +2832,7 @@ Proof.
 apply/eqP; rewrite eqEsubset; rewrite cfcenter_subset_center ?irr_char //.
 apply/subsetP=> _ /setIP[/morphimP[x /= _ Gx ->] cGx]; rewrite mem_quotient //=.
 rewrite -irrRepr cfker_repr cfcenter_repr inE Gx in cGx *.
-apply: mx_abs_irr_cent_scalar 'Chi_i _ _ _.
-  by apply: groupC; apply: socle_irr.
+apply: mx_abs_irr_cent_scalar 'Chi_i _ _ _; first exact/groupC/socle_irr.
 have nKG: G \subset 'N(rker 'Chi_i) by apply: rker_norm.
 (* GG -- locking here is critical to prevent Coq kernel divergence. *)
 apply/centgmxP=> y Gy; rewrite [eq]lock -2?(quo_repr_coset (subxx _) nKG) //.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 295b77a..fc19eba 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -943,7 +943,7 @@ Lemma cfCauchySchwarz phi psi :
   `|'[phi, psi]| ^+ 2 <= '[phi] * '[psi] ?= iff ~~ free (phi :: psi).
 Proof.
 rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC.
-have [-> | nz_psi] /= := altP (psi =P 0).
+have [-> | nz_psi] /= := eqVneq psi 0.
   by apply/leifP; rewrite !cfdot0r normCK mul0r mulr0.
 without loss ophi: phi / '[phi, psi] = 0.
   move=> IHo; pose a := '[phi, psi] / '[psi]; pose phi1 := phi - a *: psi.
@@ -978,7 +978,7 @@ rewrite (mono_leif (ler_pmul2r _)) ?ltr0n //.
 have:= leif_trans (leif_Re_Creal '[phi, psi]) (cfCauchySchwarz_sqrt phi psi).
 congr (_ <= _ ?= iff _); apply: andb_id2r.
 rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC.
-have [-> | nz_psi] := altP (psi =P 0); first by rewrite cfdot0r coord0.
+have [-> | nz_psi] := eqVneq psi 0; first by rewrite cfdot0r coord0.
 case/vlineP=> [x ->]; rewrite cfdotZl linearZ pmulr_lge0 ?cfnorm_gt0 //=.
 by rewrite (coord_free 0) ?seq1_free // eqxx mulr1.
 Qed.
@@ -1186,7 +1186,7 @@ rewrite orthonormalE; have [/= normS | not_normS] := allP; last first.
   by right=> [[_ o1S]]; case: not_normS => phi Sphi; rewrite /= o1S ?eqxx.
 apply: (iffP (pairwise_orthogonalP S)) => [] [uniqS oSS].
   split=> // [|phi psi]; first by case/andP: uniqS.
-  by have [-> _ /normS/eqP | /oSS] := altP eqP.
+  by have [-> _ /normS/eqP | /oSS] := eqVneq.
 split=> // [|phi psi Sphi Spsi /negbTE]; last by rewrite oSS // => ->.
 by rewrite /= (contra (normS _)) // cfdot0r eq_sym oner_eq0.
 Qed.
@@ -1497,7 +1497,7 @@ by rewrite -!cfMorphE // eq_phi.
 Qed.
 
 Lemma cfMorph_eq1 phi : (cfMorph phi == 1) = (phi == 1).
-Proof. by apply: rmorph_eq1; apply: cfMorph_inj. Qed.
+Proof. exact/rmorph_eq1/cfMorph_inj. Qed.
 
 Lemma cfker_morph phi : cfker (cfMorph phi) = G :&: f @*^-1 (cfker phi).
 Proof.
@@ -1526,7 +1526,7 @@ Lemma sub_morphim_cfker phi (A : {set aT}) :
 Proof. by move=> sAG; rewrite sub_cfker_morph ?sAG. Qed.
 
 Lemma cforder_morph phi : #[cfMorph phi]%CF = #[phi]%CF.
-Proof. by apply: cforder_inj_rmorph; apply: cfMorph_inj. Qed.
+Proof. exact/cforder_inj_rmorph/cfMorph_inj. Qed.
 
 End Main.
 
@@ -1607,7 +1607,7 @@ Qed.
 Lemma cfIsom_inj : injective (cfIsom isoGR). Proof. exact: can_inj cfIsomK. Qed.
 
 Lemma cfIsom_eq1 phi : (cfIsom isoGR phi == 1) = (phi == 1).
-Proof. by apply: rmorph_eq1; apply: cfIsom_inj. Qed.
+Proof. exact/rmorph_eq1/cfIsom_inj. Qed.
 
 Lemma cforder_isom phi : #[cfIsom isoGR phi]%CF = #[phi]%CF.
 Proof. exact: cforder_inj_rmorph cfIsom_inj. Qed.
@@ -1860,7 +1860,7 @@ by rewrite quotientK ?(subset_trans skerH) // -group_modr //= setIC tiKH mul1g.
 Qed.
 
 Lemma cforder_sdprod phi : #[cfSdprod phi]%CF = #[phi]%CF.
-Proof. by apply: cforder_inj_rmorph cfSdprod_inj. Qed.
+Proof. exact: cforder_inj_rmorph cfSdprod_inj. Qed.
 
 End SDproduct.
 
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index 1022afa..7e470b2 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -67,7 +67,7 @@ exists (SplittingFieldType _ _ Qn_ax).
   apply: separable_Xn_sub_1; rewrite -(fmorph_eq0 QnC) rmorph_nat.
   by rewrite pnatr_eq0 -lt0n cardG_gt0.
 exists QnC => [// nuQn|].
-  by apply: (extend_algC_subfield_aut QnC [rmorphism of nuQn]).
+  exact: (extend_algC_subfield_aut QnC [rmorphism of nuQn]).
 rewrite span_seq1 in genQn.
 exists w => // hT H phi Nphi x x_dv_n.
 apply: sig_eqW; have [rH ->] := char_reprP Nphi.
@@ -372,7 +372,7 @@ Proof.
 move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G *.
 rewrite ltnS => leGn piGle2; have [simpleG | ] := boolP (simple G); last first.
   rewrite negb_forall_in => /exists_inP[N sNG]; rewrite eq_sym.
-  have [-> | ] := altP (N =P G).
+  have [->|] := eqVneq N G.
     rewrite groupP /= genGid normG andbT eqb_id negbK => /eqP->.
     exact: solvable1.
   rewrite [N == G]eqEproper sNG eqbF_neg !negbK => ltNG /and3P[grN].
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index f5755a3..1c3fe0b 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -199,7 +199,7 @@ move=> linL; apply/eqP; rewrite eqEsubset sub_rowg_mx andbT.
 apply/subsetP=> v; rewrite inE genmxE => /submxP[u ->{v}].
 rewrite mulmx_sum_row group_prod // => i _.
 rewrite rowK; move: (enum_val i) (enum_valP i) => v Lv.
-case: (eqVneq (u 0 i) 0) => [->|]; first by rewrite scale0r group1.
+have [->|] := eqVneq (u 0 i) 0; first by rewrite scale0r group1.
 by rewrite -unitfE => aP; rewrite ((actsP linL) (FinRing.Unit _ aP)) ?inE.
 Qed.
 
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.