diff --git a/Mathlib/Algebra/Opposites.lean b/Mathlib/Algebra/Opposites.lean
index b9d19e7f62af83..6fdb56716ab364 100644
--- a/Mathlib/Algebra/Opposites.lean
+++ b/Mathlib/Algebra/Opposites.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Group.Defs
 public import Mathlib.Logic.Equiv.Defs
-public import Batteries.Tactic.Lint.Simp
+public import Batteries.Linter.Simp
 
 /-!
 # Multiplicative opposite and algebraic operations on it
diff --git a/Mathlib/Algebra/Ring/Ext.lean b/Mathlib/Algebra/Ring/Ext.lean
index b024fdbee9ac42..1b76dbc2d48819 100644
--- a/Mathlib/Algebra/Ring/Ext.lean
+++ b/Mathlib/Algebra/Ring/Ext.lean
@@ -281,7 +281,7 @@ namespace Semiring
     inst₁ = inst₂ := by
   -- Show that enough substructures are equal.
   have h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid := by
-    ext : 1 <;> assumption
+    ext : 1; assumption
   have h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring := by
     ext : 1 <;> assumption
   have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by
@@ -290,7 +290,7 @@ namespace Semiring
     ext : 1; exact h_mul
   -- Split into fields and prove they are equal using the above.
   cases inst₁; cases inst₂
-  congr <;> solve | injection h₁ | injection h₂
+  congr; solve | injection h₁ | injection h₂
 
 theorem toNonUnitalSemiring_injective :
     Function.Injective (@toNonUnitalSemiring R) := by
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean b/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean
index 994a2c97d78546..b82d471bf69a82 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean
@@ -6,7 +6,7 @@ Authors: Kim Morrison, Johannes Hölzl, Reid Barton, Sean Leather
 module
 
 public import Mathlib.Init
-public import Batteries.Tactic.Lint.Misc
+public import Batteries.Linter.Misc
 
 /-!
 # Bundled types
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index 7934ab8744cd87..076714a9ed15b2 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -11,7 +11,7 @@ public import Mathlib.Logic.OpClass
 public import Mathlib.Logic.Unique
 public import Mathlib.Tactic.Common
 public import Batteries.Data.List.Lemmas
-public import Batteries.Tactic.Lint.Simp
+public import Batteries.Linter.Simp
 public import Batteries.Tactic.SeqFocus
 public import Mathlib.Data.Subtype
 public import Mathlib.Tactic.Attr.Core
diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
index d77363c4f50ddc..a12e2e0110fd11 100644
--- a/Mathlib/Data/List/Defs.lean
+++ b/Mathlib/Data/List/Defs.lean
@@ -9,7 +9,7 @@ public import Mathlib.Data.Nat.Notation
 public import Mathlib.Control.Functor
 public import Mathlib.Data.SProd
 public import Mathlib.Util.CompileInductive
-public import Batteries.Tactic.Lint.Basic
+public import Batteries.Linter.Basic
 public import Batteries.Data.List.Basic
 public import Batteries.Logic
 
diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean
index e66b8f9b8b3ef2..b6f4f663e78ebe 100644
--- a/Mathlib/Data/Option/Basic.lean
+++ b/Mathlib/Data/Option/Basic.lean
@@ -11,7 +11,7 @@ public import Mathlib.Logic.IsEmpty.Basic
 public import Mathlib.Logic.Relator
 public import Mathlib.Util.CompileInductive
 public import Aesop
-public import Batteries.Tactic.Lint.Simp
+public import Batteries.Linter.Simp
 
 /-!
 # Option of a type
diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
index 07b1fbbd784efd..57a6d36bf25a70 100644
--- a/Mathlib/Data/Seq/Computation.lean
+++ b/Mathlib/Data/Seq/Computation.lean
@@ -9,7 +9,7 @@ public import Mathlib.Data.Nat.Find
 public import Mathlib.Data.Stream.Init
 public import Mathlib.Logic.Relator
 public import Mathlib.Tactic.Common
