running semi-automated linting on the whole library

1 files changed, 64 insertions, 64 deletions

diff --git a/mathcomp/attic/algnum_basic.v b/mathcomp/attic/algnum_basic.v
index 48adbb3..54cb1c5 100644
--- a/mathcomp/attic/algnum_basic.v
+++ b/mathcomp/attic/algnum_basic.v
@@ -102,12 +102,12 @@ pose g := fun l => let p := minPoly K l in \prod_(i < size p) f p`_i; exists g =
 pose p := minPoly K l; pose n := (size p).-1.
 pose s := mkseq (fun i => p`_i * (g l) ^+ (n - i)%N) (size p).
 have kI (i : 'I_(size p)) : p`_i \in K by apply/all_nthP => //; apply/minPolyOver.
-have glA : g l \in A by rewrite/g; elim/big_ind: _ => // i _; apply/fHa.
+have glA : g l \in A by rewrite /g; elim/big_ind: _ => // i _; apply/fHa.
 have pmon: p`_n = 1 by have /monicP := monic_minPoly K l.
-have an1: nth 0 s n = 1 by rewrite /n nth_mkseq ?pmon ?mul1r ?subnn ?size_minPoly. 
+have an1: nth 0 s n = 1 by rewrite /n nth_mkseq ?pmon ?mul1r ?subnn ?size_minPoly.
 have eqPs: (Poly s) = s :> seq L0.
   by rewrite (PolyK (c := 0)) // -nth_last size_mkseq an1 oner_neq0.
-have ilen i : i < size p -> i <= n by move => iB; rewrite /n -ltnS prednK // size_minPoly.
+have ilen i : i < size p -> i <= n by move=> iB; rewrite /n -ltnS prednK // size_minPoly.
 split => //; first by apply/prodf_neq0 => i _.
 exists (Poly s); split; last first; last by rewrite monicE lead_coefE eqPs // size_mkseq an1.
   rewrite /root -(mulr0 ((g l) ^+ n)); have <- := minPolyxx K l.
@@ -116,11 +116,11 @@ exists (Poly s); split; last first; last by rewrite monicE lead_coefE eqPs // si
   by congr (_ * _); rewrite -exprD subnK ?ilen.
 apply/(all_nthP 0) => i; rewrite eqPs size_mkseq => iB; rewrite nth_mkseq //.
   have := ilen _ iB; rewrite leq_eqVlt => /orP.
-  case; first by move /eqP ->; rewrite subnn pmon mulr1.
+  case; first by move/eqP ->; rewrite subnn pmon mulr1.
   rewrite -subn_gt0 => {pmon ilen eqPs an1} /prednK <-; rewrite exprS mulrA /= Amcl ?rpredX //.
   rewrite /g (bigD1 (Ordinal iB)) //= mulrA; apply/Amcl.
     by rewrite mulrC; apply/fHk/(kI (Ordinal iB)).
-  by rewrite rpred_prod => // j _; apply/fHa. 
+  by rewrite rpred_prod => // j _; apply/fHa.
 Qed.
 
 Lemma int_clos_incl a : a \in A -> integral a.
@@ -135,7 +135,7 @@ Lemma intPl (I : eqType) G (r : seq I) l : has (fun x => G x != 0) r ->
 Proof.
 have Aaddr : addr_closed A := Asubr; have Amulr : mulr_closed A := Asubr.
 have Aoppr : oppr_closed A := Asubr; have [Aid _ _] := Asubr.
-move => rn gen; pose s := in_tuple r; pose g j := gen (tnth s j) (mem_tnth j s).
+move=> rn gen; pose s := in_tuple r; pose g j := gen (tnth s j) (mem_tnth j s).
 pose f j := sval (g j); pose fH j := svalP (g j).
 pose M := \matrix_(i, j < size r) f j (tnth s i).
 exists (char_poly M); rewrite char_poly_monic; split => //.
@@ -153,7 +153,7 @@ Qed.
 Lemma intPr l : integral l -> exists r : seq L0,
   [/\ r != nil, all A r & \sum_(i < size r) r`_i * l ^+ i = l ^+ (size r)].
 Proof.
