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, 18 insertions, 20 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index bfdafae..5f93277 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -182,8 +182,8 @@ Qed.
 
 Lemma Mho_p_elt (p : nat) x : x \in A -> p.-elt x -> x ^+ (p ^ n) \in Mho.
 Proof.
-move=> Ax p_x; case: (eqVneq x 1) => [-> | ntx]; first by rewrite groupX.
-by apply: mem_gen; apply/imsetP; exists x; rewrite ?inE ?Ax (pdiv_p_elt p_x).
+move=> Ax p_x; have [-> | ntx] := eqVneq x 1; first by rewrite groupX.
+by apply/mem_gen/imsetP; exists x; rewrite ?inE ?Ax (pdiv_p_elt p_x).
 Qed.
 
 End Functors.
@@ -572,7 +572,7 @@ Lemma TIp1ElemP p A X Y :
 Proof.
 move=> EpX EpY; have p_pr := pnElem_prime EpX.
 have [oX oY] := (card_p1Elem EpX, card_p1Elem EpY).
-have [<- |] := altP eqP.
+have [<-|] := eqVneq.
   by right=> X1; rewrite -oX -(setIid X) X1 cards1 in p_pr.
 by rewrite eqEcard oX oY leqnn andbT; left; rewrite prime_TIg ?oX.
 Qed.
@@ -668,7 +668,7 @@ Proof.
 apply/setP=> E; rewrite inE in_setI; apply: andb_id2l => /pElemP[sEG abelE].
 apply/idP/nElemP=> [|[q]]; first by exists p; rewrite !inE sEG abelE.
 rewrite !inE -2!andbA => /and4P[_ /pgroupP qE _].
-case: (eqVneq E 1%G) => [-> | ]; first by rewrite cards1 !logn1.
+have [->|] := eqVneq E 1%G; first by rewrite cards1 !logn1.
 case/(pgroup_pdiv (abelem_pgroup abelE)) => p_pr pE _.
 by rewrite (eqnP (qE p p_pr pE)).
 Qed.
@@ -1166,7 +1166,7 @@ Qed.
 Lemma OhmE p G : p.-group G -> 'Ohm_n(G) = <<'Ldiv_(p ^ n)(G)>>.
 Proof.
 move=> pG; congr <<_>>; apply/setP=> x; rewrite !inE; apply: andb_id2l => Gx.
-case: (eqVneq x 1) => [-> | ntx]; first by rewrite !expg1n.
+have [-> | ntx] := eqVneq x 1; first by rewrite !expg1n.
 by rewrite (pdiv_p_elt (mem_p_elt pG Gx)).
 Qed.
 
@@ -1468,9 +1468,8 @@ Lemma cyclic_pgroup_dprod_trivg p A B C :
 Proof.
 move=> pC cycC; case/cyclicP: cycC pC => x ->{C} pC defC.
 case/dprodP: defC => [] [G H -> ->{A B}] defC _ tiGH; rewrite -defC.
-case: (eqVneq <[x]> 1) => [|ntC].
-  move/trivgP; rewrite -defC mulG_subG => /andP[/trivgP-> _].
-  by rewrite mul1g; left.
+have [/trivgP | ntC] := eqVneq <[x]> 1.
+  by rewrite -defC mulG_subG => /andP[/trivgP-> _]; rewrite mul1g; left.
 have [pr_p _ _] := pgroup_pdiv pC ntC; pose K := 'Ohm_1(<[x]>).
 have prK : prime #|K| by rewrite (Ohm1_cyclic_pgroup_prime _ pC) ?cycle_cyclic.
 case: (prime_subgroupVti G prK) => [sKG |]; last first.
@@ -1842,7 +1841,7 @@ Qed.
 
 Lemma rank_cycle (x : gT) : 'r(<[x]>) = (x != 1).
 Proof.
-have [->|ntx] := altP (x =P 1); first by rewrite cycle1 rank1.
+have [->|ntx] := eqVneq x 1; first by rewrite cycle1 rank1.
 apply/eqP; rewrite eqn_leq rank_gt0 cycle_eq1 ntx andbT.
 by rewrite -grank_abelian ?cycle_abelian //= -(cards1 x) grank_min.
 Qed.
@@ -1948,7 +1947,7 @@ Qed.
 Lemma abelian_type_abelem p G : p.-abelem G -> abelian_type G = nseq 'r(G) p.
 Proof.
 move=> abelG; rewrite (abelian_type_homocyclic (abelem_homocyclic abelG)).
-case: (eqVneq G 1%G) => [-> | ntG]; first by rewrite rank1.
+have [-> | ntG] := eqVneq G 1%G; first by rewrite rank1.
 congr nseq; apply/eqP; rewrite eqn_dvd; have [pG _ ->] := and3P abelG.
 have [p_pr] := pgroup_pdiv pG ntG; case/Cauchy=> // x Gx <- _.
 exact: dvdn_exponent.
diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index cb86051..e67a0f9 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -258,9 +258,9 @@ case Hcard1: (#|H| == 1%N); move/eqP: Hcard1 => Hcard1.
   by left; apply: card1_trivg; rewrite Hcard1.
 right; case Hcard60: (#|H| == 60%N); move/eqP: Hcard60 => Hcard60.
   by apply/eqP; rewrite eqEcard Hcard60 F1 andbT; case/andP: Hnorm.
-have Hcard20: #|H| = 20; last clear Hcard1 Hcard60.
+have {Hcard1 Hcard60} Hcard20: #|H| = 20.
   have Hdiv: 20 %| #|H| by apply: FF => // HH; case Hcard1; rewrite HH cards1.
-  case H20: (#|H| == 20); first by apply/eqP.
+  case H20: (#|H| == 20); first exact/eqP.
   case: Hcard60; case/andP: Hnorm; move/cardSg; rewrite F1 => Hdiv1 _.
   by case/dvdnP: Hdiv H20 Hdiv1 => n ->; move: n; do 4!case=> //.
 have prime_5: prime 5 by [].
@@ -272,7 +272,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N.
 case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS.
 have{oS} oS: #|S| = 5 by rewrite oS p_part Hcard20.
 suff: 20 %| #|S| by rewrite oS.
-apply FF => [|S1]; last by rewrite S1 cards1 in oS.
+apply: FF => [|S1]; last by rewrite S1 cards1 in oS.
 apply: char_normal_trans Hnorm; apply: lone_subgroup_char => // Q sQH isoQS.
 rewrite subEproper; apply/norP=> [[nQS _]]; move: nSyl5.
 rewrite (cardsD1 S) (cardsD1 Q) 4!{1}inE nQS !pHallE sQH sSH Hcard20 p_part.
@@ -362,8 +362,7 @@ Proof.
 have rgd_x p: rgd p x = x by rewrite permE /= insubF //= eqxx.
 have rfd_rgd p: rfd (rgd p) = p.
   apply/permP => [[z Hz]]; apply/val_eqP; rewrite !permE.
-  rewrite /= [rgd _ _]permE /= insubF eq_refl // permE /=.
-  by rewrite (@insubT _ (xpredC1 x) _ _ Hz).
+  by rewrite /= [rgd _ _]permE /= insubF eqxx // permE /= insubT.
 have sSd: 'C_('Alt_T)[x | 'P] \subset 'dom rfd.
   by apply/subsetP=> p; rewrite !inE /=; case/andP.
 apply/isogP; exists [morphism of restrm sSd rfd] => /=; last first.
@@ -449,7 +448,7 @@ have Hreg g z: g \in H -> g z = z -> g = 1.
   by rewrite memJ_norm ?(subsetP nH).
 clear K F8 F12 F13 Ksub F14.
 have Hcard: 5 < #|H|.
-  apply: (leq_trans oT); apply dvdn_leq; first by apply: cardG_gt0.
+  apply: (leq_trans oT); apply: dvdn_leq; first exact: cardG_gt0.
   by rewrite -cardsT (atrans_dvd F5).
 case Eh: (pred0b [predD1 H & 1]).
   by move: Hcard; rewrite /pred0b in Eh; rewrite (cardD1 1) group1 (eqP Eh).
diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index e6d3afb..d82009b 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -587,7 +587,7 @@ Variable u : {unit 'Z_#[a]}.
 Lemma injm_cyclem : 'injm (cyclem (val u) a).
 Proof.
 apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn.
-case: (eqVneq a 1) => [a1 | nta]; first by rewrite a1 cycle1 inE in ax.
+have [a1 | nta] := eqVneq a 1; first by rewrite a1 cycle1 inE in ax.
 rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-.
 by rewrite dvdn_gcd {2}Zp_cast ?order_gt1 // order_dvdG.
 Qed.
@@ -616,7 +616,7 @@ Canonical Zp_unit_morphism := Morphism Zp_unitmM.
 
 Lemma injm_Zp_unitm : 'injm Zp_unitm.
 Proof.
-case: (eqVneq a 1) => [a1 | nta].
+have [a1 | nta] := eqVneq a 1.
   by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1.
 apply/subsetP=> /= u /morphpreP[_ /set1P/= um1].
 have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1.
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index 71b8b34..c1c1d27 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -598,7 +598,7 @@ have partG: partition (gval K |: (H^# :^: K)) G.
   apply: Frobenius_partition; apply/andP; rewrite defG; split=> //.
   by apply/Frobenius_actionP; apply: HasFrobeniusAction FrobG.
 have{FrobG} [ffulG transG regG ntH [u Su defH]]:= FrobG.
-apply/setP=> x; rewrite !inE; have [-> | ntx] := altP eqP; first exact: group1.
+apply/setP=> x; rewrite !inE; have [-> | ntx] := eqVneq; first exact: group1.
 rewrite /= -(cover_partition partG) /cover.
 have neKHy y: gval K <> H^# :^ y.
   by move/setP/(_ 1); rewrite group1 conjD1g setD11.
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index f3ecae2..aed6351 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -255,7 +255,7 @@ Qed.
 Lemma p2group_abelian P : p.-group P -> logn p #|P| <= 2 -> abelian P.
 Proof.
 move=> pP lePp2; pose Z := 'Z(P); have sZP: Z \subset P := center_sub P.
-case: (eqVneq Z 1); first by move/(trivg_center_pgroup pP)->; apply: abelian1.
+have [/(trivg_center_pgroup pP) ->|] := eqVneq Z 1; first exact: abelian1.
 case/(pgroup_pdiv (pgroupS sZP pP)) => p_pr _ [k oZ].
 apply: cyclic_center_factor_abelian.
 have [->|] := eqVneq (P / Z) 1; first exact: cyclic1.