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

Mathlib.lean

@@ -5790,6 +5790,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/Algebra/Group/Int/Defs.lean

@@ -55,6 +55,8 @@ These also prevent non-computable instances like `Int.instNormedCommRing` being
 these instances non-computably.
 -/
 
+set_option linter.style.commandStart false
+
 instance instAddCommMonoid    : AddCommMonoid ℤ    := by infer_instance
 instance instAddMonoid        : AddMonoid ℤ        := by infer_instance
 instance instMonoid           : Monoid ℤ           := by infer_instance
@@ -64,6 +66,8 @@ instance instAddGroup         : AddGroup ℤ         := by infer_instance
 instance instAddCommSemigroup : AddCommSemigroup ℤ := by infer_instance
 instance instAddSemigroup     : AddSemigroup ℤ     := by infer_instance
 
+set_option linter.style.commandStart true
+
 end Int
 
 -- TODO: Do we really need this lemma? This is just `smul_eq_mul`

Mathlib/Algebra/Group/Nat/Defs.lean

@@ -52,6 +52,8 @@ instance instCommMonoid : CommMonoid ℕ where
 These also prevent non-computable instances being used to construct these instances non-computably.
 -/
 
+set_option linter.style.commandStart false
+
 instance instAddCommMonoid    : AddCommMonoid ℕ    := by infer_instance
 instance instAddMonoid        : AddMonoid ℕ        := by infer_instance
 instance instMonoid           : Monoid ℕ           := by infer_instance
@@ -61,6 +63,8 @@ instance instAddCommSemigroup : AddCommSemigroup ℕ := by infer_instance
 instance instAddSemigroup     : AddSemigroup ℕ     := by infer_instance
 instance instOne : One ℕ := inferInstance
 
+set_option linter.style.commandStart true
+
 /-! ### Miscellaneous lemmas -/
 
 -- We set the simp priority slightly lower than default; later more general lemmas will replace it.

Mathlib/Algebra/Ring/Int/Defs.lean

@@ -73,9 +73,13 @@ These also prevent non-computable instances like `Int.normedCommRing` being used
 these instances non-computably.
 -/
 
+set_option linter.style.commandStart false
+
 instance instCommSemiring : CommSemiring ℤ := inferInstance
 instance instSemiring     : Semiring ℤ     := inferInstance
 instance instRing         : Ring ℤ         := inferInstance
 instance instDistrib      : Distrib ℤ      := inferInstance
 
+set_option linter.style.commandStart true
+
 end Int

Mathlib/Data/FunLike/Basic.lean

@@ -134,7 +134,7 @@ For non-dependent functions you can also use the abbreviation `FunLike`.
 This typeclass is used in the definition of the homomorphism typeclasses,
 such as `ZeroHomClass`, `MulHomClass`, `MonoidHomClass`, ....
 -/
-@[notation_class * toFun Simps.findCoercionArgs]
+@[notation_class* toFun Simps.findCoercionArgs]
 class DFunLike (F : Sort*) (α : outParam (Sort*)) (β : outParam <| α → Sort*) where
   /-- The coercion from `F` to a function. -/
   coe : F → ∀ a : α, β a

Mathlib/Data/SetLike/Basic.lean

@@ -92,7 +92,7 @@ Then you should *not* repeat the `outParam` declaration so `SetLike` will supply
 This ensures your subclass will not have issues with synthesis of the `[Mul M]` parameter starting
 before the value of `M` is known.
 -/
-@[notation_class * carrier Simps.findCoercionArgs]
+@[notation_class* carrier Simps.findCoercionArgs]
 class SetLike (A : Type*) (B : outParam Type*) where
   /-- The coercion from a term of a `SetLike` to its corresponding `Set`. -/
   protected coe : A → Set B

Mathlib/Init.lean

@@ -1,4 +1,5 @@
 import Lean.Linter.Sets -- for the definition of linter sets
+import Mathlib.Tactic.Linter.CommandStart
 import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
 import Mathlib.Tactic.Linter.DirectoryDependency
 import Mathlib.Tactic.Linter.DocPrime
@@ -60,10 +61,11 @@ register_linter_set linter.mathlibStandardSet :=
   linter.allScriptsDocumented
   linter.checkInitImports
 
+  linter.hashCommand
   linter.oldObtain
   linter.style.cases
   linter.style.refine
-  linter.hashCommand
+  linter.style.commandStart
   linter.style.cdot
   linter.style.docString
   linter.style.dollarSyntax

Mathlib/RingTheory/Polynomial/ContentIdeal.lean

@@ -176,7 +176,7 @@ theorem mul_contentIdeal_le_radical_contentIdeal_mul :
     contentIdeal_eq_bot_iff, mul_eq_zero] using hpq
 
 theorem contentIdeal_mul_eq_top_of_contentIdeal_eq_top (hp : p.contentIdeal = ⊤)
-    (hq : q.contentIdeal = ⊤)  : (p * q).contentIdeal = ⊤ := by
+    (hq : q.contentIdeal = ⊤) : (p * q).contentIdeal = ⊤ := by
   rw [← Ideal.radical_eq_top]
   apply le_antisymm le_top
   calc

Mathlib/Tactic.lean

@@ -145,6 +145,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