-move => [p [pm pA pr]]; pose n := size p; pose r := take n.-1 (- p).
+move=> [p [pm pA pr]]; pose n := size p; pose r := take n.-1 (- p).
 have ps : n > 1.
   rewrite ltnNge; apply/negP => /size1_polyC pc; rewrite pc in pr pm => {pc}.
   move: pr => /rootP; rewrite hornerC => pc0.
@@ -163,10 +163,10 @@ exists r; split.
   apply/eqP => /nilP; rewrite /nilp /r size_takel; last by rewrite size_opp leq_pred.
   by rewrite -subn1 subn_eq0 leqNgt ps.
   have : - p \is a polyOver A by rewrite rpredN //; apply Asubr.
-  by move => /allP-popA; apply/allP => x /mem_take /popA.
+  by move=> /allP-popA; apply/allP => x /mem_take /popA.
 move: pr => /rootP; rewrite horner_coef -(prednK (n := size p)); last by rewrite ltnW.
 rewrite big_ord_recr /= rs; have := monicP pm; rewrite /lead_coef => ->; rewrite mul1r => /eqP.
-rewrite addrC addr_eq0 -sumrN => /eqP => ->; apply/eq_bigr => i _; rewrite /r nth_take //.    
+rewrite addrC addr_eq0 -sumrN => /eqP => ->; apply/eq_bigr => i _; rewrite /r nth_take //.
 by rewrite coefN mulNr.
 Qed.
 
@@ -174,11 +174,11 @@ Lemma int_subring_closed a b : integral a -> integral b ->
   integral (a - b) /\ integral (a * b).
 Proof.
 have [A0 _ ] := (Asubr : zmod_closed A); have [A1 Asubr2 Amulr2] := Asubr.
-move => /intPr[ra [/negbTE-ran raA raS]] /intPr[rb [/negbTE-rbn rbA rbS]].
+move=> /intPr[ra [/negbTE-ran raA raS]] /intPr[rb [/negbTE-rbn rbA rbS]].
 pose n := size ra; pose m := size rb; pose r := Finite.enum [finType of 'I_n * 'I_m].
 pose G (z : 'I_n * 'I_m) := let (k, l) := z in a ^ k * b ^l.
 have [nz mz] : 0 < n /\ 0 < m.
-  by rewrite !lt0n; split; apply/negP; move => /nilP/eqP; rewrite ?ran ?rbn.
+  by rewrite !lt0n; split; apply/negP => - /nilP/eqP; rewrite ?ran ?rbn.
 have rnn : has (fun x => G x != 0) r.
   apply/hasP; exists (Ordinal nz, Ordinal mz); first by rewrite /r -enumT mem_enum.
   by rewrite /G mulr1 oner_neq0.
@@ -186,22 +186,22 @@ pose h s i : 'I_(size s) -> L0 := fun k => if (i != size s) then (i == k)%:R els
 pose f i j (z : 'I_n * 'I_m) : L0 := let (k, l) := z in h ra i k * h rb j l.
 have fA i j : forall z, f i j z \in A.
   have hA s k l : all A s -> h s k l \in A.
-    move => /allP-sa; rewrite /h; case (eqVneq k (size s)) => [/eqP ->|->].
-      by apply/sa/mem_nth. 
+    move=> /allP-sa; rewrite /h; case (eqVneq k (size s)) => [/eqP ->|->].
+      by apply/sa/mem_nth.
     by case (eqVneq k l) => [/eqP ->|/negbTE ->].
