diff --git a/Std.lean b/Std.lean
index 84d9780369..2b6980dcf3 100644
--- a/Std.lean
+++ b/Std.lean
@@ -62,6 +62,7 @@ import Std.Lean.Meta.DiscrTree
 import Std.Lean.Meta.Expr
 import Std.Lean.Meta.Inaccessible
 import Std.Lean.Meta.InstantiateMVars
+import Std.Lean.Meta.LazyDiscrTree
 import Std.Lean.Meta.SavedState
 import Std.Lean.Meta.Simp
 import Std.Lean.Meta.UnusedNames
@@ -100,6 +101,7 @@ import Std.Tactic.HaveI
 import Std.Tactic.Instances
 import Std.Tactic.LabelAttr
 import Std.Tactic.LeftRight
+import Std.Tactic.LibrarySearch
 import Std.Tactic.Lint
 import Std.Tactic.Lint.Basic
 import Std.Tactic.Lint.Frontend
diff --git a/Std/Lean/Meta/Basic.lean b/Std/Lean/Meta/Basic.lean
index dac7a2e88a..2229675b26 100644
--- a/Std/Lean/Meta/Basic.lean
+++ b/Std/Lean/Meta/Basic.lean
@@ -457,3 +457,20 @@ def getLocalHyps [Monad m] [MonadLCtx m] : m (Array Expr) := do
   for d in ← getLCtx do
     if !d.isImplementationDetail then hs := hs.push d.toExpr
   return hs
