chore(MathlibTest): move test files for linters into the Linter subdirectory (#40397)

This means we can use the auto-labelling mechanism to also suggest appropriate labels for these files.

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Author: grunweg

Mathlib/Tactic/Linter/Header.lean

@@ -366,7 +366,8 @@ The set of files outside the `Mathlib` package to run the header style linter on
 because they are files that test the linter.
 -/
 def headerTestFiles : NameSet := .ofList
-  [`MathlibTest.Header, `MathlibTest.HeaderFail, `MathlibTest.VersoHeader, `MathlibTest.DirectoryDependencyLinter.Test]
+  [`MathlibTest.Linter.Header.Basic, `MathlibTest.Linter.Header.Fail, `MathlibTest.Linter.Header.Verso,
+  `MathlibTest.DirectoryDependencyLinter.Test]
 
 @[inherit_doc Mathlib.Linter.linter.style.header]
 def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do

MathlibTest/DoubleUnderscore.lean MathlibTest/Linter/DoubleUnderscore.leanMathlibTest/DoubleUnderscore.lean renamed to MathlibTest/Linter/DoubleUnderscore.lean

@@ -18,3 +18,12 @@ Note: This linter can be disabled with `set_option linter.style.nameCheck false`
 -/
 #guard_msgs in
 def double__underscore : Unit := ()
+
+/--
+warning: The declaration 'double__underscore'' contains '__', which does not follow the mathlib naming conventions. Consider using single underscores instead.
+
+Note: This linter can be disabled with `set_option linter.style.nameCheck false`
+-/
+#guard_msgs in
+set_option linter.style.nameCheck true in
+theorem double__underscore' : True := trivial

MathlibTest/Lint.lean MathlibTest/Linter/DupNamespace.leanMathlibTest/Lint.lean renamed to MathlibTest/Linter/DupNamespace.lean

@@ -62,13 +62,3 @@ Note: This linter can be disabled with `set_option linter.dupNamespace false`
 export Nat (add add_comm add)
 
 end add
-
-/--
-warning: The declaration 'double__underscore' contains '__',
-which does not follow the mathlib naming conventions. Consider using single underscores instead.
-
-Note: This linter can be disabled with `set_option linter.style.nameCheck false`
--/
-#guard_msgs in
-set_option linter.style.nameCheck true in
-theorem double__underscore : True := trivial