-  by move => [k l]; rewrite /f; apply/Amulr2; apply/hA.
+  by move=> [k l]; rewrite /f; apply/Amulr2; apply/hA.
 have fS i j : (i <= n) -> (j <= m) -> \sum_(z <- r) f i j z * G z = a ^ i * b ^ j.
   have hS s k c : (k <= size s) -> \sum_(l < size s) s`_l * c ^ l = c ^ (size s) ->
     \sum_(l < size s) h s k l * c ^ l = c ^ k.
-    move => kB sS; rewrite /h; case (eqVneq k (size s)) => [->|kn {sS}]; first by rewrite eqxx.
+    move=> kB sS; rewrite /h; case (eqVneq k (size s)) => [->|kn {sS}]; first by rewrite eqxx.
     rewrite kn; rewrite leq_eqVlt (negbTE kn) /= in kB => {kn}.
     rewrite (bigD1 (Ordinal kB)) //= eqxx mul1r /= -[RHS]addr0; congr (_ + _).
     by apply/big1 => l; rewrite eq_sym => kl; have : k != l := kl => /negbTE ->; rewrite mul0r.
-  move => iB jB; rewrite -(hS ra i a) // -(hS rb j b) // mulr_suml.
+  move=> iB jB; rewrite -(hS ra i a) // -(hS rb j b) // mulr_suml.
   rewrite (eq_bigr (fun k => \sum_(l < m) (h ra i k * a ^ k) * (h rb j l * b ^ l))).
     rewrite pair_bigA; apply eq_bigr => [[k l] _]; rewrite !mulrA; congr (_ * _).
     by rewrite -!mulrA [in h rb j l * a ^ k] mulrC.
-  by move => k _; rewrite mulr_sumr.
+  by move=> k _; rewrite mulr_sumr.
 pose fB i j z := f i.+1 j z - f i j.+1 z; pose fM i j z := f i.+1 j.+1 z.
 have fBA i j z : fB i j z \in A by rewrite /fB Asubr2.
 have fBM i j z : fM i j z \in A by rewrite /fM.
@@ -213,10 +213,10 @@ by rewrite /fM [in RHS]/G mulrA [in (a * b) * a ^ i] mulrC mulrA -exprSr -mulrA
 Qed.
 
 Lemma int_zmod_closed a b : integral a -> integral b -> integral (a - b).
-Proof. by move => aI bI; have [Azmod] := int_subring_closed aI bI. Qed.
+Proof. by move=> aI bI; have [Azmod] := int_subring_closed aI bI. Qed.
 
 Lemma int_mulr_closed a b : integral a -> integral b -> integral (a * b).
-Proof. by move => aI bI; have [_] := int_subring_closed aI bI. Qed.
+Proof. by move=> aI bI; have [_] := int_subring_closed aI bI. Qed.
 
 End Integral.
 
@@ -233,7 +233,7 @@ Definition tr : L0 -> L0 -> F := fun l k =>
 
 Fact tr_is_scalar l : scalar (tr l).
 Proof.
-move => c a b; rewrite /tr  -!linearP /=; congr (\tr _); apply/matrixP => i j; rewrite !mxE.
+move=> c a b; rewrite /tr  -!linearP /=; congr (\tr _); apply/matrixP => i j; rewrite !mxE.
 by rewrite mulrDr mulrDl linearD /= -scalerAr -scalerAl linearZ.
 Qed.
 
@@ -241,7 +241,7 @@ Canonical tr_additive l := Additive (@tr_is_scalar l).
 Canonical tr_linear l := AddLinear (@tr_is_scalar l).
   
 Lemma tr_sym : commutative tr.
-Proof. by move => a b; rewrite /tr mulrC. Qed.
+Proof. by move=> a b; rewrite /tr mulrC. Qed.
 
 Hypothesis Asubr : subring_closed A.
 Hypothesis Aint  : int_closed A.
@@ -267,36 +267,36 @@ Lemma dual_basis_def :
   forall (i : 'I_m), tr X`_i Y`_i = 1 /\
   forall (j : 'I_m), j != i -> tr X`_i Y`_j = 0}.
 Proof.
-pose Uv := subvs_vectType U; pose Fv := subvs_FalgType (1%AS : {aspace L0}); 
+pose Uv := subvs_vectType U; pose Fv := subvs_FalgType (1%AS : {aspace L0});
 pose HomV := [vectType _ of 'Hom(Uv, Fv)].
 pose tr_sub : Uv -> Uv -> Fv := fun u v => (tr (vsval u) (vsval v))%:A.
 have HomVdim : \dim {:HomV} = m by rewrite dimvf /Vector.dim /= /Vector.dim /= dimv1 muln1.
 have [f fH] : {f : 'Hom(Uv, HomV) | forall u, f u =1 tr_sub u}.
-  have lf1 u : linear (tr_sub u) by move => c x y; rewrite /tr_sub linearP scalerDl scalerA.
+  have lf1 u : linear (tr_sub u) by move=> c x y; rewrite /tr_sub linearP scalerDl scalerA.
   have lf2 : linear (fun u => linfun (Linear (lf1 u))).
-    move => c x y; rewrite -lfunP => v; rewrite add_lfunE scale_lfunE !lfunE /= /tr_sub.
+    move=> c x y; rewrite -lfunP => v; rewrite add_lfunE scale_lfunE !lfunE /= /tr_sub.
     by rewrite tr_sym linearP scalerDl scalerA /=; congr (_ + _); rewrite tr_sym.
   by exists (linfun (Linear lf2)) => u v; rewrite !lfunE.
 have [Xdual XdualH] : {Xdual : m.-tuple HomV |
   forall (i : 'I_m) u, Xdual`_i u = (coord X i (vsval u))%:A}.
   have lg (i : 'I_m) : linear (fun u : Uv => (coord X i (vsval u))%:A : Fv).
-    by move => c x y; rewrite linearP /= scalerDl scalerA.
+    by move=> c x y; rewrite linearP /= scalerDl scalerA.
   exists (mktuple (fun i => linfun (Linear (lg i)))) => i u.
   by rewrite -tnth_nth tnth_mktuple !lfunE.
 have [finv finvH] : {finv : 'Hom(HomV, L0) | finv =1 vsval \o (f^-1)%VF}.
-  by exists (linfun vsval \o f^-1)%VF => u; rewrite comp_lfunE lfunE. 
+  by exists (linfun vsval \o f^-1)%VF => u; rewrite comp_lfunE lfunE.
 pose Y := map_tuple finv Xdual; exists Y => Und Xb.
 have Ydef (i : 'I_m) : Y`_i = finv Xdual`_i by rewrite -!tnth_nth tnth_map.
 have XiU (i : 'I_m) : X`_i \in U by apply/(basis_mem Xb)/mem_nth; rewrite size_tuple.
 have Xii (i : 'I_m) : coord X i X`_i = 1%:R.
   by rewrite coord_free ?eqxx //; apply (basis_free Xb).
 have Xij (i j : 'I_m) : j != i -> coord X i X`_j = 0%:R.
-  by rewrite coord_free; [move => /negbTE -> | apply (basis_free Xb)].
+  by rewrite coord_free; [move=> /negbTE -> | apply (basis_free Xb)].
 have Xdualb : basis_of fullv Xdual.
   suffices Xdualf : free Xdual.
     rewrite /basis_of Xdualf andbC /= -dimv_leqif_eq ?subvf // eq_sym HomVdim.
     by move: Xdualf; rewrite /free => /eqP => ->; rewrite size_tuple.
-  apply/freeP => k sX i.  
+  apply/freeP => k sX i.
   suffices: (\sum_(i < m) k i *: Xdual`_i) (vsproj U X`_i) = (k i)%:A.
     by rewrite sX zero_lfunE => /esym /eqP; rewrite scaler_eq0 oner_eq0 orbF => /eqP.
   rewrite sum_lfunE (bigD1 i) //= scale_lfunE XdualH vsprojK // Xii.
@@ -311,10 +311,10 @@ have flimg : limg f = fullv.
   apply/eqP; rewrite -dimv_leqif_eq ?subvf // limg_dim_eq; last by rewrite finj capv0.
   by rewrite HomVdim dimvf /Vector.dim.
 have finvK : cancel finv (f \o vsproj U).
-  by move => u; rewrite finvH /= vsvalK; apply/limg_lfunVK; rewrite flimg memvf.
+  by move=> u; rewrite finvH /= vsvalK; apply/limg_lfunVK; rewrite flimg memvf.
 have finv_inj : (lker finv = 0)%VS by apply/eqP/lker0P/(can_inj finvK).
-have finv_limg : limg finv = U. 
-  apply/eqP; rewrite -dimv_leqif_eq; first by rewrite limg_dim_eq ?HomVdim ?finv_inj ?capv0.   
+have finv_limg : limg finv = U.
+  apply/eqP; rewrite -dimv_leqif_eq; first by rewrite limg_dim_eq ?HomVdim ?finv_inj ?capv0.
   by apply/subvP => u /memv_imgP [h _] ->; rewrite finvH subvsP.
 have Xt (i j : 'I_m) : (f \o vsproj U) Y`_j (vsproj U X`_i) = (tr Y`_j X`_i)%:A.
   by rewrite fH /tr_sub !vsprojK // Ydef finvH subvsP.
@@ -355,7 +355,7 @@ Definition trK : L0 -> L0 -> K' := tr (aspaceOver K L).
 Lemma trK_ndeg (U : {aspace L0}) : (K <= U)%VS ->
   (ndeg trK U <-> ndeg (tr (aspaceOver K L)) (aspaceOver K U)).
 Proof.
-move => UsubL; have UU' : aspaceOver K U =i U := mem_aspaceOver UsubL.
+move=> UsubL; have UU' : aspaceOver K U =i U := mem_aspaceOver UsubL.
 split => [ndK l lnz | nd l lnz].
   by rewrite UU' => liU; have [k] := ndK l lnz liU; exists k; rewrite UU'.
 by rewrite -UU' => liU'; have [k] := nd l lnz liU'; exists k; rewrite -UU'.
@@ -397,8 +397,8 @@ Lemma int_mod_closed : module (int_closure A L).
 Proof.
 have [A0 _] : zmod_closed A := Asubr; split.
   by rewrite /int_closure mem0v; split => //; apply/int_clos_incl.
-move => a k l aA [kI kL] [lI lL]; split; first by rewrite rpredB ?rpredM //; apply/AsubL.
-by apply/int_zmod_closed => //; apply/int_mulr_closed => //; apply/int_clos_incl. 
+move=> a k l aA [kI kL] [lI lL]; split; first by rewrite rpredB ?rpredM //; apply/AsubL.
+by apply/int_zmod_closed => //; apply/int_mulr_closed => //; apply/int_clos_incl.
 Qed.
 
 End Modules.
@@ -408,7 +408,7 @@ Variable (F0 : fieldType) (E : fieldExtType F0) (I : pred E) (Ifr K : {subfield
 Hypothesis Isubr : subring_closed I.
 Hypothesis Iint : int_closed I.
 Hypothesis Ipid : PID I.
-Hypothesis Ifrac : is_frac_field I Ifr. 
+Hypothesis Ifrac : is_frac_field I Ifr.
 Hypothesis IsubK : {subset I <= K}.
 Hypothesis Knd :  ndeg (trK Ifr K) K.
 
@@ -422,24 +422,24 @@ suffices FisK (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield
   have Ifrsub : (Ifr <= K)%VS.
     apply/subvP=> x /fHk-[fHx fHxx]; rewrite -(mulKf (fH0 x) x).
     by apply/memvM; rewrite ?memvV; apply/IsubK.
-  have LK : L =i K := mem_aspaceOver Ifrsub; have Lnd : ndeg (tr L) L by rewrite -trK_ndeg. 
+  have LK : L =i K := mem_aspaceOver Ifrsub; have Lnd : ndeg (tr L) L by rewrite -trK_ndeg.
   have Ifrac1 : is_frac_field (I : pred L0) 1.
-    split; first by move => a; rewrite /= trivial_fieldOver; apply/Isub.
+    split; first by move=> a; rewrite /= trivial_fieldOver; apply/Isub.
     by exists f => k; split => //; rewrite trivial_fieldOver => /fHk.
   have [X Xsize [Xf [Xs Xi]]] := FisK _ L0 _ _ Isubr Iint Ipid Ifrac1 Lnd.
   rewrite -dim_aspaceOver => //; have /eqP <- := Xsize; exists (in_tuple X); split; last first.
-    split => m; last by move => /Xi; rewrite /int_closure LK.  
-    by rewrite /int_closure -LK; move => /Xs.
-  move: Xf; rewrite -{1}(in_tupleE X); move => /freeP-XfL0; apply/freeP => k.
+    split => m; last by move=> /Xi; rewrite /int_closure LK.
+    by rewrite /int_closure -LK => - /Xs.
+  move: Xf; rewrite -{1}(in_tupleE X) => - /freeP-XfL0; apply/freeP => k.
   have [k' kk'] : exists k' : 'I_(size X) -> F, forall i, (k i)%:A = vsval (k' i).
     by exists (fun i => vsproj Ifr (k i)%:A) => i; rewrite vsprojK ?rpredZ ?mem1v.
   pose Ainj := fmorph_inj [rmorphism of in_alg E].
-  move => kS i; apply/Ainj => {Ainj} /=; rewrite scale0r kk'; apply/eqP.
+  move=> kS i; apply/Ainj => {Ainj} /=; rewrite scale0r kk'; apply/eqP.
   rewrite raddf_eq0; last by apply/subvs_inj.
   by apply/eqP/XfL0; rewrite -{3}kS => {i}; apply/eq_bigr => i _; rewrite -[RHS]mulr_algl kk'.
-move => Asubr Aint Apid Afrac1 Lnd; pose n := \dim L; have Amulr : mulr_closed A := Asubr.
+move=> Asubr Aint Apid Afrac1 Lnd; pose n := \dim L; have Amulr : mulr_closed A := Asubr.
 have [A0 _] : zmod_closed A := Asubr; have [Asub1 _] := Afrac1.
-have AsubL : {subset A <= L} by move => a /Asub1; apply (subvP (sub1v L) a).
+have AsubL : {subset A <= L} by move=> a /Asub1; apply (subvP (sub1v L) a).
 have [b1 [b1B b1H]] : exists (b1 : n.-tuple L0), [/\ basis_of L b1 &
   forall i : 'I_n, integral A b1`_i].
   pose b0 := vbasis L; have [f /all_and3-[fH0 fHa fHi]] := frac_field_alg_int Asubr Afrac1.
@@ -453,7 +453,7 @@ have [b1 [b1B b1H]] : exists (b1 : n.-tuple L0), [/\ basis_of L b1 &
     have dinA : d \in A by rewrite rpred_prod.
     rewrite limg_amulr; apply/eqP; rewrite -dimv_leqif_eq; first by rewrite dim_cosetv_unit.
     by apply/prodv_sub => //; apply/AsubL.
-  rewrite -lim limg_basis_of //; last by apply/vbasisP. 
+  rewrite -lim limg_basis_of //; last by apply/vbasisP.
   by have /eqP -> := lker0_amulr dun; rewrite capv0.
 have [b2 [/andP[/eqP-b2s b2f] b2H]] : exists (b2 : n.-tuple L0), [/\ basis_of L b2 &
   forall b, b \in L -> integral A b -> forall i, (coord b2 i b)%:A \in A].
@@ -465,55 +465,55 @@ have [b2 [/andP[/eqP-b2s b2f] b2H]] : exists (b2 : n.-tuple L0), [/\ basis_of L
   by congr (_ + _); apply/big1 => j jneqi; rewrite (oj j jneqi) mulr0.
 have Mbasis k (X : k.-tuple L0) M : free X -> module A M -> submod M (span_mod A X) ->
   exists B, basis_of_mod A M B.
-  move: k X M; elim => [X M _ _ Ms | k IH X M Xf [M0 Mm] Ms].
-    by exists [::]; rewrite /basis_of_mod nil_free; move: Ms; rewrite tuple0. 
+  move: k X M; elim=> [X M _ _ Ms | k IH X M Xf [M0 Mm] Ms].
+    by exists [::]; rewrite /basis_of_mod nil_free; move: Ms; rewrite tuple0.
   pose X1 := [tuple of behead X]; pose v := thead X.
   pose M1 := fun m => M m /\ coord X ord0 m = 0.
   pose M2 := fun (a : L0) => exists2 m, M m & (coord X ord0 m)%:A = a.
   have scr r m : r \in A -> exists c, r * m = c *: m.
-    by move => /Asub1/vlineP[c ->]; exists c; rewrite mulr_algl.
+    by move=> /Asub1/vlineP[c ->]; exists c; rewrite mulr_algl.
   have span_coord m : M m -> exists r : (k.+1).-tuple L0,
     [/\ all A r, m = \sum_(i < k.+1) r`_i * X`_i & forall i, (coord X i m)%:A = r`_i].
     have seqF (s : seq L0) : all A s -> exists s', s = [seq c%:A | c <- s'].
       elim: s => [_| a l IHl /= /andP[/Asub1/vlineP[c ->]]]; first by exists [::].
-      by move => /IHl[s' ->]; exists (c :: s').
-    move => mM; have := Ms m mM; rewrite /span_mod !size_tuple; move => [r rA rS].
+      by move=> /IHl[s' ->]; exists (c :: s').
+    move=> mM; have := Ms m mM; rewrite /span_mod !size_tuple => - [r rA rS].
     exists r; split => //; have [rF rFr] := seqF r rA => {seqF}; rewrite rFr in rA.
     have rFs : size rF = k.+1 by rewrite -(size_tuple r) rFr size_map.
     have -> : m = \sum_(i < k.+1) rF`_i *: X`_i.
       by rewrite rS; apply/eq_bigr => i _; rewrite rFr (nth_map 0) ?rFs // mulr_algl.
-    by move => i; rewrite coord_sum_free // rFr (nth_map 0) ?rFs. 
+    by move=> i; rewrite coord_sum_free // rFr (nth_map 0) ?rFs.
   have [B1 [B1f [B1s B1A]]] : exists B1, basis_of_mod A M1 B1.
     have X1f : free X1 by move: Xf; rewrite (tuple_eta X) free_cons => /andP[_].
     apply/(IH X1) => //.
       rewrite /module /M1 linear0; split => // a x y aA [xM xfc0] [yM yfc0].
       have := Mm a x y aA xM yM; move: aA => /Asub1/vlineP[r] ->; rewrite mulr_algl => msc.
       by rewrite /M1 linearB linearZ /= xfc0 yfc0 subr0 mulr0.
-    move => m [mM mfc0]; have := span_coord m mM; move => [r [rA rS rC]].
-    move: mfc0 (rC 0) ->; rewrite scale0r; move => r0; rewrite /span_mod size_tuple.
+    move=> m [mM mfc0]; have := span_coord m mM => - [r [rA rS rC]].
+    move: mfc0 (rC 0) ->; rewrite scale0r => - r0; rewrite /span_mod size_tuple.
     exists [tuple of behead r]; first by apply/allP => a /mem_behead/(allP rA).
     by rewrite rS big_ord_recl -r0 mul0r add0r; apply/eq_bigr => i _; rewrite !nth_behead.
   have [a [w wM wC] aG] : exists2 a, M2 a & forall v, M2 v -> exists2 d, d \in A & d * a = v.
     apply/Apid; split.
-      move => c [m mM <-]; have := span_coord m mM; move => [r [/all_nthP-rA _ rC]].
+      move=> c [m mM <-]; have := span_coord m mM => - [r [/all_nthP-rA _ rC]].
       by move: rC ->; apply/rA; rewrite size_tuple.
     split; first by exists 0 => //; rewrite linear0 scale0r.
-    move => c x y cA [mx mxM mxC] [my myM myC]; have := Mm c mx my cA mxM myM. 
+    move=> c x y cA [mx mxM mxC] [my myM myC]; have := Mm c mx my cA mxM myM.
     move: cA => /Asub1/vlineP[r] ->; rewrite !mulr_algl => mC.
     by exists (r *: mx - my) => //; rewrite linearB linearZ /= scalerBl -scalerA mxC myC.
   pose Ainj := fmorph_inj [rmorphism of in_alg L0].
   have mcM1 m : M m -> exists2 d, d \in A & d * a = (coord X 0 m)%:A.
-    by move => mM; apply/aG; exists m.
+    by move=> mM; apply/aG; exists m.
   case: (eqVneq a 0) => [| an0].
-    exists B1; split => //; split => [m mM |]; last by move => m /B1A[mM].
+    exists B1; split => //; split => [m mM |]; last by move=> m /B1A[mM].
     apply/B1s; split => //; apply/Ainj => /=; have [d _ <-] := mcM1 m mM.
-    by rewrite a0 mulr0 scale0r.      
+    by rewrite a0 mulr0 scale0r.
   exists (w :: B1); split.
     rewrite free_cons B1f andbT; move: an0; apply/contra; move: wC <-.
-    rewrite -(in_tupleE B1); move => /coord_span ->; apply/eqP.
+    rewrite -(in_tupleE B1) => - /coord_span ->; apply/eqP.
     rewrite linear_sum big1 ?scale0r => //= i _; rewrite linearZ /=.
     by have [_] := B1A B1`_i (mem_nth 0 (ltn_ord _)) => ->; rewrite mulr0.
-  split => [m mM | m]; last by rewrite in_cons; move => /orP; case => [/eqP ->|/B1A[mM]].
+  split => [m mM | m]; last by rewrite in_cons => - /orP; case=> [/eqP ->|/B1A[mM]].
   have [d dA dam] := mcM1 m mM; have mdwM1 : M1 (m - d * w).
     split; [have Mdwm := Mm d w m dA wM mM; have := Mm _ _ _ A0 Mdwm Mdwm |].
       by rewrite mul0r sub0r opprB.
@@ -525,17 +525,17 @@ have [X Xb] : exists X, basis_of_mod A (int_closure A L) X.
   apply/(Mbasis _ b2 _ b2f) => [| m [mL mI]]; first by apply/int_mod_closed.
   pose r : n.-tuple L0 := [tuple (coord b2 i m)%:A | i < n]; rewrite /span_mod size_tuple.
   exists r; have rci (i : 'I_n) : r`_i = (coord b2 i m)%:A by rewrite -tnth_nth tnth_mktuple.
-    apply/(all_nthP 0) => i; rewrite size_tuple; move => iB.
-    by have -> := rci (Ordinal iB); apply/b2H. 
-  move: mL; rewrite -b2s; move => /coord_span ->; apply/eq_bigr => i _.
+    apply/(all_nthP 0) => i; rewrite size_tuple => - iB.
+    by have -> := rci (Ordinal iB); apply/b2H.
+  move: mL; rewrite -b2s => - /coord_span ->; apply/eq_bigr => i _.
   by rewrite rci mulr_algl.
 exists X => //; move: Xb => [/eqP-Xf [Xs Xg]]; rewrite -Xf eqn_leq; apply/andP; split.
   by apply/dimvS/span_subvP => m /Xg[mL _].
 have /andP[/eqP-b1s _] := b1B; rewrite -b1s; apply/dimvS/span_subvP => b /tnthP-[i ->] {b}.
 rewrite (tnth_nth 0); have [r /all_tnthP-rA ->] : span_mod A X b1`_i.
   by apply/Xs; rewrite /int_closure (basis_mem b1B) ?mem_nth ?size_tuple => //.
-apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0); move => /Asub1/vlineP[c ->].
-by rewrite mulr_algl; apply/rpredZ/memv_span/mem_nth. 
+apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0) => - /Asub1/vlineP[c ->].
+by rewrite mulr_algl; apply/rpredZ/memv_span/mem_nth.
 Qed.
 
 End BasisLemma.
\ No newline at end of file