shake

leanprover-community · May 6, 2024 · d297310 · d297310
1 parent 3ddddc4
commit d297310
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 4 deletions.
diff --git a/Mathlib/Data/Array/ExtractLemmas.lean b/Mathlib/Data/Array/ExtractLemmas.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Jiecheng Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jiecheng Zhao
 -/
-import Std.Data.Array.Lemmas
 /-!
 # Lemmas about `Array.extract`
 

diff --git a/Mathlib/Data/List/EditDistance/Defs.lean b/Mathlib/Data/List/EditDistance/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Liesinger
 -/
 import Mathlib.Algebra.Group.Defs
-import Std.Data.List.Lemmas
 
 /-!
 # Levenshtein distances

diff --git a/Mathlib/Data/UnionFind.lean b/Mathlib/Data/UnionFind.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Order.LinearOrder
-import Std.Data.Array.Lemmas
 
 set_option autoImplicit true
 

diff --git a/Mathlib/Init/Data/List/Instances.lean b/Mathlib/Init/Data/List/Instances.lean
@@ -3,7 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.List.Lemmas
 import Mathlib.Mathport.Rename
 
 #align_import init.data.list.instances from "leanprover-community/lean"@"9af482290ef68e8aaa5ead01aa7b09b7be7019fd"