test: benchmark from Lean Hackathon

This PR disables the `import all` check across package boundaries. Now
any module can `import all` any other module.

.claude/CLAUDE.md

@@ -45,3 +45,7 @@ feat: add optional binder limit to `mkPatternFromTheorem`
 This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
 leading quantifiers are stripped when creating a pattern.
 ```
+
+## CI Log Retrieval
+
+When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v5
+      uses: actions/checkout@v6
     - name: actionlint
       uses: raven-actions/actionlint@v2
       with:

.github/workflows/build-template.yml

@@ -67,13 +67,13 @@ jobs:
         if: runner.os == 'macOS'
       - name: Checkout
         if: (!endsWith(matrix.os, '-with-cache'))
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
       - name: Namespace Checkout
         if: endsWith(matrix.os, '-with-cache')
-        uses: namespacelabs/nscloud-checkout-action@v7
+        uses: namespacelabs/nscloud-checkout-action@v8
         with:
           ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once

.github/workflows/check-prelude.yml

@@ -7,7 +7,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}

.github/workflows/check-stage0.yml

@@ -8,7 +8,7 @@ jobs:
   check-stage0-on-queue:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v6
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0

.github/workflows/ci.yml

@@ -50,7 +50,7 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         # don't schedule nightlies on forks
         if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly' || (startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4')
       - name: Set Nightly
@@ -267,14 +267,17 @@ jobs:
                 "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
-                // `StackOverflow*` correctly triggers ubsan.
-                // `reverse-ffi` fails to link in sanitizers.
-                // `interactive` and `async_select_channel` fail nondeterministically, would need to
-                // be investigated..
-                // 9366 is too close to timeout.
-                // `bv_` sometimes times out calling into cadical even though we should be using the
-                // standard compile flags for it.
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_'"
+                // * `StackOverflow*` correctly triggers ubsan.
+                // * `reverse-ffi` fails to link in sanitizers.
+                // * `interactive` and `async_select_channel` fail nondeterministically, would need
+                //   to be investigated..
+                // * 9366 is too close to timeout.
+                // * `bv_` sometimes times out calling into cadical even though we should be using
+                //   the standard compile flags for it.
+                // * `grind_guide` always times out.
+                // * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI
+                //   failures?
+                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|pkg/|lake/'"
               },
               {
                 "name": "macOS",
@@ -434,7 +437,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -455,7 +458,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         with:
           # needed for tagging
           fetch-depth: 0
@@ -480,7 +483,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/copyright-header.yml

@@ -6,7 +6,7 @@ jobs:
   check-lean-files:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v6
 
     - name: Verify .lean files start with a copyright header.
       run: |

.github/workflows/pr-release.yml

@@ -71,7 +71,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -387,7 +387,7 @@ jobs:
       # Checkout the Batteries repository with all branches
       - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         with:
           repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
@@ -447,7 +447,7 @@ jobs:
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         with:
           repository: leanprover-community/mathlib4-nightly-testing
           token: ${{ secrets.MATHLIB4_BOT }}
@@ -530,7 +530,7 @@ jobs:
       # Checkout the reference manual repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        uses: actions/checkout@v5
+        uses: actions/checkout@v6
         with:
           repository: leanprover/reference-manual
           token: ${{ secrets.MANUAL_PR_BOT }}

.github/workflows/update-stage0.yml

@@ -27,7 +27,7 @@ jobs:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
     # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v6
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
     - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"

doc/style.md

@@ -810,7 +810,7 @@ Docstrings for constants should have the following structure:
 
 The **short summary** should be 1–3 sentences (ideally 1) and provide
 enough information for most readers to quickly decide whether the
-docstring is relevant to their task. The first (or only) sentence of
+constant is relevant to their task. The first (or only) sentence of
 the short summary should be a *sentence fragment* in which the subject
 is implied to be the documented item, written in present tense
 indicative, or a *noun phrase* that characterizes the documented
@@ -1123,6 +1123,110 @@ infix:50 " ⇔ " => Bijection
 recommended_spelling "bij" for "⇔" in [Bijection, «term_⇔_»]
 ```
 
+#### Tactics
+
+Docstrings for tactics should have the following structure:
+
+* Short summary
+* Details
+* Variants
+* Examples
+
+Sometimes more than one declaration is needed to implement what the user
+sees as a single tactic. In that case, only one declaration should have
+the associated docstring, and the others should have the `tactic_alt`
+attribute to mark them as an implementation detail.
+
+The **short summary** should be 1–3 sentences (ideally 1) and provide
+enough information for most readers to quickly decide whether the
+tactic is relevant to their task. The first (or only) sentence of
+the short summary should be a full sentence in which the subject
+is an example invocation of the tactic, written in present tense
+indicative. If the example tactic invocation names parameters, then the
+short summary may refer to them. For the example invocation, prefer the
+simplest or most typical example. Explain more complicated forms in the
+variants section. If needed, abbreviate the invocation by naming part of
+the syntax and expanding it in the next sentence. The summary should be
+written as a single paragraph.
+
+**Details**, if needed, may be 1-3 paragraphs that describe further
+relevant information. They may insert links as needed. This section
+should fully explain the scope of the tactic: its syntax format,
+on which goals it works and what the resulting goal(s) look like. It
+should be clear whether the tactic fails if it does not close the main
+goal and whether it creates any side goals. The details may include
+explanatory examples that can’t necessarily be machine checked and
+don’t fit the format.
+
+If the tactic is extensible using `macro_rules`, mention this in the
+details, with a link to `lean-manual://section/tactic-macro-extension`
+and give a one-line example. If the tactic provides an attribute or a
+command that allows the user to extend its behavior, the documentation
+on how to extend the tactic belongs to that attribute or command. In the
+tactic docstring, use a single sentence to refer the reader to this
+further documentation.
+
+**Variants**, if needed, should be a bulleted list describing different
+options and forms of the same tactic. The reader should be able to parse
+and understand the parts of a tactic invocation they are hovering over,
+using this list. Each list item should describe an individual variant
+and take one of two formats: the **short summary** as above, or a
+**named list item**. A named list item consists of a title in bold
+followed by an indented short paragraph.
+
+Variants should be explained from the perspective of the tactic's users, not
+their implementers. A tactic that is implemented as a single Lean parser may
+have multiple variants from the perspective of users, while a tactic that is
+implemented as multiple parsers may have no variants, but merely an optional
+part of the syntax.
+
+**Examples** should start with the line `Examples:` (or `Example:` if
+there’s exactly one). The section should consist of a sequence of code
+blocks, each showing a Lean declaration (usually with the `example`
+keyword) that invokes the tactic. When the effect of the tactic is not
+clear from the code, you can use code comments to describe this. Do
+not include text between examples, because it can be unclear whether
+the text refers to the code before or after the example.
+
+##### Example
+
+````
+`rw [e]` uses the expression `e` as a rewrite rule on the main goal,
+then tries to close the goal by "cheap" (reducible) `rfl`.
+
+If `e` is a defined constant, then the equational theorems associated with `e`
+are used. This provides a convenient way to unfold `e`. If `e` has parameters,
+the tactic will try to fill these in by unification with the matching part of
+the target. Parameters are only filled in once per rule, restricting which
+later rewrites can be found. Parameters that are not filled in after
+unification will create side goals. If the `rfl` fails to close the main goal,
+no error is raised.
+
+`rw` may fail to rewrite terms "under binders", such as `∀ x, ...` or `∃ x,
+...`. `rw` can also fail with a "motive is type incorrect" error in the context
+of dependent types. In these cases, consider using `simp only`.
+
+* `rw [e₁, ... eₙ]` applies the given rules sequentially.
+* `rw [← e]` or `rw [<- e]` applies the rewrite in the reverse direction.
+* `rw [e] at l` rewrites with `e` at location(s) `l`.
+* `rw (occs := .pos L) [e]`, where `L` is a literal list of natural numbers,
+  only rewrites the given occurrences in the target. Occurrences count from 1.
+* `rw (occs := .neg L) [e]`, where `L` is a literal list of natural numbers,
+  skips rewriting the given occurrences in the target. Occurrences count from 1.
+
+Examples:
+
+```lean
+example {a b : Nat} (h : a + a = b) : (a + a) + (a + a) = b + b := by rw [h]
+```
+
+```lean
+example {f : Nat -> Nat} (h : ∀ x, f x = 1) (a b : Nat) : f a = f b := by
+  rw [h] -- `rw` instantiates `h` only once, so this is equivalent to: `rw [h a]`
+  -- goal: ⊢ 1 = f b
+  rw [h] -- equivalent to: `rw [h b]`
+```
+````
 
 
 ## Dictionary

script/lakefile.toml

@@ -3,9 +3,3 @@ name = "scripts"
 [[lean_exe]]
 name = "modulize"
 root = "Modulize"
-
-[[lean_exe]]
-name = "shake"
-root = "Shake"
-# needed by `Lake.loadWorkspace`
-supportInterpreter = true

src/CMakeLists.txt

@@ -40,6 +40,10 @@ find_program(LLD_PATH lld)
 if(LLD_PATH)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS_DEFAULT " -fuse-ld=lld")
 endif()
+if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
+  # Create space in install names so they can be patched later in Nix.
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS_DEFAULT " -headerpad_max_install_names")
+endif()
 
 set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
 set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
@@ -452,11 +456,14 @@ if(LLVM AND ${STAGE} GREATER 0)
     message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${CMAKE_CXX_FLAGS}'")
 endif()
 
-# get rid of unused parts of C++ stdlib
+# We always strip away unused declarations to reduce binary sizes as the time cost is small and the
+# potential benefit can be huge, especially when stripping `meta import`s.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-dead_strip")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fdata-sections -ffunction-sections")
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS " -Wl,-dead_strip")
 elseif(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,--gc-sections")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fdata-sections -ffunction-sections")
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS " -Wl,--gc-sections")
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
@@ -631,6 +638,9 @@ if(${STAGE} GREATER 1)
     COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
     COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a"
     COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/temp/libleancpp_1.a" "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
+  add_dependencies(leanrt_initial-exec copy-leancpp)
+  add_dependencies(leanrt copy-leancpp)
+  add_dependencies(leancpp_1 copy-leancpp)
   add_dependencies(leancpp copy-leancpp)
   if(LLVM)
       add_custom_target(copy-lean-h-bc
@@ -695,7 +705,7 @@ endif()
 
 set(STDLIBS Init Std Lean Leanc)
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  list(APPEND STDLIBS Lake)
+  list(APPEND STDLIBS Lake LeanChecker)
 endif()
 
 add_custom_target(make_stdlib ALL
@@ -758,6 +768,12 @@ if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     DEPENDS lake_shared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
     VERBATIM)
+
+  add_custom_target(leanchecker ALL
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS lake_shared
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanchecker
+    VERBATIM)
 endif()
 
 if(PREV_STAGE)

src/Init.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Prelude
 public import Init.Notation
@@ -38,6 +37,7 @@ public import Init.Omega
 public import Init.MacroTrace
 public import Init.Grind
 public import Init.GrindInstances
+public import Init.Sym
 public import Init.While
 public import Init.Syntax
 public import Init.Internal

src/Init/Classical.lean

@@ -102,7 +102,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
       ⟨xp.val, fun _ => xp.property⟩)
     (fun hp => ⟨choice h, fun h => absurd h hp⟩)
 
-/-- the Hilbert epsilon Function -/
+/-- The Hilbert epsilon function. -/
 noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
   (strongIndefiniteDescription p h).val
 

src/Init/Control/Basic.lean

@@ -144,7 +144,7 @@ instance : ToBool Bool where
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores
 `y`; otherwise, runs `y` and returns its result.
 
-This a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
+This is a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
 operator.
 -/
 @[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
@@ -161,7 +161,7 @@ recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»]
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise,
 returns the original result of `x`.
 
-This a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
+This is a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
 operator.
 -/
 @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do

src/Init/Core.lean

@@ -13,6 +13,10 @@ public import Init.SizeOf
 public section
 set_option linter.missingDocs true -- keep it documented
 
+-- BEq instance for Option defined here so it's available early in the import chain
+-- (before Init.Grind.Config and Init.MetaTypes which need BEq (Option Nat))
+deriving instance BEq for Option
+
 @[expose] section
 
 universe u v w
@@ -337,7 +341,7 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where
 An indication of whether a loop's body terminated early that's used to compile the `for x in xs`
 notation.
 
