chore(Algebra): fix whitespace (leanprover-community#32906)

Author: harahu

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -46,7 +46,7 @@ structure AddConstMap (G H : Type*) [Add G] [Add H] (a : G) (b : H) where
   map_add_const' (x : G) : toFun (x + a) = toFun x + b
 
 @[inherit_doc]
-scoped [AddConstMap] notation:25 G " →+c[" a ", " b "] " H => AddConstMap G H a b
+scoped[AddConstMap] notation:25 G " →+c[" a ", " b "] " H => AddConstMap G H a b
 
 /-- Typeclass for maps satisfying `f (x + a) = f x + b`.
 
@@ -67,7 +67,7 @@ namespace AddConstMapClass
 In this section we prove properties like `f (x + n • a) = f x + n • b`.
 -/
 
-scoped [AddConstMapClass] attribute [simp] map_add_const
+scoped[AddConstMapClass] attribute [simp] map_add_const
 
 variable {F G H : Type*} [FunLike F G H] {a : G} {b : H}
 

Mathlib/Algebra/AffineMonoid/Basic.lean

@@ -17,10 +17,10 @@ monoids.
 public section
 
 /-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid. -/
-class abbrev IsAffineAddMonoid (M : Type*) [AddCommMonoid M] : Prop :=
+class abbrev IsAffineAddMonoid(M : Type*)[AddCommMonoid M] : Prop :=
   IsCancelAdd M, AddMonoid.FG M, IsAddTorsionFree M
 
 /-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid. -/
 @[to_additive]
-class abbrev IsAffineMonoid (M : Type*) [CommMonoid M] : Prop :=
+class abbrev IsAffineMonoid(M : Type*)[CommMonoid M] : Prop :=
   IsCancelMul M, Monoid.FG M, IsMulTorsionFree M

Mathlib/Algebra/Algebra/Operations.lean

@@ -185,7 +185,7 @@ protected theorem smul_assoc {B} [Semiring B] [Module R B] [Module A B] [Module
       fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)
 
 theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
-    I • (⨆ i, t i)= ⨆ i, I • t i :=
+    I • (⨆ i, t i) = ⨆ i, I • t i :=
   toAddSubmonoid_injective <| by
     simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]
 

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

@@ -231,7 +231,7 @@ theorem unit_smul_eq_smul (a : A) (r : Rˣ) : σ (r • a) = r • σ a := by
   constructor
   · exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
   · rintro ⟨w, _, (x'_eq : r • w = x)⟩
-    simpa [← x'_eq ]
+    simpa [← x'_eq]
 
 -- `r ∈ σ(a*b) ↔ r ∈ σ(b*a)` for any `r : Rˣ`
 theorem unit_mem_mul_comm {a b : A} {r : Rˣ} : ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a) := by

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

@@ -280,7 +280,7 @@ lemma NonUnitalAlgHom.quasispectrum_apply_subset' {F R : Type*} (S : Type*) {A B
     forall_exists_index]
   refine fun hx this ↦ ⟨hx, ?_⟩
   rw [Units.smul_def, ← smul_one_smul S] at this ⊢
-  simpa [- smul_assoc] using this.map φ
+  simpa [-smul_assoc] using this.map φ
 
 /-- If `φ` is non-unital algebra homomorphism over a scalar ring `R`, then
 `quasispectrum R (φ a) ⊆ quasispectrum R a`. -/

Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

@@ -25,7 +25,7 @@ section Pointwise
 variable {R : Type*} {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
 
 theorem mul_toSubmodule_le (S T : Subalgebra R A) :
-    (Subalgebra.toSubmodule S)* (Subalgebra.toSubmodule T) ≤ Subalgebra.toSubmodule (S ⊔ T) := by
+    (Subalgebra.toSubmodule S) * (Subalgebra.toSubmodule T) ≤ Subalgebra.toSubmodule (S ⊔ T) := by
   rw [Submodule.mul_le]
   intro y hy z hz
   change y * z ∈ S ⊔ T

Mathlib/Algebra/Algebra/Tower.lean

@@ -404,4 +404,4 @@ theorem Algebra.algebraMapSubmonoid_map_map {R A B : Type*} [CommSemiring R] [Co
     algebraMapSubmonoid B (algebraMapSubmonoid A M) = algebraMapSubmonoid B M :=
   algebraMapSubmonoid_map_eq _ (IsScalarTower.toAlgHom R A B)
 
-end  Algebra.algebraMapSubmonoid
+end Algebra.algebraMapSubmonoid

Mathlib/Algebra/Algebra/ZMod.lean

@@ -50,7 +50,7 @@ abbrev algebra (p : ℕ) [CharP R p] : Algebra (ZMod p) R :=
 /-- Any ring with a `ZMod p`-module structure can be upgraded to a `ZMod p`-algebra. Not an
 instance because this is usually not the default way, and this will cause typeclass search loop. -/
 def algebraOfModule (n : ℕ) (R : Type*) [Ring R] [Module (ZMod n) R] : Algebra (ZMod n) R :=
-  Algebra.ofModule' (proof · ·|>.1) (proof · ·|>.2) where
+  Algebra.ofModule' (proof · · |>.1) (proof · · |>.2) where
   proof (r : ZMod n) (x : R) : r • 1 * x = r • x ∧ x * r • 1 = r • x := by
     obtain _ | n := n
     · obtain rfl : (inferInstanceAs (Module ℤ R)) = ‹_› := Subsingleton.elim _ _

Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

@@ -106,7 +106,7 @@ open Batteries.ExtendedBinder Lean Meta
 /-- A `bigOpBinder` is like an `extBinder` and has the form `x`, `x : ty`, or `x pred`
 where `pred` is a `binderPred` like `< 2`.
 Unlike `extBinder`, `x` is a term. -/
-syntax bigOpBinder := term:max ((" : " term) <|> binderPred)?
+syntax bigOpBinder := term:max((" : "term) <|> binderPred)?
 /-- A BigOperator binder in parentheses -/
 syntax bigOpBinderParenthesized := " (" bigOpBinder ")"
 /-- A list of parenthesized binders -/

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -64,7 +64,7 @@ theorem prod_hom₂ (l : List ι) (f : M → N → P) (hf : ∀ a b c d, f (a *
     (hf' : f 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) :
     (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by
   simp only [prod_eq_foldr, foldr_map]
-  rw [← foldr_hom₂ l f _ _ ((fun x y => f (f₁ x) (f₂ x) * y) ) _ _ (by simp [hf]), hf']
+  rw [← foldr_hom₂ l f _ _ ((fun x y => f (f₁ x) (f₂ x) * y)) _ _ (by simp [hf]), hf']
 
 @[to_additive (attr := simp)]
 theorem prod_map_mul {M : Type*} [CommMonoid M] {l : List ι} {f g : ι → M} :