chore: cleanup whitespace (#5988)

Grepping for `[^ .:{-]  [^ :]` and reviewing the results. Once I started I couldn't stop. :-)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Archive/Imo/Imo2019Q4.lean

@@ -90,7 +90,7 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
   -- The implication `←` holds.
   constructor
   swap
-  · rintro (h | h) <;> simp [Prod.ext_iff] at h  <;> rcases h with ⟨rfl, rfl⟩ <;>
+  · rintro (h | h) <;> simp [Prod.ext_iff] at h <;> rcases h with ⟨rfl, rfl⟩ <;>
     norm_num [prod_range_succ, succ_mul]
   intro h
   -- We know that n < 6.

Archive/Imo/Imo2021Q1.lean

@@ -60,7 +60,7 @@ theorem exists_numbers_in_interval (n : ℕ) (hn : 100 ≤ n) :
     linarith only [hn]
   rw [← Nat.sub_add_cancel hn'] at h₁ h₂ h₃
   set l := (n + 1).sqrt - 1
-  refine ⟨l, ?_,  ?_⟩
+  refine ⟨l, ?_, ?_⟩
   · calc n + 4 * l ≤ (l ^ 2 + 4 * l + 2) + 4 * l := by linarith only [h₂]
       _ ≤ 2 * l ^ 2 := by nlinarith only [h₃]
   · linarith only [h₁]

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -47,7 +47,7 @@ to the n-ball.
 
 
 
-local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y) -- Porting note: See issue #2220
+local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220
 
 open Set Real MeasureTheory intervalIntegral
 

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -888,7 +888,7 @@ noncomputable def iSupLift [Nonempty ι] (K : ι → NonUnitalSubalgebra R A) (d
             (↑(iSup K)) (by rw [coe_iSup_of_directed dir])
         map_zero' := by
           dsimp
-          exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl)  _ (by simp)
+          exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
         map_mul' := by
           dsimp
           apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -20,9 +20,9 @@ This theory will serve as the foundation for spectral theory in Banach algebras.
 ## Main definitions
 
 * `resolventSet a : Set R`: the resolvent set of an element `a : A` where
-  `A` is an  `R`-algebra.
+  `A` is an `R`-algebra.
 * `spectrum a : Set R`: the spectrum of an element `a : A` where
-  `A` is an  `R`-algebra.
+  `A` is an `R`-algebra.
 * `resolvent : R → A`: the resolvent function is `fun r ↦ Ring.inverse (↑ₐr - a)`, and hence
   when `r ∈ resolvent R A`, it is actually the inverse of the unit `(↑ₐr - a)`.
 

Mathlib/Algebra/Associated.lean

@@ -933,7 +933,7 @@ theorem dvd_of_mk_le_mk {a b : α} : Associates.mk a ≤ Associates.mk b → a 
             b = a * c * ↑d := hd.symm
             _ = a * (↑d * c) := by ac_rfl
             ⟩
-    Quotient.inductionOn c' step  hc'
+    Quotient.inductionOn c' step hc'
 #align associates.dvd_of_mk_le_mk Associates.dvd_of_mk_le_mk
 
 theorem mk_le_mk_of_dvd {a b : α} : a ∣ b → Associates.mk a ≤ Associates.mk b := fun ⟨c, hc⟩ =>

Mathlib/Algebra/BigOperators/Pi.lean

@@ -75,7 +75,7 @@ section MulSingle
 
 variable {I : Type _} [DecidableEq I] {Z : I → Type _}
 
-variable [∀ i, CommMonoid  (Z i)]
+variable [∀ i, CommMonoid (Z i)]
 
 @[to_additive]
 theorem Finset.univ_prod_mulSingle [Fintype I] (f : ∀ i, Z i) :

Mathlib/Algebra/BigOperators/Ring.lean

@@ -152,7 +152,7 @@ theorem prod_add (f g : α → β) (s : Finset α) :
             (fun a _ => a.1) (by simp) (by simp)
             (fun a ha => ⟨a, (mem_sdiff.1 ha).1⟩) (fun a ha => by simp at ha; simp; tauto)
             (by simp) (by simp))
-        (fun t _ a  _ => a ∈ t)
+        (fun t _ a _ => a ∈ t)
         (by simp [Classical.em])
         (by simp [Function.funext_iff]; tauto)
         (by simp [Finset.ext_iff, @mem_filter _ _ (id _)]; tauto)

Mathlib/Algebra/Category/GroupCat/EpiMono.lean