-A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic
+A collection's `ForIn` or `ForIn'` instance describes how to iterate over its elements. The monadic
 action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state
 used to implement features such as `let mut`.
 -/
@@ -510,12 +514,12 @@ abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a
 
 /-- Notation type class for the union operation `∪`. -/
 class Union (α : Type u) where
-  /-- `a ∪ b` is the union of`a` and `b`. -/
+  /-- `a ∪ b` is the union of `a` and `b`. -/
   union : α → α → α
 
 /-- Notation type class for the intersection operation `∩`. -/
 class Inter (α : Type u) where
-  /-- `a ∩ b` is the intersection of`a` and `b`. -/
+  /-- `a ∩ b` is the intersection of `a` and `b`. -/
   inter : α → α → α
 
 /-- Notation type class for the set difference `\`. -/
@@ -538,10 +542,10 @@ infix:50 " ⊇ " => Superset
 /-- Strict superset relation: `a ⊃ b`  -/
 infix:50 " ⊃ " => SSuperset
 
-/-- `a ∪ b` is the union of`a` and `b`. -/
+/-- `a ∪ b` is the union of `a` and `b`. -/
 infixl:65 " ∪ " => Union.union
 
-/-- `a ∩ b` is the intersection of`a` and `b`. -/
+/-- `a ∩ b` is the intersection of `a` and `b`. -/
 infixl:70 " ∩ " => Inter.inter
 
 /--
@@ -1561,6 +1565,10 @@ instance {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q) :=
   | isTrue h => isTrue (propext h)
   | isFalse h => isFalse fun heq => h (heq ▸ Iff.rfl)
 
+/-- Helper theorem for proving injectivity theorems -/
+theorem Lean.injEq_helper {P Q R : Prop} :
+  (P → Q → R) → (P ∧ Q → R) := by intro h ⟨h₁,h₂⟩; exact h h₁ h₂
+
 gen_injective_theorems% Array
 gen_injective_theorems% BitVec
 gen_injective_theorems% ByteArray

src/Init/Data/Array/DecidableEq.lean

@@ -125,6 +125,22 @@ instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) :=
   | ⟨[]⟩ => isTrue rfl
   | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h))
 
+@[inline]
+def instDecidableEqEmpImpl (xs : Array α) : Decidable (xs = #[]) :=
+  decidable_of_iff xs.isEmpty <| by rcases xs with ⟨⟨⟩⟩ <;> simp [Array.isEmpty]
+
+@[inline]
+def instDecidableEmpEqImpl (xs : Array α) : Decidable (#[] = xs) :=
+  decidable_of_iff xs.isEmpty <| by rcases xs with ⟨⟨⟩⟩ <;> simp [Array.isEmpty]
+
+@[csimp]
+theorem instDecidableEqEmp_csimp : @instDecidableEqEmp = @instDecidableEqEmpImpl :=
+  Subsingleton.allEq _ _
+
+@[csimp]
+theorem instDecidableEmpEq_csimp : @instDecidableEmpEq = @instDecidableEmpEqImpl :=
+  Subsingleton.allEq _ _
+
 theorem beq_eq_decide [BEq α] (xs ys : Array α) :
     (xs == ys) = if h : xs.size = ys.size then
       decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by

src/Init/Data/BitVec/Bootstrap.lean

@@ -159,4 +159,17 @@ theorem setWidth_neg_of_le {x : BitVec v} (h : w ≤ v) : BitVec.setWidth w (-x)
     omega
   omega
 
+@[induction_eliminator, elab_as_elim]
+theorem cons_induction {motive : (w : Nat) → BitVec w → Prop} (nil : motive 0 .nil)
+    (cons : ∀ {w : Nat} (b : Bool) (bv : BitVec w), motive w bv → motive (w + 1) (.cons b bv)) :
+    ∀ {w : Nat} (x : BitVec w), motive w x := by
+  intros w x
+  induction w
+  case zero =>
+    simp only [BitVec.eq_nil x, nil]
+  case succ wl ih =>
+    rw [← cons_msb_setWidth x]
+    apply cons
+    apply ih
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -3362,6 +3362,26 @@ theorem extractLsb'_concat {x : BitVec (w + 1)} {y : Bool} :
   · simp
   · simp [show i - 1 < t by omega]
 
+theorem concat_extractLsb'_getLsb {x : BitVec (w + 1)} :
+    BitVec.concat (x.extractLsb' 1 w) (x.getLsb 0) = x := by
+  ext i hw
+  by_cases h : i = 0
+  · simp [h]
+  · simp [h, hw, show (1 + (i - 1)) = i by omega, getElem_concat]
+
+@[elab_as_elim]
+theorem concat_induction {motive : (w : Nat) → BitVec w → Prop} (nil : motive 0 .nil)
+    (concat : ∀ {w : Nat} (bv : BitVec w) (b : Bool), motive w bv → motive (w + 1) (bv.concat b)) :
+    ∀ {w : Nat} (x : BitVec w), motive w x := by
+  intros w x
+  induction w
+  case zero =>
+    simp only [BitVec.eq_nil x, nil]
+  case succ wl ih =>
+    rw [← concat_extractLsb'_getLsb (x := x)]
+    apply concat
+    apply ih
+
 /-! ### shiftConcat -/
 
 @[grind =]
@@ -6383,73 +6403,6 @@ theorem cpopNatRec_add {x : BitVec w} {acc n : Nat} :
     x.cpopNatRec n (acc + acc') = x.cpopNatRec n acc + acc' := by
   rw [cpopNatRec_eq (acc := acc + acc'), cpopNatRec_eq (acc := acc), Nat.add_assoc]
 
-theorem cpopNatRec_le {x : BitVec w} (n : Nat) :
-    x.cpopNatRec n acc ≤ acc + n := by
-  induction n generalizing acc
-  · case zero =>
-    simp
-  · case succ n ihn =>
-    have : (x.getLsbD n).toNat ≤ 1 := by cases x.getLsbD n <;> simp
-    specialize ihn (acc := acc + (x.getLsbD n).toNat)
-    simp
-    omega
-
-@[simp]
-theorem cpopNatRec_of_le {x : BitVec w} (k n : Nat) (hn : w ≤ n) :
-    x.cpopNatRec (n + k) acc = x.cpopNatRec n acc := by
-  induction k
-  · case zero =>
-    simp
-  · case succ k ihk =>
-    simp [show n + (k + 1) = (n + k) + 1 by omega, ihk, show w ≤ n + k by omega]
-
-theorem cpopNatRec_zero_le (x : BitVec w) (n : Nat) :
-    x.cpopNatRec n 0 ≤ w := by
-  induction n
-  · case zero =>
-    simp
-  · case succ n ihn =>
-    by_cases hle : n ≤ w
-    · by_cases hx : x.getLsbD n
-      · have := cpopNatRec_le (x := x) (acc := 1) (by omega)
-        have := lt_of_getLsbD hx
-        simp [hx]
-        omega
-      · have := cpopNatRec_le (x := x) (acc := 0) (by omega)
-        simp [hx]
-        omega
-    · simp [show w ≤ n by omega]
-      omega
-
-@[simp]
-theorem cpopNatRec_allOnes (h : n ≤ w) :
-    (allOnes w).cpopNatRec n acc = acc + n := by
-  induction n
-  · case zero =>
-    simp
-  · case succ n ihn =>
-    specialize ihn (by omega)
-    simp [show n < w by omega, ihn,
-      cpopNatRec_add (acc := acc) (acc' := 1)]
-    omega
-
-@[simp]
-theorem cpop_allOnes :
-    (allOnes w).cpop = BitVec.ofNat w w := by
-  simp [cpop, cpopNatRec_allOnes]
-
-@[simp]
-theorem cpop_zero :
-    (0#w).cpop = 0#w := by
-  simp [cpop]
-
-theorem toNat_cpop_le (x : BitVec w) :
-    x.cpop.toNat ≤ w := by
-  have hlt := Nat.lt_two_pow_self (n := w)
-  have hle := cpopNatRec_zero_le (x := x) (n := w)
-  simp only [cpop, toNat_ofNat, ge_iff_le]
-  rw [Nat.mod_eq_of_lt (by omega)]
-  exact hle
 
 @[simp]
 theorem cpopNatRec_cons_of_le {x : BitVec w} {b : Bool} (hn : n ≤ w) :
@@ -6475,6 +6428,68 @@ theorem cpopNatRec_cons_of_lt {x : BitVec w} {b : Bool} (hn : w < n) :
     · simp [show w = n by omega, getElem_cons,
         cpopNatRec_add (acc := acc) (acc' := b.toNat), Nat.add_comm]
 
+theorem cpopNatRec_le {x : BitVec w} (n : Nat) :
+    x.cpopNatRec n acc ≤ acc + n := by
+  induction n generalizing acc
+  · case zero =>
+    simp
+  · case succ n ihn =>
+    have : (x.getLsbD n).toNat ≤ 1 := by cases x.getLsbD n <;> simp
+    specialize ihn (acc := acc + (x.getLsbD n).toNat)
+    simp
+    omega
+
+@[simp]
+theorem cpopNatRec_of_le {x : BitVec w} (k n : Nat) (hn : w ≤ n) :
+    x.cpopNatRec (n + k) acc = x.cpopNatRec n acc := by
+  induction k
+  · case zero =>
+    simp
+  · case succ k ihk =>
+    simp [show n + (k + 1) = (n + k) + 1 by omega, ihk, show w ≤ n + k by omega]
+
+@[simp]
+theorem cpopNatRec_allOnes (h : n ≤ w) :
+    (allOnes w).cpopNatRec n acc = acc + n := by
+  induction n
+  · case zero =>
+    simp
+  · case succ n ihn =>
+    specialize ihn (by omega)
+    simp [show n < w by omega, ihn,
+      cpopNatRec_add (acc := acc) (acc' := 1)]
+    omega
+
+@[simp]
+theorem cpop_allOnes :
+    (allOnes w).cpop = BitVec.ofNat w w := by
+  simp [cpop, cpopNatRec_allOnes]
+
+@[simp]
+theorem cpop_zero :
+    (0#w).cpop = 0#w := by
+  simp [cpop]
+
+theorem cpopNatRec_zero_le (x : BitVec w) (n : Nat) :
+    x.cpopNatRec n 0 ≤ w := by
+  induction x
+  · case nil => simp
+  · case cons w b bv ih =>
+    by_cases hle : n ≤ w
+    · have := cpopNatRec_cons_of_le (b := b) (x := bv) (n := n) (acc := 0) hle
+      omega
+    · rw [cpopNatRec_cons_of_lt (by omega)]
+      have : b.toNat ≤ 1 := by cases b <;> simp
+      omega
+
+theorem toNat_cpop_le (x : BitVec w) :
+    x.cpop.toNat ≤ w := by
+  have hlt := Nat.lt_two_pow_self (n := w)
+  have hle := cpopNatRec_zero_le (x := x) (n := w)
+  simp only [cpop, toNat_ofNat, ge_iff_le]
+  rw [Nat.mod_eq_of_lt (by omega)]
+  exact hle
+
 theorem cpopNatRec_concat_of_lt {x : BitVec w} {b : Bool} (hn : 0 < n) :
     (concat x b).cpopNatRec n acc = b.toNat + x.cpopNatRec (n - 1) acc := by
   induction n generalizing acc
@@ -6572,12 +6587,12 @@ theorem cpop_cast (x : BitVec w) (h : w = v) :
 @[simp]
 theorem toNat_cpop_append {x : BitVec w} {y : BitVec u} :
     (x ++ y).cpop.toNat = x.cpop.toNat + y.cpop.toNat := by
-  induction w generalizing u
-  · case zero =>
-    simp [cpop]
-  · case succ w ihw =>
-    rw [← cons_msb_setWidth x, toNat_cpop_cons, cons_append, cpop_cast, toNat_cast,
-      toNat_cpop_cons, ihw, ← Nat.add_assoc]
+  induction x generalizing y
+  · case nil =>
+    simp
+  · case cons w b bv ih =>
+    simp [cons_append, ih]
+    omega
 
 theorem cpop_append {x : BitVec w} {y : BitVec u} :
     (x ++ y).cpop = x.cpop.setWidth (w + u) + y.cpop.setWidth (w + u) := by
@@ -6588,4 +6603,14 @@ theorem cpop_append {x : BitVec w} {y : BitVec u} :
   simp only [toNat_cpop_append, toNat_add, toNat_setWidth, Nat.add_mod_mod, Nat.mod_add_mod]
   rw [Nat.mod_eq_of_lt (by omega)]
 
+theorem toNat_cpop_not {x : BitVec w} :
+    (~~~x).cpop.toNat = w - x.cpop.toNat := by
+  induction x
+  · case nil =>
+    simp
+  · case cons b x ih =>
+    have := toNat_cpop_le x
+    cases b
+    <;> (simp [ih]; omega)
+
 end BitVec

src/Init/Data/Iterators/Basic.lean

@@ -10,6 +10,7 @@ public import Init.Classical
 public import Init.Ext
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
@@ -349,14 +350,24 @@ abbrev PlausibleIterStep.casesOn {IsPlausibleStep : IterStep α β → Prop}
 end IterStep
 
 /--
-The typeclass providing the step function of an iterator in `Iter (α := α) β` or
-`IterM (α := α) m β`.
+The step function of an iterator in `Iter (α := α) β` or `IterM (α := α) m β`.
 
 In order to allow intrinsic termination proofs when iterating with the `step` function, the
 step object is bundled with a proof that it is a "plausible" step for the given current iterator.
 -/
 class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) where
+  /--
+  A relation that governs the allowed steps from a given iterator.
+
+  The "plausible" steps are those which make sense for a given state; plausibility can ensure
+  properties such as the successor iterator being drawn from the same collection, that an iterator
+  resulting from a skip will return the same next value, or that the next item yielded is next one
+  in the original collection.
+  -/
   IsPlausibleStep : IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop
+  /--
+  Carries out a step of iteration.
+  -/
   step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
 
 section Monadic
@@ -369,7 +380,7 @@ def IterM.mk {α : Type w} (it : α) (m : Type w → Type w') (β : Type w) :
     IterM (α := α) m β :=
   ⟨it⟩
 
-@[deprecated IterM.mk (since := "2025-12-01"), inline, expose]
+@[deprecated IterM.mk (since := "2025-12-01"), inline, expose, inherit_doc IterM.mk]
 def Iterators.toIterM := @IterM.mk
 
 @[simp]
@@ -377,6 +388,7 @@ theorem IterM.mk_internalState {α m β} (it : IterM (α := α) m β) :
     .mk it.internalState m β = it :=
   rfl
 
+set_option linter.missingDocs false in
 @[deprecated IterM.mk_internalState (since := "2025-12-01")]
 def Iterators.toIterM_internalState := @IterM.mk_internalState
 
@@ -459,8 +471,10 @@ number of steps.
 -/
 inductive IterM.IsPlausibleIndirectOutput {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     : IterM (α := α) m β → β → Prop where
+  /-- The output value could plausibly be emitted in the next step. -/
   | direct {it : IterM (α := α) m β} {out : β} : it.IsPlausibleOutput out →
       it.IsPlausibleIndirectOutput out
+  /-- The output value could plausibly be emitted in a step after the next step. -/
   | indirect {it it' : IterM (α := α) m β} {out : β} : it'.IsPlausibleSuccessorOf it →
       it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
 
@@ -470,7 +484,9 @@ finitely many steps. This relation is reflexive.
 -/
 inductive IterM.IsPlausibleIndirectSuccessorOf {α β : Type w} {m : Type w → Type w'}
     [Iterator α m β] : IterM (α := α) m β → IterM (α := α) m β → Prop where
+  /-- Every iterator is a plausible indirect successor of itself. -/
   | refl (it : IterM (α := α) m β) : it.IsPlausibleIndirectSuccessorOf it
+  /-- The iterator is a plausible successor of one of the current iterator's successors. -/
   | cons_right {it'' it' it : IterM (α := α) m β} (h' : it''.IsPlausibleIndirectSuccessorOf it')
       (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it
 
@@ -595,8 +611,10 @@ number of steps.
 -/
 inductive Iter.IsPlausibleIndirectOutput {α β : Type w} [Iterator α Id β] :
     Iter (α := α) β → β → Prop where
+  /-- The output value could plausibly be emitted in the next step. -/
   | direct {it : Iter (α := α) β} {out : β} : it.IsPlausibleOutput out →
       it.IsPlausibleIndirectOutput out
+  /-- The output value could plausibly be emitted in a step after the next step. -/
   | indirect {it it' : Iter (α := α) β} {out : β} : it'.IsPlausibleSuccessorOf it →
       it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
 
@@ -627,7 +645,9 @@ finitely many steps. This relation is reflexive.
 -/
 inductive Iter.IsPlausibleIndirectSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β] :
     Iter (α := α) β → Iter (α := α) β → Prop where
+  /-- Every iterator is a plausible indirect successor of itself. -/
   | refl (it : Iter (α := α) β) : IsPlausibleIndirectSuccessorOf it it
+  /-- The iterator is a plausible indirect successor of one of the current iterator's successors. -/
   | cons_right {it'' it' it : Iter (α := α) β} (h' : it''.IsPlausibleIndirectSuccessorOf it')
       (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it
 
@@ -701,6 +721,11 @@ recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.fi
 -/
 structure IterM.TerminationMeasures.Finite
     (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  The wrapped iterator.
+
+  In the wrapper, its finiteness is used as a termination measure.
+  -/
   it : IterM (α := α) m β
 
 /--
@@ -827,6 +852,11 @@ recursion over productive iterators. See also `IterM.finitelyManySkips` and `Ite
 -/
 structure IterM.TerminationMeasures.Productive
     (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  The wrapped iterator.
+
+  In the wrapper, its productivity is used as a termination measure.
+  -/
   it : IterM (α := α) m β
 
 /--
@@ -930,6 +960,9 @@ library.
 -/
 class LawfulDeterministicIterator (α : Type w) (m : Type w → Type w') [Iterator α m β]
     where
+  /--
+  Every iterator with state `α` in monad `m` has exactly one plausible step.
+  -/
   isPlausibleStep_eq_eq : ∀ it : IterM (α := α) m β, ∃ step, it.IsPlausibleStep = (· = step)
 
 namespace Iterators
@@ -940,14 +973,13 @@ This structure provides a more convenient way to define `Finite α m` instances
 -/
 structure FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
     [Iterator α m β] where
-  /-
-  A well-founded relation such that if `it'` is a successor iterator of `it`, then
-  `Rel it' it`.
+  /--
+  A well-founded relation such that if `it'` is a successor iterator of `it`, then `Rel it' it`.
   -/
   Rel (it' it : IterM (α := α) m β) : Prop
-  /- A proof that `Rel` is well-founded. -/
+  /-- `Rel` is well-founded. -/
   wf : WellFounded Rel
-  /- A proof that if `it'` is a successor iterator of `it`, then `Rel it' it`. -/
+  /-- If `it'` is a successor iterator of `it`, then `Rel it' it`. -/
   subrelation : ∀ {it it'}, it'.IsPlausibleSuccessorOf it → Rel it' it
 
 theorem Finite.of_finitenessRelation
@@ -967,14 +999,13 @@ This structure provides a more convenient way to define `Productive α m` instan
 -/
 structure ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
     [Iterator α m β] where
-  /-
-  A well-founded relation such that if `it'` is obtained from `it` by skipping, then
-  `Rel it' it`.
+  /--
+  A well-founded relation such that if `it'` is obtained from `it` by skipping, then `Rel it' it`.
   -/
   Rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
-  /- A proof that `Rel` is well-founded. -/
+  /-- `Rel` is well-founded. -/
   wf : WellFounded Rel
-  /- A proof that if `it'` is obtained from `it` by skipping, then `Rel it' it`. -/
+  /-- If `it'` is obtained from `it` by skipping, then `Rel it' it`. -/
   subrelation : ∀ {it it'}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it
 
 theorem Productive.of_productivenessRelation

src/Init/Data/Iterators/Consumers/Access.lean

@@ -9,6 +9,8 @@ prelude
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Access
 
+set_option linter.missingDocs true
+
 @[expose] public section
 
 namespace Std

src/Init/Data/Iterators/Consumers/Monadic/Access.lean

@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -57,8 +59,8 @@ theorem IterM.not_isPlausibleNthOutputStep_yield {α β : Type w} {m : Type w
 
 /--
 `IteratorAccess α m` provides efficient implementations for random access or iterators that support
-it. `it.nextAtIdx? n` either returns the step in which the `n`-th value of `it` is emitted
-(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`-th
+it. `it.nextAtIdx? n` either returns the step in which the `n`th value of `it` is emitted
+(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
 value.
 
 For monadic iterators, the monadic effects of this operation may differ from manually iterating
@@ -68,6 +70,11 @@ is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.
 This class is experimental and users of the iterator API should not explicitly depend on it.
 -/
 class IteratorAccess (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  `nextAtIdx? it n` either returns the step in which the `n`th value of `it` is emitted
+  (necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
+  value.
+  -/
   nextAtIdx? (it : IterM (α := α) m β) (n : Nat) :
     m (PlausibleIterStep (it.IsPlausibleNthOutputStep n))
 

src/Init/Data/Iterators/Consumers/Monadic/Collect.lean

@@ -11,6 +11,8 @@ public import Init.Data.Iterators.Consumers.Monadic.Total
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.WFExtrinsicFix
 
+set_option linter.missingDocs true
+
 @[expose] public section
 
 /-!

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -11,6 +11,8 @@ public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.WFExtrinsicFix
 public import Init.Data.Iterators.Consumers.Monadic.Total
 
+set_option linter.missingDocs true
+
 public section
 
 /-!
@@ -70,6 +72,9 @@ provided by the standard library.
 @[ext]
 class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     (n : Type x → Type x') where
+  /--
+  Iteration over the iterator `it` in the manner expected by `for` loops.
+  -/
   forIn : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x),
       (plausible_forInStep : β → γ → ForInStep γ → Prop) →
       (it : IterM (α := α) m β) → γ →
@@ -82,7 +87,9 @@ end Typeclasses
 structure IteratorLoop.WithWF (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     {γ : Type x} (PlausibleForInStep : β → γ → ForInStep γ → Prop)
     (hwf : IteratorLoop.WellFounded α m PlausibleForInStep) where
+  /-- Internal implementation detail of the iterator library. -/
   it : IterM (α := α) m β
+  /-- Internal implementation detail of the iterator library. -/
   acc : γ
 
 instance IteratorLoop.WithWF.instWellFoundedRelation
@@ -163,6 +170,7 @@ Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultIm
 -/
 class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
     [Monad m] [Monad n] [Iterator α m β] [i : IteratorLoop α m n] where
+  /-- The implementation of `IteratorLoop.forIn` in `i` is equal to the default implementation. -/
   lawful lift [LawfulMonadLiftBindFunction lift] γ it init
       (Pl : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m Pl)
       (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) :
@@ -219,6 +227,7 @@ instance IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w →
   haveI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
   instForInOfForIn'
 
+/-- Internal implementation detail of the iterator library. -/
 @[always_inline, inline]
 def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
@@ -226,6 +235,7 @@ def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
   forIn' it init f :=
     haveI := @IterM.instForIn'; forIn' it.it init f
 
+/-- Internal implementation detail of the iterator library. -/
 @[always_inline, inline]
 def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n]

src/Init/Data/Iterators/Consumers/Monadic/Partial.lean

@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -16,6 +18,9 @@ namespace Std
 A wrapper around an iterator that provides partial consumers. See `IterM.allowNontermination`.
 -/
 structure IterM.Partial {α : Type w} (m : Type w → Type w') (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `IterM.allowNontermination`.
+  -/
   it : IterM (α := α) m β
 
 /--

src/Init/Data/Iterators/Consumers/Monadic/Total.lean

@@ -9,12 +9,19 @@ prelude
 public import Init.Data.Iterators.Basic
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
 namespace Std
 
+/--
+A wrapper around an iterator that provides total consumers. See `IterM.ensureTermination`.
+-/
 structure IterM.Total {α : Type w} (m : Type w → Type w') (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `IterM.ensureTermination`.
+  -/
   it : IterM (α := α) m β
 
 /--

src/Init/Data/Iterators/Consumers/Partial.lean

@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std
@@ -16,6 +18,9 @@ namespace Std
 A wrapper around an iterator that provides partial consumers. See `Iter.allowNontermination`.
 -/
 structure Iter.Partial {α : Type w} (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `Iter.allowNontermination`.
+  -/
   it : Iter (α := α) β
 
 /--

src/Init/Data/Iterators/Consumers/Stream.lean

@@ -9,6 +9,8 @@ prelude
 public import Init.Data.Stream
 public import Init.Data.Iterators.Consumers.Access
 
+set_option linter.missingDocs true
+
 public section
 
 namespace Std

src/Init/Data/Iterators/Consumers/Total.lean

@@ -9,12 +9,19 @@ prelude
 public import Init.Data.Iterators.Basic
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
 namespace Std
 
+/--
+A wrapper around an iterator that provides total consumers. See `Iter.ensureTermination`.
+-/
 structure Iter.Total {α : Type w} (β : Type w) where
+  /--
+  The wrapped iterator, which was wrapped by `Iter.ensureTermination`.
+  -/
   it : Iter (α := α) β
 
 /--

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -72,7 +72,7 @@ def PostconditionT.liftWithProperty {α : Type w} {m : Type w → Type w'} {P :
   ⟨P, x⟩
 
 /--
-Given a function `f : α → β`, returns a a function `PostconditionT m α → PostconditionT m β`,
+Given a function `f : α → β`, returns a function `PostconditionT m α → PostconditionT m β`,
 turning `PostconditionT m` into a functor.
 
 The postcondition of the `x.map f` states that the return value is the image under `f` of some
@@ -85,7 +85,7 @@ protected def PostconditionT.map {m : Type w → Type w'} [Functor m] {α : Type
     (fun a => ⟨f a.val, _, rfl⟩) <$> x.operation⟩
 
 /--
-Given a function `α → PostconditionT m β`, returns a a function
+Given a function `α → PostconditionT m β`, returns a function
 `PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a monad.
 -/
 @[always_inline, inline, expose]

src/Init/Data/LawfulHashable.lean

@@ -11,7 +11,7 @@ public import Init.Core
 public section
 
 /--
-The `BEq α` and `Hashable α` instances on `α` are compatible. This means that that `a == b` implies
+The `BEq α` and `Hashable α` instances on `α` are compatible. This means that `a == b` implies
 `hash a = hash b`.
 
 This is automatic if the `BEq` instance is lawful.

src/Init/Data/List/Basic.lean

@@ -717,6 +717,7 @@ Examples:
  * `["red", "green", "blue"].leftpad 3 "blank" = ["red", "green", "blue"]`
  * `["red", "green", "blue"].leftpad 1 "blank" = ["red", "green", "blue"]`
 -/
+@[simp, grind =]
 def leftpad (n : Nat) (a : α) (l : List α) : List α := replicate (n - length l) a ++ l
 
 
@@ -730,6 +731,7 @@ Examples:
  * `["red", "green", "blue"].rightpad 3 "blank" = ["red", "green", "blue"]`
  * `["red", "green", "blue"].rightpad 1 "blank" = ["red", "green", "blue"]`
 -/
+@[simp, grind =]
 def rightpad (n : Nat) (a : α) (l : List α) : List α := l ++ replicate (n - length l) a
 
 /-! ### reduceOption -/

src/Init/Data/List/Control.lean

@@ -50,7 +50,7 @@ Users that want to use `mapM` with `Applicative` should use `mapA` instead.
 Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of
 results.
 
-This implementation is tail recursive. `List.mapM'` is a a non-tail-recursive variant that may be
+This implementation is tail recursive. `List.mapM'` is a non-tail-recursive variant that may be
 more convenient to reason about. `List.forM` is the variant that discards the results and
 `List.mapA` is the variant that works with `Applicative`.
 -/
@@ -107,7 +107,7 @@ Applies the monadic action `f` to the corresponding elements of two lists, left-
 at the end of the shorter list. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)`
 for lawful `Monad` instances.
 
-This implementation is tail recursive. `List.zipWithM'` is a a non-tail-recursive variant that may
+This implementation is tail recursive. `List.zipWithM'` is a non-tail-recursive variant that may
 be more convenient to reason about.
 -/
 @[inline, expose]

src/Init/Data/List/Lemmas.lean

@@ -2941,9 +2941,6 @@ theorem getLast?_replicate {a : α} {n : Nat} : (replicate n a).getLast? = if n
 
 /-! ### leftpad -/
 
--- We unfold `leftpad` and `rightpad` for verification purposes.
-attribute [simp, grind =] leftpad rightpad
-
 -- `length_leftpad` and `length_rightpad` are in `Init.Data.List.Nat.Basic`.
 
 theorem leftpad_prefix {n : Nat} {a : α} {l : List α} :

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -223,6 +223,16 @@ theorem testBit_lt_two_pow {x i : Nat} (lt : x < 2^i) : x.testBit i = false := b
     exfalso
     exact Nat.not_le_of_gt lt (ge_two_pow_of_testBit p)
 
+theorem testBit_of_two_pow_le_and_two_pow_add_one_gt {n i : Nat}
+    (hle : 2^i ≤ n) (hgt : n < 2^(i + 1)) : n.testBit i = true := by
+  rcases exists_ge_and_testBit_of_ge_two_pow hle with ⟨i', ⟨_, _⟩⟩
+  have : i = i' := by
+    false_or_by_contra
+    have : 2 ^ (i + 1) ≤ 2 ^ i' := Nat.pow_le_pow_of_le (by decide) (by omega)
+    have : n.testBit i' = false := testBit_lt_two_pow (by omega)
+    simp_all only [Bool.false_eq_true]
+  rwa [this]
+
 theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = false) : x < 2^n := by
   apply Decidable.by_contra
   intro not_lt
@@ -231,6 +241,10 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have test_false := p _ i_ge_n
   simp [test_true] at test_false
 
+theorem testBit_log2 {n : Nat} (h : n ≠ 0) : n.testBit n.log2 = true := by
+  have := log2_eq_iff (n := n) (k := n.log2) (by omega)
+  apply testBit_of_two_pow_le_and_two_pow_add_one_gt <;> omega
+
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with
   | zero =>

src/Init/Data/Nat/Lemmas.lean

@@ -10,7 +10,7 @@ import all Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.MinMax
 public import Init.Data.Nat.Log2
 import all Init.Data.Nat.Log2
-public import Init.Data.Nat.Power2
+public import Init.Data.Nat.Power2.Basic
 public import Init.Data.Nat.Mod
 import Init.TacticsExtra
 import Init.BinderPredicates

src/Init/Data/Nat/Power2.lean

@@ -6,66 +6,5 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Nat.Linear
-
-public section
-
-namespace Nat
-
-theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
-  have : power * 2 = power + power := by simp +arith
-  rw [this, Nat.sub_add_eq]
-  exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁
-
-/--
-Returns the least power of two that's greater than or equal to `n`.
-
-Examples:
- * `Nat.nextPowerOfTwo 0 = 1`
- * `Nat.nextPowerOfTwo 1 = 1`
- * `Nat.nextPowerOfTwo 2 = 2`
- * `Nat.nextPowerOfTwo 3 = 4`
- * `Nat.nextPowerOfTwo 5 = 8`
--/
-def nextPowerOfTwo (n : Nat) : Nat :=
-  go 1 (by decide)
-where
-  go (power : Nat) (h : power > 0) : Nat :=
-    if power < n then
-      go (power * 2) (Nat.mul_pos h (by decide))
-    else
-      power
-  termination_by n - power
-  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
-
-/--
-A natural number `n` is a power of two if there exists some `k : Nat` such that `n = 2 ^ k`.
--/
-def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
-
-theorem isPowerOfTwo_one : isPowerOfTwo 1 :=
-  ⟨0, by decide⟩
-
-theorem isPowerOfTwo_mul_two_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
-  have ⟨k, h⟩ := h
-  ⟨k+1, by simp [h, Nat.pow_succ]⟩
-
-theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
-  have ⟨k, h⟩ := h
-  rw [h]
-  apply Nat.pow_pos
-  decide
-
-theorem isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo := by
-  apply isPowerOfTwo_go
-  apply isPowerOfTwo_one
-where
-  isPowerOfTwo_go (power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) : (nextPowerOfTwo.go n power h₁).isPowerOfTwo := by
-    unfold nextPowerOfTwo.go
-    split
-    . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₂)
-    . assumption
-  termination_by n - power
-  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
-
-end Nat
+public import Init.Data.Nat.Power2.Basic
+public import Init.Data.Nat.Power2.Lemmas

src/Init/Data/Nat/Power2/Basic.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.Nat.Linear
+
+public section
+
+namespace Nat
+
+theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
+  have : power * 2 = power + power := by simp +arith
+  rw [this, Nat.sub_add_eq]
+  exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁
+
+/--
+Returns the least power of two that's greater than or equal to `n`.
+
+Examples:
+ * `Nat.nextPowerOfTwo 0 = 1`
+ * `Nat.nextPowerOfTwo 1 = 1`
+ * `Nat.nextPowerOfTwo 2 = 2`
+ * `Nat.nextPowerOfTwo 3 = 4`
+ * `Nat.nextPowerOfTwo 5 = 8`
+-/
+def nextPowerOfTwo (n : Nat) : Nat :=
+  go 1 (by decide)
+where
+  go (power : Nat) (h : power > 0) : Nat :=
+    if power < n then
+      go (power * 2) (Nat.mul_pos h (by decide))
+    else
+      power
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+
+/--
+A natural number `n` is a power of two if there exists some `k : Nat` such that `n = 2 ^ k`.
+-/
+def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
+
+theorem isPowerOfTwo_one : isPowerOfTwo 1 :=
+  ⟨0, by decide⟩
+
+theorem isPowerOfTwo_mul_two_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
+  have ⟨k, h⟩ := h
+  ⟨k+1, by simp [h, Nat.pow_succ]⟩
+
+theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
+  have ⟨k, h⟩ := h
+  rw [h]
+  apply Nat.pow_pos
+  decide
+
+theorem isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo := by
+  apply isPowerOfTwo_go
+  apply isPowerOfTwo_one
+where
+  isPowerOfTwo_go (power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) : (nextPowerOfTwo.go n power h₁).isPowerOfTwo := by
+    unfold nextPowerOfTwo.go
+    split
+    . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₂)
+    . assumption
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+
+end Nat

src/Init/Data/Nat/Power2/Lemmas.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) George Rennie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: George Rennie
+-/
+module
+
+prelude
+import all Init.Data.Nat.Power2.Basic
+public import Init.Data.Nat.Bitwise.Lemmas
+
+public section
+
+/-!
+# Further lemmas about `Nat.isPowerOfTwo`, with the convenience of having bitwise lemmas available.
+-/
+
+namespace Nat
+
+theorem not_isPowerOfTwo_zero : ¬isPowerOfTwo 0 := by
+  rw [isPowerOfTwo, not_exists]
+  intro x
+  have := one_le_pow x 2 (by decide)
+  omega
+
+theorem and_sub_one_testBit_log2 {n : Nat} (h : n ≠ 0) (hpow2 : ¬n.isPowerOfTwo) :
+    (n &&& (n - 1)).testBit n.log2 := by
+  rw [testBit_and, Bool.and_eq_true]
+  constructor
+  · exact testBit_log2 (by omega)
+  · by_cases n = 2^n.log2
+    · rw [isPowerOfTwo, not_exists] at hpow2
+      have := hpow2 n.log2
+      trivial
+    · have := log2_eq_iff (n := n) (k := n.log2) (by omega)
+      have : (n - 1).log2 = n.log2 := by rw [log2_eq_iff] <;> omega
+      rw [←this]
+      exact testBit_log2 (by omega)
+
+theorem and_sub_one_eq_zero_iff_isPowerOfTwo {n : Nat} (h : n ≠ 0) :
+    (n &&& (n - 1)) = 0 ↔ n.isPowerOfTwo := by
+  constructor
+  · intro hbitwise
+    false_or_by_contra
+    rename_i hpow2
+    have := and_sub_one_testBit_log2 h hpow2
+    rwa [hbitwise, zero_testBit n.log2, Bool.false_eq_true] at this
+  · intro hpow2
+    rcases hpow2 with ⟨_, hpow2⟩
+    rw [hpow2, and_two_pow_sub_one_eq_mod, mod_self]
+
+theorem ne_zero_and_sub_one_eq_zero_iff_isPowerOfTwo {n : Nat} :
+    ((n ≠ 0) ∧ (n &&& (n - 1)) = 0) ↔ n.isPowerOfTwo := by
+  match h : n with
+  | 0 => simp [not_isPowerOfTwo_zero]
+  | n + 1 => simp; exact and_sub_one_eq_zero_iff_isPowerOfTwo (by omega)
+
+@[inline]
+instance {n : Nat} : Decidable n.isPowerOfTwo :=
+  decidable_of_iff _ ne_zero_and_sub_one_eq_zero_iff_isPowerOfTwo
+
+end Nat

src/Init/Data/Order/Ord.lean

@@ -46,7 +46,7 @@ theorem ne_of_cmp_ne_eq {α : Type u} {cmp : α → α → Ordering} [Std.ReflCm
 
 end ReflCmp
 
-/-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
+/-- A typeclass for ordered types for which `compare a a = .eq` for all `a`. -/
 abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering)
 
 @[simp]

src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean

@@ -246,8 +246,12 @@ class InfinitelyUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
 This propositional typeclass ensures that `UpwardEnumerable.succ?` is injective.
 -/
 class LinearlyUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
+  /-- The implementation of `UpwardEnumerable.succ?` for `α` is injective. -/
   eq_of_succ?_eq : ∀ a b : α, UpwardEnumerable.succ? a = UpwardEnumerable.succ? b → a = b
 
+/--
+If a type is infinitely upwardly enumerable, then every element has a successor.
+-/
 theorem UpwardEnumerable.isSome_succ? {α : Type u} [UpwardEnumerable α]
     [InfinitelyUpwardEnumerable α] {a : α} : (succ? a).isSome :=
   InfinitelyUpwardEnumerable.isSome_succ? a

src/Init/Data/Slice/Array/Iterator.lean

@@ -148,6 +148,7 @@ theorem Subarray.copy_eq_toArray {s : Subarray α} :
     s.copy = s.toArray :=
   (rfl)
 
+@[grind =]
 theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :
     Slice.toArray s = s.toArray :=
   (rfl)

src/Init/Data/Slice/Array/Lemmas.lean

@@ -119,6 +119,13 @@ public theorem forIn_toList {α : Type u} {s : Subarray α}
     ForIn.forIn s.toList init f = ForIn.forIn s init f :=
   Slice.forIn_toList
 
+@[grind =]
+public theorem forIn_eq_forIn_toList {α : Type u} {s : Subarray α}
+    {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
+    {f : α → γ → m (ForInStep γ)} :
+    ForIn.forIn s init f = ForIn.forIn s.toList init f :=
+  forIn_toList.symm
+
 @[simp]
 public theorem forIn_toArray {α : Type u} {s : Subarray α}
     {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
@@ -167,22 +174,22 @@ public theorem Array.toSubarray_eq_min {xs : Array α} {lo hi : Nat} :
   simp only [Array.toSubarray]
   split <;> split <;> simp [Nat.min_eq_right (Nat.le_of_not_ge _), *]
 
-@[simp]
+@[simp, grind =]
 public theorem Array.array_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).array = xs := by
   simp [toSubarray_eq_min, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem Array.start_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).start = min lo (min hi xs.size) := by
   simp [toSubarray_eq_min, Subarray.start]
 
-@[simp]
+@[simp, grind =]
 public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).stop = min hi xs.size := by
   simp [toSubarray_eq_min, Subarray.stop]
 
-theorem Subarray.toList_eq {xs : Subarray α} :
+public theorem Subarray.toList_eq {xs : Subarray α} :
     xs.toList = (xs.array.extract xs.start xs.stop).toList := by
   let aslice := xs
   obtain ⟨⟨array, start, stop, h₁, h₂⟩⟩ := xs
@@ -199,45 +206,46 @@ theorem Subarray.toList_eq {xs : Subarray α} :
       simp [Subarray.array, Subarray.start, Subarray.stop]
   simp [this, ListSlice.toList_eq, lslice]
 
+@[grind =]
 public theorem Subarray.size_eq {xs : Subarray α} :
     xs.size = xs.stop - xs.start := by
   simp [Subarray.size]
 
-@[simp]
+@[simp, grind =]
 public theorem Subarray.toArray_toList {xs : Subarray α} :
     xs.toList.toArray = xs.toArray := by
   simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
 
-@[simp]
+@[simp, grind =]
 public theorem Subarray.toList_toArray {xs : Subarray α} :
     xs.toArray.toList = xs.toList := by
   simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
 
-@[simp]
+@[simp, grind =]
 public theorem Subarray.length_toList {xs : Subarray α} :
     xs.toList.length = xs.size := by
   have : xs.start ≤ xs.stop := xs.internalRepresentation.start_le_stop
   have : xs.stop ≤ xs.array.size := xs.internalRepresentation.stop_le_array_size
   simp [Subarray.toList_eq, Subarray.size]; omega
 
-@[simp]
+@[simp, grind =]
 public theorem Subarray.size_toArray {xs : Subarray α} :
     xs.toArray.size = xs.size := by
   simp [← Subarray.toArray_toList, Subarray.size, Slice.size, SliceSize.size, start, stop]
 
 namespace Array
 
-@[simp]
+@[simp, grind =]
 public theorem array_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].array = xs := by
   simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].start = min lo (min hi xs.size) := by
   simp [Std.Rco.Sliceable.mkSlice]
 
