leanprover-community · joneugster · May 21, 2026 · May 21, 2026 · May 21, 2026 · May 21, 2026
diff --git a/MathlibTest/aesop_cat.lean → MathlibTest/AesopCat.lean b/MathlibTest/aesop_cat.lean → MathlibTest/AesopCat.lean
diff --git a/...ibTest/instance_diamonds/algebra_rat.lean → MathlibTest/Algebra/Algebra/Rat.lean b/...ibTest/instance_diamonds/algebra_rat.lean → MathlibTest/Algebra/Algebra/Rat.lean
diff --git a/MathlibTest/Polynomial.lean → MathlibTest/Algebra/Polynomial.lean b/MathlibTest/Polynomial.lean → MathlibTest/Algebra/Polynomial.lean
diff --git a/MathlibTest/Quaternion.lean → MathlibTest/Algebra/Quaternion.lean b/MathlibTest/Quaternion.lean → MathlibTest/Algebra/Quaternion.lean
diff --git a/MathlibTest/DFinsuppMultiLinear.lean → ...st/Data/DFinsupp/DFinsuppMultiLinear.lean b/MathlibTest/DFinsuppMultiLinear.lean → ...st/Data/DFinsupp/DFinsuppMultiLinear.lean
diff --git a/MathlibTest/dfinsupp_notation.lean → MathlibTest/Data/DFinsupp/Notation.lean b/MathlibTest/dfinsupp_notation.lean → MathlibTest/Data/DFinsupp/Notation.lean
diff --git a/MathlibTest/vec_notation.lean → MathlibTest/Data/Fin/VecNotation.lean b/MathlibTest/vec_notation.lean → MathlibTest/Data/Fin/VecNotation.lean
diff --git a/MathlibTest/FunLike.lean → MathlibTest/Data/FunLike.lean b/MathlibTest/FunLike.lean → MathlibTest/Data/FunLike.lean
diff --git a/MathlibTest/Real.lean → MathlibTest/Data/Real.lean b/MathlibTest/Real.lean → MathlibTest/Data/Real.lean
diff --git a/MathlibTest/zmod.lean → MathlibTest/Data/ZMod.lean b/MathlibTest/zmod.lean → MathlibTest/Data/ZMod.lean
diff --git a/MathlibTest/deriving_countable.lean → MathlibTest/DeriveCountable.lean b/MathlibTest/deriving_countable.lean → MathlibTest/DeriveCountable.lean
diff --git a/MathlibTest/deriving_countable_module.lean → MathlibTest/DeriveCountableModule.lean b/MathlibTest/deriving_countable_module.lean → MathlibTest/DeriveCountableModule.lean
diff --git a/MathlibTest/derive_encodable.lean → MathlibTest/DeriveEncodable.lean b/MathlibTest/derive_encodable.lean → MathlibTest/DeriveEncodable.lean
diff --git a/MathlibTest/enat_to_nat.lean → MathlibTest/ENatToNat.lean b/MathlibTest/enat_to_nat.lean → MathlibTest/ENatToNat.lean
diff --git a/MathlibTest/eval_elab.lean → MathlibTest/EvalElab.lean b/MathlibTest/eval_elab.lean → MathlibTest/EvalElab.lean
diff --git a/MathlibTest/fail_if_no_progress.lean → MathlibTest/FailIfNoProgress.lean b/MathlibTest/fail_if_no_progress.lean → MathlibTest/FailIfNoProgress.lean
diff --git a/MathlibTest/fast_instance.lean → MathlibTest/FastInstance.lean b/MathlibTest/fast_instance.lean → MathlibTest/FastInstance.lean
diff --git a/MathlibTest/finset_builder.lean → MathlibTest/FinsetBuilder.lean b/MathlibTest/finset_builder.lean → MathlibTest/FinsetBuilder.lean
diff --git a/MathlibTest/finset_repr.lean → MathlibTest/FinsetRepr.lean b/MathlibTest/finset_repr.lean → MathlibTest/FinsetRepr.lean
diff --git a/MathlibTest/finsupp_notation.lean → MathlibTest/FinsuppNotation.lean b/MathlibTest/finsupp_notation.lean → MathlibTest/FinsuppNotation.lean
diff --git a/MathlibTest/format_table.lean → MathlibTest/FormatTable.lean b/MathlibTest/format_table.lean → MathlibTest/FormatTable.lean
diff --git a/MathlibTest/import_all.lean → MathlibTest/ImportAll.lean b/MathlibTest/import_all.lean → MathlibTest/ImportAll.lean
diff --git a/MathlibTest/instance_diamonds.lean → MathlibTest/InstanceDiamonds.lean b/MathlibTest/instance_diamonds.lean → MathlibTest/InstanceDiamonds.lean
diff --git a/...amonds/Analysis/Normed/Field/WithAbs.lean → ...amonds/Analysis/Normed/Field/WithAbs.lean b/...amonds/Analysis/Normed/Field/WithAbs.lean → ...amonds/Analysis/Normed/Field/WithAbs.lean
diff --git a/...nstance_diamonds/Data/Complex/Module.lean → ...InstanceDiamonds/Data/Complex/Module.lean b/...nstance_diamonds/Data/Complex/Module.lean → ...InstanceDiamonds/Data/Complex/Module.lean
diff --git a/...dTheory/IsAlgClosed/AlgebraicClosure.lean → ...dTheory/IsAlgClosed/AlgebraicClosure.lean b/...dTheory/IsAlgClosed/AlgebraicClosure.lean → ...dTheory/IsAlgClosed/AlgebraicClosure.lean
diff --git a/...ldTheory/SplittingField/Construction.lean → ...ldTheory/SplittingField/Construction.lean b/...ldTheory/SplittingField/Construction.lean → ...ldTheory/SplittingField/Construction.lean
diff --git a/MathlibTest/instance_diamonds/normed.lean → MathlibTest/InstanceDiamonds/Normed.lean b/MathlibTest/instance_diamonds/normed.lean → MathlibTest/InstanceDiamonds/Normed.lean
diff --git a/MathlibTest/jacobiSym.lean → MathlibTest/JacobiSymbol.lean b/MathlibTest/jacobiSym.lean → MathlibTest/JacobiSymbol.lean
diff --git a/MathlibTest/grind/ac.lean → MathlibTest/Lean/Tactic/Grind/AC.lean b/MathlibTest/grind/ac.lean → MathlibTest/Lean/Tactic/Grind/AC.lean
diff --git a/MathlibTest/grind/cc.lean → MathlibTest/Lean/Tactic/Grind/CC.lean b/MathlibTest/grind/cc.lean → MathlibTest/Lean/Tactic/Grind/CC.lean
diff --git a/MathlibTest/grind/field.lean → MathlibTest/Lean/Tactic/Grind/Field.lean b/MathlibTest/grind/field.lean → MathlibTest/Lean/Tactic/Grind/Field.lean
diff --git a/MathlibTest/grind/field_instance.lean → ...Test/Lean/Tactic/Grind/FieldInstance.lean b/MathlibTest/grind/field_instance.lean → ...Test/Lean/Tactic/Grind/FieldInstance.lean
diff --git a/MathlibTest/grind/grobner.lean → MathlibTest/Lean/Tactic/Grind/Grobner.lean b/MathlibTest/grind/grobner.lean → MathlibTest/Lean/Tactic/Grind/Grobner.lean
diff --git a/MathlibTest/grind/linarith.lean → MathlibTest/Lean/Tactic/Grind/Linarith.lean b/MathlibTest/grind/linarith.lean → MathlibTest/Lean/Tactic/Grind/Linarith.lean
diff --git a/MathlibTest/grind/lint.lean → MathlibTest/Lean/Tactic/Grind/Lint.lean b/MathlibTest/grind/lint.lean → MathlibTest/Lean/Tactic/Grind/Lint.lean
diff --git a/MathlibTest/grind/natCast_instance.lean → ...st/Lean/Tactic/Grind/NatCastInstance.lean b/MathlibTest/grind/natCast_instance.lean → ...st/Lean/Tactic/Grind/NatCastInstance.lean
diff --git a/MathlibTest/grind/ordered_ring.lean → ...ibTest/Lean/Tactic/Grind/OrderedRing.lean b/MathlibTest/grind/ordered_ring.lean → ...ibTest/Lean/Tactic/Grind/OrderedRing.lean
diff --git a/MathlibTest/grind/pairwise_disjoint.lean → ...t/Lean/Tactic/Grind/PairwiseDisjoint.lean b/MathlibTest/grind/pairwise_disjoint.lean → ...t/Lean/Tactic/Grind/PairwiseDisjoint.lean
diff --git a/MathlibTest/grind/panic.lean → MathlibTest/Lean/Tactic/Grind/Panic.lean b/MathlibTest/grind/panic.lean → MathlibTest/Lean/Tactic/Grind/Panic.lean
diff --git a/MathlibTest/grind/ring.lean → MathlibTest/Lean/Tactic/Grind/Ring.lean b/MathlibTest/grind/ring.lean → MathlibTest/Lean/Tactic/Grind/Ring.lean
diff --git a/MathlibTest/grind/set.lean → MathlibTest/Lean/Tactic/Grind/Set.lean b/MathlibTest/grind/set.lean → MathlibTest/Lean/Tactic/Grind/Set.lean
diff --git a/MathlibTest/grind/trig.lean → MathlibTest/Lean/Tactic/Grind/Trig.lean b/MathlibTest/grind/trig.lean → MathlibTest/Lean/Tactic/Grind/Trig.lean
diff --git a/MathlibTest/rewrites.lean → MathlibTest/Lean/Tactic/Rewrites.lean b/MathlibTest/rewrites.lean → MathlibTest/Lean/Tactic/Rewrites.lean
diff --git a/MathlibTest/DeprecatedModule.lean → ...er/DeprecatedModule/DeprecatedModule.lean b/MathlibTest/DeprecatedModule.lean → ...er/DeprecatedModule/DeprecatedModule.lean
@@ -7,7 +7,7 @@ deprecated_module (since := "2025-04-10")
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModule' deprecates to
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with no message
 -/