@@ -86,7 +86,7 @@ theorem ker_eq_bot_of_mono [Mono f] : f.ker = ⊥ :=
 
 @[to_additive]
 theorem mono_iff_ker_eq_bot : Mono f ↔ f.ker = ⊥ :=
-  ⟨fun _ => ker_eq_bot_of_mono f,  fun h =>
+  ⟨fun _ => ker_eq_bot_of_mono f, fun h =>
     ConcreteCategory.mono_of_injective _ <| (MonoidHom.ker_eq_bot_iff f).1 h⟩
 #align Group.mono_iff_ker_eq_bot GroupCat.mono_iff_ker_eq_bot
 #align AddGroup.mono_iff_ker_eq_bot AddGroupCat.mono_iff_ker_eq_bot

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -386,7 +386,7 @@ def HomEquiv.toRestriction {X Y} (g : Y ⟶ (coextendScalars f).obj X) : (restri
 #align category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction CategoryTheory.ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction
 
 -- Porting note: add to address timeout in unit'
-def app' (Y : ModuleCat S) : Y →ₗ[S] (restrictScalars f ⋙  coextendScalars f).obj Y :=
+def app' (Y : ModuleCat S) : Y →ₗ[S] (restrictScalars f ⋙ coextendScalars f).obj Y :=
   { toFun := fun y : Y =>
       { toFun := fun s : S => (s • y : Y)
         map_add' := fun s s' => add_smul _ _ _
@@ -522,7 +522,7 @@ The map `S → X →ₗ[R] Y` given by `fun s x => s • (g x)`
 -/
 @[simps]
 def HomEquiv.evalAt {X : ModuleCat R} {Y : ModuleCat S} (s : S)
-    (g : X ⟶  (restrictScalars f).obj Y) : have : Module R Y := Module.compHom Y f
+    (g : X ⟶ (restrictScalars f).obj Y) : have : Module R Y := Module.compHom Y f
     X →ₗ[R] Y :=
   @LinearMap.mk _ _ _ _ (RingHom.id R) X Y _ _ _ (_)
     { toFun := fun x => s • (g x : Y)
@@ -534,7 +534,7 @@ def HomEquiv.evalAt {X : ModuleCat R} {Y : ModuleCat S} (s : S)
 
 /--
 Given `R`-module X and `S`-module Y and a map `X ⟶ (restrict_scalars f).obj Y`, i.e `R`-linear map
-`X ⟶ Y`, there is a map `(extend_scalars f).obj X ⟶ Y`, i.e  `S`-linear map `S ⨂ X → Y` by
+`X ⟶ Y`, there is a map `(extend_scalars f).obj X ⟶ Y`, i.e `S`-linear map `S ⨂ X → Y` by
 `s ⊗ x ↦ s • g x`.
 -/
 @[simps apply]
@@ -721,4 +721,3 @@ instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+*
   ⟨_, extendRestrictScalarsAdj f⟩
 
 end CategoryTheory.ModuleCat
-

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -58,7 +58,7 @@ add_decl_doc AddMonCat.AssocAddMonoidHom
 
 @[to_additive]
 instance bundledHom : BundledHom AssocMonoidHom where
-  toFun  {X Y} _ _ f := ⇑f
+  toFun {X Y} _ _ f := ⇑f
   id _ := MonoidHom.id _
   comp _ _ _ := MonoidHom.comp
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -191,7 +191,7 @@ theorem PNat.isUnit_natCast [h : Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (
   -- But `n` generates the ideal, so its image is clearly zero.
   rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]
   exact Ideal.subset_span (Set.mem_singleton _)
-#align equal_char_zero.pnat_coe_is_unit  EqualCharZero.PNat.isUnit_natCast
+#align equal_char_zero.pnat_coe_is_unit EqualCharZero.PNat.isUnit_natCast
 
 @[coe]
 noncomputable def pnatCast [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] : ℕ+ → Rˣ :=

Mathlib/Algebra/EuclideanDomain/Instances.lean

@@ -38,7 +38,7 @@ instance Int.euclideanDomain : EuclideanDomain ℤ :=
       not_lt_of_ge <| by
         rw [← mul_one a.natAbs, Int.natAbs_mul]
         rw [←Int.natAbs_pos] at b0
-        exact Nat.mul_le_mul_of_nonneg_left b0  }
+        exact Nat.mul_le_mul_of_nonneg_left b0 }
 
 -- see Note [lower instance priority]
 instance (priority := 100) Field.toEuclideanDomain {K : Type _} [Field K] : EuclideanDomain K :=

Mathlib/Algebra/FreeAlgebra.lean

@@ -264,7 +264,7 @@ private def liftAux (f : X → A) : FreeAlgebra R X →ₐ[R] A where
       · change _ * algebraMap _ _ _ = algebraMap _ _ _
         simp
       repeat
-        change liftFun R X f _ + liftFun R X f _ =  _
+        change liftFun R X f _ + liftFun R X f _ = _
         simp only [*]
         rfl
       repeat

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -202,7 +202,7 @@ theorem casesOn_of_mul {C : FreeMonoid α → Sort _} (x : α) (xs : FreeMonoid
 @[to_additive (attr := ext)]
 theorem hom_eq ⦃f g : FreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g :=
   MonoidHom.ext fun l ↦ recOn l (f.map_one.trans g.map_one.symm)
-    (fun x xs hxs ↦ by  simp only [h, hxs, MonoidHom.map_mul])
+    (fun x xs hxs ↦ by simp only [h, hxs, MonoidHom.map_mul])
 #align free_monoid.hom_eq FreeMonoid.hom_eq
 #align free_add_monoid.hom_eq FreeAddMonoid.hom_eq
 
@@ -211,14 +211,14 @@ The purpose is to make `FreeMonoid.lift_eval_of` true by `rfl`. -/
 @[to_additive "A variant of `List.sum` that has `[x].sum = x` true definitionally.
 The purpose is to make `FreeAddMonoid.lift_eval_of` true by `rfl`."]
 def prodAux {M} [Monoid M] : List M → M
-  | []  => 1
+  | [] => 1
   | (x :: xs) => List.foldl (· * ·) x xs
 #align free_monoid.prod_aux FreeMonoid.prodAux
 #align free_add_monoid.sum_aux FreeAddMonoid.sumAux
 
 @[to_additive]
 lemma prodAux_eq : ∀ l : List M, FreeMonoid.prodAux l = l.prod
-  | []  => rfl
+  | [] => rfl
   | (_ :: xs) => congr_arg (fun x => List.foldl (· * ·) x xs) (one_mul _).symm
 #align free_monoid.prod_aux_eq FreeMonoid.prodAux_eq
 #align free_add_monoid.sum_aux_eq FreeAddMonoid.sumAux_eq

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -930,7 +930,7 @@ instance subsingleton_gcdMonoid_of_unique_units : Subsingleton (GCDMonoid α) :=
       -- Porting note: Lean4 seems to need help specifying `g₁` and `g₂`
       refine' associated_iff_eq.mp (associated_of_dvd_dvd _ _)
       · exact (@lcm_dvd_iff _ _ g₁ ..).mpr ⟨@dvd_lcm_left _ _ g₂ _ _, @dvd_lcm_right _ _ g₂ _ _⟩
-      · exact lcm_dvd_iff.mpr ⟨@dvd_lcm_left  _ _ g₁ _ _, @dvd_lcm_right _ _ g₁  _ _⟩
+      · exact lcm_dvd_iff.mpr ⟨@dvd_lcm_left _ _ g₁ _ _, @dvd_lcm_right _ _ g₁ _ _⟩
     cases g₁
     cases g₂
     dsimp only at hgcd hlcm

Mathlib/Algebra/Group/Basic.lean

@@ -977,7 +977,7 @@ theorem div_mul_cancel'' (a b : G) : a / (a * b) = b⁻¹ := by rw [← inv_div,
 
 -- This lemma is in the `simp` set under the name `mul_inv_cancel_comm_assoc`,
 -- along with the additive version `add_neg_cancel_comm_assoc`,
--- defined  in `Algebra.Group.Commute`
+-- defined in `Algebra.Group.Commute`
 @[to_additive]
 theorem mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b := by
   rw [← div_eq_mul_inv, mul_div_cancel'_right a b]

Mathlib/Algebra/Group/Defs.lean

@@ -469,7 +469,7 @@ variable {M : Type u}
 -- use `x * npowRec n x` and not `npowRec n x * x` in the definition to make sure that
 -- definitional unfolding of `npowRec` is blocked, to avoid deep recursion issues.
 /-- The fundamental power operation in a monoid. `npowRec n a = a*a*...*a` n times.
-Use instead `a ^ n`,  which has better definitional behavior. -/
+Use instead `a ^ n`, which has better definitional behavior. -/
 def npowRec [One M] [Mul M] : ℕ → M → M
   | 0, _ => 1
   | n + 1, a => a * npowRec n a
@@ -740,7 +740,7 @@ instance (priority := 100) CancelMonoid.toIsCancelMul (M : Type u) [CancelMonoid
 end CancelMonoid
 
 /-- The fundamental power operation in a group. `zpowRec n a = a*a*...*a` n times, for integer `n`.
-Use instead `a ^ n`,  which has better definitional behavior. -/
+Use instead `a ^ n`, which has better definitional behavior. -/
 def zpowRec {M : Type _} [One M] [Mul M] [Inv M] : ℤ → M → M
   | Int.ofNat n, a => npowRec n a
   | Int.negSucc n, a => (npowRec n.succ a)⁻¹

Mathlib/Algebra/Group/Opposite.lean

@@ -576,7 +576,7 @@ def MonoidHom.unop {M N} [MulOneClass M] [MulOneClass N] : (Mᵐᵒᵖ →* Nᵐ
 /-- An additive homomorphism `M →+ N` can equivalently be viewed as an additive homomorphism
 `Mᵐᵒᵖ →+ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
 @[simps]
-def AddMonoidHom.mulOp {M N} [AddZeroClass M] [AddZeroClass N] : (M →+ N) ≃ (Mᵐᵒᵖ →+  Nᵐᵒᵖ) where
+def AddMonoidHom.mulOp {M N} [AddZeroClass M] [AddZeroClass N] : (M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ) where
   toFun f :=
     { toFun := MulOpposite.op ∘ f ∘ MulOpposite.unop, map_zero' := unop_injective f.map_zero,
       map_add' := fun x y => unop_injective (f.map_add x.unop y.unop) }

Mathlib/Algebra/Group/UniqueProds.lean

@@ -11,7 +11,7 @@ Authors: Damiano Testa
 import Mathlib.Data.Finset.Preimage
 
 /-!
-#  Unique products and related notions
+# Unique products and related notions
 
 A group `G` has *unique products* if for any two non-empty finite subsets `A, B ⊂ G`, there is an
 element `g ∈ A * B` that can be written uniquely as a product of an element of `A` and an element

Mathlib/Algebra/GroupPower/Order.lean

@@ -459,7 +459,7 @@ theorem le_self_pow (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m :=
 theorem pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a ^ i ≤ b ^ i := by
   intro i
   induction i with
-  | zero =>  simp
+  | zero => simp
   | succ k ih =>
     rw [pow_succ, pow_succ]
     apply mul_le_mul hab

Mathlib/Algebra/GroupPower/Ring.lean

@@ -248,7 +248,7 @@ theorem neg_one_pow_mul_eq_zero_iff {n : ℕ} {r : R} : (-1) ^ n * r = 0 ↔ r =
 
 @[simp]
 theorem mul_neg_one_pow_eq_zero_iff {n : ℕ} {r : R} : r * (-1) ^ n = 0 ↔ r = 0 := by
-  rcases neg_one_pow_eq_or R n with h | h  <;> simp [h]
+  rcases neg_one_pow_eq_or R n with h | h <;> simp [h]
 #align mul_neg_one_pow_eq_zero_iff mul_neg_one_pow_eq_zero_iff
 
 variable [NoZeroDivisors R]

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

@@ -37,7 +37,7 @@ theorem eq_mul_inv_iff_mul_eq₀ (hc : c ≠ 0) : a = b * c⁻¹ ↔ a * c = b :
 #align eq_mul_inv_iff_mul_eq₀ eq_mul_inv_iff_mul_eq₀
 
 theorem eq_inv_mul_iff_mul_eq₀ (hb : b ≠ 0) : a = b⁻¹ * c ↔ b * a = c :=
-  IsUnit.eq_inv_mul_iff_mul_eq  hb.isUnit
+  IsUnit.eq_inv_mul_iff_mul_eq hb.isUnit
 #align eq_inv_mul_iff_mul_eq₀ eq_inv_mul_iff_mul_eq₀
 
 theorem inv_mul_eq_iff_eq_mul₀ (ha : a ≠ 0) : a⁻¹ * b = c ↔ b = a * c :=

Mathlib/Algebra/Hom/Freiman.lean

@@ -329,7 +329,7 @@ theorem one_comp (f : A →*[n] β) {hf} : (1 : B →*[n] γ).comp f hf = 1 :=
 instance : Inhabited (A →*[n] β) :=
   ⟨1⟩
 
-/-- `f * g` is the Freiman homomorphism  sends `x` to `f x * g x`. -/
+/-- `f * g` is the Freiman homomorphism sends `x` to `f x * g x`. -/
 @[to_additive "`f + g` is the Freiman homomorphism sending `x` to `f x + g x`."]
 instance : Mul (A →*[n] β) :=
   ⟨fun f g =>
@@ -524,9 +524,9 @@ theorem map_prod_eq_map_prod_of_le [FreimanHomClass F A β n] (f : F) {s t : Mul
 #align map_prod_eq_map_prod_of_le map_prod_eq_map_prod_of_le
 #align map_sum_eq_map_sum_of_le map_sum_eq_map_sum_of_le
 
-/-- `α →*[n] β` is naturally included in  `A →*[m] β` for any `m ≤ n`. -/
+/-- `α →*[n] β` is naturally included in `A →*[m] β` for any `m ≤ n`. -/
 @[to_additive AddFreimanHom.toAddFreimanHom
-      "`α →+[n] β` is naturally included in  `α →+[m] β`
+      "`α →+[n] β` is naturally included in `α →+[m] β`
       for any `m ≤ n`"]
 def FreimanHom.toFreimanHom (h : m ≤ n) (f : A →*[n] β) : A →*[m] β where
   toFun := f

Mathlib/Algebra/Hom/Group.lean

@@ -23,7 +23,7 @@ This file defines the bundled structures for monoid and group homomorphisms. Nam
 `MonoidHom` (resp., `AddMonoidHom`) to be bundled homomorphisms between multiplicative (resp.,
 additive) monoids or groups.
 
-We also define coercion to a function, and  usual operations: composition, identity homomorphism,
+We also define coercion to a function, and usual operations: composition, identity homomorphism,
 pointwise multiplication and pointwise inversion.
 
 This file also defines the lesser-used (and notation-less) homomorphism types which are used as

Mathlib/Algebra/Hom/GroupAction.lean

@@ -263,7 +263,7 @@ see also Algebra.Hom.Group -/
 @[coe]
 def _root_.DistribMulActionHomClass.toDistribMulActionHom [DistribMulActionHomClass F M A B]
   (f : F) : A →+[M] B :=
-  { (f : A →+ B),  (f : A →[M] B) with }
+  { (f : A →+ B), (f : A →[M] B) with }
 
 /-- Any type satisfying `SMulHomClass` can be cast into `MulActionHom` via
   `SMulHomClass.toMulActionHom`. -/
@@ -498,7 +498,7 @@ see also Algebra.Hom.Group -/
 @[coe]
 def _root_.MulSemiringActionHomClass.toMulSemiringActionHom [MulSemiringActionHomClass F M R S]
   (f : F) : R →+*[M] S :=
- { (f : R →+* S),  (f : R →+[M] S) with }
+ { (f : R →+* S), (f : R →+[M] S) with }
 
 /-- Any type satisfying `MulSemiringActionHomClass` can be cast into `MulSemiringActionHom` via
   `MulSemiringActionHomClass.toMulSemiringActionHom`. -/

Mathlib/Algebra/Hom/NonUnitalAlg.lean

@@ -169,7 +169,7 @@ theorem congr_fun {f g : A →ₙₐ[R] B} (h : f = g) (x : A) : f x = g x :=
 #align non_unital_alg_hom.congr_fun NonUnitalAlgHom.congr_fun
 
 @[simp]
-theorem coe_mk (f : A → B) (h₁ h₂ h₃ h₄) : ⇑(⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₙₐ[R] B)  = f :=
+theorem coe_mk (f : A → B) (h₁ h₂ h₃ h₄) : ⇑(⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₙₐ[R] B) = f :=
   rfl
 #align non_unital_alg_hom.coe_mk NonUnitalAlgHom.coe_mk
 

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -246,7 +246,7 @@ theorem hom_f_injective {C₁ C₂ : HomologicalComplex V c} :
     Function.Injective fun f : Hom C₁ C₂ => f.f := by aesop_cat
 #align homological_complex.hom_f_injective HomologicalComplex.hom_f_injective
 
-instance (X Y : HomologicalComplex V c) : Zero (X ⟶  Y) :=
+instance (X Y : HomologicalComplex V c) : Zero (X ⟶ Y) :=
   ⟨{ f := fun i => 0}⟩
 
 @[simp]

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -789,7 +789,7 @@ noncomputable def iCyclesNatTrans : cyclesFunctor C ⟶ ShortComplex.π₂ where
 noncomputable def toCyclesNatTrans :
     π₁ ⟶ cyclesFunctor C where
   app S := S.toCycles
-  naturality := fun _ _  φ => (toCycles_naturality φ).symm
+  naturality := fun _ _ φ => (toCycles_naturality φ).symm
 
 end
 

Mathlib/Algebra/Lie/Basic.lean

@@ -288,7 +288,7 @@ instance : Coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) :=
 instance : FunLike (L₁ →ₗ⁅R⁆ L₂) L₁ (fun _ => L₂) :=
   { coe := fun f => f.toFun,
     coe_injective' := fun x y h =>
-      by cases x; cases y; simp at h; simp [h]  }
+      by cases x; cases y; simp at h; simp [h] }
 
 initialize_simps_projections LieHom (toFun → apply)
 
@@ -719,7 +719,7 @@ instance : CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) :=
 instance : FunLike (M →ₗ⁅R, L⁆ N) M (fun _ => N) :=
   { coe := fun f => f.toFun,
     coe_injective' := fun x y h =>
-      by cases x; cases y; simp at h; simp [h]  }
+      by cases x; cases y; simp at h; simp [h] }
 
 @[simp, norm_cast]
 theorem coe_toLinearMap (f : M →ₗ⁅R,L⁆ N) : ((f : M →ₗ[R] N) : M → N) = f :=
@@ -843,7 +843,7 @@ theorem comp_apply (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) :
 #align lie_module_hom.comp_apply LieModuleHom.comp_apply
 
 @[norm_cast, simp]
-theorem coe_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : ⇑(f.comp g)  = f ∘ g :=
+theorem coe_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : ⇑(f.comp g) = f ∘ g :=
   rfl
 #align lie_module_hom.coe_comp LieModuleHom.coe_comp
 

Mathlib/Algebra/Lie/Free.lean

@@ -258,7 +258,7 @@ theorem lift_unique (f : X → L) (g : FreeLieAlgebra R X →ₗ⁅R⁆ L) : g 
 
 @[simp]
 theorem lift_of_apply (f : X → L) (x) : lift R f (of R x) = f x := by
-  rw [← @Function.comp_apply  _ _ _ (lift R f) (of R) x, of_comp_lift]
+  rw [← @Function.comp_apply _ _ _ (lift R f) (of R) x, of_comp_lift]
 #align free_lie_algebra.lift_of_apply FreeLieAlgebra.lift_of_apply
 
 @[simp]

Mathlib/Algebra/Lie/Submodule.lean

@@ -498,7 +498,7 @@ theorem mem_sup (x : M) : x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z =
   rw [← mem_coeSubmodule, sup_coe_toSubmodule, Submodule.mem_sup]; exact Iff.rfl
 #align lie_submodule.mem_sup LieSubmodule.mem_sup
 
-nonrec theorem eq_bot_iff : N = ⊥ ↔ ∀ m : M, m ∈ N → m = 0 := by rw [eq_bot_iff];  exact Iff.rfl
+nonrec theorem eq_bot_iff : N = ⊥ ↔ ∀ m : M, m ∈ N → m = 0 := by rw [eq_bot_iff]; exact Iff.rfl
 #align lie_submodule.eq_bot_iff LieSubmodule.eq_bot_iff
 
 instance subsingleton_of_bot : Subsingleton (LieSubmodule R L ↑(⊥ : LieSubmodule R L M)) := by

Mathlib/Algebra/Module/Injective.lean

@@ -21,7 +21,7 @@ import Mathlib.Data.TypeMax -- Porting note: added for universe issues
 
 * `Module.Injective`: an `R`-module `Q` is injective if and only if every injective `R`-linear
   map descends to a linear map to `Q`, i.e. in the following diagram, if `f` is injective then there
-  is an `R`-linear map `h : Y ⟶  Q` such that `g = h ∘ f`
+  is an `R`-linear map `h : Y ⟶ Q` such that `g = h ∘ f`
   ```
   X --- f ---> Y
   |
@@ -30,7 +30,7 @@ import Mathlib.Data.TypeMax -- Porting note: added for universe issues
   Q
   ```
 * `Module.Baer`: an `R`-module `Q` satisfies Baer's criterion if any `R`-linear map from an
-  `Ideal R` extends to an `R`-linear map `R ⟶  Q`
+  `Ideal R` extends to an `R`-linear map `R ⟶ Q`
 
 ## Main statements