-@[simp]
+@[simp, grind =]
 public theorem stop_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].stop = min hi xs.size := by
   simp [Std.Rco.Sliceable.mkSlice]
@@ -246,14 +254,14 @@ public theorem mkSlice_rco_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
     xs[lo...hi] = xs[(min lo (min hi xs.size))...(min hi xs.size)] := by
   simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray_eq_min]
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
   rw [List.take_eq_take_min, List.drop_eq_drop_min]
   simp [Std.Rco.Sliceable.mkSlice, Subarray.toList_eq, List.take_drop,
     Nat.add_sub_of_le (Nat.min_le_right _ _)]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].toArray = xs.extract lo hi := by
   simp only [← Subarray.toArray_toList, toList_mkSlice_rco]
@@ -266,12 +274,12 @@ public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     · simp; omega
     · simp; omega
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].size = min hi xs.size - lo := by
   simp [← Subarray.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -280,7 +288,7 @@ public theorem mkSlice_rcc_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
     xs[lo...=hi] = xs[(min lo (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
 
-@[simp]
+@[simp, grind =]
 public theorem array_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
     xs[lo...=hi].array = xs := by
   simp [Std.Rcc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@@ -325,7 +333,7 @@ public theorem stop_mkSlice_rci {xs : Array α} {lo : Nat} :
     xs[lo...*].stop = xs.size := by
   simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rci_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
     xs[lo...*] = xs[lo...xs.size] := by
   simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
@@ -344,7 +352,7 @@ public theorem toArray_mkSlice_rci {xs : Array α} {lo : Nat} :
     xs[lo...*].toArray = xs.extract lo := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rci {xs : Array α} {lo : Nat} :
     xs[lo...*].size = xs.size - lo := by
   simp [← Subarray.length_toList]
@@ -364,7 +372,7 @@ public theorem stop_mkSlice_roo {xs : Array α} {lo hi : Nat} :
     xs[lo<...hi].stop = min hi xs.size := by
   simp [Std.Roo.Sliceable.mkSlice]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -408,6 +416,11 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Array α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
   simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp
+
 public theorem mkSlice_roc_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(min (lo + 1) (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -452,6 +465,11 @@ public theorem mkSlice_roi_eq_mkSlice_roo {xs : Array α} {lo : Nat} :
     xs[lo<...*] = xs[lo<...xs.size] := by
   simp [mkSlice_rci_eq_mkSlice_rco]
 
+@[grind =]
+public theorem mkSlice_roi_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
+    xs[lo<...*] = xs[(lo + 1)...xs.size] := by
+  simp [mkSlice_rci_eq_mkSlice_rco]
+
 public theorem mkSlice_roi_eq_mkSlice_roo_min {xs : Array α} {lo : Nat} :
     xs[lo<...*] = xs[(min (lo + 1) xs.size)...xs.size] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -476,7 +494,7 @@ public theorem array_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...hi].array = xs := by
   simp [Std.Rio.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...hi].start = 0 := by
   simp [Std.Rio.Sliceable.mkSlice]
@@ -486,7 +504,7 @@ public theorem stop_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...hi].stop = min hi xs.size := by
   simp [Std.Rio.Sliceable.mkSlice]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -515,7 +533,7 @@ public theorem array_mkSlice_ric {xs : Array α} {hi : Nat} :
     xs[*...=hi].array = xs := by
   simp [Std.Ric.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_ric {xs : Array α} {hi : Nat} :
     xs[*...=hi].start = 0 := by
   simp [Std.Ric.Sliceable.mkSlice]
@@ -530,6 +548,11 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...=hi] = xs[*...(hi + 1)] := by
   simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp
+
 public theorem mkSlice_ric_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} :
     xs[*...=hi] = xs[*...(min (hi + 1) xs.size)] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -559,11 +582,16 @@ public theorem mkSlice_rii_eq_mkSlice_rio {xs : Array α} :
     xs[*...*] = xs[*...xs.size] := by
   simp [mkSlice_rci_eq_mkSlice_rco]
 
+@[grind =]
+public theorem mkSlice_rii_eq_mkSlice_rco {xs : Array α} :
+    xs[*...*] = xs[0...xs.size] := by
+  simp
+
 public theorem mkSlice_rii_eq_mkSlice_rio_min {xs : Array α} :
     xs[*...*] = xs[*...xs.size] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rii {xs : Array α} :
     xs[*...*].toList = xs.toList := by
   rw [mkSlice_rii_eq_mkSlice_rci, toList_mkSlice_rci, List.drop_zero]
@@ -573,7 +601,7 @@ public theorem toArray_mkSlice_rii {xs : Array α} :
     xs[*...*].toArray = xs := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rii {xs : Array α} :
     xs[*...*].size = xs.size := by
   simp [← Subarray.length_toList]
@@ -583,12 +611,12 @@ public theorem array_mkSlice_rii {xs : Array α} :
     xs[*...*].array = xs := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_rii {xs : Array α} :
     xs[*...*].start = 0 := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem stop_mkSlice_rii {xs : Array α} :
     xs[*...*].stop = xs.size := by
   simp [Std.Rii.Sliceable.mkSlice]
@@ -599,7 +627,7 @@ section SubarraySlices
 
 namespace Subarray
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
   simp only [Std.Rco.Sliceable.mkSlice, Std.Rco.HasRcoIntersection.intersection, toList_eq,
@@ -608,12 +636,12 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
   rw [Nat.add_sub_cancel' (by omega)]
   simp [Subarray.size, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...hi].toArray = xs.toArray.extract lo hi := by
   simp [← Subarray.toArray_toList, List.drop_take]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
@@ -629,7 +657,7 @@ public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
     xs[lo...*] = xs[lo...xs.size] := by
   simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
@@ -651,12 +679,17 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
   simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice,
     Std.Roc.HasRcoIntersection.intersection, Std.Roo.HasRcoIntersection.intersection]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
     Std.Roo.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
 
+@[grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by
@@ -670,8 +703,7 @@ public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
 @[simp]
 public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
-  simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
-    Std.Roc.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
+  simp
 
 @[simp]
 public theorem toList_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
@@ -689,6 +721,11 @@ public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
   simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice,
     Std.Roi.HasRcoIntersection.intersection, Std.Rci.HasRcoIntersection.intersection]
 
+@[grind =]
+public theorem mkSlice_roi_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
+    xs[lo<...*] = xs[(lo + 1)...xs.size] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roi {xs : Subarray α} {lo : Nat} :
     xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
@@ -705,12 +742,17 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
   simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice,
     Std.Ric.HasRcoIntersection.intersection, Std.Rio.HasRcoIntersection.intersection]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
     Std.Rio.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_rio {xs : Subarray α} {hi : Nat} :
     xs[*...hi].toList = xs.toList.take hi := by
@@ -737,7 +779,7 @@ public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
     xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rii {xs : Subarray α} :
     xs[*...*] = xs := by
   simp [Std.Rii.Sliceable.mkSlice]

src/Init/Data/Slice/List/Lemmas.lean

@@ -47,21 +47,28 @@ public theorem toList_eq {xs : ListSlice α} :
   simp only [Std.Slice.toList, toList_internalIter]
   rfl
 
+@[simp, grind =]
 public theorem toArray_toList {xs : ListSlice α} :
     xs.toList.toArray = xs.toArray := by
   simp [Std.Slice.toArray, Std.Slice.toList]
 
+@[simp, grind =]
 public theorem toList_toArray {xs : ListSlice α} :
     xs.toArray.toList = xs.toList := by
   simp [Std.Slice.toArray, Std.Slice.toList]
 
-@[simp]
+@[simp, grind =]
 public theorem length_toList {xs : ListSlice α} :
     xs.toList.length = xs.size := by
   simp [ListSlice.toList_eq, Std.Slice.size, Std.Slice.SliceSize.size, ← Iter.length_toList_eq_count,
     toList_internalIter]; rfl
 
-@[simp]
+@[grind =]
+public theorem size_eq_length_toList {xs : ListSlice α} :
+    xs.size = xs.toList.length :=
+  length_toList.symm
+
+@[simp, grind =]
 public theorem size_toArray {xs : ListSlice α} :
     xs.toArray.size = xs.size := by
   simp [← ListSlice.toArray_toList]
@@ -70,7 +77,7 @@ end ListSlice
 
 namespace List
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.take hi).drop lo := by
   rw [List.take_eq_take_min, List.drop_eq_drop_min]
@@ -81,17 +88,17 @@ public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
   · have : min hi xs.length ≤ lo := by omega
     simp [h, Nat.min_eq_right this]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toArray = ((xs.take hi).drop lo).toArray := by
   simp [← ListSlice.toArray_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].size = min hi xs.length - lo := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -122,12 +129,22 @@ public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].toArray = (xs.drop lo).toArray := by
   simp [← ListSlice.toArray_toList]
 
+@[grind =]
+public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo...*].toList = xs[lo...xs.length].toList := by
+  simp
+
+@[grind =]
+public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo...*].toArray = xs[lo...xs.length].toArray := by
+  simp
+
 @[simp]
 public theorem size_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].size = xs.length - lo := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -152,6 +169,11 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : List α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
   simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
 
