chore(LinearAlgebra): fix whitespace (leanprover-community#33169)

Found by extending the commandStart linter to proof bodies.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: harahu

Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean

@@ -129,7 +129,7 @@ def faceOpposite {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : Si
   s.face (fs := {i}ᶜ) (by simp [card_compl, NeZero.one_le])
 
 @[simp] lemma range_faceOpposite_points {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :
-    Set.range (s.faceOpposite i).points = s.points '' {i}ᶜ  := by
+    Set.range (s.faceOpposite i).points = s.points '' {i}ᶜ := by
   simp [faceOpposite]
 
 lemma faceOpposite_point_eq_point_succAbove {n : ℕ} [NeZero n] (s : Simplex k P n)

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -821,7 +821,7 @@ lemma genEigenspace_inf_le_add
   suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
     rw [LinearMap.smul_apply, this, smul_zero]
   rw [Finset.mem_antidiagonal] at hij
-  obtain hi|hj : l₁ ≤ i ∨ l₂ ≤ j := by lia
+  obtain hi | hj : l₁ ≤ i ∨ l₂ ≤ j := by lia
   · rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, map_zero]
   · rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, map_zero]
 

Mathlib/LinearAlgebra/FreeAlgebra.lean

@@ -46,7 +46,7 @@ end
 
 theorem rank_eq [CommRing R] [Nontrivial R] :
     Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u} (Cardinal.mk (List X)) := by
-  rw [← (Basis.mk_eq_rank'.{_,_,_,u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
+  rw [← (Basis.mk_eq_rank'.{_, _, _, u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
     Cardinal.lift_umax.{v, u}, FreeMonoid]
 
 end FreeAlgebra

Mathlib/LinearAlgebra/FreeModule/Basic.lean

@@ -158,7 +158,7 @@ instance self : Module.Free R R :=
 instance ulift [Free R M] : Free R (ULift M) := of_equiv ULift.moduleEquiv.symm
 
 instance (priority := 100) of_subsingleton [Subsingleton N] : Module.Free R N :=
-  of_basis.{u,z,z} (Basis.empty N : Basis PEmpty R N)
+  of_basis.{u, z, z} (Basis.empty N : Basis PEmpty R N)
 
 -- This was previously a global instance,
 -- but it doesn't appear to be used and has been implicated in slow typeclass resolutions.

Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

@@ -116,7 +116,7 @@ lemma charmatrix_fromBlocks :
     charmatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) =
       fromBlocks (charmatrix M₁₁) (- M₁₂.map C) (- M₂₁.map C) (charmatrix M₂₂) := by
   simp only [charmatrix]
-  ext (i|i) (j|j) : 2 <;> simp [diagonal]
+  ext (i | i) (j | j) : 2 <;> simp [diagonal]
 
 -- TODO: importing block triangular here is somewhat expensive, if more lemmas about it are added
 -- to this file, it may be worth extracting things out to Charpoly/Block.lean

Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean

@@ -47,7 +47,7 @@ theorem submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det {n : ℕ}
       · replace hv := congr_fun hv b
         rw [Fin.sum_univ_succAbove _ i.succ, Pi.add_apply, Finset.sum_apply] at hv
         rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
-      · obtain h|h := ne_iff_lt_or_gt.mp h
+      · obtain h | h := ne_iff_lt_or_gt.mp h
         · rw [Fin.succAbove_castSucc_of_lt _ _ h,
             Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
         · rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]

Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

@@ -229,7 +229,8 @@ private lemma prop_red_T_pow (hS : ∀ B, C B → C (S • B)) (hT : ∀ B, C B
   induction n with
   | zero => simp only [zpow_zero, one_smul]
   | succ n hn =>
-    simpa only [add_comm (n:ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc, prop_red_T hS hT]
+    simpa only [add_comm (n : ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc,
+      prop_red_T hS hT]
   | pred m hm =>
     rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]