-public import Batteries.Tactic.Lint.Simp
+public import Batteries.Linter.Simp
 
 /-!
 # Coinductive formalization of unbounded computations.
diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
index e49829ccc5766f..895c4d49541cf3 100644
--- a/Mathlib/Init.lean
+++ b/Mathlib/Init.lean
@@ -35,7 +35,7 @@ public import Batteries.Util.ProofWanted
 -- This import makes the `#redundant_imports`/`#min_imports`/`#find_home`/`#import_diff` commands
 -- available globally.
 public import ImportGraph.Tools
--- The following module imports `Batteries.Tactic.Lint`, where `#lint` is defined.
+-- The following module imports `Batteries.Linter`, where `#lint` is defined.
 public import Mathlib.Tactic.Linter.Lint
 -- This import makes the `#min_imports in` command available globally.
 public import Mathlib.Tactic.MinImports
diff --git a/Mathlib/Lean/Elab/InfoTree.lean b/Mathlib/Lean/Elab/InfoTree.lean
index cca33050a3b0e2..51677f36b27c13 100644
--- a/Mathlib/Lean/Elab/InfoTree.lean
+++ b/Mathlib/Lean/Elab/InfoTree.lean
@@ -8,11 +8,11 @@ module
 public import Mathlib.Lean.Environment
 public import Lean.Server.InfoUtils
 public import Lean.Meta.TryThis
-public import Batteries.Tactic.Lint.Misc
+public import Batteries.Linter.Misc
 -- Import this linter explicitly to ensure that
 -- this file has a valid copyright header and module docstring.
 import Mathlib.Tactic.Linter.Header  -- shake: keep
-public import Batteries.Tactic.Lint.Basic
+public import Batteries.Linter.Basic
 import Lean.Elab.Term.TermElabM
 
 /-!
diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean
index 970c56cfded6fc..e89fcda0ca58f5 100644
--- a/Mathlib/SetTheory/Lists.lean
+++ b/Mathlib/SetTheory/Lists.lean
@@ -9,7 +9,7 @@ public import Mathlib.Algebra.Order.Group.Nat
 public import Mathlib.Algebra.Order.Monoid.NatCast
 public import Mathlib.Algebra.Ring.Nat
 public import Mathlib.Data.Sigma.Basic
-public import Batteries.Tactic.Lint.TypeClass
+public import Batteries.Linter.TypeClass
 
 /-!
 # A computable model of ZFA without infinity
diff --git a/Mathlib/Tactic/CategoryTheory/Elementwise.lean b/Mathlib/Tactic/CategoryTheory/Elementwise.lean
index 344e463d0a2a72..787cfc63c0e8f4 100644
--- a/Mathlib/Tactic/CategoryTheory/Elementwise.lean
+++ b/Mathlib/Tactic/CategoryTheory/Elementwise.lean
@@ -91,7 +91,7 @@ def elementwiseExpr (src : Name) (pf : Expr) (simpSides := true) :
         -- check that it's not a simp-trivial equality:
         forallTelescope ty' fun _ ty' => do
           if let some (_, lhs, rhs) := ty'.eq? then
-            if ← Batteries.Tactic.Lint.isSimpEq lhs rhs then
+            if ← Batteries.Linter.isSimpEq lhs rhs then
               throwError "applying simp to both sides reduces elementwise lemma for {src} \
                 to the trivial equality {ty'}. \
                 Either add `nosimp` or remove the `elementwise` attribute."
diff --git a/Mathlib/Tactic/Linarith/Lemmas.lean b/Mathlib/Tactic/Linarith/Lemmas.lean
index c44b8b9b4d45d3..cd0f7897013b4d 100644
--- a/Mathlib/Tactic/Linarith/Lemmas.lean
+++ b/Mathlib/Tactic/Linarith/Lemmas.lean
@@ -5,7 +5,7 @@ Authors: Robert Y. Lewis
 -/
 module
 
-public meta import Batteries.Tactic.Lint.Basic
+public meta import Batteries.Linter.Basic
 public meta import Mathlib.Data.Ineq
 public import Mathlib.Data.Ineq
 public import Mathlib.Data.Nat.Cast.Order.Ring
diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean
index 4fae86eecdf634..0110d5bb76f5a5 100644
--- a/Mathlib/Tactic/Linter/DirectoryDependency.lean
+++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean
@@ -182,7 +182,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[
   -- TODO: reduce this dependency by upstreaming `Data.String.Defs to batteries
   (`Mathlib.Util.FormatTable, `Mathlib.Data.String.Defs),
 
-  (`Mathlib.Lean, `Batteries.Tactic.Lint),
+  (`Mathlib.Lean, `Batteries.Linter),
   (`Mathlib.Lean, `Batteries.CodeAction),
   -- TODO: should this be minimised further?
   (`Mathlib.Lean.Meta.CongrTheorems, `Batteries),
diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean
index 1b1bd995958ab8..2ac8670edfff11 100644
--- a/Mathlib/Tactic/Linter/Lint.lean
+++ b/Mathlib/Tactic/Linter/Lint.lean
@@ -5,13 +5,13 @@ Authors: Floris van Doorn
 -/
 module
 
--- This module imports all of `Batteries.Tactic.Lint`, not just `Batteries.Tactic.Lint.Basic`.
+-- This module imports all of `Batteries.Linter`, not just `Batteries.Linter.Basic`.
 -- It is responsible for making `#lint` available through `Mathlib.Init`.
 -- TODO: consider removing `-- shake: keep` after batteries#1613
-public import Batteries.Tactic.Lint -- shake: keep
+public import Batteries.Linter -- shake: keep
 public import Lean.Linter.Deprecated
 public import Mathlib.Tactic.DeclarationNames
-public import Batteries.Tactic.Lint.Basic
+public import Batteries.Linter.Basic
 
 /-!
 # Linters for Mathlib
@@ -24,7 +24,7 @@ Perhaps these should be moved to Batteries in the future.
 
 meta section
 
-namespace Batteries.Tactic.Lint
+namespace Batteries.Linter
 open Lean Meta
 
 /--
@@ -56,7 +56,7 @@ Linter that checks whether a structure should be in Prop.
     | some _ => return none -- TODO: enforce `YYYY-MM-DD` format
     | none => return m!"`deprecated` attribute without `since` date"
 
-end Batteries.Tactic.Lint
+end Batteries.Linter
 
 namespace Mathlib.Linter
 
diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
index d949f89d541593..3f4d2729220c5a 100644
--- a/Mathlib/Tactic/Linter/Style.lean
+++ b/Mathlib/Tactic/Linter/Style.lean
@@ -12,7 +12,7 @@ public meta import Lean.Server.InfoUtils
 public meta import Mathlib.Tactic.Linter.Header  -- shake: keep
 public import Lean.Parser.Command
 public import Mathlib.Tactic.DeclarationNames
-public import Batteries.Tactic.Lint.Basic
+public import Batteries.Linter.Basic
 
 /-!
 ## Style linters
@@ -551,10 +551,10 @@ public def isBadNameWithUnderscore (name : Name) : Bool := Id.run do
   if declName.toString.contains "_" then return true
   else return false
 
-open Batteries.Tactic.Lint in
+open Batteries.Linter in
 /-- Linter that checks for definitions whose name contains an underscore:
 such names violate the naming convention. -/
-@[env_linter] public def defsWithUnderscore : Batteries.Tactic.Lint.Linter where
+@[env_linter] public def defsWithUnderscore : Batteries.Linter where
   noErrorsFound := "no definitions with an underscore in their name found."
   errorsFound := "FOUND definitions with an underscore in their name."
   test declName := do
diff --git a/Mathlib/Tactic/Linter/TacticDocumentation.lean b/Mathlib/Tactic/Linter/TacticDocumentation.lean
index bd0874afb9d480..47bb3ec20858a7 100644
--- a/Mathlib/Tactic/Linter/TacticDocumentation.lean
+++ b/Mathlib/Tactic/Linter/TacticDocumentation.lean
@@ -10,7 +10,7 @@ public meta import Lean.Parser.Tactic.Doc
 -- Import this linter explicitly to ensure that
 -- this file has a valid copyright header and module docstring.
 public import Mathlib.Tactic.Linter.Header  -- shake: keep
-public import Batteries.Tactic.Lint.Basic
+public import Batteries.Linter.Basic
 public import Lean.Elab.Tactic.Doc
 
 /-! # The `tacticDocs` linter
@@ -28,7 +28,7 @@ meta def isNonemptyDoc (doc : TacticDoc) : Bool :=
   doc.docString.isSome || doc.extensionDocs.any (! ·.isEmpty)
 
 /-- Check that all tactics available in Mathlib have a docstring. -/
-@[env_linter] public meta def tacticDocs : Batteries.Tactic.Lint.Linter where
+@[env_linter] public meta def tacticDocs : Batteries.Linter where
   noErrorsFound := "No tactics are missing documentation."
   errorsFound := "TACTICS ARE MISSING DOCUMENTATION STRINGS:"
   test tac := do
diff --git a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean
index 4a6ec648aff168..c7bf5d91c76784 100644
--- a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean
+++ b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean
@@ -12,8 +12,8 @@ public meta import Lean.Linter.Basic
 -- Import this linter explicitly to ensure that
 -- this file has a valid copyright header and module docstring.
 public import Mathlib.Tactic.Linter.Header  -- shake: keep
-public import Batteries.Tactic.Lint.Basic
-public import Batteries.Tactic.Lint.Misc
+public import Batteries.Linter.Basic
+public import Batteries.Linter.Misc
 
 /-!
 # Linters for Unused Instances in Types
diff --git a/MathlibTest/BasicFiles/Init.lean b/MathlibTest/BasicFiles/Init.lean
index 94acda24214958..4b620f666d39d5 100644
--- a/MathlibTest/BasicFiles/Init.lean
+++ b/MathlibTest/BasicFiles/Init.lean
@@ -1,6 +1,7 @@
 module
 
 import Mathlib.Init
+import Batteries.Linter.Frontend
 
 /-! Checks that some utilities are available already when importing `Mathlib.Init`. -/
 
@@ -33,7 +34,8 @@ import Mathlib.Init
 proof_wanted please_prove_this : True
 
 -- Guard against the shake tool modifying our imports
-/-- info: [public import Init, public meta import Init, import Mathlib.Init] -/
+/-- info: [public import Init, public meta import Init, import Mathlib.Init,
+import Batteries.Linter.Frontend] -/
 #guard_msgs in
 run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}"
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 5ebacc94fd75e7..ca2572e91a4db2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7d1b02eb63b526dff04cb990cf05b06b38ccbd3f",
+   "rev": "c35ff55997866abfddeb272c3a293f941fb37f65",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "move-class-linter",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.lean b/lakefile.lean
index a4808f93fdd2c0..781efadbeb5485 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,10 +6,10 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "main"
-require "leanprover-community" / "Qq" @ git "master"
-require "leanprover-community" / "aesop" @ git "master"
-require "leanprover-community" / "proofwidgets" @ git "main"
+require "leanprover-community" / "batteries" from git "https://github.com/leanprover-community/batteries" @ "move-class-linter"
+require "leanprover-community" / "Qq" @ git "v4.31.0-rc1"
+require "leanprover-community" / "aesop" @ git "v4.31.0-rc1"
+require "leanprover-community" / "proofwidgets" @ git "v0.0.100"
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets failed to reuse pre-built JS code. \
     Please report this issue on the Lean Zulip."
diff --git a/scripts/noshake.json b/scripts/noshake.json
index b2d50ab4febb68..80bec325ccffc7 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -13,8 +13,8 @@
   "Batteries.Tactic.GuardMsgs",
   "Batteries.Tactic.HaveI",
   "Batteries.Tactic.LeftRight",
-  "Batteries.Tactic.Lint",
-  "Batteries.Tactic.Lint.Misc",
+  "Batteries.Linter",
+  "Batteries.Linter.Misc",
   "Batteries.Tactic.NoMatch",
   "Batteries.Tactic.NormCast",
   "Batteries.Tactic.NormCast.Lemmas",