shake

leanprover-community · Oct 19, 2024 · 4f6fe87 · 4f6fe87
1 parent 33407f7
commit 4f6fe87
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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