fix: remove unneeded LibrarySearch import (#3854)

Removes from `Analysis/SpecificLimits/Normed.lean` an `import Mathlib.Tactic.LibrarySearch` that was accidentally included in #3419.
leanprover-community · May 9, 2023 · a2eec64 · a2eec64
1 parent 773a35f
commit a2eec64
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -12,7 +12,6 @@ import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Analysis.Asymptotics.Asymptotics
 import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.Data.List.TFAE
-import Mathlib.Tactic.LibrarySearch
 
 /-!
 # A collection of specific limit computations