diff --git a/Mathlib.lean b/Mathlib.lean
index 07e2289cd98d40..429322c6d93b27 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Algebra/Group/Int/Defs.lean b/Mathlib/Algebra/Group/Int/Defs.lean
index 2682e53ec3e2e5..673e73c94145d8 100644
--- a/Mathlib/Algebra/Group/Int/Defs.lean
+++ b/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`
diff --git a/Mathlib/Algebra/Group/Nat/Defs.lean b/Mathlib/Algebra/Group/Nat/Defs.lean
index 545c0cebc335da..a7dad9eea13cce 100644
--- a/Mathlib/Algebra/Group/Nat/Defs.lean
+++ b/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.
diff --git a/Mathlib/Algebra/Ring/Int/Defs.lean b/Mathlib/Algebra/Ring/Int/Defs.lean
index 49a1911a35d593..845d17e17bfdba 100644
--- a/Mathlib/Algebra/Ring/Int/Defs.lean
+++ b/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
diff --git a/Mathlib/Data/FunLike/Basic.lean b/Mathlib/Data/FunLike/Basic.lean
index d5e5be09fb3dff..9606eb59f0b92b 100644
--- a/Mathlib/Data/FunLike/Basic.lean
+++ b/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
diff --git a/Mathlib/Data/SetLike/Basic.lean b/Mathlib/Data/SetLike/Basic.lean
index 5a9ab36faff756..854a5cddffb9a9 100644
--- a/Mathlib/Data/SetLike/Basic.lean
+++ b/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
diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
index 7aee07352925c7..d4ebd0197674ac 100644
--- a/Mathlib/Init.lean
+++ 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
diff --git a/Mathlib/RingTheory/Polynomial/ContentIdeal.lean b/Mathlib/RingTheory/Polynomial/ContentIdeal.lean
index 2b36167249b4fc..2ee28c45f7d864 100644
--- a/Mathlib/RingTheory/Polynomial/ContentIdeal.lean
+++ b/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
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 9d96e701366155..101a59131757cf 100644
--- a/Mathlib/Tactic.lean
+++ b/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
diff --git a/Mathlib/Tactic/Linter/CommandStart.lean b/Mathlib/Tactic/Linter/CommandStart.lean
new file mode 100644
index 00000000000000..c981cc7e6cedbe
--- /dev/null
+++ b/Mathlib/Tactic/Linter/CommandStart.lean
@@ -0,0 +1,362 @@
+/-
+Copyright (c) 2025 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+
+import Mathlib.Tactic.Linter.Header
+
+/-!
+#  The `commandStart` linter
+
+The `commandStart` linter emits a warning if
+* either a command does not start at the beginning of a line;
+* or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.
+-/
+
+open Lean Elab Command Linter
+
+namespace Mathlib.Linter
+
+/--
+The `commandStart` linter emits a warning if
+* either a command does not start at the beginning of a line;
+* or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.
+
+In practice, this makes sure that the spacing in a typical declaration looks like
+```lean
+example (a : Nat) {R : Type} [Add R] : <not linted part>
+```
+as opposed to
+```lean
+example (a: Nat) {R:Type}  [Add  R] : <not linted part>
+```
+-/
+register_option linter.style.commandStart : Bool := {
+  defValue := false
+  descr := "enable the commandStart linter"
+}
+
+/-- If the `linter.style.commandStart.verbose` option is `true`, the `commandStart` linter
+reports some helpful diagnostic information. -/
+register_option linter.style.commandStart.verbose : Bool := {
+  defValue := false
+  descr := "enable the commandStart linter"
+}
+
+/--
+`CommandStart.endPos stx` returns the position up until the `commandStart` linter checks the
+formatting.
+This is every declaration until the type-specification, if there is one, or the value,
+as well as all `variable` commands.
+-/
+def CommandStart.endPos (stx : Syntax) : Option String.Pos :=
+  if let some cmd := stx.find? (·.isOfKind ``Parser.Command.declaration) then
+    if let some ind := cmd.find? (·.isOfKind ``Parser.Command.inductive) then
+      match ind.find? (·.isOfKind ``Parser.Command.optDeclSig) with
+      | none => dbg_trace "unreachable?"; none
+      | some sig => sig.getTailPos?
+    else
+    match cmd.find? (·.isOfKind ``Parser.Term.typeSpec) with
+      | some s => s.getPos?
+      | none => match cmd.find? (·.isOfKind ``Parser.Command.declValSimple) with
+        | some s => s.getPos?
+        | none => none
+  else if stx.isOfKind ``Parser.Command.variable || stx.isOfKind ``Parser.Command.omit then
+    stx.getTailPos?
+  else none
+
+/--
+A `FormatError` is the main structure tracking how some surface syntax differs from its
+pretty-printed version.
+
+In case of deviations, it contains the deviation's location within an ambient string.
+-/
+-- Some of the information contained in `FormatError` is redundant, however, it is useful to convert
+-- between the `String.pos` and `String` length conveniently.
+structure FormatError where
+  /-- The distance to the end of the source string, as number of characters -/
+  srcNat : Nat
+  /-- The distance to the end of the source string, as number of string positions -/
+  srcEndPos : String.Pos
+  /-- The distance to the end of the formatted string, as number of characters -/
+  fmtPos : Nat
+  /-- The kind of formatting error. For example: `extra space`, `remove line break` or
+  `missing space`.
+
+  Strings starting with `Oh no` indicate an internal error.
+  -/
+  msg : String
+  /-- The length of the mismatch, as number of characters. -/
+  length : Nat
+  /-- The starting position of the mismatch, as a `String.pos`. -/
+  srcStartPos : String.Pos
+  deriving Inhabited
+
+instance : ToString FormatError where
+  toString f :=
+    s!"srcNat: {f.srcNat}, srcPos: {f.srcEndPos}, fmtPos: {f.fmtPos}, \
+      msg: {f.msg}, length: {f.length}\n"
+
+/--
+Produces a `FormatError` from the input data.  It expects
+* `ls` to be a "user-typed" string;
+* `ms` to be a "pretty-printed" string;
+* `msg` to be a custom error message, such as `extra space` or `remove line break`;
+* `length` (optional with default `1`), how many characters the error spans.
+
+In particular, it extracts the position information within the string, both as number of characters
+and as `String.Pos`.
+-/
+def mkFormatError (ls ms : String) (msg : String) (length : Nat := 1) : FormatError where
+  srcNat := ls.length
+  srcEndPos := ls.endPos
+  fmtPos := ms.length
+  msg := msg
+  length := length
+  srcStartPos := ls.endPos
+
+/--
+Add a new `FormatError` `f` to the array `fs`, trying, as much as possible, to merge the new
+`FormatError` with the last entry of `fs`.
+-/
+def pushFormatError (fs : Array FormatError) (f : FormatError) : Array FormatError :=
+  -- If there are no errors already, we simply add the new one.
+  if fs.isEmpty then fs.push f else
+  let back := fs.back!
+  -- If the latest error is of a different kind than the new one, we simply add the new one.
+  if back.msg != f.msg || back.srcNat - back.length != f.srcNat then fs.push f else
+  -- Otherwise, we are adding a further error of the same kind and we therefore merge the two.
+  fs.pop.push {back with length := back.length + f.length, srcStartPos := f.srcEndPos}
+
+/--
+Scan the two input strings `L` and `M`, assuming `M` is the pretty-printed version of `L`.
+This almost means that `L` and `M` only differ in whitespace.
+
+While scanning the two strings, accumulate any discrepancies --- with some heuristics to avoid
+flagging some line-breaking changes.
+(The pretty-printer does not always produce desirably formatted code.)
+-/
+partial
+def parallelScanAux (as : Array FormatError) (L M : String) : Array FormatError :=
+  if M.trim.isEmpty then as else
+  -- We try as hard as possible to scan the strings one character at a time.
+  -- However, single line comments introduced with `--` pretty-print differently than `/--`.
+  -- So, we first look ahead for `/--`: the linter will later ignore doc-strings, so it does not
+  -- matter too much what we do here and we simply drop `/--` from the original string and the
+  -- pretty-printed one, before continuing.
+  -- Next, if we already dealt with `/--`, finding a `--` means that this is a single line comment
+  -- (or possibly a comment embedded in a doc-string, which is ok, since we eventually discard
+  -- doc-strings).  In this case, we drop everything until the following line break in the
+  -- original syntax, and for the same amount of characters in the pretty-printed one, since the
+  -- pretty-printer *erases* the line break at the end of a single line comment.
+  if L.take 3 == "/--" && M.take 3 == "/--" then
+    parallelScanAux as (L.drop 3) (M.drop 3) else
+  if L.take 2 == "--" then
+    let newL := L.dropWhile (· != '\n')
+    let diff := L.length - newL.length
+    -- Assumption: if `L` contains an embedded inline comment, so does `M`
+    -- (modulo additional whitespace).
+    -- This holds because we call this function with `M` being a pretty-printed version of `L`.
+    -- If the pretty-printer changes in the future, this code may need to be adjusted.
+    let newM := M.dropWhile (· != '-') |>.drop diff
+    parallelScanAux as newL.trimLeft newM.trimLeft else
+  if L.take 2 == "-/" then
+    let newL := L.drop 2 |>.trimLeft
+    let newM := M.drop 2 |>.trimLeft
+    parallelScanAux as newL newM else
+  let ls := L.drop 1
+  let ms := M.drop 1
+  match L.get 0, M.get 0 with
+  | ' ', m =>
+    if m.isWhitespace then
+      parallelScanAux as ls ms.trimLeft
+    else
+      parallelScanAux (pushFormatError as (mkFormatError L M "extra space")) ls M
+  | '\n', m =>
+    if m.isWhitespace then
+      parallelScanAux as ls.trimLeft ms.trimLeft
+    else
+      parallelScanAux (pushFormatError as (mkFormatError L M "remove line break")) ls.trimLeft M
+  | l, m => -- `l` is not whitespace
+    if l == m then
+      parallelScanAux as ls ms
+    else
+      if m.isWhitespace then
+        parallelScanAux (pushFormatError as (mkFormatError L M "missing space")) L ms.trimLeft
+    else
+      -- If this code is reached, then `L` and `M` differ by something other than whitespace.
+      -- This should not happen in practice.
+      pushFormatError as (mkFormatError ls ms "Oh no! (Unreachable?)")
+
+@[inherit_doc parallelScanAux]
+def parallelScan (src fmt : String) : Array FormatError :=
+  parallelScanAux ∅ src fmt
+
+namespace Style.CommandStart
+
+/--
+`unlintedNodes` contains the `SyntaxNodeKind`s for which there is no clear formatting preference:
+if they appear in surface syntax, the linter will ignore formatting.
+
+Currently, the unlined nodes are mostly related to `Subtype`, `Set` and `Finset` notation and
+list notation.
+-/
+abbrev unlintedNodes := #[
+  -- # set-like notations, have extra spaces around the braces `{` `}`
+
+  -- subtype, the pretty-printer prefers `{ a // b }`
+  ``«term{_:_//_}»,
+  -- set notation, the pretty-printer prefers `{ a | b }`
+  `«term{_}»,
+  -- empty set, the pretty-printer prefers `{ }`
+  ``«term{}»,
+  -- set builder notation, the pretty-printer prefers `{ a : X | p a }`
+  `Mathlib.Meta.setBuilder,
+
+  -- # misc exceptions
+
+  -- We ignore literal strings.
+  `str,
+
+  -- list notation, the pretty-printer prefers `a :: b`
+  ``«term_::_»,
+
+  -- negation, the pretty-printer prefers `¬a`
+  ``«term¬_»,
+
+  -- declaration name, avoids dealing with guillemets pairs `«»`
+  ``Parser.Command.declId,
+
+  `Mathlib.Tactic.superscriptTerm, `Mathlib.Tactic.subscript,
+
+  -- notation for `Bundle.TotalSpace.proj`, the total space of a bundle
+  -- the pretty-printer prefers `π FE` over `π F E` (which we want)
+  `Bundle.termπ__,
+
+  -- notation for `Finset.slice`, the pretty-printer prefers `𝒜 #r` over `𝒜 # r` (mathlib style)
+  `Finset.«term_#_»,
+
+  -- The docString linter already takes care of formatting doc-strings.
+  ``Parser.Command.docComment,
+
+  -- The pretty-printer adds a space between the backticks and the actual name.
+  ``Parser.Term.doubleQuotedName,
+  ]
+
+/--
+Given an array `a` of `SyntaxNodeKind`s, we accumulate the ranges of the syntax nodes of the
+input syntax whose kind is in `a`.
+
+The linter uses this information to avoid emitting a warning for nodes with kind contained in
+`unlintedNodes`.
+-/
+def getUnlintedRanges (a : Array SyntaxNodeKind) :
+    Std.HashSet String.Range → Syntax → Std.HashSet String.Range
+  | curr, s@(.node _ kind args) =>
+    let new := args.foldl (init := curr) (·.union <| getUnlintedRanges a curr ·)
+    if a.contains kind then
+      new.insert (s.getRange?.getD default)
+    else
+      new
+  -- We special case `where` statements, since they may be followed by an indented doc-string.
+  | curr, .atom info "where" =>
+    if let some trail := info.getRangeWithTrailing? then
+      curr.insert trail
+    else
+      curr
+  | curr, _ => curr
+
+/-- Given a `HashSet` of `String.Range`s `rgs` and a further `String.Range` `rg`,
+`isOutside rgs rg` returns `false` if and only if `rgs` contains a range that completely contains
+`rg`.
+
+The linter uses this to figure out which nodes should be ignored.
+-/
+def isOutside (rgs : Std.HashSet String.Range) (rg : String.Range) : Bool :=
+  rgs.all fun {start := a, stop := b} ↦ !(a ≤ rg.start && rg.stop ≤ b)
+
+/-- `mkWindow orig start ctx` extracts from `orig` a string that starts at the first
+non-whitespace character before `start`, then expands to cover `ctx` more characters
+and continues still until the first non-whitespace character.
+
+In essence, it extracts the substring of `orig` that begins at `start`, continues for `ctx`
+characters plus expands left and right until it encounters the first whitespace character,
+to avoid cutting into "words".
+
+*Note*. `start` is the number of characters *from the right* where our focus is!
+-/
+def mkWindow (orig : String) (start ctx : Nat) : String :=
+  let head := orig.dropRight (start + 1) -- `orig`, up to one character before the discrepancy
+  let middle := orig.takeRight (start + 1)
+  let headCtx := head.takeRightWhile (!·.isWhitespace)
+  let tail := middle.drop ctx |>.takeWhile (!·.isWhitespace)
+  s!"{headCtx}{middle.take ctx}{tail}"
+
+@[inherit_doc Mathlib.Linter.linter.style.commandStart]
+def commandStartLinter : Linter where run := withSetOptionIn fun stx ↦ do
+  unless Linter.getLinterValue linter.style.commandStart (← getLinterOptions) do
+    return
+  if (← get).messages.hasErrors then
+    return
+  if stx.find? (·.isOfKind ``runCmd) |>.isSome then
+    return
+  -- If a command does not start on the first column, emit a warning.
+  if let some pos := stx.getPos? then
+    let colStart := ((← getFileMap).toPosition pos).column
+    if colStart ≠ 0 then
+      Linter.logLint linter.style.commandStart stx
+        m!"'{stx}' starts on column {colStart}, \
+          but all commands should start at the beginning of the line."
+  -- We skip `macro_rules`, since they cause parsing issues.
+  if stx.find? (·.isOfKind `Lean.Parser.Command.macro_rules) |>.isSome then
+    return
+  let some upTo := CommandStart.endPos stx | return
+
+  let fmt : Option Format := ←
+      try
+        liftCoreM <| PrettyPrinter.ppCategory `command stx
+      catch _ =>
+        Linter.logLintIf linter.style.commandStart.verbose (stx.getHead?.getD stx)
+          m!"The `commandStart` linter had some parsing issues: \
+            feel free to silence it and report this error!"
+        return none
+  if let some fmt := fmt then
+    let st := fmt.pretty
+    let origSubstring := stx.getSubstring?.getD default
+    let orig := origSubstring.toString
+
+    let scan := parallelScan orig st
+
+    let docStringEnd := stx.find? (·.isOfKind ``Parser.Command.docComment) |>.getD default
+    let docStringEnd := docStringEnd.getTailPos? |>.getD default
+    let forbidden := getUnlintedRanges unlintedNodes ∅ stx
+    for s in scan do
+      let center := origSubstring.stopPos - s.srcEndPos
+      let rg : String.Range := ⟨center, center + s.srcEndPos - s.srcStartPos + ⟨1⟩⟩
+      if s.msg.startsWith "Oh no" then
+        Linter.logLintIf linter.style.commandStart.verbose (.ofRange rg)
+          m!"This should not have happened: please report this issue!"
+        Linter.logLintIf linter.style.commandStart.verbose (.ofRange rg)
+          m!"Formatted string:\n{fmt}\nOriginal string:\n{origSubstring}"
+        continue
+      unless isOutside forbidden rg do
+        continue
+      unless rg.stop ≤ upTo do return
+      unless docStringEnd ≤ rg.start do return
+
+      let ctx := 4 -- the number of characters after the mismatch that linter prints
+      let srcWindow := mkWindow orig s.srcNat (ctx + s.length)
+      let expectedWindow := mkWindow st s.fmtPos (ctx + (1))
+      Linter.logLint linter.style.commandStart (.ofRange rg)
+        m!"{s.msg} in the source\n\n\
+          This part of the code\n  '{srcWindow}'\n\
+          should be written as\n  '{expectedWindow}'\n"
+      Linter.logLintIf linter.style.commandStart.verbose (.ofRange rg)
+        m!"Formatted string:\n{fmt}\nOriginal string:\n{origSubstring}"
+
+initialize addLinter commandStartLinter
+
+end Style.CommandStart
+
+end Mathlib.Linter
diff --git a/Mathlib/Tactic/Simps/NotationClass.lean b/Mathlib/Tactic/Simps/NotationClass.lean
index 31c19acb9d8517..f3df4ddefdc6ad 100644
--- a/Mathlib/Tactic/Simps/NotationClass.lean
+++ b/Mathlib/Tactic/Simps/NotationClass.lean
@@ -25,7 +25,7 @@ and this notation should be used instead of projections by `@[simps]`.
     `+` uses `HAdd.hAdd`, not `Add.add` and `0` uses `OfNat.ofNat` not `Zero.zero`.
     We also add it to non-heterogenous notation classes, like `Neg`, but it doesn't do much for any
     class that extends `Neg`.
-  * `@[notation_class * <projName> Simps.findCoercionArgs]` is used to configure the
+  * `@[notation_class* <projName> Simps.findCoercionArgs]` is used to configure the
     `SetLike` and `DFunLike` coercions.
   * The first name argument is the projection name we use as the key to search for this class
     (default: name of first projection of the class).
diff --git a/MathlibTest/CommandStart.lean b/MathlibTest/CommandStart.lean
new file mode 100644
index 00000000000000..dafa69c10563ee
--- /dev/null
+++ b/MathlibTest/CommandStart.lean
@@ -0,0 +1,492 @@
+import Aesop.Frontend.Attribute
+import Mathlib.Tactic.Linter.CommandStart
+
+set_option linter.style.commandStart true
+
+-- Constructs that are ignored by the linter, and (former) false positives.
+section noFalsePositives
+
+-- Explicit name literals: used to error (and the suggested replacement is invalid syntax).
+structure foo (name: Lean.Name) where
+
+#guard_msgs in
+def bar (_param : List (foo ``String)) := 1
+
+-- This example would trigger the linter if we did not special case
+-- `where` in `Mathlib.Linter.Style.CommandStart.getUnlintedRanges`.
+/-- A -/
+example := aux
+where
+  /-- A -/
+  aux : Unit := ()
+
+-- For structure fields, all field definitions are linted.
+-- TODO: currently, only the first field is linted
+/--
+warning: extra space in the source
+
+This part of the code
+  'field1     : Nat'
+should be written as
+  'field1 : Nat'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+structure A where
+  field1     : Nat
+  field2 : Nat
+
+-- TODO: this is not linted yet!
+structure B where
+  field1 : Nat
+  field2     : Nat
+
+-- TODO: this is not linted yet!
+structure C where
+  field1 :     Nat
+  field2     : Nat
+
+-- Note that the linter does not attempt to recognise or respect manual alignment of fields:
+-- this is often brittle and should usually be removed.
+/--
+warning: extra space in the source
+
+This part of the code
+  'field1    :  '
+should be written as
+  'field1 : Nat'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+structure D where
+  field1    :     Nat
+  field2    : Nat
+
+-- This also applies to consecutive declarations.
+/--
+warning: declaration uses 'sorry'
+---
+warning: extra space in the source
+
+This part of the code
+  'instance   {R}'
+should be written as
+  'instance {R} :'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+instance   {R} : Add R := sorry
+/--
+warning: declaration uses 'sorry'
+---
+warning: extra space in the source
+
+This part of the code
+  'instance   {R}'
+should be written as
+  'instance {R} :'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+instance   {R} : Add R := sorry
+
+-- Strings are ignored by the linter.
+variable (a : String := "  ")
+
+-- The linter skips double-quoted names.
+variable (d : Lean.Name := ``Nat) in open Nat
+
+-- Code inside `run_cmd` is not checked at all.
+run_cmd
+  for _ in [0] do
+    let _ ← `(
+      end)
+
+def Card : Type → Nat := fun _ => 0
+
+/-- Symbols for use by all kinds of grammars. -/
+inductive Symbol (T N : Type)
+  /-- Terminal symbols (of the same type as the language) -/
+  | terminal (t : T) : Symbol T N
+  /-- Nonterminal symbols (must not be present when the word being generated is finalized) -/
+  | nonterminal (n : N) : Symbol T N
+deriving
+  DecidableEq, Repr
+
+-- embedded comments do not cause problems!
+#guard_msgs in
+open Nat in -- hi
+example : True := trivial
+
+-- embedded comments do not cause problems!
+#guard_msgs in
+open Nat in
+ -- hi
+example : True := trivial
+
+-- embedded comments do not cause problems!
+#guard_msgs in
+open Nat in
+  -- hi
+example : True := trivial
+
+structure X where
+  /-- A doc -/
+  x : Nat
+
+open Nat in /- hi -/
+example : True := trivial
+
+-- The notation `0::[]` disables the linter
+variable (h : 0::[] = [])
+
+/-- A doc string -/
+-- comment
+example : True := trivial
+
+-- Test that `Prop` and `Type` that are not escaped with `«...»` do not cause problems.
+def Prop.Hello := 0
+def Type.Hello := 0
+
+namespace List
+
+variable {α β : Type} (r : α → α → Prop) (s : β → β → Prop)
+
+-- The two infix are needed.  They "hide" a `quotPrecheck`
+local infixl:50 " ≼ " => r
+-- The two infix are needed.  They "hide" a `quotPrecheck`
+local infixl:50 " ≼ " => s
+
+/--
+warning: The `commandStart` linter had some parsing issues: feel free to silence it and report this error!
+note: this linter can be disabled with `set_option linter.style.commandStart.verbose false`
+-/
+#guard_msgs in
+set_option linter.style.commandStart.verbose true in
+example {a : α} (_ : a ≼ a) : 0 = 0 := rfl
+
+end List
+
+end noFalsePositives
+
+-- Miscellaneous constructs: variable, include, omit statements; aesop rulesets
+section misc
+
+variable [h : Add Nat] [Add Nat]
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'variable    [ h'
+should be written as
+  'variable [h :'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+---
+warning: extra space in the source
+
+This part of the code
+  '[ h  '
+should be written as
+  '[h : Add'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+---
+warning: extra space in the source
+
+This part of the code
+  'h    : Add'
+should be written as
+  '[h : Add'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+---
+warning: extra space in the source
+
+This part of the code
+  'Nat   ] ['
+should be written as
+  'Nat] [Add'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+---
+warning: extra space in the source
+
+This part of the code
+  '[ Add'
+should be written as
+  '[Add Nat]'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+variable    [ h    : Add Nat   ] [ Add Nat]
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'omit  [h :'
+should be written as
+  'omit [h :'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+---
+warning: extra space in the source
+
+This part of the code
+  'Nat]  [Add'
+should be written as
+  ' [Add'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+omit  [h : Add Nat]  [Add Nat]
+
+-- Include statements are not linted.
+include     h
+
+/--
+warning: extra space in the source
+
+This part of the code
+  '@[aesop  (rule_sets'
+should be written as
+  '@[aesop (rule_sets'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+@[aesop  (rule_sets := [builtin]) safe apply] example : True := trivial
+
+end misc
+
+/--
+warning: 'section' starts on column 1, but all commands should start at the beginning of the line.
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+ section
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'example    : True'
+should be written as
+  'example : True'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example    : True := trivial
+
+-- Additional spaces after the colon are not linted yet.
+#guard_msgs in
+example :     True := trivial
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'example  :  True'
+should be written as
+  'example : True'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example  :  True :=trivial
+
+/--
+warning: missing space in the source
+
+This part of the code
+  '(a: Nat)'
+should be written as
+  '(a : Nat)'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+variable (a: Nat)
+
+/--
+warning: missing space in the source
+
+This part of the code
+  '(_a: Nat)'
+should be written as
+  '(_a : Nat)'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example (_a: Nat) : True := trivial
+
+/--
+warning: missing space in the source
+
+This part of the code
+  '{a: Nat}'
+should be written as
+  '{a : Nat}'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example {a: Nat} : a = a := rfl
+
+/--
+a
+b
+c
+d -/
+example (_a : Nat) (_b : Int) : True := trivial
+
+/--
+warning: missing space in the source
+
+This part of the code
+  ':Nat}'
+should be written as
+  ': Nat}'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example {a :Nat} : a = a := rfl
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'example  {a :Nat}'
+should be written as
+  'example {a :'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+---
+warning: missing space in the source
+
+This part of the code
+  ':Nat}'
+should be written as
+  ': Nat}'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example  {a :Nat} : a = a := rfl
+
+/--
+warning: unused variable `b`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+---
+warning: missing space in the source
+
+This part of the code
+  'Nat}{b :'
+should be written as
+  'Nat} {b :'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example {a : Nat}{b : Nat} : a = a := rfl
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'Nat}  : a'
+should be written as
+  'Nat} : a ='
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example {a : Nat}  : a = a := rfl
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'alpha   ] {a'
+should be written as
+  'alpha] {a'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+example {alpha} [Neg alpha   ] {a : Nat} : a = a := rfl
+
+/--
+warning: extra space in the source
+
+This part of the code
+  'example  : True'
+should be written as
+  'example : True'
+
+note: this linter can be disabled with `set_option linter.style.commandStart false`
+-/
+#guard_msgs in
+/-- Check that doc/strings do not get removed as comments. -/
+example  : True := trivial
+
+-- Unit tests for internal functions in the linter.
+section internal
+
+/--
+info: #[srcNat: 12, srcPos: 12, fmtPos: 2, msg: extra space, length: 7
+, srcNat: 4, srcPos: 4, fmtPos: 1, msg: extra space, length: 3
+]
+-/
+#guard_msgs in
+#eval
+  let s := "example        f   g"
+  let t := "example fg"
+  Mathlib.Linter.parallelScan s t
+
+/--
+info: #[srcNat: 19, srcPos: 19, fmtPos: 21, msg: extra space, length: 1
+, srcNat: 16, srcPos: 16, fmtPos: 19, msg: extra space, length: 2
+, srcNat: 7, srcPos: 7, fmtPos: 12, msg: missing space, length: 1
+]
+-/
+#guard_msgs in
+#eval
+  let s := "example  :   True :=trivial"
+  let t := "example : True :=
+    trivial"
+  Mathlib.Linter.parallelScan s t
+
+/--
+info: #[srcNat: 4, srcPos: 4, fmtPos: 5, msg: missing space, length: 1
+, srcNat: 2, srcPos: 2, fmtPos: 1, msg: extra space, length: 1
+]
+-/
+#guard_msgs in
+#eval
+  let l := "hac d"
+  let m := "h  acd"
+  Mathlib.Linter.parallelScan l m
+
+-- Starting from `c` (due to the `"d ef gh".length` input), form a "window" of successive sizes
+-- `1, 2,..., 6`.  The output is trimmed and contains only full words, even partially overlapping
+-- with the given lengths.
+#guard Mathlib.Linter.Style.CommandStart.mkWindow "ab cd ef gh" "d ef gh".length 1 == "cd"
+#guard Mathlib.Linter.Style.CommandStart.mkWindow "ab cd ef gh" "d ef gh".length 2 == "cd"
+#guard Mathlib.Linter.Style.CommandStart.mkWindow "ab cd ef gh" "d ef gh".length 3 == "cd ef"
+#guard Mathlib.Linter.Style.CommandStart.mkWindow "ab cd ef gh" "d ef gh".length 4 == "cd ef"
+#guard Mathlib.Linter.Style.CommandStart.mkWindow "ab cd ef gh" "d ef gh".length 5 == "cd ef"
+#guard Mathlib.Linter.Style.CommandStart.mkWindow "ab cd ef gh" "d ef gh".length 6 == "cd ef gh"
+
+end internal
diff --git a/MathlibTest/EuclideanSpace.lean b/MathlibTest/EuclideanSpace.lean
index 662b91d2a02519..3b28606ac4cc0d 100644
--- a/MathlibTest/EuclideanSpace.lean
+++ b/MathlibTest/EuclideanSpace.lean
@@ -1,5 +1,7 @@
 import Mathlib.Analysis.InnerProductSpace.PiL2
 
