* 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 <scott.morrison@gmail.com>

* fix termination_by clauses in LazyDiscrTree

fix LibrarySearch

* bump toolchain

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>

* feat: hover info for `rcases h : ...` (#486)

* feat: hover info for `rcases h : ...`

* fix

* chore: adaptations for leanprover/lean4#3123 (#502)

* chore: adaptations for leanprover/lean4#3123

* update toolchain

* chore: remove unnecessary `have` (#516)

After leanprover/lean4#3132 the linter will complain about this.

* chore: simproc PR changes (#496)

See leanprover/lean4#3124

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* chore: adaptions for nightly-2023-01-11 (#524)

* advance toolchain to nightly-2024-01-12, no updates required

* 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 <scott.morrison@gmail.com>

* fix termination_by clauses in LazyDiscrTree

fix LibrarySearch

* bump toolchain

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>

* feat: adaptations for leanprover/lean4#3159 (#557)

* merge origin/main

* chore: fixes for `simp` refactor (#571)

* move to v4.6.0-rc1

* fix proofs

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Leonardo de Moura <leonardo@microsoft.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>

)

* feat: hover info for `rcases h : ...` (leanprover-community#486)

* feat: hover info for `rcases h : ...`

* fix

* chore: adaptations for leanprover/lean4#3123 (leanprover-community#502)

* chore: adaptations for leanprover/lean4#3123

* update toolchain

* chore: remove unnecessary `have` (leanprover-community#516)

After leanprover/lean4#3132 the linter will complain about this.

* chore: simproc PR changes (leanprover-community#496)

See leanprover/lean4#3124

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* chore: adaptions for nightly-2023-01-11 (leanprover-community#524)

* advance toolchain to nightly-2024-01-12, no updates required

* chore: updates to DiscrTree for changes in nightly (leanprover-community#536)

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

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

* docs(Data/List): typo (leanprover-community#529)

* feat: Eq.rec lemma (leanprover-community#385)

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

* Incremental Library Search (leanprover-community#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 <scott.morrison@gmail.com>

* fix termination_by clauses in LazyDiscrTree

fix LibrarySearch

* bump toolchain

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>

* feat: adaptations for leanprover/lean4#3159 (leanprover-community#557)

* merge origin/main

* chore: fixes for `simp` refactor (leanprover-community#571)

* move to v4.6.0-rc1

* fix proofs

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Leonardo de Moura <leonardo@microsoft.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>