chore: updates to DiscrTree for changes in nightly (#536)

* doc: extend docstrings for `ext` and `ext1` (#525)

Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`.

* docs(Data/List): typo (#529)

* feat: Eq.rec lemma (#385)

* chore: Add empty collection instance to BinomialHeap (#532)

* Incremental Library Search (#421)

This ports library_search from Mathlib to Std.  It preserves the ability to do caching, but is designed to support a cacheless mode.  The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed.

Co-authored-by: Scott Morrison <[email protected]>

* fix termination_by clauses in LazyDiscrTree

fix LibrarySearch

* bump toolchain

---------

Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Martin Dvořák <[email protected]>
Co-authored-by: François G. Dorais <[email protected]>
Co-authored-by: Joe Hendrix <[email protected]>

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

Std/Data/BinomialHeap/Basic.lean

@@ -502,6 +502,7 @@ variable {α : Type u} {le : α → α → Bool}
 /-- `O(1)`. Make a new empty binomial heap. -/
 @[inline] def empty : BinomialHeap α le := mkBinomialHeap α le
 
+instance : EmptyCollection (BinomialHeap α le) := ⟨.empty⟩
 instance : Inhabited (BinomialHeap α le) := ⟨.empty⟩
 
 /-- `O(1)`. Is the heap empty? -/

Std/Data/List/Basic.lean

@@ -1034,7 +1034,7 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
 /--
 `ofFn f` with `f : fin n → α` returns the list whose ith element is `f i`
 ```
-ofFn f = [f 0, f 1, ... , f(n - 1)]
+ofFn f = [f 0, f 1, ... , f (n - 1)]
 ```
 -/
 def ofFn {n} (f : Fin n → α) : List α := (Array.ofFn f).toList

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