+set_option linter.style.commandStart false
+
 #guard_expr !₂[] = (WithLp.equiv 2 (∀ _ : Fin 0, _)).symm ![]
 #guard_expr !₂[1, 2, 3] = (WithLp.equiv 2 (∀ _ : Fin 3, ℕ)).symm ![1, 2, 3]
 #guard_expr !₁[1, 2, (3 : ℝ)] = (WithLp.equiv 1 (∀ _ : Fin 3, ℝ)).symm ![1, 2, 3]
diff --git a/MathlibTest/Simps.lean b/MathlibTest/Simps.lean
index 1a3a9f33965567..b3af4c2be4ba1f 100644
--- a/MathlibTest/Simps.lean
+++ b/MathlibTest/Simps.lean
@@ -9,6 +9,9 @@ import Mathlib.Tactic.Common
 -- set_option trace.simps.verbose true
 -- set_option pp.universes true
 set_option autoImplicit true
+-- A few times, fields in this file are manually aligned. While there is some consensus this
+-- is not desired, it's not important enough to change right now.
+set_option linter.style.commandStart false
 
 open Lean Meta Elab Term Command Simps
 
diff --git a/MathlibTest/Traversable.lean b/MathlibTest/Traversable.lean
index ae7c2e2279e617..99cec8e7840691 100644
--- a/MathlibTest/Traversable.lean
+++ b/MathlibTest/Traversable.lean
@@ -1,6 +1,8 @@
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Control.Traversable.Instances
 
