diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean
index 4cd548c995..f540dcde4e 100644
--- a/src/Init/Grind/Config.lean
+++ b/src/Init/Grind/Config.lean
@@ -18,9 +18,9 @@ structure Config where
   /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
   or for which no patterns can be generated. -/
   lax : Bool := false
-  /-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
-  and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
-  premises : Bool := false
+  /-- If `suggestions` is `true`, `grind` will invoke the currently configured library suggestion engine on the current goal,
+  and add attempt to use the resulting suggestions as additional parameters to the `grind` tactic. -/
+  suggestions : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
   splits : Nat := 9
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 504b1ede61..1d9b67e751 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -863,12 +863,12 @@ syntax (name := infoTreesCmd)
   "#info_trees" " in" ppLine command : command
 
 /--
-Specify a premise selection engine.
-Note that Lean does not ship a default premise selection engine,
+Specify a library suggestion engine.
+Note that Lean does not ship a default library suggestion engine,
 so this is only useful in conjunction with a downstream package which provides one.
 -/
-syntax (name := setPremiseSelectorCmd)
-  "set_premise_selector" term : command
+syntax (name := setLibrarySuggestionsCmd)
+  "set_library_suggestions" term : command
 
 namespace Parser
 
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index a652186103..04013cd5e3 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1759,11 +1759,12 @@ as well as tactics such as `next`, `case`, and `rename_i`.
 syntax (name := exposeNames) "expose_names" : tactic
 
 /--
-`#suggest_premises` will suggest premises for the current goal, using the currently registered premise selector.
+`#suggestions` will suggest relevant theorems from the library for the current goal,
+using the currently registered library suggestion engine.
 
 The suggestions are printed in the order of their confidence, from highest to lowest.
 -/
-syntax (name := suggestPremises) "suggest_premises" : tactic
+syntax (name := suggestions) "suggestions" : tactic
 
 /--
 Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
diff --git a/src/Lean.lean b/src/Lean.lean
index bf561cb653..c708d08fb7 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -40,7 +40,7 @@ public import Lean.LabelAttribute
 public import Lean.AddDecl
 public import Lean.Replay
 public import Lean.PrivateName
-public import Lean.PremiseSelection
+public import Lean.LibrarySuggestions
 public import Lean.Namespace
 public import Lean.EnvExtension
 public import Lean.ErrorExplanation
diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
index a252093241..cceb049932 100644
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Main
 public import Lean.Meta.Tactic.TryThis
 public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Config
-public import Lean.PremiseSelection.Basic
+public import Lean.LibrarySuggestions.Basic
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
@@ -77,11 +77,11 @@ private def parseModifier (s : String) : CoreM Grind.AttrKind := do
   | .ok stx => Grind.getAttrKindCore stx
   | _ => throwError "unexpected modifier {s}"
 