@@ -20,11 +20,11 @@ deprecated_module "We can also give more details about the deprecation" (since :
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModule' deprecates to
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with message 'We can also give more details about the deprecation'
 
-'MathlibTest.DeprecatedModule' deprecates to
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with no message
 -/
@@ -42,11 +42,11 @@ deprecated_module "Text" (since := "2025-02-31")
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModule' deprecates to
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with message 'We can also give more details about the deprecation'
 
-'MathlibTest.DeprecatedModule' deprecates to
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with no message
 -/

diff --git a/MathlibTest/DeprecatedModuleAllTest.lean → ...ecatedModule/DeprecatedModuleAllTest.lean b/MathlibTest/DeprecatedModuleAllTest.lean → ...ecatedModule/DeprecatedModuleAllTest.lean
@@ -1,10 +1,10 @@
 module
 
-import all MathlibTest.DeprecatedModuleNew
+import all MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
 
 /--
 warning: Testing public import deprecation
-'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
 
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString

diff --git a/MathlibTest/DeprecatedModuleMetaTest.lean → ...catedModule/DeprecatedModuleMetaTest.lean b/MathlibTest/DeprecatedModuleMetaTest.lean → ...catedModule/DeprecatedModuleMetaTest.lean
@@ -1,10 +1,10 @@
 module
 
-meta import MathlibTest.DeprecatedModuleNew
+meta import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
 
 /--
 warning: Testing public import deprecation
-'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
 
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString

diff --git a/MathlibTest/DeprecatedModuleNew.lean → ...DeprecatedModule/DeprecatedModuleNew.lean b/MathlibTest/DeprecatedModuleNew.lean → ...DeprecatedModule/DeprecatedModuleNew.lean
diff --git a/...bTest/DeprecatedModulePublicMetaTest.lean → ...odule/DeprecatedModulePublicMetaTest.lean b/...bTest/DeprecatedModulePublicMetaTest.lean → ...odule/DeprecatedModulePublicMetaTest.lean
@@ -1,10 +1,10 @@
 module
 
-public meta import MathlibTest.DeprecatedModuleNew
+public meta import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
 
 /--
 warning: Testing public import deprecation
-'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
 
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString

diff --git a/MathlibTest/DeprecatedModulePublicTest.lean → ...tedModule/DeprecatedModulePublicTest.lean b/MathlibTest/DeprecatedModulePublicTest.lean → ...tedModule/DeprecatedModulePublicTest.lean
@@ -1,10 +1,10 @@
 module
 
-public import MathlibTest.DeprecatedModuleNew
+public import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
 
 /--
 warning: Testing public import deprecation
-'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
 
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString

diff --git a/MathlibTest/DeprecatedModuleTest.lean → ...eprecatedModule/DeprecatedModuleTest.lean b/MathlibTest/DeprecatedModuleTest.lean → ...eprecatedModule/DeprecatedModuleTest.lean
@@ -1,8 +1,8 @@
-import MathlibTest.DeprecatedModule
+import MathlibTest.Linter.DeprecatedModule.DeprecatedModule
 
 /--
 warning: We can also give more details about the deprecation
-'MathlibTest.DeprecatedModule' has been deprecated: please replace this import by
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' has been deprecated: please replace this import by
 
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString
@@ -11,7 +11,7 @@ import Mathlib.Tactic.Linter.DocString
 Note: This linter can be disabled with `set_option linter.deprecated.module false`
 ---
 warning:
-'MathlibTest.DeprecatedModule' has been deprecated: please replace this import by
+'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' has been deprecated: please replace this import by
 
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString

diff --git a/MathlibTest/DeprecatedSyntaxLinter.lean → ...ibTest/Linter/DeprecatedSyntaxLinter.lean b/MathlibTest/DeprecatedSyntaxLinter.lean → ...ibTest/Linter/DeprecatedSyntaxLinter.lean
diff --git a/MathlibTest/DocPrime.lean → MathlibTest/Linter/DocPrime.lean b/MathlibTest/DocPrime.lean → MathlibTest/Linter/DocPrime.lean
diff --git a/MathlibTest/DocString.lean → MathlibTest/Linter/DocString.lean b/MathlibTest/DocString.lean → MathlibTest/Linter/DocString.lean
diff --git a/MathlibTest/EmptyLine.lean → MathlibTest/Linter/EmptyLine.lean b/MathlibTest/EmptyLine.lean → MathlibTest/Linter/EmptyLine.lean
diff --git a/MathlibTest/FlexibleLinter.lean → MathlibTest/Linter/FlexibleLinter.lean b/MathlibTest/FlexibleLinter.lean → MathlibTest/Linter/FlexibleLinter.lean
diff --git a/MathlibTest/ForbiddenModuleNames.lean → MathlibTest/Linter/ForbiddenModuleNames.lean b/MathlibTest/ForbiddenModuleNames.lean → MathlibTest/Linter/ForbiddenModuleNames.lean
diff --git a/MathlibTest/HaveLetLinter.lean → MathlibTest/Linter/HaveLetLinter.lean b/MathlibTest/HaveLetLinter.lean → MathlibTest/Linter/HaveLetLinter.lean
diff --git a/MathlibTest/ImportHeavyFlexibleLinter.lean → ...est/Linter/ImportHeavyFlexibleLinter.lean b/MathlibTest/ImportHeavyFlexibleLinter.lean → ...est/Linter/ImportHeavyFlexibleLinter.lean
diff --git a/MathlibTest/Lint.lean → MathlibTest/Linter/Lint.lean b/MathlibTest/Lint.lean → MathlibTest/Linter/Lint.lean
diff --git a/MathlibTest/ModuleCasing.lean → MathlibTest/Linter/ModuleCasing.lean b/MathlibTest/ModuleCasing.lean → MathlibTest/Linter/ModuleCasing.lean
diff --git a/MathlibTest/oldObtain.lean → MathlibTest/Linter/OldObtain.lean b/MathlibTest/oldObtain.lean → MathlibTest/Linter/OldObtain.lean
diff --git a/...t/PrivateModuleLinter/hasOnlyPrivate.lean → ...r/PrivateModuleLinter/HasOnlyPrivate.lean b/...t/PrivateModuleLinter/hasOnlyPrivate.lean → ...r/PrivateModuleLinter/HasOnlyPrivate.lean
diff --git a/...ibTest/PrivateModuleLinter/hasPublic.lean → ...Linter/PrivateModuleLinter/HasPublic.lean b/...ibTest/PrivateModuleLinter/hasPublic.lean → ...Linter/PrivateModuleLinter/HasPublic.lean
diff --git a/...bTest/PrivateModuleLinter/importOnly.lean → ...inter/PrivateModuleLinter/ImportOnly.lean b/...bTest/PrivateModuleLinter/importOnly.lean → ...inter/PrivateModuleLinter/ImportOnly.lean
diff --git a/...bTest/PrivateModuleLinter/initialize.lean → ...inter/PrivateModuleLinter/Initialize.lean b/...bTest/PrivateModuleLinter/initialize.lean → ...inter/PrivateModuleLinter/Initialize.lean
diff --git a/...ibTest/PrivateModuleLinter/nonModule.lean → ...Linter/PrivateModuleLinter/NonModule.lean b/...ibTest/PrivateModuleLinter/nonModule.lean → ...Linter/PrivateModuleLinter/NonModule.lean
diff --git a/...ibTest/PrivateModuleLinter/notation3.lean → ...Linter/PrivateModuleLinter/Notation3.lean b/...ibTest/PrivateModuleLinter/notation3.lean → ...Linter/PrivateModuleLinter/Notation3.lean
@@ -10,10 +10,10 @@ local notation3 "MyList[" (x", "* => foldr (a b => List.cons a b) List.nil) "]"
 /- Check that we have indeed created declarations, and aren't not linting just due to being an
 empty file: -/
 /--
-info: [_private.MathlibTest.PrivateModuleLinter.notation3.0.«_aux_MathlibTest_PrivateModuleLinter_notation3___delab_app__private_MathlibTest_PrivateModuleLinter_notation3_0_termMyList[_,]_2»,
- _private.MathlibTest.PrivateModuleLinter.notation3.0.«termMyList[_,]»,
- _private.MathlibTest.PrivateModuleLinter.notation3.0.«_aux_MathlibTest_PrivateModuleLinter_notation3___delab_app__private_MathlibTest_PrivateModuleLinter_notation3_0_termMyList[_,]_1»,
- _private.MathlibTest.PrivateModuleLinter.notation3.0.«_aux_MathlibTest_PrivateModuleLinter_notation3___macroRules__private_MathlibTest_PrivateModuleLinter_notation3_0_termMyList[_,]_1»]
+info: [_private.MathlibTest.Linter.PrivateModuleLinter.Notation3.0.«_aux_MathlibTest_Linter_PrivateModuleLinter_Notation3___delab_app__private_MathlibTest_Linter_PrivateModuleLinter_Notation3_0_termMyList[_,]_2»,
+ _private.MathlibTest.Linter.PrivateModuleLinter.Notation3.0.«termMyList[_,]»,
+ _private.MathlibTest.Linter.PrivateModuleLinter.Notation3.0.«_aux_MathlibTest_Linter_PrivateModuleLinter_Notation3___macroRules__private_MathlibTest_Linter_PrivateModuleLinter_Notation3_0_termMyList[_,]_1»,
+ _private.MathlibTest.Linter.PrivateModuleLinter.Notation3.0.«_aux_MathlibTest_Linter_PrivateModuleLinter_Notation3___delab_app__private_MathlibTest_Linter_PrivateModuleLinter_Notation3_0_termMyList[_,]_1»]
 -/
 #guard_msgs in
 run_cmd do

diff --git a/...st/PrivateModuleLinter/reservedName1.lean → ...er/PrivateModuleLinter/ReservedName1.lean b/...st/PrivateModuleLinter/reservedName1.lean → ...er/PrivateModuleLinter/ReservedName1.lean
diff --git a/...st/PrivateModuleLinter/reservedName2.lean → ...er/PrivateModuleLinter/ReservedName2.lean b/...st/PrivateModuleLinter/reservedName2.lean → ...er/PrivateModuleLinter/ReservedName2.lean
@@ -2,7 +2,7 @@ module
 
 import Mathlib.Init
 import all Mathlib.Tactic.Linter.PrivateModule
-public import MathlibTest.PrivateModuleLinter.reservedName1
+public import MathlibTest.Linter.PrivateModuleLinter.ReservedName1
 
 open Lean
 

diff --git a/MathlibTest/LintStyle.lean → MathlibTest/Linter/Style/LintStyle.lean b/MathlibTest/LintStyle.lean → MathlibTest/Linter/Style/LintStyle.lean
diff --git a/MathlibTest/LongFile.lean → MathlibTest/Linter/Style/LongFile.lean b/MathlibTest/LongFile.lean → MathlibTest/Linter/Style/LongFile.lean
diff --git a/MathlibTest/AesopUnusedTactic.lean → ...inter/UnusedTactic/AesopUnusedTactic.lean b/MathlibTest/AesopUnusedTactic.lean → ...inter/UnusedTactic/AesopUnusedTactic.lean
diff --git a/MathlibTest/UnusedTactic.lean → ...est/Linter/UnusedTactic/UnusedTactic.lean b/MathlibTest/UnusedTactic.lean → ...est/Linter/UnusedTactic/UnusedTactic.lean
diff --git a/MathlibTest/ValidatePRTitle.lean → MathlibTest/Linter/ValidatePRTitle.lean b/MathlibTest/ValidatePRTitle.lean → MathlibTest/Linter/ValidatePRTitle.lean
diff --git a/MathlibTest/VersoHeader.lean → MathlibTest/Linter/VersoHeader.lean b/MathlibTest/VersoHeader.lean → MathlibTest/Linter/VersoHeader.lean
diff --git a/MathlibTest/WhitespaceLinter.lean → MathlibTest/Linter/Whitespace.lean b/MathlibTest/WhitespaceLinter.lean → MathlibTest/Linter/Whitespace.lean
diff --git a/MathlibTest/norm_cast.lean → MathlibTest/NormCast.lean b/MathlibTest/norm_cast.lean → MathlibTest/NormCast.lean
diff --git a/MathlibTest/register_try_tactic.lean → MathlibTest/RegisterTryTactic.lean b/MathlibTest/register_try_tactic.lean → MathlibTest/RegisterTryTactic.lean
diff --git a/MathlibTest/right_actions.lean → MathlibTest/RightActions.lean b/MathlibTest/right_actions.lean → MathlibTest/RightActions.lean
diff --git a/MathlibTest/set_like.lean → MathlibTest/SetLike.lean b/MathlibTest/set_like.lean → MathlibTest/SetLike.lean
diff --git a/MathlibTest/simp_confluence.lean → MathlibTest/SimpConfluence.lean b/MathlibTest/simp_confluence.lean → MathlibTest/SimpConfluence.lean
diff --git a/MathlibTest/slim_check.lean → MathlibTest/SlimCheck.lean b/MathlibTest/slim_check.lean → MathlibTest/SlimCheck.lean
diff --git a/MathlibTest/slow_instances.lean → MathlibTest/SlowInstances.lean b/MathlibTest/slow_instances.lean → MathlibTest/SlowInstances.lean
diff --git a/MathlibTest/slow_simp.lean → MathlibTest/SlowSimp.lean b/MathlibTest/slow_simp.lean → MathlibTest/SlowSimp.lean
diff --git a/MathlibTest/apply_congr.lean → MathlibTest/Tactic/ApplyCongr.lean b/MathlibTest/apply_congr.lean → MathlibTest/Tactic/ApplyCongr.lean
diff --git a/MathlibTest/apply_fun.lean → MathlibTest/Tactic/ApplyFun.lean b/MathlibTest/apply_fun.lean → MathlibTest/Tactic/ApplyFun.lean
diff --git a/MathlibTest/apply_rules.lean → MathlibTest/Tactic/ApplyRules.lean b/MathlibTest/apply_rules.lean → MathlibTest/Tactic/ApplyRules.lean
diff --git a/MathlibTest/apply_with.lean → MathlibTest/Tactic/ApplyWith.lean b/MathlibTest/apply_with.lean → MathlibTest/Tactic/ApplyWith.lean
diff --git a/MathlibTest/Bound/attribute.lean → MathlibTest/Tactic/Bound/Attribute.lean b/MathlibTest/Bound/attribute.lean → MathlibTest/Tactic/Bound/Attribute.lean
diff --git a/MathlibTest/Bound/bound.lean → MathlibTest/Tactic/Bound/Bound.lean b/MathlibTest/Bound/bound.lean → MathlibTest/Tactic/Bound/Bound.lean
diff --git a/MathlibTest/byContra.lean → MathlibTest/Tactic/ByContra.lean b/MathlibTest/byContra.lean → MathlibTest/Tactic/ByContra.lean
diff --git a/MathlibTest/cancel_denoms.lean → MathlibTest/Tactic/CancelDenoms.lean b/MathlibTest/cancel_denoms.lean → MathlibTest/Tactic/CancelDenoms.lean
diff --git a/MathlibTest/cases.lean → MathlibTest/Tactic/Cases.lean b/MathlibTest/cases.lean → MathlibTest/Tactic/Cases.lean
diff --git a/MathlibTest/casesm.lean → MathlibTest/Tactic/CasesM.lean b/MathlibTest/casesm.lean → MathlibTest/Tactic/CasesM.lean
diff --git a/MathlibTest/Change.lean → MathlibTest/Tactic/Change.lean b/MathlibTest/Change.lean → MathlibTest/Tactic/Change.lean
diff --git a/MathlibTest/Check.lean → MathlibTest/Tactic/Check.lean b/MathlibTest/Check.lean → MathlibTest/Tactic/Check.lean
diff --git a/MathlibTest/choose.lean → MathlibTest/Tactic/Choose/Choose.lean b/MathlibTest/choose.lean → MathlibTest/Tactic/Choose/Choose.lean
diff --git a/MathlibTest/choose_reduction.lean → MathlibTest/Tactic/Choose/Reduction.lean b/MathlibTest/choose_reduction.lean → MathlibTest/Tactic/Choose/Reduction.lean
diff --git a/MathlibTest/Clean.lean → MathlibTest/Tactic/Clean.lean b/MathlibTest/Clean.lean → MathlibTest/Tactic/Clean.lean
diff --git a/MathlibTest/ClearExcept.lean → MathlibTest/Tactic/ClearExcept.lean b/MathlibTest/ClearExcept.lean → MathlibTest/Tactic/ClearExcept.lean
diff --git a/MathlibTest/ClearExclamation.lean → MathlibTest/Tactic/ClearExclamation.lean b/MathlibTest/ClearExclamation.lean → MathlibTest/Tactic/ClearExclamation.lean
diff --git a/MathlibTest/Clear_.lean → MathlibTest/Tactic/Clear_.lean b/MathlibTest/Clear_.lean → MathlibTest/Tactic/Clear_.lean
diff --git a/MathlibTest/congrm.lean → MathlibTest/Tactic/CongrM.lean b/MathlibTest/congrm.lean → MathlibTest/Tactic/CongrM.lean
diff --git a/MathlibTest/Constructor.lean → MathlibTest/Tactic/Constructor.lean b/MathlibTest/Constructor.lean → MathlibTest/Tactic/Constructor.lean
diff --git a/MathlibTest/Contrapose.lean → MathlibTest/Tactic/Contrapose.lean b/MathlibTest/Contrapose.lean → MathlibTest/Tactic/Contrapose.lean
diff --git a/MathlibTest/conv.lean → MathlibTest/Tactic/Conv.lean b/MathlibTest/conv.lean → MathlibTest/Tactic/Conv.lean
diff --git a/MathlibTest/convert.lean → MathlibTest/Tactic/Convert/Convert.lean b/MathlibTest/convert.lean → MathlibTest/Tactic/Convert/Convert.lean
diff --git a/MathlibTest/convert2.lean → MathlibTest/Tactic/Convert/Convert2.lean b/MathlibTest/convert2.lean → MathlibTest/Tactic/Convert/Convert2.lean
diff --git a/MathlibTest/ErwQuestion.lean → MathlibTest/Tactic/ErwQuestion.lean b/MathlibTest/ErwQuestion.lean → MathlibTest/Tactic/ErwQuestion.lean
diff --git a/MathlibTest/ExistsI.lean → MathlibTest/Tactic/ExistsI.lean b/MathlibTest/ExistsI.lean → MathlibTest/Tactic/ExistsI.lean
diff --git a/MathlibTest/ExtractGoal.lean → MathlibTest/Tactic/ExtractGoal.lean b/MathlibTest/ExtractGoal.lean → MathlibTest/Tactic/ExtractGoal.lean
diff --git a/MathlibTest/FieldSimp.lean → MathlibTest/Tactic/FieldSimp.lean b/MathlibTest/FieldSimp.lean → MathlibTest/Tactic/FieldSimp.lean
diff --git a/MathlibTest/fin_cases.lean → MathlibTest/Tactic/FinCases.lean b/MathlibTest/fin_cases.lean → MathlibTest/Tactic/FinCases.lean
diff --git a/MathlibTest/finiteness.lean → MathlibTest/Tactic/Finiteness.lean b/MathlibTest/finiteness.lean → MathlibTest/Tactic/Finiteness.lean
diff --git a/MathlibTest/GCongr/Core.lean → MathlibTest/Tactic/GCongr/Core.lean b/MathlibTest/GCongr/Core.lean → MathlibTest/Tactic/GCongr/Core.lean
diff --git a/MathlibTest/GCongr/GCongr.lean → MathlibTest/Tactic/GCongr/GCongr.lean b/MathlibTest/GCongr/GCongr.lean → MathlibTest/Tactic/GCongr/GCongr.lean
diff --git a/MathlibTest/GCongr/implications.lean → MathlibTest/Tactic/GCongr/implications.lean b/MathlibTest/GCongr/implications.lean → MathlibTest/Tactic/GCongr/implications.lean
diff --git a/MathlibTest/GCongr/inequalities.lean → MathlibTest/Tactic/GCongr/inequalities.lean b/MathlibTest/GCongr/inequalities.lean → MathlibTest/Tactic/GCongr/inequalities.lean
diff --git a/MathlibTest/GCongr/mod.lean → MathlibTest/Tactic/GCongr/mod.lean b/MathlibTest/GCongr/mod.lean → MathlibTest/Tactic/GCongr/mod.lean
diff --git a/MathlibTest/Group.lean → MathlibTest/Tactic/Group.lean b/MathlibTest/Group.lean → MathlibTest/Tactic/Group.lean
diff --git a/MathlibTest/GuardGoalNums.lean → MathlibTest/Tactic/GuardGoalNums.lean b/MathlibTest/GuardGoalNums.lean → MathlibTest/Tactic/GuardGoalNums.lean
diff --git a/MathlibTest/GuardHypNums.lean → MathlibTest/Tactic/GuardHypNums.lean b/MathlibTest/GuardHypNums.lean → MathlibTest/Tactic/GuardHypNums.lean
diff --git a/MathlibTest/Have.lean → MathlibTest/Tactic/Have.lean b/MathlibTest/Have.lean → MathlibTest/Tactic/Have.lean
diff --git a/MathlibTest/hint.lean → MathlibTest/Tactic/Hint/Hint.lean b/MathlibTest/hint.lean → MathlibTest/Tactic/Hint/Hint.lean
diff --git a/MathlibTest/hintAll.lean → MathlibTest/Tactic/Hint/HintAll.lean b/MathlibTest/hintAll.lean → MathlibTest/Tactic/Hint/HintAll.lean
diff --git a/MathlibTest/Inhabit.lean → MathlibTest/Tactic/Inhabit.lean b/MathlibTest/Inhabit.lean → MathlibTest/Tactic/Inhabit.lean
diff --git a/MathlibTest/interval_cases.lean → MathlibTest/Tactic/IntervalCases.lean b/MathlibTest/interval_cases.lean → MathlibTest/Tactic/IntervalCases.lean
diff --git a/MathlibTest/Linarith/Basic.lean → MathlibTest/Tactic/Linarith/Basic.lean b/MathlibTest/Linarith/Basic.lean → MathlibTest/Tactic/Linarith/Basic.lean
diff --git a/MathlibTest/Linarith/NNReal.lean → MathlibTest/Tactic/Linarith/NNReal.lean b/MathlibTest/Linarith/NNReal.lean → MathlibTest/Tactic/Linarith/NNReal.lean
diff --git a/MathlibTest/linear_combination.lean → .../LinearCombination/LinearCombination.lean b/MathlibTest/linear_combination.lean → .../LinearCombination/LinearCombination.lean
diff --git a/MathlibTest/linear_combination_prime.lean → ...arCombination/LinearCombinationPrime.lean b/MathlibTest/linear_combination_prime.lean → ...arCombination/LinearCombinationPrime.lean
diff --git a/MathlibTest/mod_cases.lean → MathlibTest/Tactic/ModCases.lean b/MathlibTest/mod_cases.lean → MathlibTest/Tactic/ModCases.lean
diff --git a/MathlibTest/module.lean → MathlibTest/Tactic/Module.lean b/MathlibTest/module.lean → MathlibTest/Tactic/Module.lean
diff --git a/MathlibTest/Monotonicity.lean → MathlibTest/Tactic/Monotonicity.lean b/MathlibTest/Monotonicity.lean → MathlibTest/Tactic/Monotonicity.lean
diff --git a/MathlibTest/MoveAdd.lean → MathlibTest/Tactic/MoveAdd.lean b/MathlibTest/MoveAdd.lean → MathlibTest/Tactic/MoveAdd.lean
diff --git a/MathlibTest/NoncommRing.lean → MathlibTest/Tactic/NoncommRing.lean b/MathlibTest/NoncommRing.lean → MathlibTest/Tactic/NoncommRing.lean
diff --git a/MathlibTest/norm_num.lean → MathlibTest/Tactic/NormNum/NormNum.lean b/MathlibTest/norm_num.lean → MathlibTest/Tactic/NormNum/NormNum.lean
diff --git a/MathlibTest/norm_num_abs.lean → MathlibTest/Tactic/NormNum/NormNumAbs.lean b/MathlibTest/norm_num_abs.lean → MathlibTest/Tactic/NormNum/NormNumAbs.lean
diff --git a/MathlibTest/norm_num_ext.lean → MathlibTest/Tactic/NormNum/NormNumExt.lean b/MathlibTest/norm_num_ext.lean → MathlibTest/Tactic/NormNum/NormNumExt.lean
diff --git a/MathlibTest/norm_num_flt.lean → MathlibTest/Tactic/NormNum/NormNumFLT.lean b/MathlibTest/norm_num_flt.lean → MathlibTest/Tactic/NormNum/NormNumFLT.lean
diff --git a/MathlibTest/norm_num_ordinal.lean → ...ibTest/Tactic/NormNum/NormNumOrdinal.lean b/MathlibTest/norm_num_ordinal.lean → ...ibTest/Tactic/NormNum/NormNumOrdinal.lean
diff --git a/MathlibTest/norm_num_rpow.lean → MathlibTest/Tactic/NormNum/NormNumRPow.lean b/MathlibTest/norm_num_rpow.lean → MathlibTest/Tactic/NormNum/NormNumRPow.lean
diff --git a/MathlibTest/observe.lean → MathlibTest/Tactic/Observe.lean b/MathlibTest/observe.lean → MathlibTest/Tactic/Observe.lean
diff --git a/MathlibTest/order.lean → MathlibTest/Tactic/Order.lean b/MathlibTest/order.lean → MathlibTest/Tactic/Order.lean
diff --git a/MathlibTest/pnat_to_nat.lean → MathlibTest/Tactic/PNatToNat.lean b/MathlibTest/pnat_to_nat.lean → MathlibTest/Tactic/PNatToNat.lean
diff --git a/MathlibTest/positivity.lean → MathlibTest/Tactic/Positivity.lean b/MathlibTest/positivity.lean → MathlibTest/Tactic/Positivity.lean
diff --git a/MathlibTest/ProdAssoc.lean → MathlibTest/Tactic/ProdAssoc.lean b/MathlibTest/ProdAssoc.lean → MathlibTest/Tactic/ProdAssoc.lean
diff --git a/MathlibTest/Tactic/Push.lean → MathlibTest/Tactic/Push/Push.lean b/MathlibTest/Tactic/Push.lean → MathlibTest/Tactic/Push/Push.lean
diff --git a/MathlibTest/push_neg.lean → MathlibTest/Tactic/Push/PushNeg.lean b/MathlibTest/push_neg.lean → MathlibTest/Tactic/Push/PushNeg.lean
diff --git a/MathlibTest/RecallModule.lean → MathlibTest/Tactic/Recall/Module.lean b/MathlibTest/RecallModule.lean → MathlibTest/Tactic/Recall/Module.lean
diff --git a/MathlibTest/Tactic/Recall.lean → MathlibTest/Tactic/Recall/Recall.lean b/MathlibTest/Tactic/Recall.lean → MathlibTest/Tactic/Recall/Recall.lean
diff --git a/MathlibTest/recover.lean → MathlibTest/Tactic/Recover.lean b/MathlibTest/recover.lean → MathlibTest/Tactic/Recover.lean
diff --git a/MathlibTest/reduce_mod_char.lean → MathlibTest/Tactic/ReduceModChar.lean b/MathlibTest/reduce_mod_char.lean → MathlibTest/Tactic/ReduceModChar.lean
diff --git a/MathlibTest/renameBvar.lean → MathlibTest/Tactic/RenameBVar.lean b/MathlibTest/renameBvar.lean → MathlibTest/Tactic/RenameBVar.lean
diff --git a/MathlibTest/ring_compare.lean → MathlibTest/Tactic/Ring/Compare.lean b/MathlibTest/ring_compare.lean → MathlibTest/Tactic/Ring/Compare.lean
diff --git a/MathlibTest/Tactic/Ring.lean → MathlibTest/Tactic/Ring/Ring.lean b/MathlibTest/Tactic/Ring.lean → MathlibTest/Tactic/Ring/Ring.lean
diff --git a/MathlibTest/Tactic/Says.lean → MathlibTest/Tactic/Says/Says.lean b/MathlibTest/Tactic/Says.lean → MathlibTest/Tactic/Says/Says.lean
diff --git a/MathlibTest/says_whitespace.lean → MathlibTest/Tactic/Says/Whitespace.lean b/MathlibTest/says_whitespace.lean → MathlibTest/Tactic/Says/Whitespace.lean
diff --git a/MathlibTest/Set.lean → MathlibTest/Tactic/Set.lean b/MathlibTest/Set.lean → MathlibTest/Tactic/Set.lean
diff --git a/MathlibTest/SetNotationForOrder.lean → MathlibTest/Tactic/SetNotationForOrder.lean b/MathlibTest/SetNotationForOrder.lean → MathlibTest/Tactic/SetNotationForOrder.lean
diff --git a/MathlibTest/simp_intro.lean → MathlibTest/Tactic/SimpIntro.lean b/MathlibTest/simp_intro.lean → MathlibTest/Tactic/SimpIntro.lean
diff --git a/MathlibTest/SimpRw.lean → MathlibTest/Tactic/SimpRw.lean b/MathlibTest/SimpRw.lean → MathlibTest/Tactic/SimpRw.lean
diff --git a/MathlibTest/solve_by_elim/basic.lean → MathlibTest/Tactic/SolveByElim/Basic.lean b/MathlibTest/solve_by_elim/basic.lean → MathlibTest/Tactic/SolveByElim/Basic.lean
@@ -6,7 +6,7 @@ Authors: Kim Morrison
 import Lean.Meta.Tactic.SolveByElim
 import Mathlib.Tactic.Constructor
 import Batteries.Tactic.PermuteGoals
-import MathlibTest.solve_by_elim.dummy_label_attr
+import MathlibTest.Tactic.SolveByElim.DummyLabelAttr
 
 
 example (h : Nat) : Nat := by solve_by_elim

diff --git a/...bTest/solve_by_elim/dummy_label_attr.lean → ...st/Tactic/SolveByElim/DummyLabelAttr.lean b/...bTest/solve_by_elim/dummy_label_attr.lean → ...st/Tactic/SolveByElim/DummyLabelAttr.lean
diff --git a/MathlibTest/solve_by_elim/instances.lean → ...libTest/Tactic/SolveByElim/Instances.lean b/MathlibTest/solve_by_elim/instances.lean → ...libTest/Tactic/SolveByElim/Instances.lean
diff --git a/MathlibTest/SplitIfs.lean → MathlibTest/Tactic/SplitIfs.lean b/MathlibTest/SplitIfs.lean → MathlibTest/Tactic/SplitIfs.lean
diff --git a/MathlibTest/spread.lean → MathlibTest/Tactic/Spread.lean b/MathlibTest/spread.lean → MathlibTest/Tactic/Spread.lean
diff --git a/MathlibTest/Subsingleton.lean → MathlibTest/Tactic/Subsingleton.lean b/MathlibTest/Subsingleton.lean → MathlibTest/Tactic/Subsingleton.lean
diff --git a/MathlibTest/success_if_fail_with_msg.lean → MathlibTest/Tactic/SuccessIfFailWithMsg.lean b/MathlibTest/success_if_fail_with_msg.lean → MathlibTest/Tactic/SuccessIfFailWithMsg.lean
diff --git a/MathlibTest/SwapVar.lean → MathlibTest/Tactic/SwapVar.lean b/MathlibTest/SwapVar.lean → MathlibTest/Tactic/SwapVar.lean
diff --git a/MathlibTest/TacticAnalysis.lean → MathlibTest/Tactic/TacticAnalysis.lean b/MathlibTest/TacticAnalysis.lean → MathlibTest/Tactic/TacticAnalysis.lean
diff --git a/MathlibTest/TermCongr.lean → MathlibTest/Tactic/TermCongr/TermCongr.lean b/MathlibTest/TermCongr.lean → MathlibTest/Tactic/TermCongr/TermCongr.lean
diff --git a/MathlibTest/TermCongr2.lean → MathlibTest/Tactic/TermCongr/TermCongr2.lean b/MathlibTest/TermCongr2.lean → MathlibTest/Tactic/TermCongr/TermCongr2.lean
diff --git a/MathlibTest/toAdditive.lean → ...libTest/Tactic/ToAdditive/ToAdditive.lean b/MathlibTest/toAdditive.lean → ...libTest/Tactic/ToAdditive/ToAdditive.lean
diff --git a/MathlibTest/toAdditiveIrredDef.lean → ...Tactic/ToAdditive/ToAdditiveIrredDef.lean b/MathlibTest/toAdditiveIrredDef.lean → ...Tactic/ToAdditive/ToAdditiveIrredDef.lean
diff --git a/MathlibTest/ToDual.lean → MathlibTest/Tactic/ToDual.lean b/MathlibTest/ToDual.lean → MathlibTest/Tactic/ToDual.lean
diff --git a/MathlibTest/trace.lean → MathlibTest/Tactic/Trace.lean b/MathlibTest/trace.lean → MathlibTest/Tactic/Trace.lean
diff --git a/MathlibTest/UnsetOption.lean → MathlibTest/Tactic/UnsetOption.lean b/MathlibTest/UnsetOption.lean → MathlibTest/Tactic/UnsetOption.lean
diff --git a/MathlibTest/CalcQuestionMark.lean → ...bTest/Tactic/Widget/CalcQuestionMark.lean b/MathlibTest/CalcQuestionMark.lean → ...bTest/Tactic/Widget/CalcQuestionMark.lean
diff --git a/MathlibTest/CommDiag.lean → MathlibTest/Tactic/Widget/CommDiag.lean b/MathlibTest/CommDiag.lean → MathlibTest/Tactic/Widget/CommDiag.lean
diff --git a/MathlibTest/conv_widget.lean → MathlibTest/Tactic/Widget/Conv.lean b/MathlibTest/conv_widget.lean → MathlibTest/Tactic/Widget/Conv.lean
diff --git a/MathlibTest/LibraryRewrite.lean → ...libTest/Tactic/Widget/LibraryRewrite.lean b/MathlibTest/LibraryRewrite.lean → ...libTest/Tactic/Widget/LibraryRewrite.lean
diff --git a/MathlibTest/StringDiagram.lean → MathlibTest/Tactic/Widget/StringDiagram.lean b/MathlibTest/StringDiagram.lean → MathlibTest/Tactic/Widget/StringDiagram.lean
diff --git a/MathlibTest/tactic_timeout.lean → MathlibTest/TacticTimeout.lean b/MathlibTest/tactic_timeout.lean → MathlibTest/TacticTimeout.lean
diff --git a/MathlibTest/CompileInductive.lean → MathlibTest/Util/CompileInductive.lean b/MathlibTest/CompileInductive.lean → MathlibTest/Util/CompileInductive.lean
diff --git a/MathlibTest/CountHeartbeats.lean → MathlibTest/Util/CountHeartbeats.lean b/MathlibTest/CountHeartbeats.lean → MathlibTest/Util/CountHeartbeats.lean
diff --git a/MathlibTest/notation3.lean → MathlibTest/Util/Notation3.lean b/MathlibTest/notation3.lean → MathlibTest/Util/Notation3.lean
diff --git a/MathlibTest/superscript.lean → MathlibTest/Util/Superscript.lean b/MathlibTest/superscript.lean → MathlibTest/Util/Superscript.lean
diff --git a/MathlibTest/TermReduce.lean → MathlibTest/Util/TermReduce.lean b/MathlibTest/TermReduce.lean → MathlibTest/Util/TermReduce.lean
diff --git a/...t/instances/CommRing_integralClosure.lean → ...st/instances/CommRingIntegralClosure.lean b/...t/instances/CommRing_integralClosure.lean → ...st/instances/CommRingIntegralClosure.lean
diff --git a/MathlibTest/instances/Ring_finiteness.lean → MathlibTest/instances/RingFiniteness.lean b/MathlibTest/instances/Ring_finiteness.lean → MathlibTest/instances/RingFiniteness.lean