running semi-automated linting on the whole library

1 files changed, 23 insertions, 23 deletions

diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v
index a1a987b..7098af9 100644
--- a/mathcomp/attic/forms.v
+++ b/mathcomp/attic/forms.v
@@ -20,7 +20,7 @@ Variable (R : fieldType).
 Definition r2rv x: 'rV[R^o]_1 := \row_(i < 1) x .
 
 Lemma r2rv_morph_p : linear r2rv.
-Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j;rewrite !mxE. Qed.
+Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j; rewrite !mxE. Qed.
 
 Canonical Structure r2rv_morph := Linear r2rv_morph_p.
 
@@ -28,8 +28,8 @@ Definition rv2r (A: 'rV[R]_1): R^o := A 0 0.
 
 Lemma r2rv_bij : bijective r2rv.
 Proof.
-exists rv2r; first by move => x; rewrite /r2rv /rv2r /= mxE.
-by move => x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=.
+exists rv2r; first by move=> x; rewrite /r2rv /rv2r /= mxE.
+by move=> x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=.
 Qed.
 
 Canonical Structure  RVMixin := Eval hnf in VectMixin r2rv_morph_p r2rv_bij.
@@ -48,7 +48,7 @@ Variable (F : fieldType) (V : vectType  F).
 Section SesquiLinearFormDef.
 
 Structure fautomorphism:= FautoMorph {fval :> F -> F;
-                                      _ : rmorphism  fval; 
+                                      _ : rmorphism  fval;
                                       _ : bijective fval}.
 Variable theta: fautomorphism.
 
@@ -72,7 +72,7 @@ Variable f : sesquilinear_form.
 Lemma bilin1 :  forall x, {morph f x : y z / y + z}. Proof. by case f. Qed.
 Lemma bilin2 :  forall x, {morph f ^~  x : y z / y + z}. Proof. by case f. Qed.
 Lemma bilina1 :  forall a x y, f (a *: x) y = a * f x y. Proof. by case f. Qed.
-Lemma bilina2 : forall a x y, f x (a *: y) = (theta  a) * (f x y). 
+Lemma bilina2 : forall a x y, f x (a *: y) = (theta  a) * (f x y).
 Proof. by case f. Qed.
 
 End SesquiLinearFormDef.
@@ -97,9 +97,9 @@ Inductive symmetricf (f : sqlf): Prop :=
 Lemma fsym_f0: forall  (f: sqlf) x y, (symmetricf f) ->  
                                         (f x y = 0  <-> f y x = 0).
 Proof.
-move => f x y ;case; first by  move=>  [Htheta Hf];split; rewrite Hf.
-  by move=>  [Htheta Hf];split; rewrite Hf; move/eqP;rewrite oppr_eq0; move/eqP->.
-move=> Htheta;split; first by rewrite (Htheta y x) => ->; rewrite rmorph0.
+move=> f x y; case; first by  move=> [Htheta Hf]; split; rewrite Hf.
+  by move=> [Htheta Hf]; split; rewrite Hf; move/eqP; rewrite oppr_eq0; move/eqP->.
+move=> Htheta; split; first by rewrite (Htheta y x) => ->; rewrite rmorph0.
 by rewrite (Htheta x y) => ->; rewrite rmorph0.
 Qed.
 
@@ -114,21 +114,21 @@ Section orthogonal.
 Definition orthogonal x y := f x y = 0.
 
 Lemma ortho_sym: forall x y, orthogonal x y <-> orthogonal y x.
-Proof. by move=> x y; apply:fsym_f0. Qed.
+Proof. by move=> x y; apply: fsym_f0. Qed.
 
 Theorem Pythagore: forall u v, orthogonal u v -> f (u+v) (u+v)  = f u u  + f v v.
 Proof.
-move => u v Huv; case:(ortho_sym  u v ) => Hvu _.
+move=> u v Huv; case: (ortho_sym  u v ) => Hvu _.
 by rewrite !bilin1 !bilin2 Huv (Hvu Huv) add0r addr0.
 Qed.
 
 Lemma orthoD : forall u v w , orthogonal u v -> orthogonal u w -> orthogonal u (v + w).
 Proof.
-by move => u v w Huv Huw; rewrite  /orthogonal bilin1 Huv Huw add0r.
+by move=> u v w Huv Huw; rewrite /orthogonal bilin1 Huv Huw add0r.
 Qed.
 
 Lemma orthoZ: forall u v a, orthogonal u v ->  orthogonal (a *: u) v.
-Proof. by move => u v a Huv; rewrite  /orthogonal bilina1 Huv mulr0. Qed.
+Proof. by move=> u v a Huv; rewrite /orthogonal bilina1 Huv mulr0. Qed.
 
 Variable x:V.
 
@@ -139,7 +139,7 @@ Definition alpha_lfun := (lfun_of_fun alpha).
 Definition  xbar := lker alpha_lfun .
 
 Lemma alpha_lin: linear alpha.
-Proof. by move => a b c; rewrite /alpha bilin2 bilina1. Qed.
+Proof. by move=> a b c; rewrite /alpha bilin2 bilina1. Qed.
 
 
 
@@ -151,10 +151,10 @@ Qed.
 
 
 Lemma dim_xbar :forall vs,(\dim vs ) -  1 <= \dim (vs :&: xbar).
-Proof. 
+Proof.
 move=> vs; rewrite -(addKn 1 (\dim (vs :&: xbar))) addnC leq_sub2r //.
 have H :\dim  (alpha_lfun @: vs )<= 1 by rewrite -(dimR F) -dimvf dimvS // subvf.
-by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))). 
+by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))).
 Qed.
 
 (* to be improved*)
@@ -162,16 +162,16 @@ Lemma xbar_eqvs: forall vs,  (forall v , v \in vs -> orthogonal v x )-> \dim (vs
 move=> vs  Hvs.
 rewrite -(limg_ker_dim alpha_lfun vs).
 suff-> : \dim (alpha_lfun @: vs) = 0%nat by rewrite addn0.
-apply/eqP; rewrite dimv_eq0; apply /vspaceP => w.
-rewrite memv0;apply/memv_imgP.
+apply/eqP; rewrite dimv_eq0; apply/vspaceP => w.
+rewrite memv0; apply/memv_imgP.
 case e: (w==0).
-  exists 0; split ;first by rewrite mem0v.
+  exists 0; split; first by rewrite mem0v.
   apply sym_eq; rewrite (eqP e).
   rewrite (lfun_of_funK alpha_lin 0).
   rewrite /alpha_lfun /alpha /=.
-  by move:(bilina1 f 0 x x); rewrite scale0r mul0r.
-move/eqP:e =>H2;case=> x0 [Hx0 Hw].
-apply H2;rewrite Hw;move: (Hvs x0 Hx0).
+  by move: (bilina1 f 0 x x); rewrite scale0r mul0r.
+move/eqP:e =>H2; case=> x0 [Hx0 Hw].
+apply H2; rewrite Hw; move: (Hvs x0 Hx0).
 rewrite /orthogonal.
 by rewrite (lfun_of_funK alpha_lin x0).
 Qed.
@@ -189,9 +189,9 @@ Import GRing.Theory.
 
 Lemma f2Q:  forall x, Q x + Q x = f x x.
 Proof.
-move=> x; apply:(@addrI _ (Q x + Q x)).
+move=> x; apply: (@addrI _ (Q x + Q x)).
 rewrite !addrA  -quadQ -[x + x](scaler_nat 2) quadQ.
-by rewrite  -mulrA !mulr_natl -addrA.
+by rewrite -mulrA !mulr_natl -addrA.
 Qed.
 
 End LinearForm.