running semi-automated linting on the whole library

3 files changed, 21 insertions, 21 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 1bde1f7..ecfa6ea 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -380,14 +380,14 @@ apply/subsetP=> a cSa; rewrite !inE (astab_dom cSa).
 by apply/subsetP=> x Sx; rewrite inE (astab_act cSa).
 Qed.
 
-Lemma astabsC S : 'N(~: S | to) = 'N(S | to). 
+Lemma astabsC S : 'N(~: S | to) = 'N(S | to).
 Proof.
 apply/setP=> a; apply/idP/idP=> nSa; rewrite !inE (astabs_dom nSa).
   by rewrite -setCS -preimsetC; apply/subsetP=> x; rewrite inE astabs_act.
 by rewrite preimsetC setCS; apply/subsetP=> x; rewrite inE astabs_act.
 Qed.
 
-Lemma astabsI S T : 'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to). 
+Lemma astabsI S T : 'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to).
 Proof.
 apply/subsetP=> a; rewrite !inE -!andbA preimsetI => /and4P[-> nSa _ nTa] /=.
 by rewrite setISS.
@@ -425,7 +425,7 @@ Proof.
 move=> sAD; apply/subsetP/subsetP=> [sAC x xS | sSF a aA].
   by apply/afixP=> a aA; apply: astab_act (sAC _ aA) xS.
 rewrite !inE (subsetP sAD _ aA); apply/subsetP=> x xS.
-by move/afixP/(_ _ aA): (sSF _ xS); rewrite inE => ->. 
+by move/afixP/(_ _ aA): (sSF _ xS); rewrite inE => ->.
 Qed.
 
 Section ActsSetop.
@@ -436,12 +436,12 @@ Hypotheses (AactS : [acts A, on S | to]) (AactT : [acts A, on T | to]).
 Lemma astabU : 'C(S :|: T | to) = 'C(S | to) :&: 'C(T | to).
 Proof. by apply/setP=> a; rewrite !inE subUset; case: (a \in D). Qed.
 
-Lemma astabsU : 'N(S | to) :&: 'N(T | to) \subset 'N(S :|: T | to). 
+Lemma astabsU : 'N(S | to) :&: 'N(T | to) \subset 'N(S :|: T | to).
 Proof.
 by rewrite -(astabsC S) -(astabsC T) -(astabsC (S :|: T)) setCU astabsI.
 Qed.
 
-Lemma astabsD : 'N(S | to) :&: 'N(T | to) \subset 'N(S :\: T| to). 
+Lemma astabsD : 'N(S | to) :&: 'N(T | to) \subset 'N(S :\: T| to).
 Proof. by rewrite setDE -(astabsC T) astabsI. Qed.
 
 Lemma actsI : [acts A, on S :&: T | to].
@@ -680,13 +680,13 @@ Proof. by move=> Da; rewrite afix_gen_in ?sub1set. Qed.
 
 Lemma afixYin A B :
   A \subset D -> B \subset D -> 'Fix_to(A <*> B) = 'Fix_to(A) :&: 'Fix_to(B).
-Proof. by move=> sAD sBD; rewrite afix_gen_in ?afixU // subUset sAD. Qed. 
+Proof. by move=> sAD sBD; rewrite afix_gen_in ?afixU // subUset sAD. Qed.
 
 Lemma afixMin G H :
   G \subset D -> H \subset D -> 'Fix_to(G * H) = 'Fix_to(G) :&: 'Fix_to(H).
 Proof.
 by move=> sGD sHD; rewrite -afix_gen_in ?mul_subG // genM_join afixYin.
-Qed. 
+Qed.
 
 Lemma sub_astab1_in A x :
   A \subset D -> (A \subset 'C[x | to]) = (x \in 'Fix_to(A)).
@@ -952,7 +952,7 @@ Proof. exact: sameP eqP (orbit_eqP G x y). Qed.
 Lemma orbit_inv A x y : (y \in orbit to A^-1 x) = (x \in orbit to A y).
 Proof. by rewrite orbit_inv_in ?subsetT. Qed.
 
-Lemma orbit_lcoset A a x : orbit to (a *: A) x = orbit to A (to x a). 
+Lemma orbit_lcoset A a x : orbit to (a *: A) x = orbit to A (to x a).
 Proof. by rewrite orbit_lcoset_in ?subsetT ?inE. Qed.
 
 Lemma orbit_rcoset A a x y :
@@ -1910,7 +1910,7 @@ Lemma gacentIim : 'C_(R | to)(A) = 'C_(|to)(A).
 Proof. by rewrite setIA setIid. Qed.
 
 Lemma gacentS : A \subset B -> 'C_(|to)(B) \subset 'C_(|to)(A).
-Proof. by move=> sAB; rewrite !(setIS, afixS). Qed.  
+Proof. by move=> sAB; rewrite !(setIS, afixS). Qed.
 
 Lemma gacentU : 'C_(|to)(A :|: B) = 'C_(|to)(A) :&: 'C_(|to)(B).
 Proof. by rewrite -setIIr -afixU -setIUr. Qed.
@@ -2001,8 +2001,8 @@ by move=> sGD sHB; rewrite -gacent_gen ?mul_subG // genM_join gacentY.
 Qed.
 
 Lemma astab1 : 'C(1 | to) = D.
