From 4f6fe87330270550634d33b697ee21d8ec11fc43 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 19 Oct 2024 22:30:57 +1100 Subject: [PATCH] shake --- Mathlib/Algebra/BigOperators/Group/List.lean | 1 - Mathlib/Order/Defs.lean | 1 - Mathlib/Tactic/Linter/FlexibleLinter.lean | 1 - 3 files changed, 3 deletions(-) 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