-open PremiseSelection in
-def elabGrindPremises
-    (params : Grind.Params) (premises : Array Suggestion := #[]) : MetaM Grind.Params := do
+open LibrarySuggestions in
+def elabGrindSuggestions
+    (params : Grind.Params) (suggestions : Array Suggestion := #[]) : MetaM Grind.Params := do
   let mut params := params
-  for p in premises do
+  for p in suggestions do
     let attr ← match p.flag with
     | some flag => parseModifier flag
     | none => pure <| .ematch (.default false)
@@ -89,23 +89,23 @@ def elabGrindPremises
     | .ematch kind =>
       try
         params ← addEMatchTheorem params (mkIdent p.name) p.name kind false (warn := false)
-      catch _ => pure () -- Don't worry if premise suggestion gave bad suggestions.
+      catch _ => pure () -- Don't worry if library suggestions gave bad theorems.
     | _ =>
       -- We could actually support arbitrary grind modifiers,
       -- and call `processParam` rather than `addEMatchTheorem`,
       -- but this would require a larger refactor.
-      -- Let's only do this if there is a prospect of a premise selector supporting this.
+      -- Let's only do this if there is a prospect of a library suggestion engine supporting this.
       throwError "unexpected modifier {p.flag}"
   return params
 
-open PremiseSelection in
-def elabGrindParamsAndPremises
+open LibrarySuggestions in
+def elabGrindParamsAndSuggestions
     (params : Grind.Params)
     (ps : TSyntaxArray ``Parser.Tactic.grindParam)
-    (premises : Array Suggestion := #[])
+    (suggestions : Array Suggestion := #[])
     (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do
   let params ← elabGrindParams params ps (lax := lax) (only := only)
-  elabGrindPremises params premises
+  elabGrindSuggestions params suggestions
 
 def mkGrindParams
     (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) :
@@ -119,12 +119,11 @@ def mkGrindParams
   -/
   let casesTypes ← Grind.getCasesTypes
   let params := { params with ematch, casesTypes, inj }
-  let premises ← if config.premises then
-    let suggestions ← PremiseSelection.select mvarId
-    pure suggestions
+  let suggestions ← if config.suggestions then
+    LibrarySuggestions.select mvarId
   else
     pure #[]
-  let params ← elabGrindParamsAndPremises params ps premises (only := only) (lax := config.lax)
+  let params ← elabGrindParamsAndSuggestions params ps suggestions (only := only) (lax := config.lax)
   trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
   return params
 
@@ -201,16 +200,16 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
-/-- Filter out `+premises` from the config syntax -/
-def filterPremisesFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
+/-- Filter out `+suggestions` from the config syntax -/
+def filterSuggestionsFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
   let configItems := config.raw.getArgs
   let filteredItems := configItems.filter fun item =>
-    -- Keep all items except +premises
+    -- Keep all items except +suggestions
     -- Structure: null node -> configItem -> posConfigItem -> ["+", ident]
     match item[0]? with
     | some configItem => match configItem[0]? with
       | some posConfigItem => match posConfigItem[1]? with
-        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `premises)
+        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `suggestions)
         | none => true
       | none => true
     | none => true
@@ -232,7 +231,7 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  let filteredConfig := filterPremisesFromConfig config
+  let filteredConfig := filterSuggestionsFromConfig config
   let result ← `(tactic| grind $filteredConfig:optConfig only)
   return setGrindParams result params
 
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index 6cc667778e..d73715be31 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -673,7 +673,7 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
 
 -- TODO: vanilla `induction`.
 -- TODO: make it extensible.
--- TODO: premise selection.
+-- TODO: library suggestions.
 
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
   match stx with
diff --git a/src/Lean/PremiseSelection.lean b/src/Lean/LibrarySuggestions.lean
similarity index 50%
rename from src/Lean/PremiseSelection.lean
rename to src/Lean/LibrarySuggestions.lean
index bc6af08a22..d187fb9d27 100644
--- a/src/Lean/PremiseSelection.lean
+++ b/src/Lean/LibrarySuggestions.lean
@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Lean.PremiseSelection.Basic
-import Lean.PremiseSelection.SymbolFrequency
-import Lean.PremiseSelection.MePo
-import Lean.PremiseSelection.SineQuaNon
+import Lean.LibrarySuggestions.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
+import Lean.LibrarySuggestions.MePo
+import Lean.LibrarySuggestions.SineQuaNon
diff --git a/src/Lean/PremiseSelection/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
similarity index 83%
rename from src/Lean/PremiseSelection/Basic.lean
rename to src/Lean/LibrarySuggestions/Basic.lean
index 5efeeef304..c6dcc493fa 100644
--- a/src/Lean/PremiseSelection/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -12,19 +12,20 @@ public import Lean.Meta.CompletionName
 public import Init.Data.Random
 
 /-!
-# An API for premise selection algorithms.
+# An API for library suggestion algorithms.
 
-This module provides a basic API for premise selection algorithms,
-which are used to suggest identifiers that should be introduced in a proof.
+This module provides a basic API for library suggestion algorithms,
+which are used to suggest relevant theorems from the library for the current goal.
+In the literature this is usually known as "premise selection",
+but we mostly avoid that term as most of our users will not be familiar with the term.
 
 The core interface is the `Selector` type, which is a function from a metavariable
 and a configuration to a list of suggestions.
+The `Selector` is registered as an environment extension,
+and the trivial (no suggestions) implementation is `Lean.LibrarySuggestions.empty`.
 
-The `Selector` is registered as an environment extension, and the trivial (no suggestions) implementation
-is `Lean.PremiseSelection.empty`.
-
-Lean does not provide a default premise selector, so this module is intended to be used in conjunction
-with a downstream package which registers a premise selector.
+Lean does not provide a default library suggestion engine, so this module is intended to be used in conjunction
+with a downstream package which registers a library suggestion engine.
 -/
 
 namespace Lean.Expr.FoldRelevantConstantsImpl
@@ -113,7 +114,7 @@ public def Lean.MVarId.getRelevantConstants (g : MVarId) : MetaM NameSet := with
 
 @[expose] public section
 
-namespace Lean.PremiseSelection
+namespace Lean.LibrarySuggestions
 
 /--
 A `Suggestion` is essentially just an identifier and a confidence score that the identifier is relevant.
@@ -285,52 +286,52 @@ def random (gen : StdGen := ⟨37, 59⟩) : Selector := fun _ cfg => do
       suggestions := suggestions.push { name := name, score := 1.0 / consts.size.toFloat }
   return suggestions
 
-builtin_initialize premiseSelectorExt : EnvExtension (Option Selector) ←
+builtin_initialize librarySuggestionsExt : EnvExtension (Option Selector) ←
   registerEnvExtension (pure none)
 
-/-- Generate premise suggestions for the given metavariable, using the currently registered premise selector. -/
+/-- Generate library suggestions for the given metavariable, using the currently registered library suggestions engine. -/
 def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
-  let some selector := premiseSelectorExt.getState (← getEnv) |
-    throwError "No premise selector registered. \
-      (Note that Lean does not provide a default premise selector, \
+  let some selector := librarySuggestionsExt.getState (← getEnv) |
+    throwError "No library suggestions engine registered. \
+      (Note that Lean does not provide a default library suggestions engine, \
       these must be provided by a downstream library, \
-      and configured using `set_premise_selector`.)"
+      and configured using `set_library_suggestions`.)"
   selector m c
 
 /-!
 Currently the registration mechanism is just global state.
-This means that if multiple modules register premise selectors,
+This means that if multiple modules register library suggestions engines,
 the behaviour will be dependent on the order of loading modules.
 
 We should replace this with a mechanism so that
-premise selectors are configured via options in the `lakefile`, and
+library suggestions engines are configured via options in the `lakefile`, and
 commands are only used to override in a single declaration or file.
 -/
 
-/-- Set the current premise selector.-/
-def registerPremiseSelector (selector : Selector) : CoreM Unit := do
-  modifyEnv fun env => premiseSelectorExt.setState env (some selector)
+/-- Set the current library suggestions engine.-/
+def registerLibrarySuggestions (selector : Selector) : CoreM Unit := do
+  modifyEnv fun env => librarySuggestionsExt.setState env (some selector)
 
 open Lean Elab Command in
-@[builtin_command_elab setPremiseSelectorCmd, inherit_doc setPremiseSelectorCmd]
-def elabSetPremiseSelector : CommandElab
-  | `(command| set_premise_selector $selector) => do
-    if `Lean.PremiseSelection.Basic ∉ (← getEnv).header.moduleNames then
-      logWarning "Add `import Lean.PremiseSelection.Basic` before using the `set_premise_selector` command."
+@[builtin_command_elab setLibrarySuggestionsCmd, inherit_doc setLibrarySuggestionsCmd]
+def elabSetLibrarySuggestions : CommandElab
+  | `(command| set_library_suggestions $selector) => do
+    if `Lean.LibrarySuggestions.Basic ∉ (← getEnv).header.moduleNames then
+      logWarning "Add `import Lean.LibrarySuggestions.Basic` before using the `set_library_suggestions` command."
     let selector ← liftTermElabM do
       try
         let selectorTerm ← Term.elabTermEnsuringType selector (some (Expr.const ``Selector []))
         unsafe Meta.evalExpr Selector (Expr.const ``Selector []) selectorTerm
       catch _ =>
         throwError "Failed to elaborate {selector} as a `MVarId → Config → MetaM (Array Suggestion)`."
-    liftCoreM (registerPremiseSelector selector)
+    liftCoreM (registerLibrarySuggestions selector)
   | _ => throwUnsupportedSyntax
 
 open Lean.Elab.Tactic in
-@[builtin_tactic Lean.Parser.Tactic.suggestPremises] def evalSuggestPremises : Tactic := fun _ =>
+@[builtin_tactic Lean.Parser.Tactic.suggestions] def evalSuggestions : Tactic := fun _ =>
   liftMetaTactic1 fun mvarId => do
     let suggestions ← select mvarId
-    logInfo m!"Premise suggestions: {suggestions.map (·.name)}"
+    logInfo m!"Library suggestions: {suggestions.map (·.name)}"
     return mvarId
 
-end Lean.PremiseSelection
+end Lean.LibrarySuggestions
diff --git a/src/Lean/PremiseSelection/MePo.lean b/src/Lean/LibrarySuggestions/MePo.lean
similarity index 96%
rename from src/Lean/PremiseSelection/MePo.lean
rename to src/Lean/LibrarySuggestions/MePo.lean
index 531afca6ab..d4ad7859ec 100644
--- a/src/Lean/PremiseSelection/MePo.lean
+++ b/src/Lean/LibrarySuggestions/MePo.lean
@@ -6,8 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Lean.PremiseSelection.Basic
-import Lean.PremiseSelection.SymbolFrequency
+public import Lean.LibrarySuggestions.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
 import Lean.Meta.Basic
 
 /-!
@@ -21,7 +21,7 @@ It needs to be tuned and evaluated for Lean.
 
 open Lean
 
-namespace Lean.PremiseSelection.MePo
+namespace Lean.LibrarySuggestions.MePo
 
 builtin_initialize registerTraceClass `mepo
 
diff --git a/src/Lean/PremiseSelection/SineQuaNon.lean b/src/Lean/LibrarySuggestions/SineQuaNon.lean
similarity index 98%
rename from src/Lean/PremiseSelection/SineQuaNon.lean
rename to src/Lean/LibrarySuggestions/SineQuaNon.lean
index a8ca7521da..9100abcde2 100644
--- a/src/Lean/PremiseSelection/SineQuaNon.lean
+++ b/src/Lean/LibrarySuggestions/SineQuaNon.lean
@@ -9,8 +9,8 @@ prelude
 public import Lean.CoreM
 public import Lean.Meta.Basic
 import Lean.Meta.Instances
-import Lean.PremiseSelection.SymbolFrequency
-public import Lean.PremiseSelection.Basic
+import Lean.LibrarySuggestions.SymbolFrequency
+public import Lean.LibrarySuggestions.Basic
 
 /-!
 # Sine Qua Non premise selection
@@ -21,7 +21,7 @@ This is an implementation of the "Sine Qua Non" premise selection algorithm, fro
 It needs to be tuned and evaluated for Lean.
 -/
 
-namespace Lean.PremiseSelection.SineQuaNon
+namespace Lean.LibrarySuggestions.SineQuaNon
 
 builtin_initialize registerTraceClass `sineQuaNon
 
@@ -193,4 +193,4 @@ public def sineQuaNonSelector (depthFactor : Float := 1.5) : Selector := fun g c
   let suggestions ← sineQuaNon constants config.maxSuggestions depthFactor
   return suggestions.take config.maxSuggestions
 
-end Lean.PremiseSelection
+end Lean.LibrarySuggestions
diff --git a/src/Lean/PremiseSelection/SymbolFrequency.lean b/src/Lean/LibrarySuggestions/SymbolFrequency.lean
similarity index 98%
rename from src/Lean/PremiseSelection/SymbolFrequency.lean
rename to src/Lean/LibrarySuggestions/SymbolFrequency.lean
index 3290c4e359..1b40938066 100644
--- a/src/Lean/PremiseSelection/SymbolFrequency.lean
+++ b/src/Lean/LibrarySuggestions/SymbolFrequency.lean
@@ -11,7 +11,7 @@ public import Lean.Meta.Basic
 import Lean.Meta.InferType
 import Lean.Meta.FunInfo
 import Lean.AddDecl
-import Lean.PremiseSelection.Basic
+import Lean.LibrarySuggestions.Basic
 
 /-!
 # Symbol frequency
@@ -19,7 +19,7 @@ import Lean.PremiseSelection.Basic
 This module provides a persistent environment extension for computing the frequency of symbols in the environment.
 -/
 
-namespace Lean.PremiseSelection
+namespace Lean.LibrarySuggestions
 
 /--
 Collect the frequencies for constants occurring in declarations defined in the current module,
diff --git a/tests/lean/run/grind_question_mark_premises.lean b/tests/lean/run/grind_question_mark_premises.lean
deleted file mode 100644
index a329bf8cd3..0000000000
--- a/tests/lean/run/grind_question_mark_premises.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import Lean
-
-set_premise_selector Lean.PremiseSelection.sineQuaNonSelector
-
--- Test that grind? +premises does NOT include +premises in its output
-/--
-info: Try this:
-  [apply] grind only
--/
-#guard_msgs in
-example {x y : Nat} (h : x = y) : y = x := by
-  grind? +premises
diff --git a/tests/lean/run/grind_question_mark_suggestions.lean b/tests/lean/run/grind_question_mark_suggestions.lean
new file mode 100644
index 0000000000..9568a6a2ce
--- /dev/null
+++ b/tests/lean/run/grind_question_mark_suggestions.lean
@@ -0,0 +1,12 @@
+import Lean
+
+set_library_suggestions Lean.LibrarySuggestions.sineQuaNonSelector
+
+-- Test that grind? +suggestions does NOT include +suggestions in its output
+/--
+info: Try this:
+  [apply] grind only
+-/
+#guard_msgs in
+example {x y : Nat} (h : x = y) : y = x := by
+  grind? +suggestions
diff --git a/tests/lean/run/grind_premises.lean b/tests/lean/run/grind_suggestions.lean
similarity index 54%
rename from tests/lean/run/grind_premises.lean
rename to tests/lean/run/grind_suggestions.lean
index d623be5ae5..36eb16bdde 100644
--- a/tests/lean/run/grind_premises.lean
+++ b/tests/lean/run/grind_suggestions.lean
@@ -1,17 +1,17 @@
-import Lean.PremiseSelection.Basic
+import Lean.LibrarySuggestions.Basic
 
 /--
-error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_premise_selector`.)
+error: No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
 -/
 #guard_msgs in
 example : True := by
-  grind +premises
+  grind +suggestions
 
-set_premise_selector (fun _ _ => pure #[])
+set_library_suggestions (fun _ _ => pure #[])
 
 #guard_msgs in
 example : True := by
-  grind +premises
+  grind +suggestions
 
 def P (_ : Nat) := True
 theorem p : P 7 := trivial
@@ -34,23 +34,23 @@ example : P 37 := by
 example : P 7 := by
   grind [p]
 
-set_premise_selector (fun _ _ => pure #[{ name := `p, score := 1.0 }])
+set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 1.0 }])
 
 example : P 7 := by
-  grind +premises
+  grind +suggestions
 
-set_premise_selector (fun _ _ => pure #[{ name := `List.append_assoc, score := 1.0 }])
+set_library_suggestions (fun _ _ => pure #[{ name := `List.append_assoc, score := 1.0 }])
 
 -- Make sure there is no warning about the redundant theorem.
 #guard_msgs in
 example (x y z : List Nat) : x ++ (y ++ z) = (x ++ y) ++ z := by
-  grind +premises
+  grind +suggestions
 
 theorem f : True := trivial
 
-set_premise_selector (fun _ _ => pure #[{ name := `f, score := 1.0 }])
+set_library_suggestions (fun _ _ => pure #[{ name := `f, score := 1.0 }])
 
 -- Make sure that bad suggestions (e.g. not patterns) from premise selection are dropped silently.
 #guard_msgs in
 example (x y z : List Nat) : x ++ (y ++ z) = (x ++ y) ++ z := by
-  grind +premises
+  grind +suggestions
diff --git a/tests/lean/run/library_suggestions.lean b/tests/lean/run/library_suggestions.lean
new file mode 100644
index 0000000000..e3ab1b5cb6
--- /dev/null
+++ b/tests/lean/run/library_suggestions.lean
@@ -0,0 +1,39 @@
+import Lean.LibrarySuggestions
+
+/--
+error: Type mismatch
+  Nat
+has type
+  Type
+of sort `Type 1` but is expected to have type
+  Lean.LibrarySuggestions.Selector
+of sort `Type`
+---
+error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggestion)`.
+-/
+#guard_msgs in
+set_library_suggestions Nat
+
+/--
+error: No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial
+
+set_library_suggestions (fun _ _ => pure #[])
+
+/-- info: Library suggestions: [] -/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial
+
+set_library_suggestions Lean.LibrarySuggestions.random ⟨1,1⟩
+
+-- This would be an extremely fragile test (select 10 random constants!)
+-- so we do not use #guard_msgs.
+example : True := by
+  suggestions
+  trivial
diff --git a/tests/lean/run/library_suggestions_import.lean b/tests/lean/run/library_suggestions_import.lean
new file mode 100644
index 0000000000..8a9e67aa63
--- /dev/null
+++ b/tests/lean/run/library_suggestions_import.lean
@@ -0,0 +1,5 @@
+/--
+warning: Add `import Lean.LibrarySuggestions.Basic` before using the `set_library_suggestions` command.
+-/
+#guard_msgs (warning, drop error) in
+set_library_suggestions (fun _ _ => pure #[])
diff --git a/tests/lean/run/library_suggestions_mepo.lean b/tests/lean/run/library_suggestions_mepo.lean
new file mode 100644
index 0000000000..783096ba55
--- /dev/null
+++ b/tests/lean/run/library_suggestions_mepo.lean
@@ -0,0 +1,21 @@
+import Lean.LibrarySuggestions.MePo
+
+set_library_suggestions Lean.LibrarySuggestions.mepoSelector (useRarity := false)
+
+example (a b : Int) : a + b = b + a := by
+  suggestions
+  sorry
+
+example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
+  suggestions
+  sorry
+
+set_library_suggestions Lean.LibrarySuggestions.mepoSelector (useRarity := true)
+
+example (a b : Int) : a + b = b + a := by
+  suggestions
+  sorry
+
+example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
+  suggestions
+  sorry
diff --git a/tests/lean/run/premise_selection_sine_qua_non.lean b/tests/lean/run/library_suggestions_sine_qua_non.lean
similarity index 84%
rename from tests/lean/run/premise_selection_sine_qua_non.lean
rename to tests/lean/run/library_suggestions_sine_qua_non.lean
index 6c45d7f271..eb63789a70 100644
--- a/tests/lean/run/premise_selection_sine_qua_non.lean
+++ b/tests/lean/run/library_suggestions_sine_qua_non.lean
@@ -1,19 +1,19 @@
 module
-import all Lean.PremiseSelection.SineQuaNon
+import all Lean.LibrarySuggestions.SineQuaNon
 import Lean.Meta.Basic
 import Std.Data.ExtHashMap
 
-open Lean PremiseSelection SineQuaNon
+open Lean LibrarySuggestions SineQuaNon
 
-set_premise_selector Lean.PremiseSelection.sineQuaNonSelector
+set_library_suggestions Lean.LibrarySuggestions.sineQuaNonSelector
 
 example {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x := by
   fail_if_success grind
-  grind +premises
+  grind +suggestions
 
 example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
   fail_if_success grind
-  grind +premises
+  grind +suggestions
 
 /-- info: [(HAppend.hAppend, 1.000000)] -/
 #guard_msgs in
diff --git a/tests/lean/run/premise_selection.lean b/tests/lean/run/premise_selection.lean
deleted file mode 100644
index c1e7c4afd5..0000000000
--- a/tests/lean/run/premise_selection.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import Lean.PremiseSelection
-
-/--
-error: Type mismatch
-  Nat
-has type
-  Type
-of sort `Type 1` but is expected to have type
-  Lean.PremiseSelection.Selector
-of sort `Type`
----
-error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggestion)`.
--/
-#guard_msgs in
-set_premise_selector Nat
-
-/--
-error: No premise selector registered. (Note that Lean does not provide a default premise selector, these must be provided by a downstream library, and configured using `set_premise_selector`.)
--/
-#guard_msgs in
-example : True := by
-  suggest_premises
-  trivial
-
-set_premise_selector (fun _ _ => pure #[])
-
-/-- info: Premise suggestions: [] -/
-#guard_msgs in
-example : True := by
-  suggest_premises
-  trivial
-
-set_premise_selector Lean.PremiseSelection.random ⟨1,1⟩
-
--- This would be an extremely fragile test (select 10 random constants!)
--- so we do not use #guard_msgs.
-example : True := by
-  suggest_premises
-  trivial
diff --git a/tests/lean/run/premise_selection_import.lean b/tests/lean/run/premise_selection_import.lean
deleted file mode 100644
index 424df7fe8f..0000000000
--- a/tests/lean/run/premise_selection_import.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-/--
-warning: Add `import Lean.PremiseSelection.Basic` before using the `set_premise_selector` command.
--/
-#guard_msgs (warning, drop error) in
-set_premise_selector (fun _ _ => pure #[])
diff --git a/tests/lean/run/premise_selection_mepo.lean b/tests/lean/run/premise_selection_mepo.lean
deleted file mode 100644
index 4eb8ed0cf7..0000000000
--- a/tests/lean/run/premise_selection_mepo.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-import Lean.PremiseSelection.MePo
-
-set_premise_selector Lean.PremiseSelection.mepoSelector (useRarity := false)
-
-example (a b : Int) : a + b = b + a := by
-  suggest_premises
-  sorry
-
-example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
-  suggest_premises
-  sorry
-
-set_premise_selector Lean.PremiseSelection.mepoSelector (useRarity := true)
-
-example (a b : Int) : a + b = b + a := by
-  suggest_premises
-  sorry
-
-example (x y z : List Int) : x ++ y ++ z = x ++ (y ++ z) := by
-  suggest_premises
-  sorry
diff --git a/tests/lean/run/symbolFrequency.lean b/tests/lean/run/symbolFrequency.lean
index cf24567383..17794a77ce 100644
--- a/tests/lean/run/symbolFrequency.lean
+++ b/tests/lean/run/symbolFrequency.lean
@@ -1,7 +1,7 @@
 import Lean.Meta.Basic
-import Lean.PremiseSelection.SymbolFrequency
+import Lean.LibrarySuggestions.SymbolFrequency
 
-open Lean PremiseSelection
+open Lean LibrarySuggestions
 
 /-- info: true -/
 #guard_msgs in
diff --git a/tests/lean/run/symbolFrequency_foldRelevantConsts.lean b/tests/lean/run/symbolFrequency_foldRelevantConsts.lean
index c724b32285..c206a6986d 100644
--- a/tests/lean/run/symbolFrequency_foldRelevantConsts.lean
+++ b/tests/lean/run/symbolFrequency_foldRelevantConsts.lean
@@ -1,9 +1,9 @@
 module
 
-import all Lean.PremiseSelection.SymbolFrequency
+import all Lean.LibrarySuggestions.SymbolFrequency
 import all Init.Data.Array.Basic
 
-open Lean PremiseSelection
+open Lean LibrarySuggestions
 
 /-- info: [List, Eq, HAppend.hAppend] -/
 #guard_msgs in