move: new Mathlib.Tactic.Linter dir (#11807)

Create a new `Mathlib/Tactic/Linter` dir and move there the linters.  Currently the new dir contains only one file, but there are more linters in PRs.

Mathlib.lean

@@ -3765,8 +3765,8 @@ import Mathlib.Tactic.Linarith.SimplexAlgorithm.PositiveVector
 import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
-import Mathlib.Tactic.Lint
 import Mathlib.Tactic.Linter
+import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp

Mathlib/Tactic.lean

@@ -111,8 +111,8 @@ import Mathlib.Tactic.Linarith.SimplexAlgorithm.PositiveVector
 import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
-import Mathlib.Tactic.Lint
 import Mathlib.Tactic.Linter
+import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp

Mathlib/Tactic/Common.lean

@@ -11,6 +11,14 @@ import Qq
 -- Tools for analysing imports, like `#find_home`, `#minimize_imports`, ...
 import ImportGraph.Imports
 
+-- Currently we don't need to import all of ProofWidgets,
+-- but without this, if you don't run `lake build ProofWidgets` then `make test` will fail.
+-- Hopefully `lake` will be able to handle tests later.
+import ProofWidgets
+
+-- Import Mathlib-specific linters.
+import Mathlib.Tactic.Linter.Lint
+
 -- Now import all tactics defined in Mathlib that do not require theory files.
 import Mathlib.Mathport.Rename
 import Mathlib.Tactic.ApplyCongr
@@ -114,6 +122,9 @@ thereby making tactics widely available without needing specific imports.
 
 We include some commented out imports here, with an explanation of their theory requirements,
 to save some time for anyone wondering why they are not here.
+
+We also import theory-free linters, commands, and utilities which are useful to have low in the
+import hierarchy.
 -/
 
 /-!

Mathlib/Tactic/Linter.lean

@@ -7,4 +7,4 @@ This file is ignored by `Shake`:
 * it is in `ignoreImport`, meaning that where it is imported, it is considered necessary.
 -/
 
-import Mathlib.Tactic.Lint
+import Mathlib.Tactic.Linter.Lint

test/Lint.lean

@@ -1,4 +1,4 @@
-import Mathlib.Tactic.Lint
+import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.ToAdditive
 
 -- Adaptation note: test disabled.