+set_option linter.style.commandStart false
+
 namespace Testing
 
 universe u
diff --git a/MathlibTest/antidiagonal.lean b/MathlibTest/antidiagonal.lean
index ea8da80cfaae99..ee14c6a9763a42 100644
--- a/MathlibTest/antidiagonal.lean
+++ b/MathlibTest/antidiagonal.lean
@@ -12,6 +12,8 @@ open Finset
 section
 -- set_option trace.profiler true
 
+set_option linter.style.commandStart false
+
 -- `antidiagonalTuple` is faster than `finAntidiagonal` by a small constant factor
 /-- info: 23426 -/
 #guard_msgs in #eval #(finAntidiagonal 4 50)
diff --git a/MathlibTest/delabLinearIndependent.lean b/MathlibTest/delabLinearIndependent.lean
index e85ccf90a342ef..96fe236730f35a 100644
--- a/MathlibTest/delabLinearIndependent.lean
+++ b/MathlibTest/delabLinearIndependent.lean
@@ -2,6 +2,7 @@ import Mathlib.LinearAlgebra.LinearIndependent.Defs
 
 set_option linter.style.setOption false
 set_option pp.unicode.fun true
+set_option linter.style.commandStart false
 
 variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V}
 
diff --git a/MathlibTest/matrix.lean b/MathlibTest/matrix.lean
index f4b3f5544cd2a5..3bf8c4d768ab41 100644
--- a/MathlibTest/matrix.lean
+++ b/MathlibTest/matrix.lean
@@ -7,6 +7,8 @@ import Mathlib.GroupTheory.Perm.Fin
 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
 import Qq
 
