fix: remove unneeded LibrarySearch imports (#3353)

Removes `LibrarySearch` imports that were accidentally included in #2843 and #2361.
leanprover-community · Apr 9, 2023 · 3fb0331 · 3fb0331
1 parent a8db3aa
commit 3fb0331
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 3 deletions.
diff --git a/Mathlib/CategoryTheory/ConnectedComponents.lean b/Mathlib/CategoryTheory/ConnectedComponents.lean
@@ -12,7 +12,6 @@ import Mathlib.Data.List.Chain
 import Mathlib.CategoryTheory.IsConnected
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.FullSubcategory
-import Mathlib.Tactic.LibrarySearch
 
 /-!
 # Connected components of a category

diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean
@@ -15,8 +15,6 @@ import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.Finset.Sym
 import Mathlib.Data.Finsupp.Multiset
 
-import Mathlib.Tactic.LibrarySearch
-
 /-!
 # Multinomial