chore: remove some double spaces (#7983)

Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Oct 30, 2023 · 24cd315 · 24cd315
1 parent 0121543
commit 24cd315
Show file tree

Hide file tree

Showing 37 changed files with 54 additions and 54 deletions.
diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean
@@ -86,7 +86,7 @@ end AlgEquivClass
 
 namespace AlgEquiv
 
-universe uR  uA₁ uA₂ uA₃ uA₁' uA₂' uA₃'
+universe uR uA₁ uA₂ uA₃ uA₁' uA₂' uA₃'
 variable {R : Type uR}
 variable {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃}
 variable {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'}

diff --git a/Mathlib/Algebra/Algebra/Opposite.lean b/Mathlib/Algebra/Algebra/Opposite.lean
@@ -153,7 +153,7 @@ theorem toRingEquiv_op (f : A ≃ₐ[R] B) :
     (AlgEquiv.op f).toRingEquiv = RingEquiv.op f.toRingEquiv :=
   rfl
 
-/-- The 'unopposite' of an algebra iso  `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. Inverse to `AlgEquiv.op`. -/
+/-- The 'unopposite' of an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. Inverse to `AlgEquiv.op`. -/
 abbrev unop : (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ A ≃ₐ[R] B := AlgEquiv.op.symm
 
 theorem toAlgHom_unop (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) : f.unop.toAlgHom = AlgHom.unop f.toAlgHom :=

diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean
@@ -80,7 +80,7 @@ section WithDivisionRing
 /-!
 ### Translations Between Computational Functions
 
-Here we  give some basic translations that hold by definition for the computational methods of a
+Here we give some basic translations that hold by definition for the computational methods of a
 continued fraction.
 -/
 

diff --git a/Mathlib/Algebra/GradedMulAction.lean b/Mathlib/Algebra/GradedMulAction.lean
@@ -47,7 +47,7 @@ graded action
 -/
 
 
-variable {ιA ιB ιM  : Type*}
+variable {ιA ιB ιM : Type*}
 
 namespace GradedMonoid
 

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
@@ -80,7 +80,7 @@ def shiftFunctorZero' (n : ℤ) (h : n = 0) :
 /-- The compatibility of the shift functors on `CochainComplex C ℤ` with respect
 to the addition of integers. -/
 @[simps!]
-def shiftFunctorAdd' (n₁ n₂ n₁₂ : ℤ) (h : n₁ + n₂ = n₁₂ ) :
+def shiftFunctorAdd' (n₁ n₂ n₁₂ : ℤ) (h : n₁ + n₂ = n₁₂) :
     shiftFunctor C n₁₂ ≅ shiftFunctor C n₁ ⋙ shiftFunctor C n₂ :=
   NatIso.ofComponents (fun K => Hom.isoOfComponents
     (fun i => K.shiftFunctorObjXIso _ _ _ (by linarith))

diff --git a/Mathlib/Algebra/Homology/ShortComplex/Homology.lean b/Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@@ -1123,7 +1123,7 @@ lemma asIsoHomologyπ_inv_comp_homologyπ (hf : S.f = 0) [S.HasHomology] :
 
 @[reassoc (attr := simp)]
 lemma homologyπ_comp_asIsoHomologyπ_inv (hf : S.f = 0) [S.HasHomology] :
-    S.homologyπ ≫ (S.asIsoHomologyπ hf).inv  = 𝟙 _ := (S.asIsoHomologyπ hf).hom_inv_id
+    S.homologyπ ≫ (S.asIsoHomologyπ hf).inv = 𝟙 _ := (S.asIsoHomologyπ hf).hom_inv_id
 
 /-- The canonical isomorphism `S.homology ≅ S.opcycles` when `S.g = 0`. -/
 @[simps! hom]

diff --git a/Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean b/Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@@ -158,7 +158,7 @@ lemma cyclesMap_add : cyclesMap (φ + φ') = cyclesMap φ + cyclesMap φ' :=
 
 @[simp]
 lemma leftHomologyMap_sub : leftHomologyMap (φ - φ') = leftHomologyMap φ - leftHomologyMap φ' :=
-  leftHomologyMap'_sub  _ _
+  leftHomologyMap'_sub _ _
 
 @[simp]
 lemma cyclesMap_sub : cyclesMap (φ - φ') = cyclesMap φ - cyclesMap φ' :=
@@ -269,7 +269,7 @@ lemma opcyclesMap_add : opcyclesMap (φ + φ') = opcyclesMap φ + opcyclesMap φ
 @[simp]
 lemma rightHomologyMap_sub :
     rightHomologyMap (φ - φ') = rightHomologyMap φ - rightHomologyMap φ' :=
-  rightHomologyMap'_sub  _ _
+  rightHomologyMap'_sub _ _
 
 @[simp]
 lemma opcyclesMap_sub : opcyclesMap (φ - φ') = opcyclesMap φ - opcyclesMap φ' :=
@@ -342,7 +342,7 @@ lemma homologyMap_add : homologyMap (φ + φ')  = homologyMap φ + homologyMap
 
 @[simp]
 lemma homologyMap_sub : homologyMap (φ - φ') = homologyMap φ - homologyMap φ' :=
-  homologyMap'_sub  _ _
+  homologyMap'_sub _ _
 
 end
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean b/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
@@ -53,14 +53,14 @@ open AlgebraicTopology.DoldKan
 `N' : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)` and the inverse
 of the equivalence `ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ)`. -/
 @[simps!, nolint unusedArguments]
-def N  [IsIdempotentComplete C] [HasFiniteCoproducts C] : SimplicialObject C ⥤ ChainComplex C ℕ :=
+def N [IsIdempotentComplete C] [HasFiniteCoproducts C] : SimplicialObject C ⥤ ChainComplex C ℕ :=
   N₁ ⋙ (toKaroubiEquivalence _).inverse
 set_option linter.uppercaseLean3 false in
 #align category_theory.idempotents.dold_kan.N CategoryTheory.Idempotents.DoldKan.N
 
 /-- The functor `Γ` for the equivalence is `Γ'`. -/
 @[simps!, nolint unusedArguments]
-def Γ  [IsIdempotentComplete C] [HasFiniteCoproducts C] : ChainComplex C ℕ ⥤ SimplicialObject C :=
+def Γ [IsIdempotentComplete C] [HasFiniteCoproducts C] : ChainComplex C ℕ ⥤ SimplicialObject C :=
   Γ₀
 #align category_theory.idempotents.dold_kan.Γ CategoryTheory.Idempotents.DoldKan.Γ
 

diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean
@@ -607,7 +607,7 @@ theorem le_op_norm₂ [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL
 
 -- porting note: new theorem
 theorem le_of_op_norm₂_le_of_le [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {x : E} {y : F}
-    {a b c : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) (hy : ‖y‖ ≤ c)  :
+    {a b c : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) (hy : ‖y‖ ≤ c) :
     ‖f x y‖ ≤ a * b * c :=
   (f x).le_of_op_norm_le_of_le (f.le_of_op_norm_le_of_le hf hx) hy
 
@@ -1180,7 +1180,7 @@ class _root_.RegularNormedAlgebra : Prop :=
 
 /-- Every (unital) normed algebra such that `‖1‖ = 1` is a `RegularNormedAlgebra`. -/
 instance _root_.NormedAlgebra.instRegularNormedAlgebra {𝕜 𝕜' : Type*} [NontriviallyNormedField 𝕜]
-    [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : RegularNormedAlgebra 𝕜 𝕜'  where
+    [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : RegularNormedAlgebra 𝕜 𝕜' where
   isometry_mul' := AddMonoidHomClass.isometry_of_norm (mul 𝕜 𝕜') <|
     fun x => le_antisymm (op_norm_mul_apply_le _ _ _) <| by
       convert ratio_le_op_norm ((mul 𝕜 𝕜') x) (1 : 𝕜')

diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
@@ -312,7 +312,7 @@ def preservesColimitOfNatIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [Preser
 /-- Transfer preservation of colimits of shape along a natural isomorphism in the functor. -/
 def preservesColimitsOfShapeOfNatIso {F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfShape J F] :
     PreservesColimitsOfShape J G where
-  preservesColimit {K}  := preservesColimitOfNatIso K h
+  preservesColimit {K} := preservesColimitOfNatIso K h
 #align category_theory.limits.preserves_colimits_of_shape_of_nat_iso CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso
 
 /-- Transfer preservation of colimits along a natural isomorphism in the functor. -/

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
@@ -2029,7 +2029,7 @@ theorem biprod.symmetry (P Q : C) : (biprod.braiding P Q).hom ≫ (biprod.braidi
 
 /-- The associator isomorphism which associates a binary biproduct. -/
 @[simps]
-def biprod.associator (P Q R : C) : (P ⊞ Q) ⊞ R ≅ P ⊞ (Q ⊞ R)  where
+def biprod.associator (P Q R : C) : (P ⊞ Q) ⊞ R ≅ P ⊞ (Q ⊞ R) where
   hom := biprod.lift (biprod.fst ≫ biprod.fst) (biprod.lift (biprod.fst ≫ biprod.snd) biprod.snd)
   inv := biprod.lift (biprod.lift biprod.fst (biprod.snd ≫ biprod.fst)) (biprod.snd ≫ biprod.snd)
 

diff --git a/Mathlib/CategoryTheory/Monoidal/Skeleton.lean b/Mathlib/CategoryTheory/Monoidal/Skeleton.lean
@@ -67,7 +67,7 @@ noncomputable instance instBraidedCategory [BraidedCategory C] : BraidedCategory
   braidedCategoryOfFullyFaithful (Monoidal.fromTransported (skeletonEquivalence C).symm)
 
 /--
-The skeleton of a braided monoidal category can be viewed as a commutative  monoid, where the
+The skeleton of a braided monoidal category can be viewed as a commutative monoid, where the
 multiplication is given by the tensor product, and satisfies the monoid axioms since it is a
 skeleton.
 -/

diff --git a/Mathlib/CategoryTheory/Shift/Induced.lean b/Mathlib/CategoryTheory/Shift/Induced.lean
@@ -118,7 +118,7 @@ noncomputable def induced : HasShift D A :=
       add_zero_hom_app := fun n => by
         have := hF.2
         suffices (Induced.add F s i hF n 0).hom =
-            eqToHom (by rw [add_zero]; rfl) ≫ whiskerLeft (s n) (Induced.zero F s i hF).inv  by
+            eqToHom (by rw [add_zero]; rfl) ≫ whiskerLeft (s n) (Induced.zero F s i hF).inv by
           intro X
           simpa using NatTrans.congr_app this X
         apply ((whiskeringLeft C D D).obj F).map_injective

diff --git a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean b/Mathlib/CategoryTheory/Sites/IsSheafFor.lean
@@ -145,7 +145,7 @@ theorem pullbackCompatible_iff (x : FamilyOfElements P R) [R.hasPullbacks] :
     haveI := hasPullbacks.has_pullbacks hf₁ hf₂
     apply pullback.condition
   · intro t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
-    haveI := hasPullbacks.has_pullbacks  hf₁ hf₂
+    haveI := hasPullbacks.has_pullbacks hf₁ hf₂
     rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t hf₁ hf₂,
       ← FunctorToTypes.map_comp_apply, ← op_comp, pullback.lift_snd]
 #align category_theory.presieve.pullback_compatible_iff CategoryTheory.Presieve.pullbackCompatible_iff

diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
@@ -421,11 +421,11 @@ lemma yonedaEquiv_naturality' {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : y
     (g : X ⟶ Y) : F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f) :=
   yonedaEquiv_naturality _ _
 
-lemma yonedaEquiv_comp {X : C} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda.obj X ⟶ F) (β : F ⟶ G)  :
+lemma yonedaEquiv_comp {X : C} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda.obj X ⟶ F) (β : F ⟶ G) :
     yonedaEquiv (α ≫ β) = β.app _ (yonedaEquiv α) :=
   rfl
 
-lemma yonedaEquiv_comp' {X : Cᵒᵖ} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda.obj (unop X) ⟶ F) (β : F ⟶ G)  :
+lemma yonedaEquiv_comp' {X : Cᵒᵖ} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda.obj (unop X) ⟶ F) (β : F ⟶ G) :
     yonedaEquiv (α ≫ β) = β.app X (yonedaEquiv α) :=
   rfl
 

diff --git a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean
@@ -143,9 +143,9 @@ theorem compress_injOn : Set.InjOn (compress u v) ↑(s.filter (compress u v ·
   intro a ha b hb hab
   rw [mem_coe, mem_filter] at ha hb
   rw [compress] at ha hab
-  split_ifs at ha hab  with has
+  split_ifs at ha hab with has
   · rw [compress] at hb hab
-    split_ifs at hb hab  with hbs
+    split_ifs at hb hab with hbs
     · exact sup_sdiff_injOn u v has hbs hab
     · exact (hb.2 hb.1).elim
   · exact (ha.2 ha.1).elim

diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean
@@ -226,7 +226,7 @@ theorem ofReal_add (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s :=
 #align complex.of_real_add Complex.ofReal_add
 
 @[simp, norm_cast]
-theorem ofReal_bit0 (r : ℝ) : ((bit0 r : ℝ) : ℂ) = bit0 (r : ℂ)  :=
+theorem ofReal_bit0 (r : ℝ) : ((bit0 r : ℝ) : ℂ) = bit0 (r : ℂ) :=
   ext_iff.2 <| by simp [bit0]
 #align complex.of_real_bit0 Complex.ofReal_bit0
 

diff --git a/Mathlib/Data/Finset/LocallyFinite.lean b/Mathlib/Data/Finset/LocallyFinite.lean
@@ -357,12 +357,12 @@ theorem Ico_filter_le_of_left_le {a b c : α} [DecidablePred ((· ≤ ·) c)] (h
 
 theorem Icc_filter_lt_of_lt_right {a b c : α} [DecidablePred (· < c)] (h : b < c) :
     (Icc a b).filter (· < c) = Icc a b :=
-  filter_true_of_mem  fun _ hx => lt_of_le_of_lt (mem_Icc.1 hx).2 h
+  filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Icc.1 hx).2 h
 #align finset.Icc_filter_lt_of_lt_right Finset.Icc_filter_lt_of_lt_right
 
 theorem Ioc_filter_lt_of_lt_right {a b c : α} [DecidablePred (· < c)] (h : b < c) :
     (Ioc a b).filter (· < c) = Ioc a b :=
-  filter_true_of_mem  fun _ hx => lt_of_le_of_lt (mem_Ioc.1 hx).2 h
+  filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Ioc.1 hx).2 h
 #align finset.Ioc_filter_lt_of_lt_right Finset.Ioc_filter_lt_of_lt_right
 
 theorem Iic_filter_lt_of_lt_right {α} [Preorder α] [LocallyFiniteOrderBot α] {a c : α}

diff --git a/Mathlib/FieldTheory/Subfield.lean b/Mathlib/FieldTheory/Subfield.lean
@@ -418,7 +418,7 @@ instance toAlgebra : Algebra s K :=
 #align subfield.to_algebra Subfield.toAlgebra
 
 @[simp]
-theorem coe_subtype : ⇑(s.subtype) = ((↑) : s → K)  :=
+theorem coe_subtype : ⇑(s.subtype) = ((↑) : s → K) :=
   rfl
 #align subfield.coe_subtype Subfield.coe_subtype
 

diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -679,7 +679,7 @@ theorem sum_card_orderOf_eq_card_pow_eq_one [Fintype G] [DecidableEq G] (hn : n
 #align sum_card_order_of_eq_card_pow_eq_one sum_card_orderOf_eq_card_pow_eq_one
 #align sum_card_add_order_of_eq_card_nsmul_eq_zero sum_card_addOrderOf_eq_card_nsmul_eq_zero
 
-@[to_additive ]
+@[to_additive]
 theorem orderOf_le_card_univ [Fintype G] : orderOf x ≤ Fintype.card G :=
   Finset.le_card_of_inj_on_range ((· ^ ·) x) (fun _ _ => Finset.mem_univ _) fun _ hi _ hj =>
     pow_injective_of_lt_orderOf x hi hj

diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean
@@ -71,7 +71,7 @@ abbrev ofHom {X : Type v} [AddCommGroup X] [Module R X]
     (f ≫ g).toIsometry = g.toIsometry.comp f.toIsometry :=
   rfl
 
-@[simp] theorem toIsometry_id {M : QuadraticModuleCat.{v} R}  :
+@[simp] theorem toIsometry_id {M : QuadraticModuleCat.{v} R} :
     Hom.toIsometry (𝟙 M) = Isometry.id _ :=
   rfl
 

diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
@@ -90,12 +90,12 @@ theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) :
     Q.baseChange A (a ⊗ₜ m₂) = Q m₂ • (a * a) :=
   tensorDistrib_tmul _ _ _ _
 
-theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂)  :
+theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
     associated (R := A) (Q.baseChange A) = (associated (R := R) Q).baseChange A := by
   dsimp only [QuadraticForm.baseChange, BilinForm.baseChange]
   rw [associated_tmul (QuadraticForm.sq (R := A)) Q, associated_sq]
 
-theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂)  :
+theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
     polarBilin (Q.baseChange A) = (polarBilin Q).baseChange A := by
   rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul,
     ←LinearMap.map_smul, smul_tmul', ←two_nsmul_associated R, coe_associatedHom, associated_sq,

diff --git a/Mathlib/MeasureTheory/Integral/Layercake.lean b/Mathlib/MeasureTheory/Integral/Layercake.lean
@@ -178,7 +178,7 @@ theorem lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite
   rw [aux₂]
   have mble₀ : MeasurableSet {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := by
     simpa only [mem_univ, Pi.zero_apply, gt_iff_lt, not_lt, ge_iff_le, true_and] using
-      measurableSet_region_between_oc measurable_zero f_mble  MeasurableSet.univ
+      measurableSet_region_between_oc measurable_zero f_mble MeasurableSet.univ
   exact (ENNReal.measurable_ofReal.comp (g_mble.comp measurable_snd)).aemeasurable.indicator₀
     mble₀.nullMeasurableSet
 #align measure_theory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite

diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
@@ -732,12 +732,12 @@ lemma map_apply_of_aemeasurable (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemb
     ν.map f A = ν (f ⁻¹' A) :=
   map_apply_of_aemeasurable ν f_mble.aemeasurable A_mble
 
-@[simp] lemma map_add {f : Ω → Ω'} (f_mble : Measurable f) (ν₁ ν₂ : FiniteMeasure Ω)  :
+@[simp] lemma map_add {f : Ω → Ω'} (f_mble : Measurable f) (ν₁ ν₂ : FiniteMeasure Ω) :
     (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f := by
   ext s s_mble
   simp [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_add]
 
-@[simp] lemma map_smul {f : Ω → Ω'} (f_mble : Measurable f) (c : ℝ≥0) (ν : FiniteMeasure Ω)  :
+@[simp] lemma map_smul {f : Ω → Ω'} (f_mble : Measurable f) (c : ℝ≥0) (ν : FiniteMeasure Ω) :
     (c • ν).map f = c • (ν.map f) := by
   ext s s_mble
   simp [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_smul]

diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -263,7 +263,7 @@ theorem log_le_of_logEmbedding_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r) (h :
     refine (le_trans ?_ hyp).trans ?_
     · rw [← hw]
       exact tool _ (abs_nonneg _)
-    · refine (sum_le_card_nsmul univ _  _
+    · refine (sum_le_card_nsmul univ _ _
         (fun w _ => logEmbedding_component_le hr h w)).trans ?_
       rw [nsmul_eq_mul]
       refine mul_le_mul ?_ le_rfl hr (Fintype.card (InfinitePlace K)).cast_nonneg
@@ -400,9 +400,9 @@ theorem seq_norm_le (n : ℕ) :
       exact (seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2
 
 /-- Construct a unit associated to the place `w₁`. The family, for `w₁ ≠ w₀`, formed by the
-image by the `logEmbedding` of these units  is `ℝ`-linearly independent, see
+image by the `logEmbedding` of these units is `ℝ`-linearly independent, see
 `unitLattice_span_eq_top`. -/
-theorem exists_unit (w₁ : InfinitePlace K ) :
+theorem exists_unit (w₁ : InfinitePlace K) :
     ∃ u : (𝓞 K)ˣ, ∀ w : InfinitePlace K, w ≠ w₁ → Real.log (w u) < 0 := by
   obtain ⟨B, hB⟩ : ∃ B : ℕ, minkowskiBound K < (convexBodyLtFactor K) * B := by
     simp_rw [mul_comm]
@@ -427,7 +427,7 @@ theorem exists_unit (w₁ : InfinitePlace K ) :
     (fun n => ?_) ?_
   · rw [Set.mem_setOf_eq, Ideal.absNorm_span_singleton]
     refine ⟨?_, seq_norm_le K w₁ hB n⟩
-    exact  Nat.one_le_iff_ne_zero.mpr (Int.natAbs_ne_zero.mpr (seq_norm_ne_zero K w₁ hB n))
+    exact Nat.one_le_iff_ne_zero.mpr (Int.natAbs_ne_zero.mpr (seq_norm_ne_zero K w₁ hB n))
   · rw [show { I : Ideal (𝓞 K) | 1 ≤ Ideal.absNorm I ∧ Ideal.absNorm I ≤ B } =
           (⋃ n ∈ Set.Icc 1 B, { I : Ideal (𝓞 K) | Ideal.absNorm I = n }) by ext; simp]
     exact Set.Finite.biUnion (Set.finite_Icc _ _) (fun n hn => Ideal.finite_setOf_absNorm_eq hn.1)

diff --git a/Mathlib/Order/Filter/Germ.lean b/Mathlib/Order/Filter/Germ.lean
@@ -829,7 +829,7 @@ instance orderedCommMonoid [OrderedCommMonoid β] : OrderedCommMonoid (Germ l β
         inductionOn h fun _h => H.mono fun _x H => mul_le_mul_left' H _ }
 
 @[to_additive]
-instance orderedCancelCommMonoid [OrderedCancelCommMonoid β]  :
+instance orderedCancelCommMonoid [OrderedCancelCommMonoid β] :
     OrderedCancelCommMonoid (Germ l β) :=
   { Germ.orderedCommMonoid with
     le_of_mul_le_mul_left := fun f g h =>

diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean
@@ -164,11 +164,11 @@ lemma iIndep_iff (m : ι → MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Meas
       μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) := by
   simp only [iIndep_iff_iIndepSets, iIndepSets_iff]; rfl
 
-lemma Indep_iff_IndepSets (m₁ m₂ : MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω ) :
+lemma Indep_iff_IndepSets (m₁ m₂ : MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω) :
     Indep m₁ m₂ μ ↔ IndepSets {s | MeasurableSet[m₁] s} {s | MeasurableSet[m₂] s} μ := by
   simp only [Indep, IndepSets, kernel.Indep]
 
-lemma Indep_iff (m₁ m₂ : MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω ) :
+lemma Indep_iff (m₁ m₂ : MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω) :
     Indep m₁ m₂ μ
       ↔ ∀ t1 t2, MeasurableSet[m₁] t1 → MeasurableSet[m₂] t2 → μ (t1 ∩ t2) = μ t1 * μ t2 := by
   rw [Indep_iff_IndepSets, IndepSets_iff]; rfl

diff --git a/Mathlib/Tactic/MkIffOfInductiveProp.lean b/Mathlib/Tactic/MkIffOfInductiveProp.lean
@@ -131,7 +131,7 @@ structure Shape : Type where
 while proving the iff theorem, and a proposition representing the constructor.
 -/
 def constrToProp (univs : List Level) (params : List Expr) (idxs : List Expr) (c : Name) :
-    MetaM (Shape × Expr)  :=
+    MetaM (Shape × Expr) :=
 do let type := (← getConstInfo c).instantiateTypeLevelParams univs
    let type' ← Meta.forallBoundedTelescope type (params.length) fun fvars ty ↦ do
      pure $ ty.replaceFVars fvars params.toArray

diff --git a/Mathlib/Tactic/NormNum/OfScientific.lean b/Mathlib/Tactic/NormNum/OfScientific.lean
@@ -50,7 +50,7 @@ to rat casts if the scientific notation is inherited from the one for rationals.
   haveI' : $e =Q OfScientific.ofScientific $m $b $exp := ⟨⟩
   haveI' lh : @OfScientific.ofScientific $α $σα =Q (fun m s e ↦ (Rat.ofScientific m s e : $α)) := ⟨⟩
   match b with
-  | ~q(true)  =>
+  | ~q(true) =>
     let rme ← derive (q(mkRat $m (10 ^ $exp)) : Q($α))
     let some ⟨q, n, d, p⟩ := rme.toRat' dα | failure
     return .isRat' dα q n d q(isRat_ofScientific_of_true $σα $lh $p)

diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean
@@ -462,7 +462,7 @@ def expand (e : Expr) : MetaM Expr := do
       trace[to_additive_detail] "expanded {e} to {e'}"
       return .continue e'
   if e != e₂ then
-    trace[to_additive_detail] "expand:\nBefore: {e}\nAfter:  {e₂}"
+    trace[to_additive_detail] "expand:\nBefore: {e}\nAfter: {e₂}"
   return e₂
 
 /-- Reorder pi-binders. See doc of `reorderAttr` for the interpretation of the argument -/
@@ -951,7 +951,7 @@ partial def applyAttributes (stx : Syntax) (rawAttrs : Array Syntax) (thisAttr s
     let env ← getEnv
     match getAttributeImpl env attr.name with
     | Except.error errMsg => throwError errMsg
-    | Except.ok attrImpl  =>
+    | Except.ok attrImpl =>
       let runAttr := do
         attrImpl.add src attr.stx attr.kind
         attrImpl.add tgt attr.stx attr.kind

diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean
@@ -91,7 +91,7 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
     else
       s!"_ {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {newRhsStr} := by sorry\n" ++
       s!"{spc}_ {relStr} {rhsStr} := by sorry"
-  | false, true  =>
+  | false, true =>
     if params.isFirst then
       s!"{lhsStr} {relStr} {newRhsStr} := by sorry\n{spc}_ {relStr} {rhsStr} := by sorry"
     else