-Proof. 
-by apply/setP=> x; rewrite ?(inE, sub1set) andb_idr //; move/gact1=> ->. 
+Proof.
+by apply/setP=> x; rewrite ?(inE, sub1set) andb_idr //; move/gact1=> ->.
 Qed.
 
 Lemma astab_range : 'C(R | to) = 'C(setT | to).
@@ -2599,10 +2599,10 @@ Lemma actsQ A B H :
   A \subset 'N(H) -> A \subset 'N(B) -> [acts A, on B / H | 'Q].
 Proof.
 by move=> nHA nBA; rewrite acts_quotient // subsetI dom_qactJ nHA astabsJ.
-Qed. 
+Qed.
 
 Lemma astabsQ G H : H <| G -> 'N(G / H | 'Q) = 'N(H) :&: 'N(G).
-Proof. by move=> nsHG; rewrite astabs_quotient // dom_qactJ astabsJ. Qed. 
+Proof. by move=> nsHG; rewrite astabs_quotient // dom_qactJ astabsJ. Qed.
 
 Lemma astabQ H Abar : 'C(Abar |'Q) = coset H @*^-1 'C(Abar).
 Proof.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 9d7bcc8..dd57af4 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1163,7 +1163,7 @@ move=> Ax; apply/setP=> y.
 by apply/imsetP/set1P=> [[a Aa]|] ->; last exists x; rewrite ?conj1g.
 Qed.
 
-Lemma classVg x A : x^-1 ^: A = (x ^: A)^-1. 
+Lemma classVg x A : x^-1 ^: A = (x ^: A)^-1.
 Proof.
 apply/setP=> xy; rewrite inE; apply/imsetP/imsetP=> [] [y Ay def_xy].
   by rewrite def_xy conjVg invgK; exists y.
@@ -2661,7 +2661,7 @@ Lemma norms_class_support : A \subset 'N(class_support B C).
 Proof.
 apply/subsetP=> x Ax; rewrite inE sub_conjg class_supportEr.
 apply/bigcupsP=> y Cy; rewrite -sub_conjg -conjsgM conjgC conjsgM.
-by rewrite  (normsP nBA) // bigcup_sup ?memJ_norm ?(subsetP nCA).
+by rewrite (normsP nBA) // bigcup_sup ?memJ_norm ?(subsetP nCA).
 Qed.
 
 End norm_trans.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 94304c4..cd129f2 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -524,7 +524,7 @@ Lemma bigcprodWY I (r : seq I) P F G :
   \big[cprod/1]_(i <- r | P i) F i = G -> << \bigcup_(i <- r | P i) F i >> = G.
 Proof.
 elim/big_rec2: _ G => [|i A B _ IH G]; first by rewrite gen0.
-case /cprodP => [[K H -> defB] <- cKH].
+case/cprodP => [[K H -> defB] <- cKH].
 by rewrite -[<<_>>]joing_idr (IH H) ?cent_joinEr -?defB.
 Qed.
 
@@ -1034,7 +1034,7 @@ Proof. by move=> x y. Qed.
 
 Canonical fst_morphism := @Morphism _ _ setT _ (in2W fst_morphM).
 
-Canonical snd_morphism := @Morphism _ _ setT _ (in2W snd_morphM). 
+Canonical snd_morphism := @Morphism _ _ setT _ (in2W snd_morphM).
 
 Lemma injm_pair1g : 'injm pair1g.
 Proof. by apply/subsetP=> x /morphpreP[_ /set1P[->]]; apply: set11. Qed.
@@ -1052,7 +1052,7 @@ Lemma morphim_fstX (H1: {set gT1}) (H2 : {group gT2}) :
   [morphism of fun x => x.1] @* setX H1 H2 = H1.
 Proof.
 apply/eqP; rewrite eqEsubset morphimE setTI /=.
-apply/andP; split; apply/subsetP=> x. 
+apply/andP; split; apply/subsetP=> x.
   by case/imsetP=> x0; rewrite inE; move/andP=> [Hx1 _] ->.
 move=> Hx1; apply/imsetP; exists (x, 1); last by trivial.
 by rewrite in_setX Hx1 /=.
@@ -1062,9 +1062,9 @@ Lemma morphim_sndX (H1: {group gT1}) (H2 : {set gT2}) :
   [morphism of fun x => x.2] @* setX H1 H2 = H2.
 Proof.
 apply/eqP; rewrite eqEsubset morphimE setTI /=.
-apply/andP; split; apply/subsetP=> x. 
+apply/andP; split; apply/subsetP=> x.
   by case/imsetP=> x0; rewrite inE; move/andP=> [_ Hx2] ->.
-move=>Hx2; apply/imsetP; exists (1, x); last by [].
+move=> Hx2; apply/imsetP; exists (1, x); last by [].
 by rewrite in_setX Hx2 andbT.
 Qed.
 
@@ -1084,7 +1084,7 @@ Lemma setX_dprod (H1 : {group gT1}) (H2 : {group gT2}) :
 Proof.
 rewrite dprodE ?setX_prod //.
   apply/centsP=> [[x u]]; rewrite !inE /= => /andP[/eqP-> _] [v y].
-  by rewrite !inE /= => /andP[_ /eqP->]; congr (_, _); rewrite ?mul1g ?mulg1. 
+  by rewrite !inE /= => /andP[_ /eqP->]; congr (_, _); rewrite ?mul1g ?mulg1.
 apply/trivgP; apply/subsetP=> [[x y]]; rewrite !inE /= -!andbA.
 by case/and4P=> _ /eqP-> /eqP->; rewrite eqxx.
 Qed.