diff --git a/Mathlib/Algebra/BigOperators/Group/List.lean b/Mathlib/Algebra/BigOperators/Group/List.lean
index a7bbbd486cdf5..08b3745443eb9 100644
--- a/Mathlib/Algebra/BigOperators/Group/List.lean
+++ b/Mathlib/Algebra/BigOperators/Group/List.lean
@@ -9,7 +9,6 @@ import Mathlib.Algebra.Group.Nat
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.Units.Basic
 import Mathlib.Data.List.Perm
-import Mathlib.Data.List.ProdSigma
 import Mathlib.Data.List.Range
 import Mathlib.Data.List.Rotate
 import Mathlib.Data.List.Pairwise
diff --git a/Mathlib/Order/Defs.lean b/Mathlib/Order/Defs.lean
index 75d603ee2c080..14a3cebd9de8f 100644
--- a/Mathlib/Order/Defs.lean
+++ b/Mathlib/Order/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Batteries.Classes.Order
-import Batteries.Tactic.Trans
 import Mathlib.Data.Ordering.Basic
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.SplitIfs
diff --git a/Mathlib/Tactic/Linter/FlexibleLinter.lean b/Mathlib/Tactic/Linter/FlexibleLinter.lean
index ae157b8775b05..f4408bdd14693 100644
--- a/Mathlib/Tactic/Linter/FlexibleLinter.lean
+++ b/Mathlib/Tactic/Linter/FlexibleLinter.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import Lean.Elab.Command
-import Batteries.Data.Array.Basic
 
 /-!
 #  The "flexible" linter