+@[simp, grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roc {xs : List α} {lo hi : Nat} :
     xs[lo<...=hi].toList = (xs.take (hi + 1)).drop (lo + 1) := by
@@ -167,11 +189,27 @@ public theorem size_mkSlice_roc {xs : List α} {lo hi : Nat} :
     xs[lo<...=hi].size = min (hi + 1) xs.length - (lo + 1) := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roi_eq_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo<...*] = xs[(lo + 1)...*] := by
   simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
 
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : List α} {lo : Nat} :
+    xs[lo<...*].toList = xs[lo<...xs.length].toList := by
+  simp
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : List α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[lo<...xs.length].toArray := by
+  simp
+
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo<...*].toList = xs[(lo + 1)...xs.length].toList := by
+  simp
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[(lo + 1)...xs.length].toArray := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roi {xs : List α} {lo : Nat} :
     xs[lo<...*].toList = xs.drop (lo + 1) := by
@@ -187,7 +225,7 @@ public theorem size_mkSlice_roi {xs : List α} {lo : Nat} :
     xs[lo<...*].size = xs.length - (lo + 1) := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : List α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -212,6 +250,11 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : List α} {hi : Nat} :
     xs[*...=hi] = xs[*...(hi + 1)] := by
   simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : List α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_ric {xs : List α} {hi : Nat} :
     xs[*...=hi].toList = xs.take (hi + 1) := by
@@ -227,11 +270,19 @@ public theorem size_mkSlice_ric {xs : List α} {hi : Nat} :
     xs[*...=hi].size = min (hi + 1) xs.length := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rii_eq_mkSlice_rci {xs : List α} :
     xs[*...*] = xs[0...*] := by
   simp [Std.Rii.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
 
+public theorem toList_mkSlice_rii_eq_toList_mkSlice_rco {xs : List α} :
+    xs[*...*].toList = xs[0...xs.length].toList := by
+  simp
+
+public theorem toArray_mkSlice_rii_eq_toArray_mkSlice_rco {xs : List α} :
+    xs[*...*].toArray = xs[0...xs.length].toArray := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_rii {xs : List α} :
     xs[*...*].toList = xs := by
@@ -253,7 +304,7 @@ section ListSubslices
 
 namespace ListSlice
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
   simp only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
@@ -262,12 +313,12 @@ public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
   · simp
   · simp [List.take_take, Nat.min_comm]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toArray = xs.toArray.extract lo hi := by
   simp [← toArray_toList, List.drop_take]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -295,9 +346,19 @@ public theorem toArray_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo...*].toArray = xs.toArray.extract lo := by
   simp only [← toArray_toList, toList_mkSlice_rci]
   rw (occs := [1]) [← List.take_length (l := List.drop lo xs.toList)]
+  simp [- toArray_toList]
+
+@[grind =]
+public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo...*].toList = xs[lo...xs.size].toList := by
+  simp [← length_toList, - Slice.length_toList_eq_size]
+
+@[grind =]
+public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo...*].toArray = xs[lo...xs.size].toArray := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -322,6 +383,11 @@ public theorem mkSlice_roc_eq_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
   simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
 
+@[simp, grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
+
 @[simp]
 public theorem toList_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by
@@ -332,11 +398,28 @@ public theorem toArray_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...=hi].toArray = xs.toArray.extract (lo + 1) (hi + 1) := by
   simp [← toArray_toList, List.drop_take]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roi_eq_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo<...*] = xs[(lo + 1)...*] := by
   simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
 
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toList = xs[lo<...xs.size].toList := by
+  simp [← length_toList, - Slice.length_toList_eq_size]
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[lo<...xs.size].toArray := by
+  simp only [mkSlice_roi_eq_mkSlice_rci, toArray_mkSlice_rci, size_toArray_eq_size,
+    mkSlice_roo_eq_mkSlice_rco, toArray_mkSlice_rco]
+
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toList = xs[(lo + 1)...xs.size].toList := by
+  simp [← length_toList, - Slice.length_toList_eq_size]
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[(lo + 1)...xs.size].toArray := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
     xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
@@ -347,9 +430,9 @@ public theorem toArray_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
     xs[lo<...*].toArray = xs.toArray.extract (lo + 1) := by
   simp only [← toArray_toList, toList_mkSlice_roi]
   rw (occs := [1]) [← List.take_length (l := List.drop (lo + 1) xs.toList)]
-  simp
+  simp [- toArray_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -374,6 +457,11 @@ public theorem mkSlice_ric_eq_mkSlice_rcc {xs : ListSlice α} {hi : Nat} :
     xs[*...=hi] = xs[0...=hi] := by
   simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
+
 @[simp]
 public theorem toList_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
     xs[*...=hi].toList = xs.toList.take (hi + 1) := by
@@ -384,7 +472,7 @@ public theorem toArray_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
     xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
   simp [← toArray_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rii {xs : ListSlice α} :
     xs[*...*] = xs := by
   simp [Std.Rii.Sliceable.mkSlice]

src/Init/Data/Slice/Notation.lean

@@ -40,7 +40,7 @@ class Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type
 This typeclass indicates how to obtain slices of elements of {lit}`α` over ranges in the index type
 {lit}`β`, the ranges being left-closed right-open.
 
-The type of resulting the slices is {lit}`γ`.
+The type of the resulting slices is {lit}`γ`.
 -/
 class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
   /--

src/Init/Data/String/Bootstrap.lean

@@ -123,18 +123,6 @@ opaque getUTF8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
 
 end String.Internal
 
-/--
-Creates a string that contains the characters in a list, in order.
-
-Examples:
- * `['L', '∃', '∀', 'N'].asString = "L∃∀N"`
- * `[].asString = ""`
- * `['a', 'a', 'a'].asString = "aaa"`
--/
-@[extern "lean_string_mk", expose]
-def String.ofList (data : List Char) : String :=
-  ⟨List.utf8Encode data,.intro data rfl⟩
-
 @[extern "lean_string_mk", expose, deprecated String.ofList (since := "2025-10-30")]
 def String.mk (data : List Char) : String :=
   ⟨List.utf8Encode data,.intro data rfl⟩

src/Init/Data/String/Pattern/String.lean

@@ -119,7 +119,7 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w
       -- **Invariant 1:** we have already covered everything up until `stackPos - needlePos` (exclusive),
       -- with matches and rejections.
       -- **Invariant 2:** `stackPos - needlePos` is a valid position
-      -- **Invariant 3:** the range from from `stackPos - needlePos` to `stackPos` (exclusive) is a
+      -- **Invariant 3:** the range from `stackPos - needlePos` to `stackPos` (exclusive) is a
       -- prefix of the pattern.
       if h₁ : stackPos < s.rawEndPos then
         let stackByte := s.getUTF8Byte stackPos h₁

src/Init/Data/String/Slice.lean

@@ -20,7 +20,7 @@ functionality for searching for various kinds of pattern matches in slices to it
 provide subslices according to matches etc. The key design principles behind this module are:
 - Instead of providing one function per kind of pattern the API is generic over various kinds of
   patterns. Thus it only provides e.g. one kind of function for looking for the position of the
-  first occurence of a pattern. Currently the supported patterns are:
+  first occurrence of a pattern. Currently the supported patterns are:
   - {name}`Char`
   - {lean}`Char → Bool`
   - {name}`String` and {name}`String.Slice` (partially: doing non trivial searches backwards is not

src/Init/Grind/Config.lean

@@ -21,6 +21,8 @@ structure Config where
   /-- 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
+  /-- If `locals` is `true`, `grind` will add all definitions from the current file. -/
+  locals : 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. -/

src/Init/Grind/Ring/CommSolver.lean

@@ -766,7 +766,7 @@ def Poly.cancelVar (c : Int) (x : Var) (p : Poly) : Poly :=
           (fun _ _ _ _ => a.toPoly_k.pow k)
           (fun _ _ _ _ => a.toPoly_k.pow k)
           (fun _ _ _ => a.toPoly_k.pow k)
-          a) = match (generalizing := false) a with
+          a) = match a with
             | num n => Poly.num (n ^ k)
             | .intCast n => .num (n^k)
             | .natCast n => .num (n^k)

src/Init/MetaTypes.lean

@@ -132,12 +132,18 @@ structure Config where
   Unused `have`s are still removed if `zeta` or `zetaUnused` are true.
   -/
   zetaHave : Bool := true
+  /--
+  If `locals` is `true`, `dsimp` will unfold all definitions from the current file.
+  For local theorems, use `+suggestions` instead.
+  -/
+  locals : Bool := false
   deriving Inhabited, BEq
 
 end DSimp
 
 namespace Simp
 
+@[inline]
 def defaultMaxSteps := 100000
 
 /--
@@ -297,6 +303,11 @@ structure Config where
   and attempt to use the resulting suggestions as parameters to the `simp` tactic.
   -/
   suggestions : Bool := false
+  /--
+  If `locals` is `true`, `simp` will unfold all definitions from the current file.
+  For local theorems, use `+suggestions` instead.
+  -/
+  locals : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Init/Notation.lean

@@ -523,7 +523,7 @@ macro_rules
   | `(bif $c then $t else $e) => `(cond $c $t $e)
 
 /--
-Haskell-like pipe operator `<|`. `f <| x` means the same as the same as `f x`,
+Haskell-like pipe operator `<|`. `f <| x` means the same as `f x`,
 except that it parses `x` with lower precedence, which means that `f <| g <| x`
 is interpreted as `f (g x)` rather than `(f g) x`.
 -/
@@ -557,7 +557,7 @@ macro_rules
   | `($a |> $f)        => `($f $a)
 
 /--
-Alternative syntax for `<|`. `f $ x` means the same as the same as `f x`,
+Alternative syntax for `<|`. `f $ x` means the same as `f x`,
 except that it parses `x` with lower precedence, which means that `f $ g $ x`
 is interpreted as `f (g x)` rather than `(f g) x`.
 -/
@@ -782,9 +782,16 @@ Position reporting for `#guard_msgs`:
 -/
 syntax guardMsgsPositions := &"positions" " := " guardMsgsPositionsArg
 
+/--
+Substring matching for `#guard_msgs`:
+- `substring := true` checks that the docstring appears as a substring of the output.
+- `substring := false` (the default) requires exact matching (modulo whitespace normalization).
+-/
+syntax guardMsgsSubstring := &"substring" " := " (&"true" <|> &"false")
+
 set_option linter.missingDocs false in
 syntax guardMsgsSpecElt :=
-  guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering <|> guardMsgsPositions
+  guardMsgsFilter <|> guardMsgsWhitespace <|> guardMsgsOrdering <|> guardMsgsPositions <|> guardMsgsSubstring
 
 set_option linter.missingDocs false in
 syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
@@ -860,6 +867,11 @@ Position reporting:
   `#guard_msgs` appears.
 - `positions := false` does not report position info.
 
+Substring matching:
+- `substring := true` checks that the docstring appears as a substring of the output
+  (after whitespace normalization). This is useful when you only care about part of the message.
+- `substring := false` (the default) requires exact matching (modulo whitespace normalization).
+
 For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop
 everything else.
 
@@ -873,6 +885,13 @@ The top-level command elaborator only runs the linters if `#guard_msgs` is not p
 syntax (name := guardMsgsCmd)
   (plainDocComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
 
+/--
+`#guard_panic in cmd` runs `cmd` and succeeds if the command produces a panic message.
+This is useful for testing that a command panics without matching the exact (volatile) panic text.
+-/
+syntax (name := guardPanicCmd)
+  "#guard_panic" " in" ppLine command : command
+
 /--
 Format and print the info trees for a given command.
 This is mostly useful for debugging info trees.

src/Init/NotationExtra.lean

@@ -67,7 +67,7 @@ syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
 syntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
-  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") unifConstraint : command
+  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") ppSpace unifConstraint : command
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do
@@ -120,7 +120,7 @@ calc
   _ = z := pyz
 ```
 It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
-<proof>`. This is useful for aligning relation symbols, especially on longer:
+<proof>`. This is useful for aligning relation symbols, especially on longer
 identifiers:
 ```
 calc abc

src/Init/Prelude.lean

@@ -907,7 +907,7 @@ instance [Inhabited α] : Inhabited (ULift α) where
 Lifts a type or proposition to a higher universe level.
 
 `PULift α` wraps a value of type `α`. It is a generalization of
-`PLift` that allows lifting values who's type may live in `Sort s`.
+`PLift` that allows lifting values whose type may live in `Sort s`.
 It also subsumes `PLift`.
 -/
 -- The universe variable `r` is written first so that `ULift.{r} α` can be used
@@ -3192,7 +3192,7 @@ Constructs a new empty array with initial capacity `0`.
 
 Use `Array.emptyWithCapacity` to create an array with a greater initial capacity.
 -/
-@[expose]
+@[expose, inline]
 def Array.empty {α : Type u} : Array α := emptyWithCapacity 0
 
 /--
@@ -3481,6 +3481,18 @@ structure String where ofByteArray ::
 attribute [extern "lean_string_to_utf8"] String.toByteArray
 attribute [extern "lean_string_from_utf8_unchecked"] String.ofByteArray
 
+/--
+Creates a string that contains the characters in a list, in order.
+
+Examples:
+ * `String.ofList ['L', '∃', '∀', 'N'] = "L∃∀N"`
+ * `String.ofList [] = ""`
+ * `String.ofList ['a', 'a', 'a'] = "aaa"`
+-/
+@[extern "lean_string_mk"]
+def String.ofList (data : List Char) : String :=
+  ⟨List.utf8Encode data, .intro data rfl⟩
+
 /--
 Decides whether two strings are equal. Normally used via the `DecidableEq String` instance and the
 `=` operator.
@@ -3525,7 +3537,7 @@ instance : DecidableEq String.Pos.Raw :=
 /--
 A region or slice of some underlying string.
 
-A substring contains an string together with the start and end byte positions of a region of
+A substring contains a string together with the start and end byte positions of a region of
 interest. Actually extracting a substring requires copying and memory allocation, while many
 substrings of the same underlying string may exist with very little overhead, and they are more
 convenient than tracking the bounds by hand.

src/Init/SimpLemmas.lean

@@ -38,6 +38,12 @@ theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) :
 theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   h₁ ▸ h₂ ▸ rfl
 
+theorem implies_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) : (p₁ → q) = (p₂ → q) :=
+  h ▸ rfl
+
+theorem implies_congr_right {p : Sort u} {q₁ q₂ : Sort v} (h : q₁ = q₂) : (p → q₁) = (p → q₂) :=
+  h ▸ rfl
+
 theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) :=
   Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl)
 

src/Init/Sym.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Init.Sym.Lemmas

src/Init/Sym/Lemmas.lean