+
+/--
+Given a monadic function `F` that takes a type and a term of that type and produces a new term,
+lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
+and then builds the lambda telescope term for the new term.
+-/
+def mapForallTelescope' (F : Expr → Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
+  forallTelescope (← Meta.inferType forallTerm) fun xs ty => do
+    Meta.mkLambdaFVars xs (← F ty (mkAppN forallTerm xs))
+
+/--
+Given a monadic function `F` that takes a term and produces a new term,
+lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
+and then builds the lambda telescope term for the new term.
+-/
+def mapForallTelescope (F : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
+  mapForallTelescope' (fun _ e => F e) forallTerm
diff --git a/Std/Lean/Meta/LazyDiscrTree.lean b/Std/Lean/Meta/LazyDiscrTree.lean
new file mode 100644
index 0000000000..ab45798e64
--- /dev/null
+++ b/Std/Lean/Meta/LazyDiscrTree.lean
@@ -0,0 +1,881 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix, Scott Morrison
+-/
+
+import Lean.Meta.DiscrTree
+import Std.Data.Nat.Init.Lemmas
+
+/-!
+# Lazy Discrimination Tree
+
+This file defines a new type of discrimination tree optimized for
+rapidly population of imported modules for use in tactics.  It uses a
+lazy initialization strategy.
+
+The discrimination tree can be created through
+`createImportedEnvironment`. This creates a discrimination tree from all
+imported modules in an environment using a callback that provides the
+entries as `InitEntry` values.
+
+The function `getMatch` can be used to get the values that match the
+expression as well as an updated lazy discrimination tree that has
+elaborated additional parts of the tree.
+-/
+namespace Lean.Meta.LazyDiscrTree
+
+-- This namespace contains definitions copied from Lean.Meta.DiscrTree.
+namespace MatchClone
+
+/--
+Discrimination tree key.
+-/
+private inductive Key where
+    /-- Constant -/
+  | const : Name → Nat → Key
+  | fvar  : FVarId → Nat → Key
+  | lit   : Literal → Key
+  | star  : Key
+  | other : Key
+  | arrow : Key
+  | proj  : Name → Nat → Nat → Key
+  deriving Inhabited, BEq, Repr
+
+namespace Key
+
+/-- Hash function -/
+protected def hash : Key → UInt64
+  | .const n a   => mixHash 5237 $ mixHash n.hash (hash a)
+  | .fvar n a    => mixHash 3541 $ mixHash (hash n) (hash a)
+  | .lit v       => mixHash 1879 $ hash v
+  | .star        => 7883
+  | .other       => 2411
+  | .arrow       => 17
+  | .proj s i a  =>  mixHash (hash a) $ mixHash (hash s) (hash i)
+
+instance : Hashable Key := ⟨Key.hash⟩
+
+end Key
+
+private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
+private def tmpStar := mkMVar tmpMVarId
+
+/--
+  Return true iff the argument should be treated as a "wildcard" by the discrimination tree.
+
+  - We ignore proofs because of proof irrelevance. It doesn't make sense to try to
+    index their structure.
+
+  - We ignore instance implicit arguments (e.g., `[Add α]`) because they are "morally" canonical.
+    Moreover, we may have many definitionally equal terms floating around.
+    Example: `Ring.hasAdd Int Int.isRing` and `Int.hasAdd`.
+
+  - We considered ignoring implicit arguments (e.g., `{α : Type}`) since users don't "see" them,
+    and may not even understand why some simplification rule is not firing.
+    However, in type class resolution, we have instance such as `Decidable (@Eq Nat x y)`,
+    where `Nat` is an implicit argument. Thus, we would add the path
+    ```
+    Decidable -> Eq -> * -> * -> * -> [Nat.decEq]
+    ```
+    to the discrimination tree IF we ignored the implicit `Nat` argument.
+    This would be BAD since **ALL** decidable equality instances would be in the same path.
+    So, we index implicit arguments if they are types.
+    This setting seems sensible for simplification theorems such as:
+    ```
+    forall (x y : Unit), (@Eq Unit x y) = true
+    ```
+    If we ignore the implicit argument `Unit`, the `DiscrTree` will say it is a candidate
+    simplification theorem for any equality in our goal.
+
+  Remark: if users have problems with the solution above, we may provide a `noIndexing` annotation,
+  and `ignoreArg` would return true for any term of the form `noIndexing t`.
+-/
+private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
+  if h : i < infos.size then
+    let info := infos.get ⟨i, h⟩
+    if info.isInstImplicit then
+      return true
+    else if info.isImplicit || info.isStrictImplicit then
+      return not (← isType a)
+    else
+      isProof a
+  else
+    isProof a
+
+private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr →
+    MetaM (Array Expr)
+  | i, .app f a, todo => do
+    if (← ignoreArg a i infos) then
+      pushArgsAux infos (i-1) f (todo.push tmpStar)
+    else
+      pushArgsAux infos (i-1) f (todo.push a)
+  | _, _, todo => return todo
+
+/--
+  Return true if `e` is one of the following
+  - A nat literal (numeral)
+  - `Nat.zero`
+  - `Nat.succ x` where `isNumeral x`
+  - `OfNat.ofNat _ x _` where `isNumeral x` -/
+private partial def isNumeral (e : Expr) : Bool :=
+  if e.isNatLit then true
+  else
+    let f := e.getAppFn
+    if !f.isConst then false
+    else
+      let fName := f.constName!
+      if fName == ``Nat.succ && e.getAppNumArgs == 1 then isNumeral e.appArg!
+      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then isNumeral (e.getArg! 1)
+      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then true
+      else false
+
+private partial def toNatLit? (e : Expr) : Option Literal :=
+  if isNumeral e then
+    if let some n := loop e then
+      some (.natVal n)
+    else
+      none
+  else
+    none
+where
+  loop (e : Expr) : OptionT Id Nat := do
+    let f := e.getAppFn
+    match f with
+    | .lit (.natVal n) => return n
+    | .const fName .. =>
+      if fName == ``Nat.succ && e.getAppNumArgs == 1 then
+        let r ← loop e.appArg!
+        return r+1
+      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then
+        loop (e.getArg! 1)
+      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then
+        return 0
+      else
+        failure
+    | _ => failure
+
+private def isNatType (e : Expr) : MetaM Bool :=
+  return (← whnf e).isConstOf ``Nat
+
+/--
+  Return true if `e` is one of the following
+  - `Nat.add _ k` where `isNumeral k`
+  - `Add.add Nat _ _ k` where `isNumeral k`
+  - `HAdd.hAdd _ Nat _ _ k` where `isNumeral k`
+  - `Nat.succ _`
+  This function assumes `e.isAppOf fName`
+-/
+private def isOffset (fName : Name) (e : Expr) : MetaM Bool := do
+  if fName == ``Nat.add && e.getAppNumArgs == 2 then
+    return isNumeral e.appArg!
+  else if fName == ``Add.add && e.getAppNumArgs == 4 then
+    if (← isNatType (e.getArg! 0)) then return isNumeral e.appArg! else return false
+  else if fName == ``HAdd.hAdd && e.getAppNumArgs == 6 then
+    if (← isNatType (e.getArg! 1)) then return isNumeral e.appArg! else return false
+  else
+    return fName == ``Nat.succ && e.getAppNumArgs == 1
+
+/--
+  TODO: add hook for users adding their own functions for controlling `shouldAddAsStar`
+  Different `DiscrTree` users may populate this set using, for example, attributes.
+
+  Remark: we currently tag "offset" terms as star to avoid having to add special
+  support for offset terms.
+  Example, suppose the discrimination tree contains the entry
+  `Nat.succ ?m |-> v`, and we are trying to retrieve the matches for
+  `Expr.lit (Literal.natVal 1) _`.
+  In this scenario, we want to retrieve `Nat.succ ?m |-> v`
+-/
+private def shouldAddAsStar (fName : Name) (e : Expr) : MetaM Bool := do
+  isOffset fName e
+
+/--
+  Try to eliminate loose bound variables by performing beta-reduction.
+  We use this method when processing terms in discrimination trees.
+  These trees distinguish dependent arrows from nondependent ones.
+  Recall that dependent arrows are indexed as `.other`, but nondependent arrows as `.arrow ..`.
+  Motivation: we want to "discriminate" implications and simple arrows in our index.
+
+  Now suppose we add the term `Foo (Nat → Nat)` to our index. The nested arrow appears as
+  `.arrow ..`. Then, suppose we want to check whether the index contains
+  `(x : Nat) → (fun _ => Nat) x`, but it will fail to retrieve `Foo (Nat → Nat)` because
+  it assumes the nested arrow is a dependent one and uses `.other`.
+
+  We use this method to address this issue by beta-reducing terms containing loose bound variables.
+  See issue #2232.
+
+  Remark: we expect the performance impact will be minimal.
+-/
+private def elimLooseBVarsByBeta (e : Expr) : CoreM Expr :=
+  Core.transform e
+    (pre := fun e => do
+      if !e.hasLooseBVars then
+        return .done e
+      else if e.isHeadBetaTarget then
+        return .visit e.headBeta
+      else
+        return .continue)
+
+private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) :
+    MetaM (Key × Array Expr) := do
+  let e ← DiscrTree.reduceDT e root config
+  unless root do
+    -- See pushArgs
+    if let some v := toNatLit? e then
+      return (.lit v, #[])
+  match e.getAppFn with
+  | .lit v         => return (.lit v, #[])
+  | .const c _     =>
+    if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
+      if (← isReducible c) then
+        /- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not
+            unfolded.  This can happen if the metavariables in `e` are "blocking" smart unfolding.
+           If `isDefEqStuckEx` is enabled, then we must throw the `isDefEqStuck` exception to
+           postpone TC resolution.
+           Here is an example. Suppose we have
+           ```
+            inductive Ty where
+              | bool | fn (a ty : Ty)
+
+
+            @[reducible] def Ty.interp : Ty → Type
+              | bool   => Bool
+              | fn a b => a.interp → b.interp
+           ```
+           and we are trying to synthesize `BEq (Ty.interp ?m)`
+        -/
+        Meta.throwIsDefEqStuck
+      else if let some matcherInfo := isMatcherAppCore? (← getEnv) e then
+        -- A matcher application is stuck if one of the discriminants has a metavariable
+        let args := e.getAppArgs
+        let start := matcherInfo.getFirstDiscrPos
+        for arg in args[ start : start + matcherInfo.numDiscrs ] do
+          if arg.hasExprMVar then
+            Meta.throwIsDefEqStuck
+      else if (← isRec c) then
+        /- Similar to the previous case, but for `match` and recursor applications. It may be stuck
+           (i.e., did not reduce) because of metavariables. -/
+        Meta.throwIsDefEqStuck
+    let nargs := e.getAppNumArgs
+    return (.const c nargs, e.getAppRevArgs)
+  | .fvar fvarId   =>
+    let nargs := e.getAppNumArgs
+    return (.fvar fvarId nargs, e.getAppRevArgs)
+  | .mvar mvarId   =>
+    if isMatch then
+      return (.other, #[])
+    else do
+      let ctx ← read
+      if ctx.config.isDefEqStuckEx then
+        /-
+          When the configuration flag `isDefEqStuckEx` is set to true,
+          we want `isDefEq` to throw an exception whenever it tries to assign
+          a read-only metavariable.
+          This feature is useful for type class resolution where
+          we may want to notify the caller that the TC problem may be solvable
+          later after it assigns `?m`.
+          The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`.
+          That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (Add ?m)`
+          where `?m` is a read-only metavariable, and the discrimination tree contains the keys
+          `HadAdd Nat` and `Add Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as
+          a regular metavariable here, otherwise we return the empty set of candidates.
+          This is incorrect because it is equivalent to saying that there is no solution even if
+          the caller assigns `?m` and try again. -/
+        return (.star, #[])
+      else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
+        return (.other, #[])
+      else
+        return (.star, #[])
+  | .proj s i a .. =>
+    let nargs := e.getAppNumArgs
+    return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
+  | .forallE _ d b _ =>
+    -- See comment at elimLooseBVarsByBeta
+    let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
+    if b.hasLooseBVars then
+      return (.other, #[])
+    else
+      return (.arrow, #[d, b])
+  | .bvar _ | .letE _ _ _ _ _ | .lam _ _ _ _ | .mdata _ _ | .app _ _ | .sort _ =>
+    return (.other, #[])
+
+/-
+Given an expression we are looking for patterns that match, return the key and sub-expressions.
+-/
+private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) :
+    MetaM (Key × Array Expr) :=
+  getKeyArgs e (isMatch := true) (root := root) (config := config)
+
+end MatchClone
+
+export MatchClone (Key Key.const)
+
+/--
+An unprocessed entry in the lazy discrimination tree.
+-/
+private abbrev LazyEntry α := Array Expr × ((LocalContext × LocalInstances) × α)
+
+/--
+Index identifying trie in a discrimination tree.
+-/
+@[reducible]
+private def TrieIndex := Nat
+
+/--
+Discrimination tree trie. See `LazyDiscrTree`.
+-/
+private structure Trie (α : Type) where
+  node ::
+    /-- Values for matches ending at this trie. -/
+    values : Array α
+    /-- Index of trie matching star. -/
+    star : TrieIndex
+    /-- Following matches based on key of trie. -/
+    children : HashMap Key TrieIndex
+    /-- Lazy entries at this trie that are not processed. -/
+    pending : Array (LazyEntry α)
+  deriving Inhabited
+
+instance : EmptyCollection (Trie α) := ⟨.node #[] 0 {} #[]⟩
+
+/-- Push lazy entry to trie. -/
+private def Trie.pushPending : Trie α → LazyEntry α → Trie α
+| .node vs star cs p, e => .node vs star cs (p.push e)
+
+end LazyDiscrTree
+
+/--
+`LazyDiscrTree` is a variant of the discriminator tree datatype
+`DiscrTree` in Lean core that is designed to be efficiently
+initializable with a large number of patterns.  This is useful
+in contexts such as searching an entire Lean environment for
+expressions that match a pattern.
+
+Lazy discriminator trees achieve good performance by minimizing
+the amount of work that is done up front to build the discriminator
+tree.  When first adding patterns to the tree, only the root
+discriminator key is computed and processing the remaining
+terms is deferred until demanded by a match.
+-/
+structure LazyDiscrTree (α : Type) where
+  /-- Configuration for normalization. -/
+  config : Lean.Meta.WhnfCoreConfig := {}
+  /-- Backing array of trie entries.  Should be owned by this trie. -/
+  tries : Array (LazyDiscrTree.Trie α) := #[default]
+  /-- Map from discriminator trie roots to the index. -/
+  roots : Lean.HashMap LazyDiscrTree.Key LazyDiscrTree.TrieIndex := {}
+
+namespace LazyDiscrTree
+
+open Lean Elab Meta
+
+instance : Inhabited (LazyDiscrTree α) where
+  default := {}
+
+open Lean.Meta.DiscrTree (mkNoindexAnnotation hasNoindexAnnotation reduceDT)
+
+/--
+Specialization of Lean.Meta.DiscrTree.pushArgs
+-/
+private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) :
+    MetaM (Key × Array Expr) := do
+  if hasNoindexAnnotation e then
+    return (.star, todo)
+  else
+    let e ← reduceDT e root config
+    let fn := e.getAppFn
+    let push (k : Key) (nargs : Nat) (todo : Array Expr) : MetaM (Key × Array Expr) := do
+      let info ← getFunInfoNArgs fn nargs
+      let todo ← MatchClone.pushArgsAux info.paramInfo (nargs-1) e todo
+      return (k, todo)
+    match fn with
+    | .lit v     =>
+      return (.lit v, todo)
+    | .const c _ =>
+      unless root do
+        if let some v := MatchClone.toNatLit? e then
+          return (.lit v, todo)
+        if (← MatchClone.shouldAddAsStar c e) then
+          return (.star, todo)
+      let nargs := e.getAppNumArgs
+      push (.const c nargs) nargs todo
+    | .proj s i a =>
+      /-
+      If `s` is a class, then `a` is an instance. Thus, we annotate `a` with `no_index` since we do
+      not index instances. This should only happen if users mark a class projection function as
+      `[reducible]`.
+
+      TODO: add better support for projections that are functions
+      -/
+      let a := if isClass (← getEnv) s then mkNoindexAnnotation a else a
+      let nargs := e.getAppNumArgs
+      push (.proj s i nargs) nargs (todo.push a)
+    | .fvar _fvarId   =>
+--      let bi ← fvarId.getBinderInfo
+--      if bi.isInstImplicit then
+--        return (.other, todo)
+--      else
+      return (.star, todo)
+    | .mvar mvarId   =>
+      if mvarId == MatchClone.tmpMVarId then
+        -- We use `tmp to mark implicit arguments and proofs
+        return (.star, todo)
+      else
+        failure
+    | .forallE _ d b _ =>
+      -- See comment at elimLooseBVarsByBeta
+      let b ← if b.hasLooseBVars then MatchClone.elimLooseBVarsByBeta b else pure b
+      if b.hasLooseBVars then
+        return (.other, todo)
+      else
+        return (.arrow, (todo.push d).push b)
+    | _ =>
+      return (.other, todo)
+
+/-- Initial capacity for key and todo vector. -/
+private def initCapacity := 8
+
+/--
+Get the root key and rest of terms of an expression using the specified config.
+-/
+private def rootKey (cfg: WhnfCoreConfig) (e : Expr) : MetaM (Key × Array Expr) :=
+  pushArgs true (Array.mkEmpty initCapacity) e cfg
+
+private partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key)
+    (config : WhnfCoreConfig) : MetaM (Array Key) := do
+  if todo.isEmpty then
+    return keys
+  else
+    let e    := todo.back
+    let todo := todo.pop
+    let (k, todo) ← pushArgs root todo e config
+    mkPathAux false todo (keys.push k) config
+
+/--
+Create a path from an expression.
+
+This differs from Lean.Meta.DiscrTree.mkPath in that the expression
+should uses free variables rather than meta-variables for holes.
+-/
+private def mkPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+  let todo : Array Expr := .mkEmpty initCapacity
+  let keys : Array Key := .mkEmpty initCapacity
+  mkPathAux (root := true) (todo.push e) keys config
+
+/- Monad for finding matches while resolving deferred patterns. -/
+@[reducible]
+private def MatchM α := ReaderT WhnfCoreConfig (StateRefT (Array (Trie α)) MetaM)
+
+private def runMatch (d : LazyDiscrTree α) (m : MatchM α β)  : MetaM (β × LazyDiscrTree α) := do
+  let { config := c, tries := a, roots := r } := d
+  let (result, a) ← withReducible $ (m.run c).run a
+  pure (result, { config := c, tries := a, roots := r})
+
+private def setTrie (i : TrieIndex) (v : Trie α) : MatchM α Unit :=
+  modify (·.set! i v)
+
+/-- Create a new trie with the given lazy entry. -/
+private def newTrie [Monad m] [MonadState (Array (Trie α)) m] (e : LazyEntry α) : m TrieIndex := do
+  modifyGet fun a => let sz := a.size; (sz, a.push (.node #[] 0 {} #[e]))
+
+/-- Add a lazy entry to an existing trie. -/
+private def addLazyEntryToTrie (i:TrieIndex) (e : LazyEntry α) : MatchM α Unit :=
+  modify (·.modify i (·.pushPending e))
+
+/--
+This evaluates all lazy entries in a trie and updates `values`, `starIdx`, and `children`
+accordingly.
+-/
+private partial def evalLazyEntries (config : WhnfCoreConfig)
+    (values : Array α) (starIdx : TrieIndex) (children : HashMap Key TrieIndex)
+    (entries : Array (LazyEntry α)) :
+    MatchM α (Array α × TrieIndex × HashMap Key TrieIndex) := do
+  let rec iter values starIdx children (i : Nat) : MatchM α _ := do
+        if p : i < entries.size then
+          let (todo, lctx, v) := entries[i]
+          if todo.isEmpty then
+            let values := values.push v
+            iter values starIdx children (i+1)
+          else
+            let e    := todo.back
+            let todo := todo.pop
+            let (k, todo) ← withLCtx lctx.1 lctx.2 $ pushArgs false todo e config
+            if k == .star then
+              if starIdx = 0 then
+                let starIdx ← newTrie (todo, lctx, v)
+                iter values starIdx children (i+1)
+              else
+                addLazyEntryToTrie starIdx (todo, lctx, v)
+                iter values starIdx children (i+1)
+            else
+              match children.find? k with
+              | none =>
+                let children := children.insert k (← newTrie (todo, lctx, v))
+                iter values starIdx children (i+1)
+              | some idx =>
+                addLazyEntryToTrie idx (todo, lctx, v)
+                iter values starIdx children (i+1)
+        else
+          pure (values, starIdx, children)
+  iter values starIdx children 0
+
+private def evalNode (c : TrieIndex) :
+    MatchM α (Array α × TrieIndex × HashMap Key TrieIndex) := do
+  let .node vs star cs pending := (←get).get! c
+  if pending.size = 0 then
+    pure (vs, star, cs)
+  else
+    let config ← read
+    setTrie c default
+    let (vs, star, cs) ← evalLazyEntries config vs star cs pending
+    setTrie c <| .node vs star cs #[]
+    pure (vs, star, cs)
+
+/--
+Return the information about the trie at the given idnex.
+
+Used for internal debugging purposes.
+-/
+private def getTrie (d : LazyDiscrTree α) (idx : TrieIndex) :
+    MetaM ((Array α × TrieIndex × HashMap Key TrieIndex) × LazyDiscrTree α) :=
+  runMatch d (evalNode idx)
+
+/--
+A match result repres
+-/
+private structure MatchResult (α : Type) where
+  elts : Array (Array (Array α)) := #[]
+
+private def MatchResult.push (r : MatchResult α) (score : Nat) (e : Array α) : MatchResult α :=
+  if e.isEmpty then
+    r
+  else if score < r.elts.size then
+    { elts := r.elts.modify score (·.push e) }
+  else
+    let rec loop (a : Array (Array (Array α))) :=
+        if a.size < score then
+          loop (a.push #[])
+        else
+          { elts := a.push #[e] }
+    loop r.elts
+  termination_by loop _ => score - a.size
+
+private partial def MatchResult.toArray (mr : MatchResult α) : Array α :=
+    loop (Array.mkEmpty n) mr.elts
+  where n := mr.elts.foldl (fun i a => a.foldl (fun n a => n + a.size) i) 0
+        loop (r : Array α) (a : Array (Array (Array α))) :=
+          if a.isEmpty then
+            r
+          else
+            loop (a.back.foldl (init := r) (fun r a => r ++ a)) a.pop
+
+private partial def getMatchLoop (todo : Array Expr) (score : Nat) (c : TrieIndex)
+    (result : MatchResult α) : MatchM α (MatchResult α) := do
+  let (vs, star, cs) ← evalNode c
+  if todo.isEmpty then
+    return result.push score vs
+  else if star == 0 && cs.isEmpty then
+    return result
+  else
+    let e     := todo.back
+    let todo  := todo.pop
+    /- We must always visit `Key.star` edges since they are wildcards.
+        Thus, `todo` is not used linearly when there is `Key.star` edge
+        and there is an edge for `k` and `k != Key.star`. -/
+    let visitStar (result : MatchResult α) : MatchM α (MatchResult α) :=
+      if star != 0 then
+        getMatchLoop todo score star result
+      else
+        return result
+    let visitNonStar (k : Key) (args : Array Expr) (result : MatchResult α) :=
+      match cs.find? k with
+      | none   => return result
+      | some c => getMatchLoop (todo ++ args) (score + 1) c result
+    let result ← visitStar result
+    let (k, args) ← MatchClone.getMatchKeyArgs e (root := false) (←read)
+    match k with
+    | .star  => return result
+    /-
+      Note: dep-arrow vs arrow
+      Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are
+      `(Key.arrow, #[a, b])`.
+      A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`).
+      Thus, we also visit the `Key.other` child.
+    -/
+    | .arrow => visitNonStar .other #[] (← visitNonStar k args result)
+    | _      => visitNonStar k args result
+
+private def getStarResult (root : Lean.HashMap Key TrieIndex) : MatchM α (MatchResult α) :=
+  match root.find? .star with
+  | none =>
+    pure <| {}
+  | some idx => do
+    let (vs, _) ← evalNode idx
+    pure <| ({} : MatchResult α).push 0 vs
+
+private def getMatchRoot (r : Lean.HashMap Key TrieIndex) (k : Key) (args : Array Expr)
+    (result : MatchResult α) : MatchM α (MatchResult α) :=
+  match r.find? k with
+  | none => pure result
+  | some c => getMatchLoop args 1 c result
+
+/--
+  Find values that match `e` in `root`.
+-/
+private def getMatchCore (root : Lean.HashMap Key TrieIndex) (e : Expr) :
+    MatchM α (MatchResult α) := do
+  let result ← getStarResult root
+  let (k, args) ← MatchClone.getMatchKeyArgs e (root := true) (←read)
+  match k with
+  | .star  => return result
+  /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
+  | .arrow =>
+    getMatchRoot root k args (←getMatchRoot root .other #[] result)
+  | _ =>
+    getMatchRoot root k args result
+
+/--
+  Find values that match `e` in `d`.
+
+  The results are ordered so that the longest matches in terms of number of
+  non-star keys are first with ties going to earlier operators first.
+-/
+def getMatch (d : LazyDiscrTree α) (e : Expr) : MetaM (Array α × LazyDiscrTree α) :=
+  withReducible <| runMatch d <| (·.toArray) <$> getMatchCore d.roots e
+
+/--
+Structure for quickly initializing a lazy discrimination tree with a large number
+of elements using concurrent functions for generating entries.
+-/
+private structure PreDiscrTree (α : Type) where
+  /-- Maps keys to index in tries array. -/
+  roots : HashMap Key Nat := {}
+  /-- Lazy entries for root of trie. -/
+  tries : Array (Array (LazyEntry α)) := #[]
+  deriving Inhabited
+
+namespace PreDiscrTree
+
+private def modifyAt (d : PreDiscrTree α) (k : Key)
+    (f : Array (LazyEntry α) → Array (LazyEntry α)) : PreDiscrTree α :=
+  let { roots, tries } := d
+  match roots.find? k with
+  | .none =>
+    let roots := roots.insert k tries.size
+    { roots, tries := tries.push (f #[]) }
+  | .some i =>
+    { roots, tries := tries.modify i f }
+
+/-- Add an entry to the pre-discrimination tree.-/
+private def push (d : PreDiscrTree α) (k : Key) (e : LazyEntry α) : PreDiscrTree α :=
+  d.modifyAt k (·.push e)
+
+/-- Convert a pre-discrimination tree to a lazy discrimination tree. -/
+private def toLazy (d : PreDiscrTree α) (config : WhnfCoreConfig := {}) : LazyDiscrTree α :=
+  let { roots, tries } := d
+  { config, roots, tries := tries.map (.node {} 0 {}) }
+
+/-- Merge two discrimination trees. -/
+protected def append (x y : PreDiscrTree α) : PreDiscrTree α :=
+  let (x, y, f) :=
+        if x.roots.size ≥ y.roots.size then
+          (x, y, fun y x => x ++ y)
+        else
+          (y, x, fun x y => x ++ y)
+  let { roots := yk, tries := ya } := y
+  yk.fold (init := x) fun d k yi => d.modifyAt k (f ya[yi]!)
+
+instance : Append (PreDiscrTree α) where
+  append := PreDiscrTree.append
+
+end PreDiscrTree
+
+/-- Initial entry in lazy discrimination tree -/
+@[reducible]
+structure InitEntry (α : Type) where
+  /-- Return root key for an entry. -/
+  key : Key
+  /-- Returns rest of entry for later insertion. -/
+  entry : LazyEntry α
+
+namespace InitEntry
+
+/--
+Constructs an initial entry from an expression and value.
+-/
+def fromExpr (expr : Expr) (value : α) (config : WhnfCoreConfig := {}) : MetaM (InitEntry α) := do
+  let lctx ← getLCtx
+  let linst ← getLocalInstances
+  let lctx := (lctx, linst)
+  let (key, todo) ← LazyDiscrTree.rootKey config expr
+  pure <| { key, entry := (todo, lctx, value) }
+
+/--
+Creates an entry for a subterm of an initial entry.
+
+This is slightly more efficient than using `fromExpr` on subterms since it avoids a redundant call
+to `whnf`.
+-/
+def mkSubEntry (e : InitEntry α) (idx : Nat) (value : α) (config : WhnfCoreConfig := {}) :
+    MetaM (InitEntry α) := do
+  let (todo, lctx, _) := e.entry
+  let (key, todo) ← LazyDiscrTree.rootKey config todo[idx]!
+  pure <| { key, entry := (todo, lctx, value) }
+
+end InitEntry
+
+/-- Information about a failed import. -/
+private structure ImportFailure where
+  /-- Module with constant that import failed on. -/
+  module  : Name
+  /-- Constant that import failed on. -/
+  const   : Name
+  /-- Exception that triggers error. -/
+  exception : Exception
+
+/-- Information generation from imported modules. -/
+private structure ImportData where
+  cache : IO.Ref (Lean.Meta.Cache)
+  errors : IO.Ref (Array ImportFailure)
+
+private def ImportData.new : BaseIO ImportData := do
+  let cache ← IO.mkRef {}
+  let errors ← IO.mkRef #[]
+  pure { cache, errors }
+
+/--
+An even wider class of "internal" names than reported by `Name.isInternalDetail`.
+-/
+-- from Lean.Server.Completion
+def isBlackListed (env : Environment) (declName : Name) : Bool :=
+  declName == ``sorryAx
+  || declName.isInternalDetail
+  || declName matches .str _ "inj"
+  || declName matches .str _ "noConfusionType"
+  || isAuxRecursor env declName
+  || isNoConfusion env declName
+  || isRecCore env declName
+  || isMatcherCore env declName
+
+private def addConstImportData
+    (env : Environment)
+    (modName : Name)
+    (d : ImportData)
+    (tree : PreDiscrTree α)
+    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+    (name : Name) (constInfo : ConstantInfo) : BaseIO (PreDiscrTree α) := do
+  if constInfo.isUnsafe then return tree
+  if isBlackListed env name then return tree
+  let mstate : Meta.State := { cache := ←d.cache.get }
+  d.cache.set {}
+  let ctx : Meta.Context := { config := { transparency := .reducible } }
+  let cm := (act name constInfo).run ctx mstate
+  let cctx : Core.Context := {
+    fileName := default,
+    fileMap := default
+  }
+  let cstate : Core.State := {env}
+  match ←(cm.run cctx cstate).toBaseIO with
+  | .ok ((a, ms), _) =>
+    d.cache.set ms.cache
+    pure <| a.foldl (fun t e => t.push e.key e.entry) tree
+  | .error e =>
+    let i : ImportFailure := {
+      module := modName,
+      const := name,
+      exception := e
+    }
+    d.errors.modify (·.push i)
+    pure tree
+
+/--
+Contains the pre discrimination tree and any errors occuring during initialization of
+the library search tree.
+-/
+private structure InitResults (α : Type) where
+  tree  : PreDiscrTree α := {}
+  errors : Array ImportFailure := #[]
+
+instance : Inhabited (InitResults α) where
+  default := {}
+
+namespace InitResults
+
+/-- Combine two initial results. -/
+protected def append (x y : InitResults α) : InitResults α :=
+  let { tree := xv, errors := xe } := x
+  let { tree := yv, errors := ye } := y
+  { tree := xv ++ yv, errors := xe ++ ye }
+
+instance : Append (InitResults α) where
+  append := InitResults.append
+
+end InitResults
+
+private def toFlat (d : ImportData) (tree : PreDiscrTree α) :
+    BaseIO (InitResults α) := do
+  let de ← d.errors.swap #[]
+  pure ⟨tree, de⟩
+
+private partial def loadImportedModule (env : Environment)
+    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+    (d : ImportData)
+    (tree : PreDiscrTree α)
+    (mname : Name)
+    (mdata : ModuleData)
+    (i : Nat := 0) : BaseIO (PreDiscrTree α) := do
+  if h : i < mdata.constNames.size then
+    let name := mdata.constNames[i]
+    let constInfo  := mdata.constants[i]!
+    let tree ← addConstImportData env mname d tree act name constInfo
+    loadImportedModule env act d tree mname mdata (i+1)
+  else
+    pure tree
+
+private def createImportedEnvironmentSeq (env : Environment)
+    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+    (start stop : Nat) : BaseIO (InitResults α) :=
+      do go (← ImportData.new) {} start stop
+    where go d (tree : PreDiscrTree α) (start stop : Nat) : BaseIO _ := do
+            if start < stop then
+              let mname := env.header.moduleNames[start]!
+              let mdata := env.header.moduleData[start]!
+              let tree ← loadImportedModule env act d tree mname mdata
+              go d tree (start+1) stop
+            else
+              toFlat d tree
+  termination_by go _ idx stop => stop - idx
+
+/-- Get the results of each task and merge using combining function -/
+private def combineGet [Append α] (z : α) (tasks : Array (Task α)) : α :=
+  tasks.foldl (fun x t => x ++ t.get) (init := z)
+
+/-- Create an imported environment for tree. -/
+def createImportedEnvironment (env : Environment)
+    (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+    (constantsPerTask : Nat := 1000) :
+    EIO Exception (LazyDiscrTree α) := do
+  let n := env.header.moduleData.size
+  let rec
+    /-- Allocate constants to tasks according to `constantsPerTask`. -/
+    go tasks start cnt idx := do
+      if h : idx < env.header.moduleData.size then
+        let mdata := env.header.moduleData[idx]
+        let cnt := cnt + mdata.constants.size
+        if cnt > constantsPerTask then
+          let t ← createImportedEnvironmentSeq env act start (idx+1) |>.asTask
+          go (tasks.push t) (idx+1) 0 (idx+1)
+        else
+          go tasks start cnt (idx+1)
+      else
+        if start < n then
+          tasks.push <$> (createImportedEnvironmentSeq env act start n).asTask
+        else
+          pure tasks
+  let tasks ← go #[] 0 0 0
+  let r := combineGet default tasks
+  if p : r.errors.size > 0 then
+    throw r.errors[0].exception
+  pure <| r.tree.toLazy
+  termination_by go _ idx => env.header.moduleData.size - idx
diff --git a/Std/Tactic/LibrarySearch.lean b/Std/Tactic/LibrarySearch.lean
new file mode 100644
index 0000000000..86800aef9c
--- /dev/null
+++ b/Std/Tactic/LibrarySearch.lean
@@ -0,0 +1,524 @@
+/-
+Copyright (c) 2021-2023 Gabriel Ebner and Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
+-/
+import Std.Lean.CoreM
+import Std.Lean.Expr
+import Std.Lean.Meta.DiscrTree
+import Std.Lean.Meta.LazyDiscrTree
+import Std.Tactic.SolveByElim
+import Std.Util.Pickle
+
+/-!
+# Library search
+
+This file defines tactics `std_exact?` and `std_apply?`,
+(formerly known as `library_search`)
+and a term elaborator `std_exact?%`
+that tries to find a lemma
+solving the current goal
+(subgoals are solved using `solveByElim`).
+
+```
+example : x < x + 1 := std_exact?%
+example : Nat := by std_exact?
+```
+
+These functions will likely lose their `std_` prefix once
+we are ready to replace the corresponding implementations in Mathlib.
+-/
+
+namespace Std.Tactic.LibrarySearch
+
+open Lean Meta Std.Tactic.TryThis
+
+initialize registerTraceClass `Tactic.stdLibrarySearch
+initialize registerTraceClass `Tactic.stdLibrarySearch.lemmas
+
+/-- Configuration for `DiscrTree`. -/
+def discrTreeConfig : WhnfCoreConfig := {}
+
+/--
+A "modifier" for a declaration.
+* `none` indicates the original declaration,
+* `mp` indicates that (possibly after binders) the declaration is an `↔`,
+  and we want to consider the forward direction,
+* `mpr` similarly, but for the backward direction.
+-/
+inductive DeclMod
+  | /-- the original declaration -/ none
+  | /-- the forward direction of an `iff` -/ mp
+  | /-- the backward direction of an `iff` -/ mpr
+deriving DecidableEq, Inhabited, Ord
+
+instance : ToString DeclMod where
+  toString m := match m with | .none => "" | .mp => "mp" | .mpr => "mpr"
+
+/--
+LibrarySearch has an extension mechanism for replacing the function used
+to find candidate lemmas.
+-/
+@[reducible]
+def CandidateFinder := Expr → MetaM (Array (Name × DeclMod))
+
+open LazyDiscrTree (InitEntry isBlackListed createImportedEnvironment)
+
+namespace DiscrTreeFinder
+
+open System (FilePath)
+
+
+/--
+Once we reach Mathlib, and have `cache` available,
+we may still want to load a precomputed cache for `exact?` from a `.olean` file.
+
+This makes no sense here in Std, where there is no caching mechanism.
+-/
+def cachePath : IO FilePath := do
+  let sp ← searchPathRef.get
+  if let buildPath :: _ := sp then
+    let path := buildPath / "LibrarySearch.extra"
+    if ← path.pathExists then
+      return path
+  return ".lake" / "build" / "lib" / "LibrarySearch.extra"
+
+/-- Add a path to a discrimination tree.-/
+private def addPath [BEq α] (config : WhnfCoreConfig) (tree : DiscrTree α) (tp : Expr) (v : α) :
+    MetaM (DiscrTree α) := do
+  let k ← DiscrTree.mkPath tp config
+  pure <| tree.insertCore k v config
+
+/-- Adds a constant with given name to tree. -/
+private def updateTree (config : WhnfCoreConfig) (tree : DiscrTree (Name × DeclMod))
+    (name : Name) (constInfo : ConstantInfo) : MetaM (DiscrTree (Name × DeclMod)) := do
+  if constInfo.isUnsafe then return tree
+  if isBlackListed (←getEnv) name then return tree
+  withReducible do
+    let (_, _, type) ← forallMetaTelescope constInfo.type
+    let tree ← addPath config tree type (name, DeclMod.none)
+    match type.getAppFnArgs with
+    | (``Iff, #[lhs, rhs]) => do
+      let tree ← addPath config tree rhs (name, DeclMod.mp)
+      let tree ← addPath config tree lhs (name, DeclMod.mpr)
+      return tree
+    | _ =>
+      return tree
+
+/--
+Constructs an discriminator tree from the current environment.
+-/
+def buildImportCache (config : WhnfCoreConfig) : MetaM (DiscrTree (Name × DeclMod)) := do
+  let profilingName := "apply?: init cache"
+  -- Sort so lemmas with longest names come first.
+  let post (A : Array (Name × DeclMod)) :=
+        A.map (fun (n, m) => (n.toString.length, n, m)) |>.qsort (fun p q => p.1 > q.1) |>.map (·.2)
+  profileitM Exception profilingName (← getOptions) do
+    (·.mapArrays post) <$> (← getEnv).constants.map₁.foldM (init := {}) (updateTree config)
+
+/--
+Return matches from local constants.
+
+N.B. The efficiency of this could likely be considerably improved by caching in environment
+extension.
+-/
+def localMatches (config : WhnfCoreConfig) (ty : Expr) : MetaM (Array (Name × DeclMod)) := do
+  let locals ← (← getEnv).constants.map₂.foldlM (init := {}) (DiscrTreeFinder.updateTree config)
+  pure <| (← locals.getMatch  ty config).reverse
+
+/--
+Candidate finding function that uses strict discrimination tree for resolution.
+-/
+def mkImportFinder (config : WhnfCoreConfig) (importTree : DiscrTree (Name × DeclMod))
+    (ty : Expr) : MetaM (Array (Name × DeclMod)) := do
+  pure <| (← importTree.getMatch ty config).reverse
+
+end DiscrTreeFinder
+
+namespace IncDiscrTreeFinder
+
+
+/--
+The maximum number of constants an individual task performed.
+
+The value below was picked because it roughly correponded to 50ms of work on the machine this was
+developed on.  Smaller numbers did not seem to improve performance when importing Std and larger
+numbers (<10k) seemed to degrade initialization performance.
+-/
+private def constantsPerTask : Nat := 6500
+
+private def addImport (name : Name) (constInfo : ConstantInfo) :
+    MetaM (Array (InitEntry (Name × DeclMod))) :=
+  forallTelescope constInfo.type fun _ type => do
+    let e ← InitEntry.fromExpr type (name, DeclMod.none)
+    let a := #[e]
+    if e.key == .const ``Iff 2 then
+      let a := a.push (←e.mkSubEntry 0 (name, DeclMod.mp))
+      let a := a.push (←e.mkSubEntry 1 (name, DeclMod.mpr))
+      pure a
+    else
+      pure a
+
+/--
+Candidate finding function that uses strict discrimination tree for resolution.
+-/
+def mkImportFinder : IO CandidateFinder := do
+  let ref ← IO.mkRef none
+  pure fun ty => do
+    let importTree ← (←ref.get).getDM $ do
+      profileitM Exception  "librarySearch launch" (←getOptions) $
+        createImportedEnvironment (←getEnv) (constantsPerTask := constantsPerTask) addImport
+    let (imports, importTree) ← importTree.getMatch ty
+    ref.set importTree
+    pure imports
+
+end IncDiscrTreeFinder
+
+private unsafe def mkImportFinder : IO CandidateFinder := do
+  let path ← DiscrTreeFinder.cachePath
+  if ← path.pathExists then
+    let (imports, _) ← unpickle (DiscrTree (Name × DeclMod)) path
+    -- `DiscrTree.getMatch` returns results in batches, with more specific lemmas coming later.
+    -- Hence we reverse this list, so we try out more specific lemmas earlier.
+    pure <| DiscrTreeFinder.mkImportFinder {} imports
+  else do
+    IncDiscrTreeFinder.mkImportFinder
+
+/--
+The preferred candidate finding function.
+-/
+initialize defaultCandidateFinder : IO.Ref CandidateFinder ← unsafe do
+  IO.mkRef (←mkImportFinder)
+
+/--
+Update the candidate finder used by library search.
+-/
+def setDefaultCandidateFinder (cf : CandidateFinder) : IO Unit :=
+  defaultCandidateFinder.set cf
+
+private def emoji (e:Except ε α) := if e.toBool then checkEmoji else crossEmoji
+
+/-- Create lemma from name and mod. -/
+def mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr := do
+  let lem ← mkConstWithFreshMVarLevels lem
+  match mod with
+  | .none => pure lem
+  | .mp => mapForallTelescope (fun e => mkAppM ``Iff.mp #[e]) lem
+  | .mpr => mapForallTelescope (fun e => mkAppM ``Iff.mpr #[e]) lem
+
+/--
+A library search candidate using symmetry includes the goal to solve, the metavar
+context for that goal, and the name and orientation of a rule to try using with goal.
+-/
+@[reducible]
+def Candidate :=  (MVarId × MetavarContext) × (Name × DeclMod)
+
+/--
+Try applying the given lemma (with symmetry modifier) to the goal,
+then try to close subsequent goals using `solveByElim`.
+If `solveByElim` succeeds, we return `[]` as the list of new subgoals,
+otherwise the full list of subgoals.
+-/
+private def librarySearchLemma (cfg : ApplyConfig) (act : List MVarId → MetaM (List MVarId))
+    (allowFailure : Bool) (cand : Candidate)  : MetaM (List MVarId) := do
+  let ((goal, mctx), (name, mod)) := cand
+  withTraceNode `Tactic.stdLibrarySearch (return m!"{emoji ·} trying {name} with {mod} ") do
+    setMCtx mctx
+    let lem ← mkLibrarySearchLemma name mod
+    let newGoals ← goal.apply lem cfg
+    try
+      act newGoals
+    catch _ =>
+      if allowFailure then
+        pure newGoals
+      else
+        failure
+
+/--
+Interleave x y interleaves the elements of x and y until one is empty and then returns
+final elements in other list.
+-/
+def interleaveWith {α β γ} (f : α → γ) (x : Array α) (g : β → γ) (y : Array β) : Array γ :=
+    Id.run do
+  let mut res := Array.mkEmpty (x.size + y.size)
+  let n := min x.size y.size
+  for h : i in [0:n] do
+    have p : i < min x.size y.size := h.2
+    have q : i < x.size := Nat.le_trans p (Nat.min_le_left ..)
+    have r : i < y.size := Nat.le_trans p (Nat.min_le_right ..)
+    res := res.push (f x[i])
+    res := res.push (g y[i])
+  let last :=
+        if x.size > n then
+          (x.extract n x.size).map f
+        else
+          (y.extract n y.size).map g
+  pure $ res ++ last
+
+/--
+Run `searchFn` on both the goal and `symm` applied to the goal.
+-/
+def librarySearchSymm (searchFn : CandidateFinder) (goal : MVarId) : MetaM (Array Candidate) := do
+  let tgt ← goal.getType
+  let l1 ← searchFn tgt
+  let coreMCtx ← getMCtx
+  let coreGoalCtx := (goal, coreMCtx)
+  if let some symmGoal ← observing? goal.applySymm then
+    let newType ← instantiateMVars  (← symmGoal.getType)
+    let l2 ← searchFn newType
+    let symmMCtx ← getMCtx
+    let symmGoalCtx := (symmGoal, symmMCtx)
+    setMCtx coreMCtx
+    pure $ interleaveWith (coreGoalCtx, ·) l1 (symmGoalCtx, ·) l2
+  else
+    pure $ l1.map (coreGoalCtx, ·)
+
+/-- A type synonym for our subgoal ranking algorithm. -/
+def SubgoalRankType := Bool × Nat × Int
+  deriving ToString
+
+instance : Ord SubgoalRankType :=
+  have : Ord (Nat × Int) := lexOrd
+  lexOrd
+
+/-- Count how many local hypotheses appear in an expression. -/
+def countLocalHypsUsed [Monad m] [MonadLCtx m] [MonadMCtx m] (e : Expr) : m Nat := do
+  let e' ← instantiateMVars e
+  return (← getLocalHyps).foldr (init := 0) fun h n => if h.occurs e' then n + 1 else n
+
+/-- Returns a tuple:
+* are there no remaining goals?
+* how many local hypotheses were used?
+* how many goals remain, negated?
+
+Larger values (i.e. no remaining goals, more local hypotheses, fewer remaining goals)
+are better.
+-/
+def subgoalRanking (goal : MVarId) (subgoals : List MVarId) : MetaM SubgoalRankType := do
+  return (subgoals.isEmpty, ← countLocalHypsUsed (.mvar goal), - subgoals.length)
+
+/--
+An exception Id that indicates further speculation on candidate lemmas should stop
+and current results returned.
+-/
+private initialize abortSpeculationId : InternalExceptionId ←
+  registerInternalExceptionId `Std.Tactic.LibrarySearch.abortSpeculation
+
+/--
+Called to abort speculative execution in library search.
+-/
+def abortSpeculation [MonadExcept Exception m] : m α :=
+  throw (Exception.internal abortSpeculationId {})
+
+/-- Returns true if this is an abort speculation exception. -/
+def isAbortSpeculation : Exception → Bool
+| .internal id _ => id == abortSpeculationId
+| _ => false
+
+/--
+Sequentially invokes a tactic `act` on each value in candidates on the current state.
+
+The tactic `act` should return a list of meta-variables that still need to be resolved.
+If this list is empty, then no variables remain to be solved, and `tryOnEach` returns
+`none` with the environment set so each goal is resolved.
+
+If the action throws an internal exception with the `abortSpeculationId` id then
+further computation is stopped and intermediate results returned. If any other
+exception is thrown, then it is silently discarded.
+-/
+def tryOnEach
+    (act : Candidate → MetaM (List MVarId))
+    (candidates : Array Candidate) :
+    MetaM (Option (Array (List MVarId × MetavarContext))) := do
+  let mut a := #[]
+  let s ← saveState
+  for c in candidates do
+    match ← (tryCatch (Except.ok <$> act c) (pure ∘ Except.error)) with
+    | .error e =>
+      restoreState s
+      if isAbortSpeculation e then
+        break
+    | .ok remaining =>
+      if remaining.isEmpty then
+        return none
+      let ctx ← getMCtx
+      restoreState s
+      a := a.push (remaining, ctx)
+  return (.some a)
+
+/--
+Return an action that returns true when  the remaining heartbeats is less
+than the currently remaining heartbeats * leavePercent / 100.
+-/
+def mkHeartbeatCheck (leavePercent : Nat) : MetaM (MetaM Bool) := do
+  let maxHB ← getMaxHeartbeats
+  let hbThreshold := (← getRemainingHeartbeats) * leavePercent / 100
+  -- Return true if we should stop
+  pure $
+    if maxHB = 0 then
+      pure false
+    else do
+      return (← getRemainingHeartbeats) < hbThreshold
+
+/-- Shortcut for calling `solveByElim`. -/
+def solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (maxDepth : Nat) := do
+  -- There is only a marginal decrease in performance for using the `symm` option for `solveByElim`.
+  -- (measured via `lake build && time lake env lean test/librarySearch.lean`).
+  let cfg : SolveByElim.Config :=
+    { maxDepth, exfalso := exfalso, symm := true, commitIndependentGoals := true }
+  let ⟨lemmas, ctx⟩ ← SolveByElim.mkAssumptionSet false false [] [] #[]
+  let cfg := if !required.isEmpty then cfg.requireUsingAll required else cfg
+  SolveByElim.solveByElim cfg lemmas ctx goals
+
+/-- State for resolving imports -/
+private def LibSearchState := IO.Ref (Option CandidateFinder)
+
+private initialize LibSearchState.default : IO.Ref (Option CandidateFinder) ← do
+  IO.mkRef .none
+
+private instance : Inhabited LibSearchState where
+  default := LibSearchState.default
+
+private initialize ext : EnvExtension LibSearchState ←
+  registerEnvExtension (IO.mkRef .none)
+
+private def librarySearchEmoji : Except ε (Option α) → String
+| .error _ => bombEmoji
+| .ok (some _) => crossEmoji
+| .ok none => checkEmoji
+
+private def librarySearch' (goal : MVarId)
+    (tactic : List MVarId → MetaM (List MVarId))
+    (allowFailure : Bool)
+    (leavePercentHeartbeats : Nat) :
+    MetaM (Option (Array (List MVarId × MetavarContext))) := do
+  withTraceNode `Tactic.stdLibrarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
+  profileitM Exception "librarySearch" (← getOptions) do
+  let importFinder ← do
+        let r := ext.getState (←getEnv)
+        match ←r.get with
+        | .some f => pure f
+        | .none =>
+          let f ← defaultCandidateFinder.get
+          r.set (.some f)
+          pure f
+  let searchFn (ty : Expr) := do
+      let localMap ← (← getEnv).constants.map₂.foldlM (init := {}) (DiscrTreeFinder.updateTree {})
+      let locals := (← localMap.getMatch  ty {}).reverse
+      pure <| locals ++ (← importFinder ty)
+  -- Create predicate that returns true when running low on heartbeats.
+  let shouldAbort ← mkHeartbeatCheck leavePercentHeartbeats
+  let candidates ← librarySearchSymm searchFn goal
+  let cfg : ApplyConfig := { allowSynthFailures := true }
+  let act := fun cand => do
+      if ←shouldAbort then
+        abortSpeculation
+      librarySearchLemma cfg tactic allowFailure cand
+  tryOnEach act candidates
+
+/--
+Try to solve the goal either by:
+* calling `tactic true`
+* or applying a library lemma then calling `tactic false` on the resulting goals.
+
+Typically here `tactic` is `solveByElim`,
+with the `Bool` flag indicating whether it may retry with `exfalso`.
+
+If it successfully closes the goal, returns `none`.
+Otherwise, it returns `some a`, where `a : Array (List MVarId × MetavarContext)`,
+with an entry for each library lemma which was successfully applied,
+containing a list of the subsidiary goals, and the metavariable context after the application.
+
+(Always succeeds, and the metavariable context stored in the monad is reverted,
+unless the goal was completely solved.)
+
+(Note that if `solveByElim` solves some but not all subsidiary goals,
+this is not currently tracked.)
+-/
+def librarySearch (goal : MVarId)
+    (tactic : Bool → List MVarId → MetaM (List MVarId))
+    (allowFailure : Bool := true)
+    (leavePercentHeartbeats : Nat := 10) :
+    MetaM (Option (Array (List MVarId × MetavarContext))) := do
+  (tactic true [goal] *> pure none) <|>
+  librarySearch' goal (tactic false) allowFailure leavePercentHeartbeats
+
+open Lean.Parser.Tactic
+
+-- TODO: implement the additional options for `library_search` from Lean 3,
+-- in particular including additional lemmas
+-- with `std_exact? [X, Y, Z]` or `std_exact? with attr`.
+
+-- For now we only implement the basic functionality.
+-- The full syntax is recognized, but will produce a "Tactic has not been implemented" error.
+
+/-- Syntax for `std_exact?` -/
+syntax (name := std_exact?') "std_exact?" (config)? (simpArgs)? (" using " (colGt ident),+)?
+    ("=>" tacticSeq)? : tactic
+
+/-- Syntax for `std_apply?` -/
+syntax (name := std_apply?') "std_apply?" (config)? (simpArgs)? (" using " (colGt term),+)? : tactic
+
+open Elab.Tactic Elab Tactic
+open Parser.Tactic (tacticSeq)
+
+/-- Implementation of the `exact?` tactic. -/
+def exact? (tk : Syntax) (required : Option (Array (TSyntax `term)))
+   (solver : Option (TSyntax `Lean.Parser.Tactic.tacticSeq)) (requireClose : Bool) :
+    TacticM Unit := do
+  let mvar ← getMainGoal
+  let (_, goal) ← (← getMainGoal).intros
+  goal.withContext do
+    let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
+    let tactic ←
+      match solver with
+      | none =>
+        pure (fun exfalso => solveByElim required (exfalso := exfalso) (maxDepth := 6))
+      | some t =>
+        let _ <- mkInitialTacticInfo t
+        throwError "Do not yet support custom std_exact?/std_apply? tactics."
+    match ← librarySearch goal tactic (allowFailure := required.isEmpty) with
+    -- Found goal that closed problem
+    | none =>
+      addExactSuggestion tk (← instantiateMVars (mkMVar mvar)).headBeta
+    -- Found suggestions
+    | some suggestions =>
+      if requireClose then throwError
+        "`std_exact?` could not close the goal. Try `std_apply?` to see partial suggestions."
+      reportOutOfHeartbeats `library_search tk
+      for (_, suggestionMCtx) in suggestions do
+        withMCtx suggestionMCtx do
+          addExactSuggestion tk (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
+      if suggestions.isEmpty then logError "std_apply? didn't find any relevant lemmas"
+      admitGoal goal
+
+elab_rules : tactic
+  | `(tactic| std_exact? $[using $[$lemmas],*]? $[=> $solver]?) => do
+  exact? (← getRef) lemmas solver true
+
+elab_rules : tactic | `(tactic| std_apply? $[using $[$required],*]?) => do
+  exact? (← getRef) required none false
+
+--/-- Deprecation warning for `library_search`. -/
+--elab tk:"library_search" : tactic => do
+--  logWarning ("`library_search` has been renamed to `apply?`" ++
+--    " (or `exact?` if you only want solutions closing the goal)")
+--  exact? tk none false
+
+open Elab Term in
+/-- Term elaborator using the `exact?` tactic. -/
+elab tk:"std_exact?%" : term <= expectedType => do
+  let goal ← mkFreshExprMVar expectedType
+  let (_, introdGoal) ← goal.mvarId!.intros
+  introdGoal.withContext do
+    let tactic := fun exfalso g => solveByElim []  (maxDepth := 6) exfalso g
+    if let some suggestions ← librarySearch introdGoal tactic then
+      reportOutOfHeartbeats `library_search tk
+      for suggestion in suggestions do
+        withMCtx suggestion.2 do
+          addTermSuggestion tk (← instantiateMVars goal).headBeta
+      if suggestions.isEmpty then logError "std_exact? didn't find any relevant lemmas"
+      mkSorry expectedType (synthetic := true)
+    else
+      addTermSuggestion tk (← instantiateMVars goal).headBeta
+      instantiateMVars goal
diff --git a/Std/Tactic/Relation/Symm.lean b/Std/Tactic/Relation/Symm.lean
index 490b981820..ad008f8d86 100644
--- a/Std/Tactic/Relation/Symm.lean
+++ b/Std/Tactic/Relation/Symm.lean
@@ -50,64 +50,49 @@ open Std.Tactic
 
 namespace Lean.Expr
 
+/-- Return the symmetry lemmas that match the target type. -/
+def getSymmLems (tgt : Expr) : MetaM (Array Name) := do
+  let .app (.app rel _) _ := tgt
+    | throwError "symmetry lemmas only apply to binary relations, not{indentExpr tgt}"
+  (symmExt.getState (← getEnv)).getMatch rel symmExt.config
+
 /-- Given a term `e : a ~ b`, construct a term in `b ~ a` using `@[symm]` lemmas. -/
 def applySymm (e : Expr) : MetaM Expr := do
-  go (← instantiateMVars (← inferType e)) fun lem args body => do
-    let .true ← isDefEq args.back e | failure
-    mkExpectedTypeHint (mkAppN lem args) (← instantiateMVars body)
-where
-  /--
-  Internal implementation of `Lean.Expr.applySymm`, `Lean.MVarId.applySymm`,
-  and the user-facing tactic.
-
-  `tgt` should be of the form `a ~ b`, and is used to index the symm lemmas.
-
-  `k lem args body` should calculate a result,
-  given a candidate `symm` lemma `lem`, which will have type `∀ args, body`.
-
-  In `Lean.Expr.applySymm` this result will be a new `Expr`,
-  and in `Lean.MVarId.applySymm` and `Lean.MVarId.applySymmAt` this result will be a new goal.
-  -/
-  -- This function is rather opaque, but the design with a generic continuation `k`
-  -- is necessary in order to factor out all the common requirements below.
-  go (tgt : Expr) {α} (k : Expr → Array Expr → Expr → MetaM α) : MetaM α := do
-    let .app (.app rel _) _ := tgt
-      | throwError "symmetry lemmas only apply to binary relations, not{indentExpr tgt}"
-    for lem in ← (symmExt.getState (← getEnv)).getMatch rel symmExt.config do
-      try
+  let tgt <- instantiateMVars (← inferType e)
+  let lems ← getSymmLems tgt
+  let s ← saveState
+  let act lem := do
+        restoreState s
         let lem ← mkConstWithFreshMVarLevels lem
         let (args, _, body) ← withReducible <| forallMetaTelescopeReducing (← inferType lem)
-        return (← k lem args body)
-      catch _ => pure ()
-    throwError "no applicable symmetry lemma found for{indentExpr tgt}"
+        let .true ← isDefEq args.back e | failure
+        mkExpectedTypeHint (mkAppN lem args) (← instantiateMVars body)
+  lems.toList.firstM act
+    <|> throwError m!"no applicable symmetry lemma found for {indentExpr tgt}"
 
 end Lean.Expr
 
+
 namespace Lean.MVarId
 
-/-- Apply a symmetry lemma (i.e. marked with `@[symm]`) to a metavariable. -/
+/--
+Apply a symmetry lemma (i.e. marked with `@[symm]`) to a metavariable.
+
+The type of `g` should be of the form `a ~ b`, and is used to index the symm lemmas.
+-/
 def applySymm (g : MVarId) : MetaM MVarId := do
-  go (← g.getTypeCleanup) g fun lem args body g => do
-    let .true ← isDefEq (← g.getType) body | failure
-    g.assign (mkAppN lem args)
-    return args.back.mvarId!
-where
-  /--
-  Internal implementation of `Lean.MVarId.applySymm` and the user-facing tactic.
-
-  `tgt` should be of the form `a ~ b`, and is used to index the symm lemmas.
-
-  `k lem args body goal` should transform `goal` into a new goal,
-  given a candidate `symm` lemma `lem`, which will have type `∀ args, body`.
-  Depending on whether we are working on a hypothesis or a goal,
-  `k` will internally use either `replace` or `assign`.
-  -/
-  go (tgt : Expr) (g : MVarId) (k : Expr → Array Expr → Expr → MVarId → MetaM MVarId) :
-    MetaM MVarId := do
-  Expr.applySymm.go tgt fun lem args body => do
-    let g' ← k lem args body g
-    g'.setTag (← g.getTag)
-    return g'
+  let tgt <- g.getTypeCleanup
+  let lems ← Expr.getSymmLems tgt
+  let act lem : MetaM MVarId := do
+        let lem ← mkConstWithFreshMVarLevels lem
+        let (args, _, body) ← withReducible <| forallMetaTelescopeReducing (← inferType lem)
+        let .true ← isDefEq (← g.getType) body | failure
+        g.assign (mkAppN lem args)
+        let g' := args.back.mvarId!
+        g'.setTag (← g.getTag)
+        pure g'
+  lems.toList.firstM act
+    <|> throwError m!"no applicable symmetry lemma found for {indentExpr tgt}"
 
 /-- Use a symmetry lemma (i.e. marked with `@[symm]`) to replace a hypothesis in a goal. -/
 def applySymmAt (h : FVarId) (g : MVarId) : MetaM MVarId := do
diff --git a/test/library_search/basic.lean b/test/library_search/basic.lean
new file mode 100644
index 0000000000..138e4d2086
--- /dev/null
+++ b/test/library_search/basic.lean
@@ -0,0 +1,224 @@
+import Std
+set_option autoImplicit true
+
+-- Enable this option for tracing:
+-- set_option trace.Tactic.stdLibrarySearch true
+-- And this option to trace all candidate lemmas before application.
+-- set_option trace.Tactic.stdLibrarySearch.lemmas true
+
+noncomputable section
+
+/-- info: Try this: exact Nat.lt.base x -/
+#guard_msgs in
+example (x : Nat) : x ≠ x.succ := Nat.ne_of_lt (by std_apply?)
+
+/-- info: Try this: exact Nat.zero_lt_succ 1 -/
+#guard_msgs in
+example : 0 ≠ 1 + 1 := Nat.ne_of_lt (by std_apply?)
+
+example : 0 ≠ 1 + 1 := Nat.ne_of_lt (by exact Fin.size_pos')
+
+/-- info: Try this: exact Nat.add_comm x y -/
+#guard_msgs in
+example (x y : Nat) : x + y = y + x := by std_apply?
+
+/-- info: Try this: exact fun a => Nat.add_le_add_right a k -/
+#guard_msgs in
+example (n m k : Nat) : n ≤ m → n + k ≤ m + k := by std_apply?
+
+/-- info: Try this: exact Nat.mul_dvd_mul_left a w -/
+#guard_msgs in
+example (ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by std_apply?
+
+-- Could be any number of results (`Int.one`, `Int.zero`, etc)
+#guard_msgs (drop info) in
+example : Int := by std_apply?
+
+/-- info: Try this: Nat.lt.base x -/
+#guard_msgs in
+example : x < x + 1 := std_exact?%
+
+/-- info: Try this: exact p -/
+#guard_msgs in
+example (P : Prop) (p : P) : P := by std_apply?
+/-- info: Try this: exact False.elim (np p) -/
+#guard_msgs in
+example (P : Prop) (p : P) (np : ¬P) : false := by std_apply?
+/-- info: Try this: exact h x rfl -/
+#guard_msgs in
+example (X : Type) (P : Prop) (x : X) (h : ∀ x : X, x = x → P) : P := by std_apply?
+
+-- Could be any number of results (`fun x => x`, `id`, etc)
+#guard_msgs (drop info) in
+example (α : Prop) : α → α := by std_apply?
+
+-- Note: these examples no longer work after we turned off lemmas with discrimination key `#[*]`.
+-- example (p : Prop) : (¬¬p) → p := by std_apply? -- says: `exact not_not.mp`
+-- example (a b : Prop) (h : a ∧ b) : a := by std_apply? -- says: `exact h.left`
+-- example (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by std_apply? -- say: `exact Function.mtr`
+
+/-- info: Try this: exact Nat.add_comm a b -/
+#guard_msgs in
+example (a b : Nat) : a + b = b + a :=
+by std_apply?
+
+/-- info: Try this: exact Nat.mul_sub_left_distrib n m k -/
+#guard_msgs in
+example (n m k : Nat) : n * (m - k) = n * m - n * k :=
+by std_apply?
+
+attribute [symm] Eq.symm
+
+/-- info: Try this: exact Eq.symm (Nat.mul_sub_left_distrib n m k) -/
+#guard_msgs in
+example (n m k : Nat) : n * m - n * k = n * (m - k) := by
+  std_apply?
+
+/-- info: Try this: exact eq_comm -/
+#guard_msgs in
+example {α : Type} (x y : α) : x = y ↔ y = x := by std_apply?
+
+/-- info: Try this: exact Nat.add_pos_left ha b -/
+#guard_msgs in
+example (a b : Nat) (ha : 0 < a) (_hb : 0 < b) : 0 < a + b := by std_apply?
+
+/-- info: Try this: exact Nat.add_pos_left ha b -/
+#guard_msgs in
+-- Verify that if maxHeartbeats is 0 we don't stop immediately.
+set_option maxHeartbeats 0 in
+example (a b : Nat) (ha : 0 < a) (_hb : 0 < b) : 0 < a + b := by std_apply?
+
+section synonym
+
+/-- info: Try this: exact Nat.add_pos_left ha b -/
+#guard_msgs in
+example (a b : Nat) (ha : a > 0) (_hb : 0 < b) : 0 < a + b := by std_apply?
+
+/-- info: Try this: exact Nat.le_of_dvd w h -/
+#guard_msgs in
+example (a b : Nat) (h : a ∣ b) (w : b > 0) : a ≤ b :=
+by std_apply?
+
+/-- info: Try this: exact Nat.le_of_dvd w h -/
+#guard_msgs in
+example (a b : Nat) (h : a ∣ b) (w : b > 0) : b ≥ a := by std_apply?
+
+-- TODO: A lemma with head symbol `¬` can be used to prove `¬ p` or `⊥`
+/-- info: Try this: exact Nat.not_lt_zero a -/
+#guard_msgs in
+example (a : Nat) : ¬ (a < 0) := by std_apply?
+/-- info: Try this: exact Nat.not_succ_le_zero a h -/
+#guard_msgs in
+example (a : Nat) (h : a < 0) : False := by std_apply?
+
+-- An inductive type hides the constructor's arguments enough
+-- so that `apply?` doesn't accidentally close the goal.
+inductive P : Nat → Prop
+  | gt_in_head {n : Nat} : n < 0 → P n
+
+-- This lemma with `>` as its head symbol should also be found for goals with head symbol `<`.
+theorem lemma_with_gt_in_head (a : Nat) (h : P a) : 0 > a := by cases h; assumption
+
+-- This lemma with `false` as its head symbols should also be found for goals with head symbol `¬`.
+theorem lemma_with_false_in_head (a b : Nat) (_h1 : a < b) (h2 : P a) : False := by
+  apply Nat.not_lt_zero; cases h2; assumption
+
+/-- info: Try this: exact lemma_with_gt_in_head a h -/
+#guard_msgs in
+example (a : Nat) (h : P a) : 0 > a := by std_apply?
+/-- info: Try this: exact lemma_with_gt_in_head a h -/
+#guard_msgs in
+example (a : Nat) (h : P a) : a < 0 := by std_apply?
+
+/-- info: Try this: exact lemma_with_false_in_head a b h1 h2 -/
+#guard_msgs in
+example (a b : Nat) (h1 : a < b) (h2 : P a) : False := by std_apply?
+
+-- TODO this no longer works:
+-- example (a b : Nat) (h1 : a < b) : ¬ (P a) := by std_apply? -- says `exact lemma_with_false_in_head a b h1`
+
+end synonym
+
+/-- info: Try this: exact fun P => iff_not_self -/
+#guard_msgs in
+example : ∀ P : Prop, ¬(P ↔ ¬P) := by std_apply?
+
+-- We even find `iff` results:
+/-- info: Try this: exact Iff.mpr (Nat.dvd_add_iff_left h₁) h₂ -/
+#guard_msgs in
+example {a b c : Nat} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b := by std_apply?
+
+-- Note: these examples no longer work after we turned off lemmas with discrimination key `#[*]`.
+-- example {α : Sort u} (h : Empty) : α := by std_apply? -- says `exact Empty.elim h`
+-- example (f : A → C) (g : B → C) : (A ⊕ B) → C := by std_apply? -- says `exact Sum.elim f g`
+-- example (n : Nat) (r : ℚ) : ℚ := by std_apply? using n, r -- exact nsmulRec n r
+
+opaque f : Nat → Nat
+axiom F (a b : Nat) : f a ≤ f b ↔ a ≤ b
+
+/-- info: Try this: exact Iff.mpr (F a b) h -/
+#guard_msgs in
+example (a b : Nat) (h : a ≤ b) : f a ≤ f b := by std_apply?
+
+/-- info: Try this: exact List.join L -/
+#guard_msgs in
+example (L : List (List Nat)) : List Nat := by std_apply? using L
+
+-- Could be any number of results
+#guard_msgs (drop info) in
+example (P _Q : List Nat) (h : Nat) : List Nat := by std_apply? using h, P
+
+-- Could be any number of results
+#guard_msgs (drop info) in
+example (l : List α) (f : α → β ⊕ γ) : List β × List γ := by
+  std_apply? using f -- partitionMap f l
+
+-- Could be any number of results (`Nat.mul n m`, `Nat.add n m`, etc)
+#guard_msgs (drop info) in
+example (n m : Nat) : Nat := by std_apply? using n, m
+
+#guard_msgs (drop info) in
+example (P Q : List Nat) (_h : Nat) : List Nat := by std_exact? using P, Q
+
+-- Check that we don't use sorryAx:
+-- (see https://github.com/leanprover-community/mathlib4/issues/226)
+theorem Bool_eq_iff {A B : Bool} : (A = B) = (A ↔ B) :=
+  by (cases A <;> cases B <;> simp)
+
+/-- info: Try this: exact Bool_eq_iff -/
+#guard_msgs in
+theorem Bool_eq_iff2 {A B : Bool} : (A = B) = (A ↔ B) := by
+  std_apply? -- exact Bool_eq_iff
+
+-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20regression/near/354025788
+-- Disabled for Std
+--/-- info: Try this: exact surjective_quot_mk r -/
+--#guard_msgs in
+--example {r : α → α → Prop} : Function.Surjective (Quot.mk r) := by exact?
+
+-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20failing.20to.20apply.20symm
+-- Disabled for Std
+-- /-- info: Try this: exact Iff.symm Nat.prime_iff -/
+--#guard_msgs in
+--example (n : Nat) : Prime n ↔ Nat.Prime n := by
+--  std_exact?
+
+-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exact.3F.20recent.20regression.3F/near/387691588
+-- Disabled for Std
+--lemma ex' (x : Nat) (_h₁ : x = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by
+--  std_exact? says exact dvd_of_mul_left_dvd h
+
+-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/apply.3F.20failure/near/402534407
+-- Disabled for Std
+--example (P Q : Prop) (h : P → Q) (h' : ¬Q) : ¬P := by
+--  std_exact? says exact mt h h'
+
+-- Removed until we come up with a way of handling nonspecific lemmas
+-- that does not pollute the output or cause too much slow-down.
+-- -- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Exact.3F.20fails.20on.20le_antisymm/near/388993167
+-- set_option linter.unreachableTactic false in
+-- example {x y : ℝ} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
+--   -- This example non-deterministically picks between `le_antisymm hxy hyx` and `ge_antisymm hyx hxy`.
+--   first
+--   | exact? says exact le_antisymm hxy hyx
+--   | exact? says exact ge_antisymm hyx hxy