[Merged by Bors] - feat: a linter to enforce formatting

Mathlib.lean

@@ -5693,6 +5693,7 @@ import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.LinearCombination'
 import Mathlib.Tactic.LinearCombination.Lemmas
 import Mathlib.Tactic.Linter
+import Mathlib.Tactic.Linter.CommandStart
 import Mathlib.Tactic.Linter.DeprecatedModule
 import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
 import Mathlib.Tactic.Linter.DirectoryDependency

Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

@@ -76,7 +76,7 @@ theorem Cover.iUnion_range {X : Scheme.{u}} (𝒰 : X.Cover P) :
 lemma Cover.exists_eq (𝒰 : X.Cover P) (x : X) : ∃ i y, (𝒰.map i).base y = x :=
   ⟨_, 𝒰.covers x⟩
 
-instance Cover.nonempty_of_nonempty  [Nonempty X] (𝒰 : X.Cover P) : Nonempty 𝒰.J :=
+instance Cover.nonempty_of_nonempty [Nonempty X] (𝒰 : X.Cover P) : Nonempty 𝒰.J :=
   Nonempty.map 𝒰.f ‹_›
 
 /-- Given a family of schemes with morphisms to `X` satisfying `P` that jointly

Mathlib/Analysis/NormedSpace/Alternating/Basic.lean

@@ -286,7 +286,7 @@ section
   NNReal.eq <| norm_ofSubsingleton i f
 
 /-- `ContinuousAlternatingMap.ofSubsingleton` as a linear isometry. -/
-@[simps (config := {simpRhs := true})]
+@[simps (config := { simpRhs := true })]
 def ofSubsingletonLIE [Subsingleton ι] (i : ι) : (E →L[𝕜] F) ≃ₗᵢ[𝕜] (E [⋀^ι]→L[𝕜] F) where
   __ := ofSubsingleton 𝕜 E F i
   map_add' _ _ := rfl
@@ -406,7 +406,7 @@ def compContinuousAlternatingMapCLM : (F →L[𝕜] G) →L[𝕜] (E [⋀^ι]→
     simpa using f.norm_compContinuousAlternatingMap_le g
 
 /-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled continuous linear equiv. -/
-@[simps (config := {simpRhs := true}) apply]
+@[simps (config := { simpRhs := true }) apply]
 def _root_.ContinuousLinearEquiv.continuousAlternatingMapCongrRight (g : F ≃L[𝕜] G) :
     (E [⋀^ι]→L[𝕜] F) ≃L[𝕜] (E [⋀^ι]→L[𝕜] G) where
   __ := g.continuousAlternatingMapCongrRightEquiv

Mathlib/Data/Fin/Tuple/Embedding.lean

@@ -116,7 +116,7 @@ def twoEmbeddingEquiv : (Fin 2 ↪ α) ≃ { (a, b) : α × α | a ≠ b } where
   right_inv := fun ⟨⟨a, b⟩, h⟩ ↦ by simp
 
 /-- Two distinct elements of `α` give an embedding `Fin 2 ↪ α`. -/
-def embFinTwo {a b: α} (h : a ≠ b) : Fin 2 ↪ α :=
+def embFinTwo {a b : α} (h : a ≠ b) : Fin 2 ↪ α :=
   twoEmbeddingEquiv.invFun ⟨(a, b), h⟩
 
 theorem embFinTwo_apply_zero {a b : α} (h : a ≠ b) :
@@ -126,4 +126,3 @@ theorem embFinTwo_apply_one {a b : α} (h : a ≠ b) :
     embFinTwo h 1 = b := rfl
 
 end Function.Embedding
-

Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

@@ -209,7 +209,7 @@ theorem isPretransitive_of_is_two_pretransitive
       exact ⟨g, h⟩
 
 /-- A `2`-transitive action is primitive. -/
-@[to_additive "A `2`-transitive additive action is primitive." ]
+@[to_additive "A `2`-transitive additive action is primitive."]
 theorem isPreprimitive_of_is_two_pretransitive
     (h2 : IsMultiplyPretransitive G α 2) : IsPreprimitive G α := by
   have : IsPretransitive G α := isPretransitive_of_is_two_pretransitive

Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

@@ -128,7 +128,7 @@ instance isTotallyReal_iSup {ι : Type*} {k : ι → Subfield K} [∀ i, IsTotal
     IsTotallyReal (⨆ i, k i : Subfield K) := by
   simp_all [isTotallyReal_iff_le_maximalRealSubfield]
 
- end maximalRealSubfield
+end maximalRealSubfield
 
 end TotallyRealField
 

Mathlib/Tactic.lean

@@ -142,6 +142,7 @@ import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.LinearCombination'
 import Mathlib.Tactic.LinearCombination.Lemmas
 import Mathlib.Tactic.Linter
+import Mathlib.Tactic.Linter.CommandStart
 import Mathlib.Tactic.Linter.DeprecatedModule
 import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
 import Mathlib.Tactic.Linter.DirectoryDependency

Mathlib/Tactic/Linter.lean

@@ -8,6 +8,8 @@ This file is ignored by `shake`:
 * it is in `ignoreImport`, meaning that where it is imported, it is considered necessary.
 -/
 
+import Mathlib.Tactic.Linter.CommandStart
+import Mathlib.Tactic.Linter.FlexibleLinter
 import Mathlib.Tactic.Linter.DeprecatedModule
 import Mathlib.Tactic.Linter.HaveLetLinter
 import Mathlib.Tactic.Linter.MinImports