+set_option linter.style.commandStart false
+
 open Qq
 
 variable {α β : Type} [Semiring α] [Ring β]
diff --git a/MathlibTest/norm_num.lean b/MathlibTest/norm_num.lean
index f4390d52222f83..3bdeefb78d8be2 100644
--- a/MathlibTest/norm_num.lean
+++ b/MathlibTest/norm_num.lean
@@ -535,6 +535,7 @@ example : - (-4 / 3) = 1 / (3 / (4 : α)) := by norm_num1
 end
 
 -- user command
+set_option linter.style.commandStart false
 
 /-- info: True -/
 #guard_msgs in #norm_num 1 = 1
diff --git a/MathlibTest/set_like.lean b/MathlibTest/set_like.lean
index 991935f4da54f6..73d922976329e8 100644
--- a/MathlibTest/set_like.lean
+++ b/MathlibTest/set_like.lean
@@ -8,6 +8,8 @@ set_option autoImplicit true
 section Delab
 variable {M : Type u} [Monoid M] (S S' : Submonoid M)
 
+set_option linter.style.commandStart false
+
 /-- info: ↥S → ↥S' : Type u -/
 #guard_msgs in #check S → S'
 
diff --git a/MathlibTest/vec_notation.lean b/MathlibTest/vec_notation.lean
index 381399e7b31988..d2cd4363e03c94 100644
--- a/MathlibTest/vec_notation.lean
+++ b/MathlibTest/vec_notation.lean
@@ -38,6 +38,8 @@ run_elab do
 
 /-! These tests are testing delaborators -/
 
+set_option linter.style.commandStart false
+
 /-- info: fun x => ![0, 1] x : Fin 2 → ℕ -/
 #guard_msgs in #check fun x : Fin 2 => (![0, 1] : Fin 2 → ℕ) x
 /-- info: fun x => ![] x : Fin 0 → ℕ -/