@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Init.Data.Nat.Basic
+public import Init.Data.Rat.Basic
+public import Init.Data.Int.Basic
+public import Init.Data.UInt.Basic
+public import Init.Data.SInt.Basic
+public section
+namespace Lean.Sym
+
+theorem ne_self (a : α) : (a ≠ a) = False := by simp
+
+theorem ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α)
+    (c' : Prop) {inst' : Decidable c'} (h : c = c') : @ite α c inst a b = @ite α c' inst' a b := by
+  simp [*]
+
+theorem dite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α)
+    (c' : Prop) {inst' : Decidable c'} (h : c = c')
+    : @dite α c inst a b = @dite α c' inst' (fun h' => a (h.mpr_prop h')) (fun h' => b (h.mpr_not h')) := by
+  simp [*]
+
+theorem cond_cond_eq_true {α : Sort u} (c : Bool) (a b : α) (h : c = true) : cond c a b = a := by
+  simp [*]
+
+theorem cond_cond_eq_false {α : Sort u} (c : Bool) (a b : α) (h : c = false) : cond c a b = b := by
+  simp [*]
+
+theorem cond_cond_congr {α : Sort u} (c : Bool) (a b : α) (c' : Bool) (h : c = c') : cond c a b = cond c' a b := by
+  simp [*]
+
+theorem Nat.lt_eq_true (a b : Nat) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Int.lt_eq_true (a b : Int) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Rat.lt_eq_true (a b : Rat) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Int8.lt_eq_true (a b : Int8) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Int16.lt_eq_true (a b : Int16) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Int32.lt_eq_true (a b : Int32) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Int64.lt_eq_true (a b : Int64) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem UInt8.lt_eq_true (a b : UInt8) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem UInt16.lt_eq_true (a b : UInt16) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem UInt32.lt_eq_true (a b : UInt32) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem UInt64.lt_eq_true (a b : UInt64) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Fin.lt_eq_true (a b : Fin n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem BitVec.lt_eq_true (a b : BitVec n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+
+theorem Nat.lt_eq_false (a b : Nat) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Int.lt_eq_false (a b : Int) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Rat.lt_eq_false (a b : Rat) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Int8.lt_eq_false (a b : Int8) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Int16.lt_eq_false (a b : Int16) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Int32.lt_eq_false (a b : Int32) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Int64.lt_eq_false (a b : Int64) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem UInt8.lt_eq_false (a b : UInt8) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem UInt16.lt_eq_false (a b : UInt16) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem UInt32.lt_eq_false (a b : UInt32) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem UInt64.lt_eq_false (a b : UInt64) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Fin.lt_eq_false (a b : Fin n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem BitVec.lt_eq_false (a b : BitVec n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+
+theorem Nat.le_eq_true (a b : Nat) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Int.le_eq_true (a b : Int) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Rat.le_eq_true (a b : Rat) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Int8.le_eq_true (a b : Int8) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Int16.le_eq_true (a b : Int16) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Int32.le_eq_true (a b : Int32) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Int64.le_eq_true (a b : Int64) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem UInt8.le_eq_true (a b : UInt8) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem UInt16.le_eq_true (a b : UInt16) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem UInt32.le_eq_true (a b : UInt32) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem UInt64.le_eq_true (a b : UInt64) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Fin.le_eq_true (a b : Fin n) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem BitVec.le_eq_true (a b : BitVec n) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+
+theorem Nat.le_eq_false (a b : Nat) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Int.le_eq_false (a b : Int) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Rat.le_eq_false (a b : Rat) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Int8.le_eq_false (a b : Int8) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Int16.le_eq_false (a b : Int16) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Int32.le_eq_false (a b : Int32) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Int64.le_eq_false (a b : Int64) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem UInt8.le_eq_false (a b : UInt8) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem UInt16.le_eq_false (a b : UInt16) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem UInt32.le_eq_false (a b : UInt32) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem UInt64.le_eq_false (a b : UInt64) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Fin.le_eq_false (a b : Fin n) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem BitVec.le_eq_false (a b : BitVec n) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+
+theorem Nat.gt_eq_true (a b : Nat) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem Int.gt_eq_true (a b : Int) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem Rat.gt_eq_true (a b : Rat) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem Int8.gt_eq_true (a b : Int8) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem Int16.gt_eq_true (a b : Int16) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem Int32.gt_eq_true (a b : Int32) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem Int64.gt_eq_true (a b : Int64) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem UInt8.gt_eq_true (a b : UInt8) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem UInt16.gt_eq_true (a b : UInt16) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem UInt32.gt_eq_true (a b : UInt32) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem UInt64.gt_eq_true (a b : UInt64) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem Fin.gt_eq_true (a b : Fin n) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+theorem BitVec.gt_eq_true (a b : BitVec n) (h : decide (a > b) = true) : (a > b) = True := by simp_all
+
+theorem Nat.gt_eq_false (a b : Nat) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem Int.gt_eq_false (a b : Int) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem Rat.gt_eq_false (a b : Rat) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem Int8.gt_eq_false (a b : Int8) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem Int16.gt_eq_false (a b : Int16) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem Int32.gt_eq_false (a b : Int32) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem Int64.gt_eq_false (a b : Int64) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem UInt8.gt_eq_false (a b : UInt8) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem UInt16.gt_eq_false (a b : UInt16) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem UInt32.gt_eq_false (a b : UInt32) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem UInt64.gt_eq_false (a b : UInt64) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem Fin.gt_eq_false (a b : Fin n) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+theorem BitVec.gt_eq_false (a b : BitVec n) (h : decide (a > b) = false) : (a > b) = False := by simp_all
+
+theorem Nat.ge_eq_true (a b : Nat) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem Int.ge_eq_true (a b : Int) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem Rat.ge_eq_true (a b : Rat) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem Int8.ge_eq_true (a b : Int8) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem Int16.ge_eq_true (a b : Int16) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem Int32.ge_eq_true (a b : Int32) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem Int64.ge_eq_true (a b : Int64) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem UInt8.ge_eq_true (a b : UInt8) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem UInt16.ge_eq_true (a b : UInt16) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem UInt32.ge_eq_true (a b : UInt32) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem UInt64.ge_eq_true (a b : UInt64) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem Fin.ge_eq_true (a b : Fin n) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+theorem BitVec.ge_eq_true (a b : BitVec n) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
+
+theorem Nat.ge_eq_false (a b : Nat) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem Int.ge_eq_false (a b : Int) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem Rat.ge_eq_false (a b : Rat) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem Int8.ge_eq_false (a b : Int8) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem Int16.ge_eq_false (a b : Int16) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem Int32.ge_eq_false (a b : Int32) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem Int64.ge_eq_false (a b : Int64) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem UInt8.ge_eq_false (a b : UInt8) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem UInt16.ge_eq_false (a b : UInt16) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem UInt32.ge_eq_false (a b : UInt32) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem UInt64.ge_eq_false (a b : UInt64) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem Fin.ge_eq_false (a b : Fin n) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem BitVec.ge_eq_false (a b : BitVec n) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+
+theorem Nat.eq_eq_true (a b : Nat) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Int.eq_eq_true (a b : Int) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Rat.eq_eq_true (a b : Rat) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Int8.eq_eq_true (a b : Int8) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Int16.eq_eq_true (a b : Int16) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Int32.eq_eq_true (a b : Int32) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Int64.eq_eq_true (a b : Int64) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem UInt8.eq_eq_true (a b : UInt8) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem UInt16.eq_eq_true (a b : UInt16) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem UInt32.eq_eq_true (a b : UInt32) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem UInt64.eq_eq_true (a b : UInt64) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Fin.eq_eq_true (a b : Fin n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem BitVec.eq_eq_true (a b : BitVec n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+
+theorem Nat.eq_eq_false (a b : Nat) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Int.eq_eq_false (a b : Int) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Rat.eq_eq_false (a b : Rat) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Int8.eq_eq_false (a b : Int8) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Int16.eq_eq_false (a b : Int16) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Int32.eq_eq_false (a b : Int32) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Int64.eq_eq_false (a b : Int64) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem UInt8.eq_eq_false (a b : UInt8) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem UInt16.eq_eq_false (a b : UInt16) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem UInt32.eq_eq_false (a b : UInt32) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem UInt64.eq_eq_false (a b : UInt64) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Fin.eq_eq_false (a b : Fin n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem BitVec.eq_eq_false (a b : BitVec n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+
+theorem Nat.ne_eq_true (a b : Nat) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem Int.ne_eq_true (a b : Int) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem Rat.ne_eq_true (a b : Rat) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem Int8.ne_eq_true (a b : Int8) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem Int16.ne_eq_true (a b : Int16) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem Int32.ne_eq_true (a b : Int32) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem Int64.ne_eq_true (a b : Int64) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem UInt8.ne_eq_true (a b : UInt8) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem UInt16.ne_eq_true (a b : UInt16) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem UInt32.ne_eq_true (a b : UInt32) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem UInt64.ne_eq_true (a b : UInt64) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem Fin.ne_eq_true (a b : Fin n) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+theorem BitVec.ne_eq_true (a b : BitVec n) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
+
+theorem Nat.ne_eq_false (a b : Nat) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem Int.ne_eq_false (a b : Int) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem Rat.ne_eq_false (a b : Rat) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem Int8.ne_eq_false (a b : Int8) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem Int16.ne_eq_false (a b : Int16) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem Int32.ne_eq_false (a b : Int32) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem Int64.ne_eq_false (a b : Int64) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem UInt8.ne_eq_false (a b : UInt8) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem UInt16.ne_eq_false (a b : UInt16) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem UInt32.ne_eq_false (a b : UInt32) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem UInt64.ne_eq_false (a b : UInt64) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem Fin.ne_eq_false (a b : Fin n) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem BitVec.ne_eq_false (a b : BitVec n) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+
+theorem Nat.dvd_eq_true (a b : Nat) (h : decide (a ∣ b) = true) : (a ∣ b) = True := by simp_all
+theorem Int.dvd_eq_true (a b : Int) (h : decide (a ∣ b) = true) : (a ∣ b) = True := by simp_all
+
+theorem Nat.dvd_eq_false (a b : Nat) (h : decide (a ∣ b) = false) : (a ∣ b) = False := by simp_all
+theorem Int.dvd_eq_false (a b : Int) (h : decide (a ∣ b) = false) : (a ∣ b) = False := by simp_all
+
+end Lean.Sym

src/Init/System/FilePath.lean

@@ -150,7 +150,7 @@ def parent (p : FilePath) : Option FilePath :=
 /--
 Extracts the last element of a path if it is a file or directory name.
 
-Returns `none ` if the last entry is a special name (such as `.` or `..`) or if the path is the root
+Returns `none` if the last entry is a special name (such as `.` or `..`) or if the path is the root
 directory.
 -/
 def fileName (p : FilePath) : Option String :=

src/Init/System/IO.lean

@@ -561,7 +561,7 @@ Waits for the task to finish, then returns its result.
   return t.get
 
 /--
-Waits until any of the tasks in the list has finished, then return its result.
+Waits until any of the tasks in the list has finished, then returns its result.
 -/
 @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α))
     (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α :=
@@ -679,7 +679,7 @@ File handles wrap the underlying operating system's file descriptors. There is n
 to close a file: when the last reference to a file handle is dropped, the file is closed
 automatically.
 
-Handles have an associated read/write cursor that determines the where reads and writes occur in the
+Handles have an associated read/write cursor that determines where reads and writes occur in the
 file.
 -/
 opaque FS.Handle : Type := Unit
@@ -790,7 +790,7 @@ An exception is thrown if the file cannot be opened.
 /--
 Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary.
 
-Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
 works on Unix-like systems but not on Windows.
 -/
 @[extern "lean_io_prim_handle_lock"] opaque lock (h : @& Handle) (exclusive := true) : IO Unit
@@ -798,7 +798,7 @@ works on Unix-like systems but not on Windows.
 Tries to acquire an exclusive or shared lock on the handle and returns `true` if successful. Will
 not block if the lock cannot be acquired, but instead returns `false`.
 
-Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it
+Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it
 works on Unix-like systems but not on Windows.
 -/
 @[extern "lean_io_prim_handle_try_lock"] opaque tryLock (h : @& Handle) (exclusive := true) : IO Bool
@@ -1350,7 +1350,7 @@ def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → Fi
     removeFile path
 
 /--
-Creates a temporary directory in the most secure manner possible, providing a its path to an `IO`
+Creates a temporary directory in the most secure manner possible, providing its path to an `IO`
 action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how
 or when they were created.
 
@@ -1480,7 +1480,7 @@ possible to close the child's standard input before the process terminates, whic
 @[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
 
 /--
-Blocks until the child process has exited and return its exit code.
+Blocks until the child process has exited and returns its exit code.
 -/
 @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
@@ -1586,7 +1586,7 @@ end Process
 /--
 POSIX-style file permissions.
 
-The `FileRight` structure describes these permissions for a file's owner, members of it's designated
+The `FileRight` structure describes these permissions for a file's owner, members of its designated
 group, and all others.
 -/
 structure AccessRight where
@@ -1863,7 +1863,7 @@ unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a
 
 set_option linter.unusedVariables false in
 /--
-Discards the passed owned reference. This leads to `a` any any object reachable from it never being
+Discards the passed owned reference. This leads to `a` and any object reachable from it never being
 freed. This can be a useful optimization for eliding deallocation time of big object graphs that are
 kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent`
 would be similarly costly to deallocation). It is still considered a safe operation as it cannot

src/Init/Tactics.lean

@@ -546,7 +546,7 @@ introducing new local definitions.
 For example, given a local hypotheses if the form `h : let x := v; b x`, then `extract_lets z at h`
 introduces a new local definition `z := v` and changes `h` to be `h : b z`.
 -/
-syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* (location)? : tactic
+syntax (name := extractLets) "extract_lets" ppSpace optConfig (ppSpace colGt (ident <|> hole))* (location)? : tactic
 
 /--
 Lifts `let` and `have` expressions within a term as far out as possible.

src/Init/Try.lean

@@ -58,6 +58,9 @@ syntax (name := attemptAll) "attempt_all " withPosition((ppDedent(ppLine) colGe
 /-- Helper internal tactic for implementing the tactic `try?` with parallel execution. -/
 syntax (name := attemptAllPar) "attempt_all_par " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
+/-- Helper internal tactic for implementing the tactic `try?` with parallel execution, returning first success. -/
+syntax (name := firstPar) "first_par " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
+
 /-- Helper internal tactic used to implement `evalSuggest` in `try?` -/
 syntax (name := tryResult) "try_suggestions " tactic* : tactic
 

src/Init/WF.lean

@@ -463,7 +463,7 @@ variable {motive : α → Sort v}
 variable (h : α → Nat)
 variable (F : (x : α) → ((y : α) → InvImage (· < ·) h y x → motive y) → motive x)
 
-/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evalutes to a ground term. -/
+/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evaluates to a ground term. -/
 def Nat.eager (n : Nat) : Nat :=
   if Nat.beq n n = true then n else n
 
@@ -474,8 +474,8 @@ A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a
 its higher order function argument `F` to invoke its argument only on values `y` that are smaller
 than `x` with regard to `h`.
 
-In contrast to to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
-when `h x` evalutes to a ground value)
+In contrast to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
+when `h x` evaluates to a ground value)
 
 -/
 def Nat.fix : (x : α) → motive x :=

src/Lean/Compiler/ClosedTermCache.lean

@@ -28,7 +28,8 @@ builtin_initialize closedTermCacheExt : EnvExtension ClosedTermCache ←
         { s with map := s.map.insert e c, constNames := s.constNames.insert c, revExprs := e :: s.revExprs })
 
 def cacheClosedTermName (env : Environment) (e : Expr) (n : Name) : Environment :=
-  closedTermCacheExt.modifyState env fun s => { s with map := s.map.insert e n, constNames := s.constNames.insert n }
+  closedTermCacheExt.modifyState env fun s =>
+    { s with map := s.map.insert e n, constNames := s.constNames.insert n, revExprs := e :: s.revExprs }
 
 def getClosedTermName? (env : Environment) (e : Expr) : Option Name :=
   (closedTermCacheExt.getState env).map.find? e

src/Lean/Compiler/IR/CompilerM.lean

@@ -44,7 +44,7 @@ def log (entry : LogEntry) : CompilerM Unit :=
 def tracePrefixOptionName := `trace.compiler.ir
 
 private def isLogEnabledFor (opts : Options) (optName : Name) : Bool :=
-  match opts.find optName with
+  match opts.get? optName with
   | some (DataValue.ofBool v) => v
   | _     => opts.getBool tracePrefixOptionName
 

src/Lean/Compiler/LCNF.lean

@@ -45,3 +45,4 @@ public import Lean.Compiler.LCNF.LambdaLifting
 public import Lean.Compiler.LCNF.ReduceArity
 public import Lean.Compiler.LCNF.Probing
 public import Lean.Compiler.LCNF.Irrelevant
+public import Lean.Compiler.LCNF.SplitSCC

src/Lean/Compiler/LCNF/Basic.lean

@@ -147,18 +147,11 @@ inductive Alt where
   | alt (ctorName : Name) (params : Array Param) (code : Code)
   | default (code : Code)
 
-structure FunDecl where
-  fvarId : FVarId
-  binderName : Name
-  params : Array Param
-  type : Expr
-  value : Code
+inductive FunDecl where
+  | mk (fvarId : FVarId) (binderName : Name) (params : Array Param) (type : Expr) (value : Code)
 
-structure Cases where
-  typeName : Name
-  resultType : Expr
-  discr : FVarId
-  alts : Array Alt
+inductive Cases where
+  | mk (typeName : Name) (resultType : Expr) (discr : FVarId) (alts : Array Alt)
   deriving Inhabited
 
 inductive Code where
@@ -173,6 +166,57 @@ inductive Code where
 
 end
 
+@[inline]
+def FunDecl.fvarId : FunDecl → FVarId
+  | .mk (fvarId := fvarId) .. => fvarId
+
+@[inline]
+def FunDecl.binderName : FunDecl → Name
+  | .mk (binderName := binderName) .. => binderName
+
+@[inline]
+def FunDecl.params : FunDecl → Array Param
+  | .mk (params := params) .. => params
+
+@[inline]
+def FunDecl.type : FunDecl → Expr
+  | .mk (type := type) .. => type
+
+@[inline]
+def FunDecl.value : FunDecl → Code
+  | .mk (value := value) .. => value
+
+@[inline]
+def FunDecl.updateBinderName : FunDecl → Name → FunDecl
+  | .mk fvarId _ params type value, new =>
+    .mk fvarId new params type value
+
+@[inline]
+def FunDecl.toParam (decl : FunDecl) (borrow : Bool) : Param :=
+  match decl with
+  | .mk fvarId binderName _ type .. => ⟨fvarId, binderName, type, borrow⟩
+
+@[inline]
+def Cases.typeName : Cases → Name
+  | .mk (typeName := typeName) .. => typeName
+
+@[inline]
+def Cases.resultType : Cases → Expr
+  | .mk (resultType := resultType) .. => resultType
+
+@[inline]
+def Cases.discr : Cases → FVarId
+  | .mk (discr := discr) .. => discr
+
+@[inline]
+def Cases.alts : Cases → Array Alt
+  | .mk (alts := alts) .. => alts
+
+@[inline]
+def Cases.updateAlts : Cases → Array Alt → Cases
+  | .mk typeName resultType discr _, new =>
+    .mk typeName resultType discr new
+
 deriving instance Inhabited for Alt
 deriving instance Inhabited for FunDecl
 
@@ -281,14 +325,18 @@ private unsafe def updateAltImp (alt : Alt) (ps' : Array Param) (k' : Code) : Al
 
 @[inline] private unsafe def updateAltsImp (c : Code) (alts : Array Alt) : Code :=
   match c with
-  | .cases cs => if ptrEq cs.alts alts then c else .cases { cs with alts }
+  | .cases cs => if ptrEq cs.alts alts then c else .cases <| cs.updateAlts alts
   | _ => unreachable!
 
 @[implemented_by updateAltsImp] opaque Code.updateAlts! (c : Code) (alts : Array Alt) : Code
 
 @[inline] private unsafe def updateCasesImp (c : Code) (resultType : Expr) (discr : FVarId) (alts : Array Alt) : Code :=
   match c with
-  | .cases cs => if ptrEq cs.alts alts && ptrEq cs.resultType resultType && cs.discr == discr then c else .cases { cs with discr, resultType, alts }
+  | .cases cs =>
+    if ptrEq cs.alts alts && ptrEq cs.resultType resultType && cs.discr == discr then
+      c
+    else
+      .cases <| ⟨cs.typeName, resultType, discr, alts⟩
   | _ => unreachable!
 
 @[implemented_by updateCasesImp] opaque Code.updateCases! (c : Code) (resultType : Expr) (discr : FVarId) (alts : Array Alt) : Code
@@ -368,7 +416,7 @@ private unsafe def updateFunDeclCoreImp (decl: FunDecl) (type : Expr) (params :
   if ptrEq type decl.type && ptrEq params decl.params && ptrEq value decl.value then
     decl
   else
-    { decl with type, params, value }
+    ⟨decl.fvarId, decl.binderName, params, type, value⟩
 
 /--
 Low-level update `FunDecl` function. It does not update the local context.
@@ -378,7 +426,7 @@ to be updated.
 @[implemented_by updateFunDeclCoreImp] opaque FunDecl.updateCore (decl : FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
 def Cases.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
-  let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
+  let found i := (cases.alts[i]!, cases.updateAlts (cases.alts.eraseIdx! i))
   if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
     found i
   else if let some i := cases.alts.findFinIdx? fun | .default _ => true | _ => false then

src/Lean/Compiler/LCNF/Bind.lean

@@ -48,7 +48,7 @@ where
       if alts.isEmpty then
         throwError "`Code.bind` failed, empty `cases` found"
       let resultType ← mkCasesResultType alts
-      return .cases { c with alts, resultType }
+      return .cases ⟨c.typeName, resultType, c.discr, alts⟩
     | .return fvarId => f fvarId
     | .jmp fvarId .. =>
       unless (← read).contains fvarId do

src/Lean/Compiler/LCNF/Check.lean

@@ -258,45 +258,4 @@ end Check
 def Decl.check (decl : Decl) : CompilerM Unit := do
   Check.run do decl.value.forCodeM (Check.checkFunDeclCore decl.name decl.params decl.type)
 
-/--
-Check whether every local declaration in the local context is used in one of given `decls`.
--/
-partial def checkDeadLocalDecls (decls : Array Decl) : CompilerM Unit := do
-  let (_, s) := visitDecls decls |>.run {}
-  let usesFVar (binderName : Name) (fvarId : FVarId) :=
-    unless s.contains fvarId do
-      throwError "LCNF local context contains unused local variable declaration `{binderName}`"
-  let lctx := (← get).lctx
-  lctx.params.forM fun fvarId decl => usesFVar decl.binderName fvarId
-  lctx.letDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
-  lctx.funDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
-where
-  visitFVar (fvarId : FVarId) : StateM FVarIdHashSet Unit :=
-    modify (·.insert fvarId)
-
-  visitParam (param : Param) : StateM FVarIdHashSet Unit := do
-    visitFVar param.fvarId
-
-  visitParams (params : Array Param) : StateM FVarIdHashSet Unit := do
-    params.forM visitParam
-
-  visitCode (code : Code) : StateM FVarIdHashSet Unit := do
-    match code with
-    | .jmp .. | .return .. | .unreach .. => return ()
-    | .let decl k => visitFVar decl.fvarId; visitCode k
-    | .fun decl k | .jp decl k =>
-      visitFVar decl.fvarId; visitParams decl.params; visitCode decl.value
-      visitCode k
-    | .cases c => c.alts.forM fun alt => do
-      match alt with
-      | .default k => visitCode k
-      | .alt _ ps k => visitParams ps; visitCode k
-
-  visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
-    visitParams decl.params
-    decl.value.forCodeM visitCode
-
-  visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
-    decls.forM visitDecl
-
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Closure.lean

@@ -137,7 +137,7 @@ mutual
         /- We only collect the variables in the scope of the function application being specialized. -/
         if let some funDecl ← findFunDecl? fvarId then
           if ctx.abstract funDecl.fvarId then
-            modify fun s => { s with params := s.params.push <| { funDecl with borrow := false } }
+            modify fun s => { s with params := s.params.push <| funDecl.toParam false }
           else
             collectFunDecl funDecl
             modify fun s => { s with decls := s.decls.push <| .fun funDecl }
@@ -156,7 +156,8 @@ mutual
 
   /-- Collect dependencies of the given expression. -/
   partial def collectType (type : Expr) : ClosureM Unit := do
-    type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId!
+    if type.hasFVar then
+      type.forEachWhere Expr.isFVar fun e => collectFVar e.fvarId!
 
 end
 

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -359,7 +359,7 @@ def mkLetDecl (binderName : Name) (type : Expr) (value : LetValue) : CompilerM L
 def mkFunDecl (binderName : Name) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl := do
   let fvarId ← mkFreshFVarId
   let binderName ← ensureNotAnonymous binderName `_f
-  let funDecl := { fvarId, binderName, type, params, value }
+  let funDecl := ⟨fvarId, binderName, params, type, value⟩
   modifyLCtx fun lctx => lctx.addFunDecl funDecl
   return funDecl
 
@@ -397,7 +397,7 @@ private unsafe def updateFunDeclImp (decl : FunDecl) (type : Expr) (params : Arr
   if ptrEq type decl.type && ptrEq params decl.params && ptrEq value decl.value then
     return decl
   else
-    let decl := { decl with type, params, value }
+    let decl := ⟨decl.fvarId, decl.binderName, params, type, value⟩
     modifyLCtx fun lctx => lctx.addFunDecl decl
     return decl
 

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -52,6 +52,10 @@ structure Context where
 
 structure State where
   decls : Array Decl := {}
+  /--
+  Cache for `shouldExtractFVar` in order to avoid superlinear behavior.
+  -/
+  fvarDecisionCache : Std.HashMap FVarId Bool := {}
 
 abbrev M := ReaderT Context $ StateRefT State CompilerM
 
@@ -78,6 +82,10 @@ partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
         | _ => true
         if !shouldExtract then
           return false
+      if let some decl ← LCNF.getMonoDecl? name then
+        -- We don't want to extract constants as root terms
+        if decl.getArity == 0 then
+          return false
     args.allM shouldExtractArg
   | .fvar fnVar args => return (← shouldExtractFVar fnVar) && (← args.allM shouldExtractArg)
   | .proj _ _ baseVar => shouldExtractFVar baseVar
@@ -88,10 +96,18 @@ partial def shouldExtractArg (arg : Arg) : M Bool := do
   | .type _ | .erased => return true
 
 partial def shouldExtractFVar (fvarId : FVarId) : M Bool := do
-  if let some letDecl ← findLetDecl? fvarId then
-    shouldExtractLetValue false letDecl.value
+  if let some result := (← get).fvarDecisionCache[fvarId]? then
+    return result
   else
-    return false
+    let result ← go
+    modify fun s => { s with fvarDecisionCache := s.fvarDecisionCache.insert fvarId result }
+    return result
+where
+  go : M Bool := do
+    if let some letDecl ← findLetDecl? fvarId then
+      shouldExtractLetValue false letDecl.value
+    else
+      return false
 
 end
 

src/Lean/Compiler/LCNF/FloatLetIn.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Compiler.LCNF.FVarUtil
 public import Lean.Compiler.LCNF.PassManager
+import Lean.Compiler.IR.CompilerM
 
 public section
 
@@ -19,30 +20,27 @@ namespace FloatLetIn
 The decision of the float mechanism.
 -/
 inductive Decision where
-|
   /--
   Push into the arm with name `name`.
   -/
-  arm (name : Name)
-| /--
+  | arm (name : Name)
+  /--
   Push into the default arm.
   -/
-  default
-|
+  | default
   /--
   Don't move this declaration it is needed where it is right now.
   -/
-  dont
-|
+  | dont
   /--
   No decision has been made yet.
   -/
-  unknown
+  | unknown
 deriving Hashable, BEq, Inhabited, Repr
 
 def Decision.ofAlt : Alt → Decision
-| .alt name _ _ => .arm name
-| .default _ => .default
+  | .alt name _ _ => .arm name
+  | .default _ => .default
 
 /--
 The context for `BaseFloatM`.
@@ -112,6 +110,7 @@ def ignore? (decl : LetDecl) : BaseFloatM Bool :=  do
 Compute the initial decision for all declarations that `BaseFloatM` collected
 up to this point, with respect to `cs`. The initial decisions are:
 - `dont` if the declaration is detected by `ignore?`
+- `dont` if the a variable used by the declaration is later used as a potentially owned parameter
 - `dont` if the declaration is the discriminant of `cs` since we obviously need
   the discriminant to be computed before the match.
 - `dont` if we see the declaration being used in more than one cases arm
@@ -120,20 +119,55 @@ up to this point, with respect to `cs`. The initial decisions are:
 -/
 def initialDecisions (cs : Cases) : BaseFloatM (Std.HashMap FVarId Decision) := do
   let mut map := Std.HashMap.emptyWithCapacity (← read).decls.length
-  map ← (← read).decls.foldrM (init := map) fun val acc => do
+  let owned : Std.HashSet FVarId := ∅
+  (map, _) ← (← read).decls.foldlM (init := (map, owned)) fun (acc, owned) val => do
     if let .let decl := val then
       if (← ignore? decl) then
-        return acc.insert decl.fvarId .dont
-    return acc.insert val.fvarId .unknown
+        return (acc.insert decl.fvarId .dont, owned)
+    let (dont, owned) := (visitDecl (← getEnv) val).run owned
+    if dont then
+      return (acc.insert val.fvarId .dont, owned)
+    else
+      return (acc.insert val.fvarId .unknown, owned)
 
   if map.contains cs.discr then
     map := map.insert cs.discr .dont
   (_, map) ← goCases cs |>.run map
   return map
 where
+  visitDecl (env : Environment) (value : CodeDecl) : StateM (Std.HashSet FVarId) Bool := do
+    match value with
+    | .let decl => visitLetValue env decl.value
+    | _ => return false -- will need to investigate whether that can be a problem
+
+  visitLetValue (env : Environment) (value : LetValue) : StateM (Std.HashSet FVarId) Bool := do
+    match value with
+    | .proj _ _ x => visitArg (.fvar x) true
+    | .const nm _ args =>
+      let decl? := IR.findEnvDecl env nm
+      match decl? with
+      | none => args.foldlM (fun b arg => visitArg arg false <||> pure b) false
+      | some decl =>
+        let mut res := false
+        for h : i in *...args.size do
+          if ← visitArg args[i] (decl.params[i]?.any (·.borrow)) then
+            res := true
+        return res
+    | .fvar x args =>
+      args.foldlM (fun b arg => visitArg arg false <||> pure b)
+        (← visitArg (.fvar x) false)
+    | .erased | .lit _ => return false
+
+  visitArg (var : Arg) (borrowed : Bool) : StateM (Std.HashSet FVarId) Bool := do
+    let .fvar v := var | return false
+    let res := (← get).contains v
+    unless borrowed do
+      modify (·.insert v)
+    return res
+
   goFVar (plannedDecision : Decision) (var : FVarId) : StateRefT (Std.HashMap FVarId Decision) BaseFloatM Unit := do
     if let some decision := (← get)[var]? then
-      if decision == .unknown then
+      if decision matches .unknown then
         modify fun s => s.insert var plannedDecision
       else if decision != plannedDecision then
         modify fun s => s.insert var .dont

src/Lean/Compiler/LCNF/Internalize.lean

@@ -119,7 +119,7 @@ partial def internalizeFunDecl (decl : FunDecl) : InternalizeM FunDecl := do
   let params ← decl.params.mapM internalizeParam
   let value ← internalizeCode decl.value
   let fvarId ← mkNewFVarId decl.fvarId
-  let decl := { decl with binderName, fvarId, params, type, value }
+  let decl := ⟨fvarId, binderName, params, type, value⟩
   modifyLCtx fun lctx => lctx.addFunDecl decl
   return decl
 
@@ -139,7 +139,7 @@ partial def internalizeCode (code : Code) : InternalizeM Code := do
       let alts ← c.alts.mapM fun
         | .alt ctorName params k => return .alt ctorName (← params.mapM internalizeParam) (← internalizeAltCode k)
         | .default k => return .default (← internalizeAltCode k)
-      return .cases { c with discr, alts, resultType }
+      return .cases ⟨c.typeName, resultType, discr, alts⟩
 
 end
 

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -229,10 +229,8 @@ where
       | _, _ => return Code.updateLet! code decl (← go k)
     | .fun decl k =>
       if let some replacement := (← read)[decl.fvarId]? then
-        let newDecl := { decl with
-          binderName := replacement,
-          value := (← go decl.value)
-        }
+        let newValue ← go decl.value
+        let newDecl := ⟨decl.fvarId, replacement, decl.params, decl.type, newValue⟩
         modifyLCtx fun lctx => lctx.addFunDecl newDecl
         return .jp newDecl (← go k)
       else

src/Lean/Compiler/LCNF/Main.lean

@@ -11,6 +11,7 @@ public import Lean.Compiler.LCNF.Passes
 public import Lean.Compiler.LCNF.ToDecl
 public import Lean.Compiler.LCNF.Check
 import Lean.Meta.Match.MatcherInfo
+import Lean.Compiler.LCNF.SplitSCC
 public section
 namespace Lean.Compiler.LCNF
 /--
@@ -50,14 +51,12 @@ The trace can be viewed with `set_option trace.Compiler.step true`.
 def checkpoint (stepName : Name) (decls : Array Decl) (shouldCheck : Bool) : CompilerM Unit := do
   for decl in decls do
     trace[Compiler.stat] "{decl.name} : {decl.size}"
-    withOptions (fun opts => opts.setBool `pp.motives.pi false) do
+    withOptions (fun opts => opts.set `pp.motives.pi false) do
       let clsName := `Compiler ++ stepName
       if (← Lean.isTracingEnabledFor clsName) then
         Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}"
       if shouldCheck then
         decl.check
-  if shouldCheck then
-    checkDeadLocalDecls decls
 
 def isValidMainType (type : Expr) : Bool :=
   let isValidResultName (name : Name) : Bool :=
@@ -74,7 +73,7 @@ def isValidMainType (type : Expr) : Bool :=
 
 namespace PassManager
 
-def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRecDepth 8192 do
+def run (declNames : Array Name) : CompilerM (Array (Array IR.Decl)) := withAtLeastMaxRecDepth 8192 do
   /-
   Note: we need to increase the recursion depth because we currently do to save phase1
   declarations in .olean files. Then, we have to recursively compile all dependencies,
@@ -100,31 +99,33 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
   let decls := markRecDecls decls
   let manager ← getPassManager
   let isCheckEnabled := compiler.check.get (← getOptions)
-  let decls ← profileitM Exception "compilation (LCNF base)" (← getOptions) do
-    let mut decls := decls
-    for pass in manager.basePasses do
-      decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
-        withPhase pass.phase <| pass.run decls
-      withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
-    return decls
-  let decls ← profileitM Exception "compilation (LCNF mono)" (← getOptions) do
-    let mut decls := decls
-    for pass in manager.monoPasses do
-      decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
-        withPhase pass.phase <| pass.run decls
-      withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
-    return decls
-  if (← Lean.isTracingEnabledFor `Compiler.result) then
-    for decl in decls do
-      let decl ← normalizeFVarIds decl
-      Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
-  profileitM Exception "compilation (IR)" (← getOptions) do
-    let irDecls ← IR.toIR decls
-    IR.compile irDecls
+  let decls ← runPassManagerPart "compilation (LCNF base)" manager.basePasses decls isCheckEnabled
+  let decls ← runPassManagerPart "compilation (LCNF mono)" manager.monoPasses decls isCheckEnabled
+  let sccs ← withTraceNode `Compiler.splitSCC (fun _ => return m!"Splitting up SCC") do
+    splitScc decls
+  sccs.mapM fun decls => do
+    let decls ← runPassManagerPart "compilation (LCNF mono)" manager.monoPassesNoLambda decls isCheckEnabled
+    if (← Lean.isTracingEnabledFor `Compiler.result) then
+      for decl in decls do
+        let decl ← normalizeFVarIds decl
+        Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
+    profileitM Exception "compilation (IR)" (← getOptions) do
+      let irDecls ← IR.toIR decls
+      IR.compile irDecls
+where
+  runPassManagerPart (profilerName : String) (passes : Array Pass) (decls : Array Decl)
+      (isCheckEnabled : Bool) : CompilerM (Array Decl) := do
+    profileitM Exception profilerName (← getOptions) do
+      let mut decls := decls
+      for pass in passes do
+        decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
+          withPhase pass.phase <| pass.run decls
+        withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
+      return decls
 
 end PassManager
 
-def compile (declNames : Array Name) : CoreM (Array IR.Decl) :=
+def compile (declNames : Array Name) : CoreM (Array (Array IR.Decl)) :=
   CompilerM.run <| PassManager.run declNames
 
 def showDecl (phase : Phase) (declName : Name) : CoreM Format := do

src/Lean/Compiler/LCNF/PassManager.lean

@@ -87,6 +87,7 @@ pipeline.
 structure PassManager where
   basePasses : Array Pass
   monoPasses : Array Pass
+  monoPassesNoLambda : Array Pass
   deriving Inhabited
 
 instance : ToString Phase where
@@ -114,6 +115,7 @@ private def validatePasses (phase : Phase) (passes : Array Pass) : CoreM Unit :=
 def validate (manager : PassManager) : CoreM Unit := do
   validatePasses .base manager.basePasses
   validatePasses .mono manager.monoPasses
+  validatePasses .mono manager.monoPassesNoLambda
 
 def findOccurrenceBounds (targetName : Name) (passes : Array Pass) : CoreM (Nat × Nat) := do
   let mut lowest := none

src/Lean/Compiler/LCNF/Passes.lean

@@ -115,6 +115,8 @@ def builtinPassManager : PassManager := {
     simp (occurrence := 4) (phase := .mono),
     floatLetIn (phase := .mono) (occurrence := 2),
     lambdaLifting,
+  ]
+  monoPassesNoLambda := #[
     extendJoinPointContext (phase := .mono) (occurrence := 1),
     simp (occurrence := 5) (phase := .mono),
     elimDeadBranches,

src/Lean/Compiler/LCNF/Renaming.lean

@@ -35,7 +35,7 @@ def LetDecl.applyRenaming (decl : LetDecl) (r : Renaming) : CompilerM LetDecl :=
 mutual
 partial def FunDecl.applyRenaming (decl : FunDecl) (r : Renaming) : CompilerM FunDecl := do
   if let some binderName := r.get? decl.fvarId then
-    let decl := { decl with binderName }
+    let decl := decl.updateBinderName binderName
     modifyLCtx fun lctx => lctx.addFunDecl decl
     decl.updateValue (← decl.value.applyRenaming r)
   else

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -213,13 +213,17 @@ def Folder.mkBinary [Literal α] [Literal β] [Literal γ] (folder : α → β
   mkLit <| folder arg₁ arg₂
 
 def Folder.mkBinaryDecisionProcedure [Literal α] [Literal β] {r : α → β → Prop} (folder : (a : α) → (b : β) → Decidable (r a b)) : Folder := fun args => do
-  if (← getPhase) < .mono then
-    return none
   let #[.fvar fvarId₁, .fvar fvarId₂] := args | return none
   let some arg₁ ← getLit fvarId₁ | return none
   let some arg₂ ← getLit fvarId₂ | return none
-  let boolLit := folder arg₁ arg₂ |>.decide
-  mkLit boolLit
+  let result := folder arg₁ arg₂ |>.decide
+  if (← getPhase) < .mono then
+    if result then
+      return some <| .const ``Decidable.isTrue [] #[.erased, .erased]
+    else
+      return some <| .const ``Decidable.isFalse [] #[.erased, .erased]
+  else
+    mkLit result
 
 /--
 Provide a folder for an operation with a left neutral element.

src/Lean/Compiler/LCNF/Simp/JpCases.lean

@@ -268,7 +268,7 @@ where
         else
           altsNew := altsNew.push (alt.updateCode k)
     modify fun s => s.insert decl.fvarId jpAltMap
-    let value := LCNF.attachCodeDecls decls (.cases { cases with alts := altsNew })
+    let value := LCNF.attachCodeDecls decls (.cases <| cases.updateAlts altsNew)
     let decl ← decl.updateValue value
     let code := .jp decl (← visit k)
     return LCNF.attachCodeDecls jpAltDecls code

src/Lean/Compiler/LCNF/Specialize.lean

@@ -115,7 +115,7 @@ def isGround [TraverseFVar α] (e : α) : SpecializeM Bool := do
       match ← findFunDecl? fnFVarId with
       -- This ascription to `Bool` is required to avoid this being inferred as `Prop`,
       -- even with a type specified on the `let` binding.
-      | some { params, .. } => pure ((args.size < params.size) : Bool)
+      | some (.mk (params := params) ..) => pure ((args.size < params.size) : Bool)
       | none => pure false
     | _ => pure false
   let fvarId := decl.fvarId

src/Lean/Compiler/LCNF/SplitSCC.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+import Lean.Util.SCC
+
+namespace Lean.Compiler.LCNF
+
+namespace SplitScc
+
+partial def findSccCalls (scc : Std.HashMap Name Decl) (decl : Decl) : BaseIO (Std.HashSet Name) := do
+  match decl.value with
+  | .code code =>
+    let (_, calls) ← goCode code |>.run {}
+    return calls
+  | .extern .. => return {}
+where
+  goCode (c : Code) : StateRefT (Std.HashSet Name) BaseIO Unit := do
+    match c with
+    | .let decl k =>
+      if let .const name .. := decl.value then
+        if scc.contains name then
+          modify fun s => s.insert name
+      goCode k
+    | .fun decl k | .jp decl k =>
+      goCode decl.value
+      goCode k
+    | .cases cases => cases.alts.forM (·.forCodeM goCode)
+    | .jmp .. | .return .. | .unreach .. => return ()
+
+end SplitScc
+
+public def splitScc (scc : Array Decl) : CompilerM (Array (Array Decl)) := do
+  if scc.size == 1 then
+    return #[scc]
+  let declMap := Std.HashMap.ofArray <| scc.map fun decl => (decl.name, decl)
+  let callers := Std.HashMap.ofArray <| ← scc.mapM fun decl => do
+    let calls ← SplitScc.findSccCalls declMap decl
+    return (decl.name, calls.toList)
+  let newSccs := Lean.SCC.scc (scc.toList.map (·.name)) (callers.getD · [])
+  trace[Compiler.splitSCC] m!"Split SCC into {newSccs}"
+  return newSccs.toArray.map (fun scc => scc.toArray.map declMap.get!)
+
+builtin_initialize
+  registerTraceClass `Compiler.splitSCC (inherited := true)
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/StructProjCases.lean

@@ -72,7 +72,7 @@ partial def visitCode (code : Code) : M Code := do
         modify fun s => { s with projMap := s.projMap.erase base }
         let resultType ← toMonoType (← k.inferType)
         let alts := #[.alt ctorInfo.name params k]
-        return .cases { typeName, resultType, discr := base, alts }
+        return .cases ⟨typeName, resultType, base, alts⟩
     | _ => return code.updateLet! (← decl.updateValue (← visitLetValue decl.value)) (← visitCode k)
   | .fun decl k =>
     let decl ← decl.updateValue (← visitCode decl.value)

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -63,7 +63,7 @@ That is, our goal is to try to promote the pre join points `_alt.<idx>` into a p
 partial def bindCases (jpDecl : FunDecl) (cases : Cases) : CompilerM Code := do
   let (alts, s) ← visitAlts cases.alts |>.run {}
   let resultType ← mkCasesResultType alts
-  let result := .cases { cases with alts, resultType }
+  let result := .cases ⟨cases.typeName, resultType, cases.discr, alts⟩
   let result := s.foldl (init := result) fun result _ altJp => .jp altJp result
   return .jp jpDecl result
 where
@@ -147,7 +147,7 @@ where
       if alts.isEmpty then
         throwError "`Code.bind` failed, empty `cases` found"
       let resultType ← mkCasesResultType alts
-      return .cases { c with alts, resultType }
+      return .cases ⟨c.typeName, resultType, c.discr, alts⟩
     | .return fvarId => return .jmp jpDecl.fvarId #[.fvar fvarId]
     | .jmp .. | .unreach .. => return code
 
@@ -183,7 +183,7 @@ where
           result instead of a join point that takes a closure.
           -/
           eraseParam auxParam
-          let auxFunDecl := { auxParam with params := #[], value := .cases cases : FunDecl }
+          let auxFunDecl := ⟨auxParam.fvarId, auxParam.binderName, #[], auxParam.type, .cases cases⟩
           modifyLCtx fun lctx => lctx.addFunDecl auxFunDecl
           let auxFunDecl ← auxFunDecl.etaExpand
           go seq (i - 1) (.fun auxFunDecl c)
@@ -597,7 +597,7 @@ where
           let (altType, alt) ← visitAlt numParams args[i]!
           resultType := joinTypes altType resultType
           alts := alts.push alt
-        let cases : Cases := { typeName, discr := discrFVarId, resultType, alts }
+        let cases := ⟨typeName, resultType, discrFVarId, alts⟩
         let auxDecl ← mkAuxParam resultType
         pushElement (.cases auxDecl cases)
         let result := .fvar auxDecl.fvarId

src/Lean/Compiler/LCNF/ToMono.lean

@@ -205,7 +205,7 @@ partial def decToMono (c : Cases) (_ : c.typeName == ``Decidable) : ToMonoM Code
       eraseParams ps
       let ctorName := if ctorName == ``Decidable.isTrue then ``Bool.true else ``Bool.false
       return .alt ctorName #[] (← k.toMono)
-  return .cases { c with resultType, alts, typeName := ``Bool }
+  return .cases ⟨``Bool, resultType, c.discr, alts⟩
 
 /-- Eliminate `cases` for `Nat`. -/
 partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code := do
@@ -226,7 +226,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
         return .alt ``Bool.false #[] (.let oneDecl (.let subOneDecl (← k.toMono)))
       else
         return .alt ``Bool.true #[] (← k.toMono)
-  return .let zeroDecl (.let isZeroDecl (.cases { discr := isZeroDecl.fvarId, resultType, alts, typeName := ``Bool }))
+  return .let zeroDecl (.let isZeroDecl (.cases ⟨``Bool, resultType, isZeroDecl.fvarId, alts⟩))
 
 /-- Eliminate `cases` for `Int`. -/
 partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code := do
@@ -251,7 +251,7 @@ partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code :
         let absDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Int.natAbs [] #[.fvar c.discr] }
         modifyLCtx fun lctx => lctx.addLetDecl absDecl
         return .alt ``Bool.false #[] (.let absDecl (← k.toMono))
-  return .let zeroNatDecl (.let zeroIntDecl (.let isNegDecl (.cases { discr := isNegDecl.fvarId, resultType, alts, typeName := ``Bool })))
+  return .let zeroNatDecl (.let zeroIntDecl (.let isNegDecl (.cases ⟨``Bool, resultType, isNegDecl.fvarId, alts⟩)))
 
 /-- Eliminate `cases` for `UInt` types. -/
 partial def casesUIntToMono (c : Cases) (uintName : Name) (_ : c.typeName == uintName) : ToMonoM Code := do
@@ -317,13 +317,13 @@ partial def casesThunkToMono (c : Cases) (_ : c.typeName == ``Thunk) : ToMonoM C
   let letValue := .const ``Thunk.get [] #[.erased, .fvar c.discr]
   let letDecl ← mkLetDecl (← mkFreshBinderName `_x) anyExpr letValue
   let paramType := .const `PUnit []
-  let decl := {
-    fvarId := p.fvarId
-    binderName := p.binderName
-    type := (← mkArrow paramType anyExpr)
-    params := #[← mkAuxParam paramType]
-    value := .let letDecl (.return letDecl.fvarId)
-  }
+  let decl := ⟨
+    p.fvarId,
+    p.binderName,
+    #[← mkAuxParam paramType],
+    (← mkArrow paramType anyExpr),
+    .let letDecl (.return letDecl.fvarId)
+  ⟩
   modifyLCtx fun lctx => lctx.addFunDecl decl
   let k ← k.toMono
   return .fun decl k
@@ -418,7 +418,7 @@ partial def Code.toMono (code : Code) : ToMonoM Code := do
             let ps ← mkFieldParamsForComputedFields ctorInfo.type ctorInfo.numParams numNewFields ps
             let k ← k.toMono
             return .alt implCtorName ps k
-        return .cases { discr := c.discr, resultType, typeName, alts }
+        return .cases ⟨typeName, resultType, c.discr, alts⟩
       else
         let alts ← c.alts.mapM fun alt =>
           match alt with

src/Lean/CoreM.lean

@@ -543,10 +543,12 @@ def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM
 /-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/
 def wrapAsync {α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelToken) :
     CoreM (α → EIO Exception β) := do
-  let (childNGen, parentNGen) := (← getDeclNGen).mkChild
-  setDeclNGen parentNGen
+  let (childNGen, parentNGen) := (← getNGen).mkChild
+  setNGen parentNGen
+  let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild
+  setDeclNGen parentDeclNGen
   let st ← get
-  let st := { st with auxDeclNGen := childNGen }
+  let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
   let ctx ← read
   let ctx := { ctx with cancelTk? }
   let heartbeats := (← IO.getNumHeartbeats) - ctx.initHeartbeats

src/Lean/Data/Json/FromToJson/Basic.lean

@@ -226,7 +226,13 @@ def opt [ToJson α] (k : String) : Option α → List (String × Json)
   | none   => []
   | some o => [⟨k, toJson o⟩]
 
-/-- Parses a JSON-encoded `structure` or `inductive` constructor. Used mostly by `deriving FromJson`. -/
+/-- Returns the string value or single key name, if any. -/
+def getTag? : Json → Option String
+  | .str tag => some tag
+  | .obj kvs => guard (kvs.size == 1) *> kvs.minKey?
+  | _        => none
+
+-- TODO: delete after rebootstrap
 def parseTagged
     (json : Json)
     (tag : String)
@@ -259,5 +265,28 @@ def parseTagged
           | Except.error err => Except.error err
     | Except.error err => Except.error err
 
+/--
+Parses a JSON-encoded `structure` or `inductive` constructor, assuming the tag has already been
+checked and `nFields` is nonzero. Used mostly by `deriving FromJson`.
+-/
+def parseCtorFields
+    (json : Json)
+    (tag : String)
+    (nFields : Nat)
+    (fieldNames? : Option (Array Name)) : Except String (Array Json) := do
+  let payload  ← getObjVal? json tag
+  match fieldNames? with
+  | some fieldNames =>
+    fieldNames.mapM (getObjVal? payload ·.getString!)
+  | none =>
+    if nFields == 1 then
+      Except.ok #[payload]
+    else
+      let fields ← getArr? payload
+      if fields.size == nFields then
+        Except.ok fields
+      else
+        Except.error s!"incorrect number of fields: {fields.size} ≟ {nFields}"
+
 end Json
 end Lean

src/Lean/Data/Options.lean

@@ -14,14 +14,72 @@ public section
 
 namespace Lean
 
-@[expose] def Options := KVMap
+structure Options where
+  private map : NameMap DataValue
+  /--
+  Whether any option with prefix `trace` is set. This does *not* imply that any of such option is
+  set to `true` but it does capture the most common case that no such option has ever been touched.
+  -/
+  hasTrace : Bool
+
+namespace Options
+
+def empty : Options where
+  map := {}
+  hasTrace := false
+
+@[export lean_options_get_empty]
+private def getEmpty (_ : Unit) : Options := .empty
 
-def Options.empty : Options  := {}
 instance : Inhabited Options where
-  default := {}
-instance : ToString Options := inferInstanceAs (ToString KVMap)
-instance [Monad m] : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
-instance : BEq Options := inferInstanceAs (BEq KVMap)
+  default := .empty
+instance : ToString Options where
+  toString o := private toString o.map.toList
+instance [Monad m] : ForIn m Options (Name × DataValue) where
+  forIn o init f := private forIn o.map init f
+instance : BEq Options where
+  beq o1 o2 := private o1.map.beq o2.map
+instance : EmptyCollection Options where
+  emptyCollection := .empty
+
+@[inline] def find? (o : Options) (k : Name) : Option DataValue :=
+  o.map.find? k
+
+@[deprecated find? (since := "2026-01-15")]
+def find := find?
+
+@[inline] def get? {α : Type} [KVMap.Value α] (o : Options) (k : Name) : Option α :=
+  o.map.find? k |>.bind KVMap.Value.ofDataValue?
+
+@[inline] def get {α : Type} [KVMap.Value α] (o : Options) (k : Name) (defVal : α) : α :=
+  o.get? k |>.getD defVal
+
+@[inline] def getBool (o : Options) (k : Name) (defVal : Bool := false) : Bool :=
+  o.get k defVal
+
+@[inline] def contains (o : Options) (k : Name) : Bool :=
+  o.map.contains k
+
+@[inline] def insert (o : Options) (k : Name) (v : DataValue) : Options where
+  map := o.map.insert k v
+  hasTrace := o.hasTrace || (`trace).isPrefixOf k
+
+def set {α : Type} [KVMap.Value α] (o : Options) (k : Name) (v : α) : Options :=
+  o.insert k (KVMap.Value.toDataValue v)
+
+@[inline] def setBool (o : Options) (k : Name) (v : Bool) : Options :=
+  o.set k v
+
+def erase (o : Options) (k : Name) : Options where
+  map := o.map.erase k
+  -- `erase` is expected to be used even more rarely than `set` so O(n) is fine
+  hasTrace := o.map.keys.any (`trace).isPrefixOf
+
+def mergeBy (f : Name → DataValue → DataValue → DataValue) (o1 o2 : Options) : Options where
+  map := o1.map.mergeWith f o2.map
+  hasTrace := o1.hasTrace || o2.hasTrace
+
+end Options
 
 structure OptionDecl where
   name     : Name
@@ -90,11 +148,11 @@ variable [Monad m] [MonadOptions m]
 
 def getBoolOption (k : Name) (defValue := false) : m Bool := do
   let opts ← getOptions
-  return opts.getBool k defValue
+  return opts.get k defValue
 
 def getNatOption (k : Name) (defValue := 0) : m Nat := do
   let opts ← getOptions
-  return opts.getNat k defValue
+  return opts.get k defValue
 
 class MonadWithOptions (m : Type → Type) where
   withOptions (f : Options → Options) (x : m α) : m α
@@ -108,10 +166,10 @@ instance [MonadFunctor m n] [MonadWithOptions m] : MonadWithOptions n where
    the term being delaborated should be treated as a pattern. -/
 
 def withInPattern [MonadWithOptions m] (x : m α) : m α :=
-  withOptions (fun o => o.setBool `_inPattern true) x
+  withOptions (fun o => o.set `_inPattern true) x
 
 def Options.getInPattern (o : Options) : Bool :=
-  o.getBool `_inPattern
+  o.get `_inPattern false
 
 /-- A strongly-typed reference to an option. -/
 protected structure Option (α : Type) where
@@ -131,12 +189,20 @@ protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Op
 protected def get [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α :=
   opts.get opt.name opt.defValue
 
+@[export lean_options_get_bool]
+private def getBool (opts : Options) (name : Name) (defValue : Bool) : Bool :=
+  opts.get name defValue
+
 protected def getM [Monad m] [MonadOptions m] [KVMap.Value α] (opt : Lean.Option α) : m α :=
   return opt.get (← getOptions)
 
 protected def set [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options :=
   opts.set opt.name val
 
+@[export lean_options_update_bool]
+private def updateBool (opts : Options) (name : Name) (val : Bool) : Options :=
+  opts.set name val
+
 /-- Similar to `set`, but update `opts` only if it doesn't already contains an setting for `opt.name` -/
 protected def setIfNotSet [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options :=
   if opts.contains opt.name then opts else opt.set opts val

src/Lean/DocString/Parser.lean

@@ -1220,7 +1220,7 @@ Disables the option `doc.verso` while running a parser.
 public def withoutVersoSyntax (p : Parser) : Parser where
   fn :=
     adaptUncacheableContextFn
-      (fun c => { c with options := c.options.setBool `doc.verso false })
+      (fun c => { c with options := c.options.set `doc.verso false })
       p.fn
   info := p.info
 

src/Lean/Elab/Attributes.lean

@@ -45,26 +45,29 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
-  /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
-  let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
-  let attr := attrInstance[1]
-  let attr ← liftMacroM <| expandMacros attr
-  let attrName ← if attr.getKind == ``Parser.Attr.simple then
-    pure attr[0].getId.eraseMacroScopes
-  else match attr.getKind with
-    | .str _ s => pure <| Name.mkSimple s
-    | _ => throwErrorAt attr  "Unknown attribute"
-  let .ok _impl := getAttributeImpl (← getEnv) attrName
-    | throwError "Unknown attribute `[{attrName}]`"
-  if let .ok impl := getAttributeImpl (← getEnv) attrName then
-    if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then  -- skip `builtin_initialize` attributes
-      recordExtraModUseFromDecl (isMeta := true) impl.ref
-  /- The `AttrM` does not have sufficient information for expanding macros in `args`.
-     So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
-  return { kind := attrKind, name := attrName, stx := attr }
+def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] [MonadFinally m] (attrInstance : Syntax) : m Attribute := do
+  -- Resolving the attribute itself can be done in the private scope; running the attribute handler
+  -- will later be done in a scope determined by `applyAttributesCore`.
+  withoutExporting do
+    /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
+    let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
+    let attr := attrInstance[1]
+    let attr ← liftMacroM <| expandMacros attr
+    let attrName ← if attr.getKind == ``Parser.Attr.simple then
+      pure attr[0].getId.eraseMacroScopes
+    else match attr.getKind with
+      | .str _ s => pure <| Name.mkSimple s
+      | _ => throwErrorAt attr  "Unknown attribute"
+    let .ok _impl := getAttributeImpl (← getEnv) attrName
+      | throwError "Unknown attribute `[{attrName}]`"
+    if let .ok impl := getAttributeImpl (← getEnv) attrName then
+      if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then  -- skip `builtin_initialize` attributes
+        recordExtraModUseFromDecl (isMeta := true) impl.ref
+    /- The `AttrM` does not have sufficient information for expanding macros in `args`.
+      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
+    return { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] [MonadFinally m] (attrInstances : Array Syntax) : m (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
     try
@@ -74,7 +77,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] [MonadFinally m] (stx : Syntax) : m (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab

src/Lean/Elab/BuiltinCommand.lean

@@ -456,7 +456,7 @@ where
       withRef tk <| Meta.check e
       let e ← Term.levelMVarToParam (← instantiateMVars e)
       -- TODO: add options or notation for setting the following parameters
-      withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
+      withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.set `smartUnfolding false }) do
         let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes)
         logInfoAt tk e
 

src/Lean/Elab/Command.lean

@@ -274,10 +274,12 @@ def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option
     CommandElabM (α → EIO Exception β) := do
   let ctx ← read
   let ctx := { ctx with cancelTk? }
-  let (childNGen, parentNGen) := (← getDeclNGen).mkChild
-  setDeclNGen parentNGen
+  let (childNGen, parentNGen) := (← get).ngen.mkChild
+  modify fun s => { s with ngen := parentNGen }
+  let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild
+  setDeclNGen parentDeclNGen
   let st ← get
-  let st := { st with auxDeclNGen := childNGen }
+  let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
   return (act · |>.run ctx |>.run' st)
 
 open Language in

src/Lean/Elab/Deriving/Basic.lean

@@ -232,7 +232,7 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) (setExpose
   withScope (fun sc => { sc with
     attrs := if setExpose then Unhygienic.run `(Parser.Term.attrInstance| expose) :: sc.attrs else sc.attrs
     -- Deactivate some linting options that only make writing deriving handlers more painful.
-    opts := sc.opts.setBool `warn.exposeOnPrivate false
+    opts := sc.opts.set `warn.exposeOnPrivate false
     -- When any of the types are private, the deriving handler will need access to the private scope
     -- and should create private instances.
     isPublic := !typeNames.any isPrivateName }) do

src/Lean/Elab/Deriving/FromToJson.lean

@@ -111,14 +111,18 @@ def mkFromJsonBodyForStruct (indName : Name) : TermElabM Term := do
 
 def mkFromJsonBodyForInduct (ctx : Context) (indName : Name) : TermElabM Term := do
   let indVal ← getConstInfoInduct indName
-  let alts ← mkAlts indVal
-  let auxTerm ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched"))
-  `($auxTerm)
+  let (ctors, alts) := (← mkAlts indVal).unzip
+  `(match Json.getTag? json with
+    | some tag => match tag with
+      $[| $(ctors.map Syntax.mkStrLit) => $(alts)]*
+      | _ => Except.error "no inductive constructor matched"
+    | none => Except.error "no inductive tag found")
 where
-  mkAlts (indVal : InductiveVal) : TermElabM (Array Term) := do
+  mkAlts (indVal : InductiveVal) : TermElabM (Array (String × Term)) := do
   let mut alts := #[]
   for ctorName in indVal.ctors do
     let ctorInfo ← getConstInfoCtor ctorName
+    let ctorStr := ctorName.eraseMacroScopes.getString!
     let alt ← do forallTelescopeReducing ctorInfo.type fun xs _ => do
         let mut binders   := #[]
         let mut userNames := #[]
@@ -142,11 +146,14 @@ where
         else
           ``(none)
         let stx ←
-          `((Json.parseTagged json $(quote ctorName.eraseMacroScopes.getString!) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind
-            (fun jsons => do
-              $[let $identNames:ident ← $fromJsons:doExpr]*
-              return $(mkIdent ctorName):ident $identNames*))
-        pure (stx, ctorInfo.numFields)
+          if ctorInfo.numFields == 0 then
+            `(return $(mkIdent ctorName):ident $identNames*)
+          else
+            `((Json.parseCtorFields json $(quote ctorStr) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind
+              (fun jsons => do
+                $[let $identNames:ident ← $fromJsons:doExpr]*
+                return $(mkIdent ctorName):ident $identNames*))
+        pure ((ctorStr, stx), ctorInfo.numFields)
       alts := alts.push alt
   -- the smaller cases, especially the ones without fields are likely faster
   let alts' := alts.qsort (fun (_, x) (_, y) => x < y)

src/Lean/Elab/DocString/Builtin.lean

@@ -1267,7 +1267,7 @@ def «set_option» (option : Ident) (value : DataValue) : DocM (Block ElabInline
   pushInfoLeaf <| .ofOptionInfo { stx := option, optionName, declName := decl.declName }
   validateOptionValue optionName decl value
   let o ← getOptions
-  modify fun s => { s with options := o.insert optionName value }
+  modify fun s => { s with options := o.set optionName value }
   return .empty
 
 /--

src/Lean/Elab/Extra.lean

@@ -573,11 +573,16 @@ def elabDefaultOrNonempty : TermElab :=  fun stx expectedType? => do
   | some expectedType =>
     try
       mkDefault expectedType
-    catch ex => try
+    catch _ => try
       mkOfNonempty expectedType
     catch _ =>
       if stx[1].isNone then
-        throw ex
+        throwError "\
+          failed to synthesize '{.ofConstName ``Inhabited}' or '{.ofConstName ``Nonempty}' instance for\
+          {indentExpr expectedType}\n\
+          \n\
+          If this type is defined using the 'structure' or 'inductive' command, \
+          you can try adding a 'deriving Nonempty' clause to it."
       else
         -- It is in the context of an `unsafe` constant. We can use sorry instead.
         -- Another option is to make a recursive application since it is unsafe.

src/Lean/Elab/GuardMsgs.lean

@@ -11,10 +11,13 @@ public import Lean.Server.CodeActions.Attr
 
 public section
 
-/-! `#guard_msgs` command for testing commands
+/-! `#guard_msgs` and `#guard_panic` commands for testing commands
 
-This module defines a command to test that another command produces the expected messages.
-See the docstring on the `#guard_msgs` command.
+This module defines commands to test that other commands produce expected messages:
+- `#guard_msgs`: tests that a command produces exactly the expected messages
+- `#guard_panic`: tests that a command produces a panic message (without checking the exact text)
+
+See the docstrings on the individual commands.
 -/
 
 open Lean Parser.Tactic Elab Command
@@ -88,6 +91,8 @@ structure GuardMsgsSpec where
   ordering : MessageOrdering := .exact
   /-- Whether to report position information. -/
   reportPositions : Bool := false
+  /-- Whether to check for substring containment instead of exact match. -/
+  substring : Bool := false
 
 def parseGuardMsgsFilterAction (action? : Option (TSyntax ``guardMsgsFilterAction)) :
     CommandElabM FilterSpec := do
@@ -118,7 +123,7 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) : CommandElabM
     | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => pure elts
     | _ => throwUnsupportedSyntax
   let defaultFilterFn := cfg.filterFn
-  let mut { whitespace, ordering, reportPositions .. } := cfg
+  let mut { whitespace, ordering, reportPositions, substring .. } := cfg
   let mut p? : Option (Message → FilterSpec) := none
   let pushP (action : FilterSpec) (msgP : Message → Bool) (p? : Option (Message → FilterSpec))
       (msg : Message) : FilterSpec :=
@@ -136,9 +141,11 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) : CommandElabM
     | `(guardMsgsSpecElt| ordering := sorted)       => ordering := .sorted
     | `(guardMsgsSpecElt| positions := true)        => reportPositions := true
     | `(guardMsgsSpecElt| positions := false)       => reportPositions := false
+    | `(guardMsgsSpecElt| substring := true)        => substring := true
+    | `(guardMsgsSpecElt| substring := false)       => substring := false
     | _ => throwUnsupportedSyntax
   let filterFn := p?.getD defaultFilterFn
-  return { filterFn, whitespace, ordering, reportPositions }
+  return { filterFn, whitespace, ordering, reportPositions, substring }
 
 /-- An info tree node corresponding to a failed `#guard_msgs` invocation,
 used for code action support. -/
@@ -176,22 +183,31 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
   | .exact => msgs
   | .sorted => msgs |>.toArray.qsort (· < ·) |>.toList
 
+/--
+Runs a command and collects all messages (sync and async) it produces.
+Clears the snapshot tasks after collection.
+Returns the collected messages.
+-/
+def runAndCollectMessages (cmd : Syntax) : CommandElabM MessageLog := do
+  -- do not forward snapshot as we don't want messages assigned to it to leak outside
+  withReader ({ · with snap? := none }) do
+    -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
+    elabCommandTopLevel cmd
+  -- collect sync and async messages
+  let msgs := (← get).messages ++
+    (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) .empty) .empty
+  -- clear async messages as we don't want them to leak outside
+  modify ({ · with snapshotTasks := #[] })
+  return msgs
+
 @[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
   | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
     let expected : String := (← dc?.mapM (getDocStringText ·)).getD ""
         |>.trimAscii |>.copy |> removeTrailingWhitespaceMarker
-    let { whitespace, ordering, filterFn, reportPositions } ← parseGuardMsgsSpec spec?
-    -- do not forward snapshot as we don't want messages assigned to it to leak outside
-    withReader ({ · with snap? := none }) do
-      -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
-      elabCommandTopLevel cmd
-    -- collect sync and async messages
-    let msgs := (← get).messages ++
-      (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) {}) {}
-    -- clear async messages as we don't want them to leak outside
-    modify ({ · with snapshotTasks := #[] })
-    let mut toCheck : MessageLog := .empty
-    let mut toPassthrough : MessageLog := .empty
+    let { whitespace, ordering, filterFn, reportPositions, substring } ← parseGuardMsgsSpec spec?
+    let msgs ← runAndCollectMessages cmd
+    let mut toCheck : MessageLog := MessageLog.empty
+    let mut toPassthrough : MessageLog := MessageLog.empty
     for msg in msgs.toList do
       if msg.isSilent then
         continue
@@ -207,7 +223,13 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
     let strings ← toCheck.toList.mapM (messageToString · reportPos?)
     let strings := ordering.apply strings
     let res := "---\n".intercalate strings |>.trimAscii |>.copy
-    if whitespace.apply expected == whitespace.apply res then
+    let passed := if substring then
+      -- Substring mode: check that expected appears within res (after whitespace normalization)
+      (whitespace.apply res).contains (whitespace.apply expected)
+    else
+      -- Exact mode: check equality (after whitespace normalization)
+      whitespace.apply expected == whitespace.apply res
+    if passed then
       -- Passed. Only put toPassthrough messages back on the message log
       modify fun st => { st with messages := toPassthrough }
     else
@@ -257,4 +279,24 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
       }
   }]
 
+@[builtin_command_elab Lean.guardPanicCmd] def elabGuardPanic : CommandElab
+  | `(command| #guard_panic in $cmd) => do
+    let msgs ← runAndCollectMessages cmd
+    -- Check if any message contains "PANIC"
+    let mut foundPanic := false
+    for msg in msgs.toList do
+      if msg.isSilent then continue
+      let msgStr ← msg.data.toString
+      if msgStr.contains "PANIC" then
+        foundPanic := true
+        break
+    if foundPanic then
+      -- Success - clear the messages so they don't appear
+      modify fun st => { st with messages := MessageLog.empty }
+    else
+      -- Failed - put the messages back and add our error
+      modify fun st => { st with messages := msgs }
+      logError "Expected a PANIC but none was found"
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.GuardMsgs

src/Lean/Elab/Inductive.lean

@@ -29,72 +29,76 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
   let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
-  if modifiers.isMeta then
-    modifyEnv (markMeta · declName)
-  addDeclarationRangesForBuiltin declName modifiers.stx decl
-  /-
-    Relates to issue
-    https://github.com/leanprover/lean4/issues/10503
-  -/
-  if declName.hasMacroScopes && isCoinductive then
-    throwError "Coinductive predicates are not allowed inside of macro scopes"
-  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-    /-
-    ```
-    def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    ```
-    -/
-    let modifiersStx := ctor[2]
-    let mut ctorModifiers ← elabModifiers ⟨modifiersStx⟩
-    if let some leadingDocComment := ctor[0].getOptional? then
-      if ctorModifiers.docString?.isSome then
-        logErrorAt leadingDocComment "Duplicate doc string"
-      ctorModifiers := { ctorModifiers with
-        docString? := some (⟨leadingDocComment⟩, doc.verso.get (← getOptions)) }
-    if ctorModifiers.isPrivate && modifiers.isPrivate then
-      let hint ← do
-        let .original .. := modifiersStx.getHeadInfo | pure .nil
-        let some range := modifiersStx[2].getRangeWithTrailing? | pure .nil
-        -- Drop the doc comment from both the `declModifiers` and outer `ctor`, as well as
-        -- everything after the constructor name (yielding invalid syntax with the desired range)
-        let previewSpan? := ctor.modifyArgs (·[2...4].toArray.modify 0 (·.modifyArgs (·[1...*])))
-        MessageData.hint "Remove `private` modifier from constructor" #[{
-          suggestion := ""
-          span? := Syntax.ofRange range
-          previewSpan?
-          toCodeActionTitle? := some fun _ => "Delete `private` modifier"
-        }]
-      throwError m!"Constructor cannot be marked `private` because it is already in a `private` inductive datatype" ++ hint
-    if ctorModifiers.isProtected && modifiers.isPrivate then
-      throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
-    checkValidCtorModifier ctorModifiers
-    let ctorName := ctor.getIdAt 3
-    let ctorName := declName ++ ctorName
-    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
-    let (binders, type?) := expandOptDeclSig ctor[4]
-    addDeclarationRangesFromSyntax ctorName ctor ctor[3]
+  -- In the case of mutual inductives, this is the earliests point where we can establish the
+  -- correct scope for each individual inductive declaration (used e.g. to infer ctor visibility
+  -- below), so let's do that now.
+  withExporting (isExporting := !isPrivateName declName) do
     if modifiers.isMeta then
-      modifyEnv (markMeta · ctorName)
-    return { ref := ctor, declId := ctor[3], modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
-  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
-    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← getOptDerivingClasses decl[6]
-  if decl[3][0].isToken ":=" then
-    -- https://github.com/leanprover/lean4/issues/5236
-    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
-      "`inductive ... :=` has been deprecated in favor of `inductive ... where`"
-  return {
-    ref             := decl
-    shortDeclName   := name
-    derivingClasses := classes
-    allowIndices    := true
-    allowSortPolymorphism := true
-    declId, modifiers, isClass, declName, levelNames
-    binders, type?, ctors
-    computedFields
-    docString?
-    isCoinductive := isCoinductive
-  }
+      modifyEnv (markMeta · declName)
+    addDeclarationRangesForBuiltin declName modifiers.stx decl
+    /-
+      Relates to issue
+      https://github.com/leanprover/lean4/issues/10503
+    -/
+    if declName.hasMacroScopes && isCoinductive then
+      throwError "Coinductive predicates are not allowed inside of macro scopes"
+    let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
+      /-
+      ```
+      def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
+      ```
+      -/
+      let modifiersStx := ctor[2]
+      let mut ctorModifiers ← elabModifiers ⟨modifiersStx⟩
+      if let some leadingDocComment := ctor[0].getOptional? then
+        if ctorModifiers.docString?.isSome then
+          logErrorAt leadingDocComment "Duplicate doc string"
+        ctorModifiers := { ctorModifiers with
+          docString? := some (⟨leadingDocComment⟩, doc.verso.get (← getOptions)) }
+      if ctorModifiers.isPrivate && modifiers.isPrivate then
+        let hint ← do
+          let .original .. := modifiersStx.getHeadInfo | pure .nil
+          let some range := modifiersStx[2].getRangeWithTrailing? | pure .nil
+          -- Drop the doc comment from both the `declModifiers` and outer `ctor`, as well as
+          -- everything after the constructor name (yielding invalid syntax with the desired range)
+          let previewSpan? := ctor.modifyArgs (·[2...4].toArray.modify 0 (·.modifyArgs (·[1...*])))
+          MessageData.hint "Remove `private` modifier from constructor" #[{
+            suggestion := ""
+            span? := Syntax.ofRange range
+            previewSpan?
+            toCodeActionTitle? := some fun _ => "Delete `private` modifier"
+          }]
+        throwError m!"Constructor cannot be marked `private` because it is already in a `private` inductive datatype" ++ hint
+      if ctorModifiers.isProtected && modifiers.isPrivate then
+        throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
+      checkValidCtorModifier ctorModifiers
+      let ctorName := ctor.getIdAt 3
+      let ctorName := declName ++ ctorName
+      let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
+      let (binders, type?) := expandOptDeclSig ctor[4]
+      addDeclarationRangesFromSyntax ctorName ctor ctor[3]
+      if modifiers.isMeta then
+        modifyEnv (markMeta · ctorName)
+      return { ref := ctor, declId := ctor[3], modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+    let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
+      return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
+    let classes ← getOptDerivingClasses decl[6]
+    if decl[3][0].isToken ":=" then
+      -- https://github.com/leanprover/lean4/issues/5236
+      withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
+        "`inductive ... :=` has been deprecated in favor of `inductive ... where`"
+    return {
+      ref             := decl
+      shortDeclName   := name
+      derivingClasses := classes
+      allowIndices    := true
+      allowSortPolymorphism := true
+      declId, modifiers, isClass, declName, levelNames
+      binders, type?, ctors
+      computedFields
+      docString?
+      isCoinductive := isCoinductive
+    }
 
 private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do
   let indFVarType ← inferType indFVar

src/Lean/Elab/Match.lean

@@ -886,7 +886,7 @@ private def generalize (discrs : Array Discr) (matchType : Expr) (altViews : Arr
       let matchType' ← forallBoundedTelescope matchType discrs.size fun ds type => do
         let type ← mkForallFVars ys type
         let (discrs', ds') := Array.unzip <| Array.zip discrExprs ds |>.filter fun (di, _) => di.isFVar
-        let type ← type.replaceFVarsM discrs' ds'
+        let type := type.replaceFVars discrs' ds'
         mkForallFVars ds type
       if (← isTypeCorrect matchType') then
         let discrs := discrs ++  ys.map fun y => { expr := y : Discr }
@@ -1119,11 +1119,11 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
       withRef altLHS.ref do
         for d in altLHS.fvarDecls do
           if d.hasExprMVar then
-            -- This code path is a vestige prior to fixing #8099, but it is still appears to be
-            -- important for testcase 1300.lean.
             tryPostpone
             withExistingLocalDecls altLHS.fvarDecls do
               runPendingTacticsAt d.type
+              if (← instantiateMVars d.type).hasExprMVar then
+                throwMVarError m!"Invalid match expression: The type of pattern variable '{d.toExpr}' contains metavariables:{indentExpr d.type}"
         for p in altLHS.patterns do
           if (← Match.instantiatePatternMVars p).hasExprMVar then
             tryPostpone

src/Lean/Elab/MutualInductive.lean

@@ -1210,8 +1210,8 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM
     computedFields := computedFields.push (declName, computedFieldNames)
   withScope (fun scope => { scope with
       opts := scope.opts
-        |>.setBool `bootstrap.genMatcherCode false
-        |>.setBool `elaboratingComputedFields true}) <|
+        |>.set `bootstrap.genMatcherCode false
+        |>.set `elaboratingComputedFields true}) <|
     elabCommand <| ← `(mutual $computedFieldDefs* end)
 
   liftTermElabM do Term.withDeclName indViews[0]!.declName do