fix: broadcast test

This PR adds `suggest_for` annotations such that `Int*.toNatClamp` is
suggested for `Int*.toNat`.

.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/Modulize.lean

@@ -29,7 +29,7 @@ def main (args : List String) : IO Unit := do
     if !msgs.toList.isEmpty then -- skip this file if there are parse errors
       msgs.forM fun msg => msg.toString >>= IO.println
       throw <| .userError "parse errors in file"
-    let `(header| $[module%$moduleTk?]? $imps:import*) := header
+    let `(header| $[module%$moduleTk?]? $[prelude%$preludeTk?]? $imps:import*) := header
       | throw <| .userError s!"unexpected header syntax of {path}"
     if moduleTk?.isSome then
       continue
@@ -38,11 +38,11 @@ def main (args : List String) : IO Unit := do
     let startPos := header.raw.getPos? |>.getD parserState.pos
 
     let dummyEnv ← mkEmptyEnvironment
-    let (initCmd, parserState', _) :=
+    let (initCmd, parserState', msgs') :=
       Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
 
-    -- insert section if any trailing command
-    if !initCmd.isOfKind ``Parser.Command.eoi then
+    -- insert section if any trailing command (or error, which could be from an unknown command)
+    if !initCmd.isOfKind ``Parser.Command.eoi || msgs'.hasErrors then
       let insertPos? :=
           -- put below initial module docstring if any
           guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>
@@ -57,19 +57,21 @@ def main (args : List String) : IO Unit := do
         sec := "\n\n" ++ sec
       if insertPos?.isNone then
         sec := sec ++ "\n\n"
-      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
+      let insertPos := text.pos! insertPos
+      text := text.extract text.startPos insertPos ++ sec ++ text.extract insertPos text.endPos
 
     -- prepend each import with `public `
     for imp in imps.reverse do
       let insertPos := imp.raw.getPos?.get!
       let prfx := if doMeta then "public meta " else "public "
-      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
+      let insertPos := text.pos! insertPos
+      text := text.extract text.startPos insertPos ++ prfx ++ text.extract insertPos text.endPos
 
     -- insert `module` header
-    let mut initText := text.extract 0 startPos
-    if !initText.trim.isEmpty then
+    let mut initText := text.extract text.startPos (text.pos! startPos)
+    if !initText.trimAscii.isEmpty then
       -- If there is a header comment, preserve it and put `module` in the line after
-      initText := initText.trimRight ++ "\n"
-    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
+      initText := initText.trimAsciiEnd.toString ++ "\n"
+    text := initText ++ "module\n\n" ++ text.extract (text.pos! startPos) text.endPos
 
     IO.FS.writeFile path text

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/Char.lean

@@ -9,3 +9,4 @@ prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
 public import Init.Data.Char.Order
+public import Init.Data.Char.Ordinal

src/Init/Data/Char/Ordinal.lean

@@ -0,0 +1,242 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Fin.OverflowAware
+public import Init.Data.UInt.Basic
+public import Init.Data.Function
+import Init.Data.Char.Lemmas
+import Init.Data.Char.Order
+import Init.Grind
+
+/-!
+# Bijection between `Char` and `Fin Char.numCodePoints`
+
+In this file, we construct a bijection between `Char` and `Fin Char.numCodePoints` and show that
+it is compatible with various operations. Since `Fin` is simpler than `Char` due to being based
+on natural numbers instead of `UInt32` and not having a hole in the middle (surrogate code points),
+this is sometimes useful to simplify reasoning about `Char`.
+
+We use these declarations in the construction of `Char` ranges, see the module
+`Init.Data.Range.Polymorphic.Char`.
+-/
+
+set_option doc.verso true
+
+public section
+
+namespace Char
+
+/-- The number of surrogate code points. -/
+abbrev numSurrogates : Nat :=
+  -- 0xe000 - 0xd800
+  2048
+
+/-- The size of the {name}`Char` type. -/
+abbrev numCodePoints : Nat :=
+  -- 0x110000 - numSurrogates
+  1112064
+
+/--
+Packs {name}`Char` bijectively into {lean}`Fin Char.numCodePoints` by shifting code points which are
+greater than the surrogate code points by the number of surrogate code points.
+
+The inverse of this function is called {name (scope := "Init.Data.Char.Ordinal")}`Char.ofOrdinal`.
+-/
+def ordinal (c : Char) : Fin Char.numCodePoints :=
+  if h : c.val < 0xd800 then
+    ⟨c.val.toNat, by grind [UInt32.lt_iff_toNat_lt]⟩
+  else
+    ⟨c.val.toNat - Char.numSurrogates, by grind [UInt32.lt_iff_toNat_lt]⟩
+
+/--
+Unpacks {lean}`Fin Char.numCodePoints` bijectively to {name}`Char` by shifting code points which are
+greater than the surrogate code points by the number of surrogate code points.
+
+The inverse of this function is called {name}`Char.ordinal`.
+-/
+def ofOrdinal (f : Fin Char.numCodePoints) : Char :=
+  if h : (f : Nat) < 0xd800 then
+    ⟨UInt32.ofNatLT f (by grind), by grind [UInt32.toNat_ofNatLT]⟩
+  else
+    ⟨UInt32.ofNatLT (f + Char.numSurrogates) (by grind), by grind [UInt32.toNat_ofNatLT]⟩
+
+/--
+Computes the next {name}`Char`, skipping over surrogate code points (which are not valid
+{name}`Char`s) as necessary.
+
+This function is specified by its interaction with {name}`Char.ordinal`, see
+{name (scope := "Init.Data.Char.Ordinal")}`Char.succ?_eq`.
+-/
+def succ? (c : Char) : Option Char :=
+  if h₀ : c.val < 0xd7ff then
+    some ⟨c.val + 1, by grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_add]⟩
+  else if h₁ : c.val = 0xd7ff then
+    some ⟨0xe000, by decide⟩
+  else if h₂ : c.val < 0x10ffff then
+    some ⟨c.val + 1, by
+      simp only [UInt32.lt_iff_toNat_lt, UInt32.reduceToNat, Nat.not_lt, ← UInt32.toNat_inj,
+        UInt32.isValidChar, Nat.isValidChar, UInt32.toNat_add, Nat.reducePow] at *
+      grind⟩
+  else none
+
+/--
+Computes the {name}`m`-th next {name}`Char`, skipping over surrogate code points (which are not
+valid {name}`Char`s) as necessary.
+
+This function is specified by its interaction with {name}`Char.ordinal`, see
+{name (scope := "Init.Data.Char.Ordinal")}`Char.succMany?_eq`.
+-/
+def succMany? (m : Nat) (c : Char) : Option Char :=
+  c.ordinal.addNat? m |>.map Char.ofOrdinal
+
+@[grind =]
+theorem coe_ordinal {c : Char} :
+    (c.ordinal : Nat) =
+      if c.val < 0xd800 then
+        c.val.toNat
+      else
+        c.val.toNat - Char.numSurrogates := by
+  grind [Char.ordinal]
+
+@[simp]
+theorem ordinal_zero : '\x00'.ordinal = 0 := by
+  ext
+  simp [coe_ordinal]
+
+@[grind =]
+theorem val_ofOrdinal {f : Fin Char.numCodePoints} :
+    (Char.ofOrdinal f).val =
+      if h : (f : Nat) < 0xd800 then
+        UInt32.ofNatLT f (by grind)
+      else
+        UInt32.ofNatLT (f + Char.numSurrogates) (by grind) := by
+  grind [Char.ofOrdinal]
+
+@[simp]
+theorem ofOrdinal_ordinal {c : Char} : Char.ofOrdinal c.ordinal = c := by
+  ext
+  simp only [val_ofOrdinal, coe_ordinal, UInt32.ofNatLT_add]
+  split
+  · grind [UInt32.lt_iff_toNat_lt, UInt32.ofNatLT_toNat]
+  · rw [dif_neg]
+    · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+      grind [UInt32.toNat_lt, UInt32.lt_iff_toNat_lt]
+    · grind [UInt32.lt_iff_toNat_lt]
+
+@[simp]
+theorem ordinal_ofOrdinal {f : Fin Char.numCodePoints} : (Char.ofOrdinal f).ordinal = f := by
+  ext
+  simp [coe_ordinal, val_ofOrdinal]
+  split
+  · rw [if_pos, UInt32.toNat_ofNatLT]
+    simpa [UInt32.lt_iff_toNat_lt]
+  · rw [if_neg, UInt32.toNat_add, UInt32.toNat_ofNatLT, UInt32.toNat_ofNatLT, Nat.mod_eq_of_lt,
+      Nat.add_sub_cancel]
+    · grind
+    · simp only [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow,
+        UInt32.reduceToNat, Nat.not_lt]
+      grind
+
+@[simp]
+theorem ordinal_comp_ofOrdinal : Char.ordinal ∘ Char.ofOrdinal = id := by
+  ext; simp
+
+@[simp]
+theorem ofOrdinal_comp_ordinal : Char.ofOrdinal ∘ Char.ordinal = id := by
+  ext; simp
+
+@[simp]
+theorem ordinal_inj {c d : Char} : c.ordinal = d.ordinal ↔ c = d :=
+  ⟨fun h => by simpa using congrArg Char.ofOrdinal h, (· ▸ rfl)⟩
+
+theorem ordinal_injective : Function.Injective Char.ordinal :=
+  fun _ _ => ordinal_inj.1
+
+@[simp]
+theorem ofOrdinal_inj {f g : Fin Char.numCodePoints} :
+    Char.ofOrdinal f = Char.ofOrdinal g ↔ f = g :=
+  ⟨fun h => by simpa using congrArg Char.ordinal h, (· ▸ rfl)⟩
+
+theorem ofOrdinal_injective : Function.Injective Char.ofOrdinal :=
+   fun _ _ => ofOrdinal_inj.1
+
+theorem ordinal_le_of_le {c d : Char} (h : c ≤ d) : c.ordinal ≤ d.ordinal := by
+  simp only [le_def, UInt32.le_iff_toNat_le] at h
+  simp only [Fin.le_def, coe_ordinal, UInt32.lt_iff_toNat_lt, UInt32.reduceToNat]
+  grind
+
+theorem ofOrdinal_le_of_le {f g : Fin Char.numCodePoints} (h : f ≤ g) :
+    Char.ofOrdinal f ≤ Char.ofOrdinal g := by
+  simp only [Fin.le_def] at h
+  simp only [le_def, val_ofOrdinal, UInt32.ofNatLT_add, UInt32.le_iff_toNat_le]
+  split
+  · simp only [UInt32.toNat_ofNatLT]
+    split
+    · simpa
+    · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+      grind
+  · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+    rw [dif_neg (by grind)]
+    simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+    grind
+
+theorem le_iff_ordinal_le {c d : Char} : c ≤ d ↔ c.ordinal ≤ d.ordinal :=
+  ⟨ordinal_le_of_le, fun h => by simpa using ofOrdinal_le_of_le h⟩
+
+theorem le_iff_ofOrdinal_le {f g : Fin Char.numCodePoints} :
+    f ≤ g ↔ Char.ofOrdinal f ≤ Char.ofOrdinal g :=
+  ⟨ofOrdinal_le_of_le, fun h => by simpa using ordinal_le_of_le h⟩
+
+theorem lt_iff_ordinal_lt {c d : Char} : c < d ↔ c.ordinal < d.ordinal := by
+  simp only [Std.lt_iff_le_and_not_ge, le_iff_ordinal_le]
+
+theorem lt_iff_ofOrdinal_lt {f g : Fin Char.numCodePoints} :
+    f < g ↔ Char.ofOrdinal f < Char.ofOrdinal g := by
+  simp only [Std.lt_iff_le_and_not_ge, le_iff_ofOrdinal_le]
+
+theorem succ?_eq {c : Char} : c.succ? = (c.ordinal.addNat? 1).map Char.ofOrdinal := by
+  fun_cases Char.succ? with
+  | case1 h =>
+    rw [Fin.addNat?_eq_some]
+    · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal,
+        UInt32.ofNatLT_add, UInt32.reduceOfNatLT]
+      split
+      · simp only [UInt32.ofNatLT_toNat, dite_eq_ite, left_eq_ite_iff, Nat.not_lt,
+          Nat.reduceLeDiff, UInt32.left_eq_add]
+        grind [UInt32.lt_iff_toNat_lt]
+      · grind
+    · simp [coe_ordinal]
+      grind [UInt32.lt_iff_toNat_lt]
+  | case2 =>
+    rw [Fin.addNat?_eq_some]
+    · simp [coe_ordinal, *, Char.ext_iff, val_ofOrdinal, numSurrogates]
+    · simp [coe_ordinal, *, numCodePoints]
+  | case3 =>
+    rw [Fin.addNat?_eq_some]
+    · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal,
+        UInt32.ofNatLT_add, UInt32.reduceOfNatLT]
+      split
+      · grind
+      · rw [dif_neg]
+        · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.reduceToNat, Nat.reducePow,
+            UInt32.toNat_ofNatLT, Nat.mod_add_mod]
+          grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj]
+        · grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj]
+    · grind [UInt32.lt_iff_toNat_lt]
+  | case4 =>
+    rw [eq_comm]
+    grind [UInt32.lt_iff_toNat_lt]
+
+theorem map_ordinal_succ? {c : Char} : c.succ?.map ordinal = c.ordinal.addNat? 1 := by
+  simp [succ?_eq]
+
+theorem succMany?_eq {m : Nat} {c : Char} :
+    c.succMany? m = (c.ordinal.addNat? m).map Char.ofOrdinal := by
+  rfl
+
+end Char

src/Init/Data/Fin.lean

@@ -11,3 +11,4 @@ public import Init.Data.Fin.Log2
 public import Init.Data.Fin.Iterate
 public import Init.Data.Fin.Fold
 public import Init.Data.Fin.Lemmas
+public import Init.Data.Fin.OverflowAware

src/Init/Data/Fin/OverflowAware.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Fin.Basic
+import Init.Data.Fin.Lemmas
+
+set_option doc.verso true
+
+public section
+
+namespace Fin
+
+/--
+Overflow-aware addition of a natural number to an element of {lean}`Fin n`.
+
+Examples:
+* {lean}`(2 : Fin 3).addNat? 1 = (none : Option (Fin 3))`
+* {lean}`(2 : Fin 4).addNat? 1 = (some 3 : Option (Fin 4))`
+-/
+@[inline]
+protected def addNat? (i : Fin n) (m : Nat) : Option (Fin n) :=
+  if h : i + m < n then some ⟨i + m, h⟩ else none
+
+theorem addNat?_eq_some {i : Fin n} (h : i + m < n) : i.addNat? m = some ⟨i + m, h⟩ := by
+  simp [Fin.addNat?, h]
+
+theorem addNat?_eq_some_iff {i : Fin n} :
+    i.addNat? m = some j ↔ i + m < n ∧ j = i + m := by
+  simp only [Fin.addNat?]
+  split <;> simp [Fin.ext_iff, eq_comm, *]
+
+@[simp]
+theorem addNat?_eq_none_iff {i : Fin n} : i.addNat? m = none ↔ n ≤ i + m := by
+  simp only [Fin.addNat?]
+  split <;> simp_all [Nat.not_lt]
+
+@[simp]
+theorem addNat?_zero {i : Fin n} : i.addNat? 0 = some i := by
+  simp [addNat?_eq_some_iff]
+
+@[grind =]
+theorem addNat?_eq_dif {i : Fin n} :
+    i.addNat? m = if h : i + m < n then some ⟨i + m, h⟩ else none := by
+  rfl
+
+end Fin

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/Option.lean

@@ -15,3 +15,4 @@ public import Init.Data.Option.Attach
 public import Init.Data.Option.List
 public import Init.Data.Option.Monadic
 public import Init.Data.Option.Array
+public import Init.Data.Option.Function

src/Init/Data/Option/Function.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Function
+import Init.Data.Option.Lemmas
+
+public section
+
+namespace Option
+
+theorem map_injective {f : α → β} (hf : Function.Injective f) :
+    Function.Injective (Option.map f) := by
+  intros a b hab
+  cases a <;> cases b
+  · simp
+  · simp at hab
+  · simp at hab
+  · simp only [map_some, some.injEq] at hab
+    simpa using hf hab
+
+end Option

src/Init/Data/Option/Lemmas.lean

@@ -307,12 +307,20 @@ theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
 
 theorem map_id_apply' {α : Type u} {x : Option α} : Option.map (fun (a : α) => a) x = x := by simp
 
+/-- See `Option.apply_get` for a version that can be rewritten in the reverse direction. -/
 @[simp, grind =] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
     (o.map f).get h = f (o.get (by simpa using h)) := by
   cases o with
   | none => simp at h
   | some a => simp
 
+/-- See `Option.get_map` for a version that can be rewritten in the reverse direction. -/
+theorem apply_get {f : α → β} {o : Option α} {h} :
+    f (o.get h) = (o.map f).get (by simp [h]) := by
+  cases o
+  · simp at h
+  · simp
+
 @[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
     (x.map g).map h = x.map (h ∘ g) := by
   cases x <;> simp only [map_none, map_some, ·∘·]
@@ -732,6 +740,11 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
 theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
   cases h : p a <;> simp [*, guard]
 
+@[simp]
+theorem Option.elim_map {f : α → β} {g' : γ} {g : β → γ} (o : Option α) :
+    (o.map f).elim g' g = o.elim g' (g ∘ f) := by
+  cases o <;> simp
+
 -- I don't see how to construct a good grind pattern to instantiate this.
 @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl

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.lean

@@ -10,7 +10,10 @@ public import Init.Data.Range.Polymorphic.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Stream
 public import Init.Data.Range.Polymorphic.Lemmas
+public import Init.Data.Range.Polymorphic.Map
 
+public import Init.Data.Range.Polymorphic.Fin
+public import Init.Data.Range.Polymorphic.Char
 public import Init.Data.Range.Polymorphic.Nat
 public import Init.Data.Range.Polymorphic.Int
 public import Init.Data.Range.Polymorphic.BitVec

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

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Char.Ordinal
+public import Init.Data.Range.Polymorphic.Fin
+import Init.Data.Range.Polymorphic.Lemmas
+import Init.Data.Range.Polymorphic.Map
+import Init.Data.Char.Order
+
+open Std Std.PRange Std.PRange.UpwardEnumerable
+
+namespace Char
+
+public instance : UpwardEnumerable Char where
+  succ?
+  succMany?
+
+@[simp]
+public theorem pRangeSucc?_eq : PRange.succ? (α := Char) = Char.succ? := rfl
+
+@[simp]
+public theorem pRangeSuccMany?_eq : PRange.succMany? (α := Char) = Char.succMany? := rfl
+
+public instance : Rxc.HasSize Char where
+  size lo hi := Rxc.HasSize.size lo.ordinal hi.ordinal
+
+public instance : Rxo.HasSize Char where
+  size lo hi := Rxo.HasSize.size lo.ordinal hi.ordinal
+
+public instance : Rxi.HasSize Char where
+  size hi := Rxi.HasSize.size hi.ordinal
+
+public instance : Least? Char where
+  least? := some '\x00'
+
+@[simp]
+public theorem least?_eq : Least?.least? (α := Char) = some '\x00' := rfl
+
+def map : Map Char (Fin Char.numCodePoints) where
+  toFun := Char.ordinal
+  injective := ordinal_injective
+  succ?_toFun := by simp [succ?_eq]
+  succMany?_toFun := by simp [succMany?_eq]
+
+@[simp]
+theorem toFun_map : map.toFun = Char.ordinal := rfl
+
+instance : Map.PreservesLE map where
+  le_iff := by simp [le_iff_ordinal_le]
+
+instance : Map.PreservesRxcSize map where
+  size_eq := rfl
+
+instance : Map.PreservesRxoSize map where
+  size_eq := rfl
+
+instance : Map.PreservesRxiSize map where
+  size_eq := rfl
+
+instance : Map.PreservesLeast? map where
+  map_least? := by simp
+
+public instance : LawfulUpwardEnumerable Char := .ofMap map
+public instance : LawfulUpwardEnumerableLE Char := .ofMap map
+public instance : LawfulUpwardEnumerableLT Char := .ofMap map
+public instance : LawfulUpwardEnumerableLeast? Char := .ofMap map
+public instance : Rxc.LawfulHasSize Char := .ofMap map
+public instance : Rxc.IsAlwaysFinite Char := .ofMap map
+public instance : Rxo.LawfulHasSize Char := .ofMap map
+public instance : Rxo.IsAlwaysFinite Char := .ofMap map
+public instance : Rxi.LawfulHasSize Char := .ofMap map
+public instance : Rxi.IsAlwaysFinite Char := .ofMap map
+
+end Char

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

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Fin.OverflowAware
+import Init.Grind
+
+public section
+
+open Std Std.PRange
+
+namespace Fin
+
+instance : UpwardEnumerable (Fin n) where
+  succ? i := i.addNat? 1
+  succMany? m i := i.addNat? m
+
+@[simp, grind =]
+theorem pRangeSucc?_eq : PRange.succ? (α := Fin n) = (·.addNat? 1) := rfl
+
+@[simp, grind =]
+theorem pRangeSuccMany?_eq : PRange.succMany? m (α := Fin n) = (·.addNat? m) :=
+  rfl
+
+instance : LawfulUpwardEnumerable (Fin n) where
+  ne_of_lt a b := by grind [UpwardEnumerable.LT]
+  succMany?_zero a := by simp
+  succMany?_add_one m a := by grind
+
+instance : LawfulUpwardEnumerableLE (Fin n) where
+  le_iff x y := by
+    simp only [le_def, UpwardEnumerable.LE, pRangeSuccMany?_eq, Fin.addNat?_eq_dif,
+      Option.dite_none_right_eq_some, Option.some.injEq, ← val_inj, exists_prop]
+    exact ⟨fun h => ⟨y - x, by grind⟩, by grind⟩
+
+instance : Least? (Fin 0) where
+  least? := none
+
+instance : LawfulUpwardEnumerableLeast? (Fin 0) where
+  least?_le a := False.elim (Nat.not_lt_zero _ a.isLt)
+
+@[simp]
+theorem least?_eq_of_zero : Least?.least? (α := Fin 0) = none := rfl
+
+instance [NeZero n] : Least? (Fin n) where
+  least? := some 0
+
+instance [NeZero n] : LawfulUpwardEnumerableLeast? (Fin n) where
+  least?_le a := ⟨0, rfl, (LawfulUpwardEnumerableLE.le_iff 0 a).1 (Fin.zero_le _)⟩
+
+@[simp]
+theorem least?_eq [NeZero n] : Least?.least? (α := Fin n) = some 0 := rfl
+
+instance : LawfulUpwardEnumerableLT (Fin n) := inferInstance
+
+instance : Rxc.HasSize (Fin n) where
+  size lo hi := hi + 1 - lo
+
+@[grind =]
+theorem rxcHasSize_eq :
+    Rxc.HasSize.size (α := Fin n) = fun (lo hi : Fin n) => (hi + 1 - lo : Nat) := rfl
+
+instance : Rxc.LawfulHasSize (Fin n) where
+  size_eq_zero_of_not_le bound x := by grind
+  size_eq_one_of_succ?_eq_none lo hi := by grind
+  size_eq_succ_of_succ?_eq_some lo hi x := by grind
+
+instance : Rxc.IsAlwaysFinite (Fin n) := inferInstance
+
+instance : Rxo.HasSize (Fin n) := .ofClosed
+instance : Rxo.LawfulHasSize (Fin n) := inferInstance
+instance : Rxo.IsAlwaysFinite (Fin n) := inferInstance
+
+instance : Rxi.HasSize (Fin n) where
+  size lo := n - lo
+
+@[grind =]
+theorem rxiHasSize_eq :
+    Rxi.HasSize.size (α := Fin n) = fun (lo : Fin n) => (n - lo : Nat) := rfl
+
+instance : Rxi.LawfulHasSize (Fin n) where
+  size_eq_one_of_succ?_eq_none x := by grind
+  size_eq_succ_of_succ?_eq_some lo lo' := by grind
+
+instance : Rxi.IsAlwaysFinite (Fin n) := inferInstance
+
+end Fin

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

@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Function
+import Init.Data.Order.Lemmas
+import Init.Data.Option.Function
+
+public section
+
+/-!
+# Mappings between `UpwardEnumerable` types
+
+In this file we build machinery for pulling back lawfulness properties for `UpwardEnumerable` along
+injective functions that commute with the relevant operations.
+-/
+
+namespace Std
+
+namespace PRange
+
+namespace UpwardEnumerable
+
+/--
+An injective mapping between two types implementing `UpwardEnumerable` that commutes with `succ?`
+and `succMany?`.
+
+Having such a mapping means that all of the `Prop`-valued lawfulness classes around
+`UpwardEnumerable` can be pulled back.
+-/
+structure Map (α : Type u) (β : Type v) [UpwardEnumerable α] [UpwardEnumerable β] where
+  toFun : α → β
+  injective : Function.Injective toFun
+  succ?_toFun (a : α) : succ? (toFun a) = (succ? a).map toFun
+  succMany?_toFun (n : Nat) (a : α) : succMany? n (toFun a) = (succMany? n a).map toFun
+
+namespace Map
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem succ?_eq_none_iff (f : Map α β) {a : α} :
+    succ? a = none ↔ succ? (f.toFun a) = none := by
+  rw [← (Option.map_injective f.injective).eq_iff, Option.map_none, ← f.succ?_toFun]
+
+theorem succ?_eq_some_iff (f : Map α β) {a b : α} :
+    succ? a = some b ↔ succ? (f.toFun a) = some (f.toFun b) := by
+  rw [← (Option.map_injective f.injective).eq_iff, Option.map_some, ← f.succ?_toFun]
+
+theorem le_iff (f : Map α β) {a b : α} :
+    UpwardEnumerable.LE a b ↔ UpwardEnumerable.LE (f.toFun a) (f.toFun b) := by
+  simp only [UpwardEnumerable.LE, f.succMany?_toFun, Option.map_eq_some_iff]
+  refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩
+  rw [hn.1, Option.some_inj, f.injective hn.2]
+
+theorem lt_iff (f : Map α β) {a b : α} :
+    UpwardEnumerable.LT a b ↔ UpwardEnumerable.LT (f.toFun a) (f.toFun b) := by
+  simp only [UpwardEnumerable.LT, f.succMany?_toFun, Option.map_eq_some_iff]
+  refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩
+  rw [hn.1, Option.some_inj, f.injective hn.2]
+
+theorem succ?_toFun' (f : Map α β) : succ? ∘ f.toFun = Option.map f.toFun ∘ succ? := by
+  ext
+  simp [f.succ?_toFun]
+
+/-- Compatibility class for `Map` and `≤`. -/
+class PreservesLE [LE α] [LE β] (f : Map α β) where
+  le_iff : a ≤ b ↔ f.toFun a ≤ f.toFun b
+
+/-- Compatibility class for `Map` and `<`. -/
+class PreservesLT [LT α] [LT β] (f : Map α β) where
+  lt_iff : a < b ↔ f.toFun a < f.toFun b
+
+/-- Compatibility class for `Map` and `Rxc.HasSize`. -/
+class PreservesRxcSize [Rxc.HasSize α] [Rxc.HasSize β] (f : Map α β) where
+  size_eq : Rxc.HasSize.size a b = Rxc.HasSize.size (f.toFun a) (f.toFun b)
+
+/-- Compatibility class for `Map` and `Rxo.HasSize`. -/
+class PreservesRxoSize [Rxo.HasSize α] [Rxo.HasSize β] (f : Map α β) where
+  size_eq : Rxo.HasSize.size a b = Rxo.HasSize.size (f.toFun a) (f.toFun b)
+
+/-- Compatibility class for `Map` and `Rxi.HasSize`. -/
+class PreservesRxiSize [Rxi.HasSize α] [Rxi.HasSize β] (f : Map α β) where
+  size_eq : Rxi.HasSize.size b = Rxi.HasSize.size (f.toFun b)
+
+/-- Compatibility class for `Map` and `Least?`. -/
+class PreservesLeast? [Least? α] [Least? β] (f : Map α β) where
+  map_least? : Least?.least?.map f.toFun = Least?.least?
+
+end UpwardEnumerable.Map
+
+open UpwardEnumerable
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem LawfulUpwardEnumerable.ofMap [LawfulUpwardEnumerable β] (f : Map α β) :
+    LawfulUpwardEnumerable α where
+  ne_of_lt a b := by
+    simpa only [f.lt_iff, ← f.injective.ne_iff] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero a := by
+    apply Option.map_injective f.injective
+    simpa [← f.succMany?_toFun] using LawfulUpwardEnumerable.succMany?_zero _
+  succMany?_add_one n a := by
+    apply Option.map_injective f.injective
+    rw [← f.succMany?_toFun, LawfulUpwardEnumerable.succMany?_add_one,
+      f.succMany?_toFun, Option.bind_map, Map.succ?_toFun', Option.map_bind]
+
+instance [LE α] [LT α] [LawfulOrderLT α] [LE β] [LT β] [LawfulOrderLT β] (f : Map α β)
+    [f.PreservesLE] : f.PreservesLT where
+  lt_iff := by simp [lt_iff_le_and_not_ge, Map.PreservesLE.le_iff (f := f)]
+
+theorem LawfulUpwardEnumerableLE.ofMap [LE α] [LE β] [LawfulUpwardEnumerableLE β] (f : Map α β)
+    [f.PreservesLE] : LawfulUpwardEnumerableLE α where
+  le_iff := by simp [Map.PreservesLE.le_iff (f := f), f.le_iff, LawfulUpwardEnumerableLE.le_iff]
+
+theorem LawfulUpwardEnumerableLT.ofMap [LT α] [LT β] [LawfulUpwardEnumerableLT β] (f : Map α β)
+    [f.PreservesLT] : LawfulUpwardEnumerableLT α where
+  lt_iff := by simp [Map.PreservesLT.lt_iff (f := f), f.lt_iff, LawfulUpwardEnumerableLT.lt_iff]
+
+theorem LawfulUpwardEnumerableLeast?.ofMap [Least? α] [Least? β] [LawfulUpwardEnumerableLeast? β]
+    (f : Map α β) [f.PreservesLeast?] : LawfulUpwardEnumerableLeast? α where
+  least?_le a := by
+    obtain ⟨l, hl, hl'⟩ := LawfulUpwardEnumerableLeast?.least?_le (f.toFun a)
+    have : (Least?.least? (α := α)).isSome := by
+      rw [← Option.isSome_map (f := f.toFun), Map.PreservesLeast?.map_least?,
+        hl, Option.isSome_some]
+    refine ⟨Option.get _ this, by simp, ?_⟩
+    rw [f.le_iff, Option.apply_get (f := f.toFun)]
+    simpa [Map.PreservesLeast?.map_least?, hl] using hl'
+
+end PRange
+
+open PRange PRange.UpwardEnumerable
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem Rxc.LawfulHasSize.ofMap [LE α] [LE β] [Rxc.HasSize α] [Rxc.HasSize β] [Rxc.LawfulHasSize β]
+    (f : Map α β) [f.PreservesLE] [f.PreservesRxcSize] : Rxc.LawfulHasSize α where
+  size_eq_zero_of_not_le a b := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f)] using
+      Rxc.LawfulHasSize.size_eq_zero_of_not_le _ _
+  size_eq_one_of_succ?_eq_none lo hi := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f),
+        f.succ?_eq_none_iff] using
+      Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _
+  size_eq_succ_of_succ?_eq_some lo hi lo' := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f),
+        f.succ?_eq_some_iff] using
+      Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _
+
+theorem Rxo.LawfulHasSize.ofMap [LT α] [LT β] [Rxo.HasSize α] [Rxo.HasSize β] [Rxo.LawfulHasSize β]
+    (f : Map α β) [f.PreservesLT] [f.PreservesRxoSize] : Rxo.LawfulHasSize α where
+  size_eq_zero_of_not_le a b := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f)] using
+      Rxo.LawfulHasSize.size_eq_zero_of_not_le _ _
+  size_eq_one_of_succ?_eq_none lo hi := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f),
+        f.succ?_eq_none_iff] using
+      Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _
+  size_eq_succ_of_succ?_eq_some lo hi lo' := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f),
+        f.succ?_eq_some_iff] using
+      Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _
+
+theorem Rxi.LawfulHasSize.ofMap [Rxi.HasSize α] [Rxi.HasSize β] [Rxi.LawfulHasSize β]
+    (f : Map α β) [f.PreservesRxiSize] : Rxi.LawfulHasSize α where
+  size_eq_one_of_succ?_eq_none lo := by
+    simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_none_iff] using
+      Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _
+  size_eq_succ_of_succ?_eq_some lo lo' := by
+    simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_some_iff] using
+      Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _
+
+theorem Rxc.IsAlwaysFinite.ofMap [LE α] [LE β] [Rxc.IsAlwaysFinite β] (f : Map α β)
+    [f.PreservesLE] : Rxc.IsAlwaysFinite α where
+  finite init hi := by
+    obtain ⟨n, hn⟩ := Rxc.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi)
+    exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLE.le_iff (f := f)] using hn⟩
+
+theorem Rxo.IsAlwaysFinite.ofMap [LT α] [LT β] [Rxo.IsAlwaysFinite β] (f : Map α β)
+    [f.PreservesLT] : Rxo.IsAlwaysFinite α where
+  finite init hi := by
+    obtain ⟨n, hn⟩ := Rxo.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi)
+    exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLT.lt_iff (f := f)] using hn⟩
+
+theorem Rxi.IsAlwaysFinite.ofMap [Rxi.IsAlwaysFinite β] (f : Map α β) : Rxi.IsAlwaysFinite α where
+  finite init := by
+    obtain ⟨n, hn⟩ := Rxi.IsAlwaysFinite.finite (f.toFun init)
+    exact ⟨n, by simpa [f.succMany?_toFun] using hn⟩
+
+end Std

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/SInt/Basic.lean

@@ -157,7 +157,7 @@ Converts an 8-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int8.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int8.toNatClampNeg (i : Int8) : Nat := i.toInt.toNat
+@[suggest_for Int8.toNat, inline] def Int8.toNatClampNeg (i : Int8) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
 @[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := ⟨⟨b⟩⟩
@@ -510,7 +510,7 @@ Converts a 16-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int16.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int16.toNatClampNeg (i : Int16) : Nat := i.toInt.toNat
+@[suggest_for Int16.toNat, inline] def Int16.toNatClampNeg (i : Int16) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
 @[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := ⟨⟨b⟩⟩
@@ -880,7 +880,7 @@ Converts a 32-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int32.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int32.toNatClampNeg (i : Int32) : Nat := i.toInt.toNat
+@[suggest_for Int32.toNat, inline] def Int32.toNatClampNeg (i : Int32) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
 @[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := ⟨⟨b⟩⟩
@@ -1270,7 +1270,7 @@ Converts a 64-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int64.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int64.toNatClampNeg (i : Int64) : Nat := i.toInt.toNat
+@[suggest_for Int64.toNat, inline] def Int64.toNatClampNeg (i : Int64) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
 @[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := ⟨⟨b⟩⟩
@@ -1637,7 +1637,7 @@ Converts a word-sized signed integer to a natural number, mapping all negative n
 
 Use `ISize.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def ISize.toNatClampNeg (i : ISize) : Nat := i.toInt.toNat
+@[suggest_for ISize.toNat, inline] def ISize.toNatClampNeg (i : ISize) : Nat := i.toInt.toNat
 
 /-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
 @[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := ⟨⟨b⟩⟩

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/Grind/Util.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Classical
-
 public section
-
 namespace Lean.Grind
 
 /-- A helper gadget for annotating nested proofs in goals. -/

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
@@ -2810,6 +2810,8 @@ structure Char where
   /-- The value must be a legal scalar value. -/
   valid : val.isValidChar
 
+grind_pattern Char.valid => self.val
+
 private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
   match h with
   | Or.inl h      => Nat.lt_trans h (of_decide_eq_true rfl)
@@ -3192,7 +3194,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 +3483,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 +3539,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,140 @@
+/-
+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 not_true_eq : (¬ True) = False := by simp
+theorem not_false_eq : (¬ False) = True := 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 String.lt_eq_true (a b : String) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Char.lt_eq_true (a b : Char) (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 String.lt_eq_false (a b : String) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Char.lt_eq_false (a b : Char) (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 String.le_eq_true (a b : String) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Char.le_eq_true (a b : Char) (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 String.le_eq_false (a b : String) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Char.le_eq_false (a b : Char) (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 String.eq_eq_true (a b : String) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Char.eq_eq_true (a b : Char) (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 String.eq_eq_false (a b : String) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Char.eq_eq_false (a b : Char) (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

@@ -518,14 +518,13 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)
   assuming these are definitionally equal.
 * `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
   assuming `t` and `t'` are definitionally equal.
--/
-syntax (name := change) "change " term (location)? : tactic
-
-/--
 * `change a with b` will change occurrences of `a` to `b` in the goal,
   assuming `a` and `b` are definitionally equal.
 * `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
 -/
+syntax (name := change) "change " term (location)? : tactic
+
+@[tactic_alt change]
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
 /--
@@ -546,7 +545,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.
@@ -905,8 +904,13 @@ The tactic supports all the same syntax variants and options as the `let` term.
 -/
 macro "let" c:letConfig d:letDecl : tactic => `(tactic| refine_lift let $c:letConfig $d:letDecl; ?_)
 
-/-- `let rec f : t := e` adds a recursive definition `f` to the current goal.
-The syntax is the same as term-mode `let rec`. -/
+/--
+`let rec f : t := e` adds a recursive definition `f` to the current goal.
+The syntax is the same as term-mode `let rec`.
+
+The tactic supports all the same syntax variants and options as the `let` term.
+-/
+@[tactic_name "let rec"]
 syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
 macro_rules
   | `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_)
@@ -1212,22 +1216,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
 syntax (name := congr) "congr" (ppSpace num)? : tactic
 
 
-/--
-In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
-```
-by_cases h : t
-· tac1
-· tac2
-```
-It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs.
-
-You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
-if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
-by the end of the block.
--/
-syntax (name := tacDepIfThenElse)
-  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
-    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
 
 /--
 In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
@@ -1236,16 +1224,34 @@ by_cases t
 · tac1
 · tac2
 ```
-It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous
-hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use
-nondependent `if`, since this wouldn't add anything to the context and hence would be
-useless for proving theorems. To actually insert an `ite` application use
-`refine if t then ?_ else ?_`.)
+It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and
+`tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't
+add anything to the context and hence would be useless for proving theorems. To actually insert an
+`ite` application use `refine if t then ?_ else ?_`.)
+
+The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as
+alternative syntax for:
+```
+by_cases h : t
+· tac1
+· tac2
+```
+It performs case distinction on `h : t` or `h : ¬t`.
+
+You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
+if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
+by the end of the block.
 -/
 syntax (name := tacIfThenElse)
   ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq)
     ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
 
+
+@[tactic_alt tacIfThenElse]
+syntax (name := tacDepIfThenElse)
+  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
+    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
+
 /--
 The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an
 empty pattern match, closing the goal if the introduced pattern is impossible.

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/Compiler/ModPkgExt.lean

@@ -56,9 +56,9 @@ public def Environment.getModulePackageByIdx? (env : Environment) (idx : ModuleI
 Returns the standard base of the native symbol for the compiled constant {lean}`declName`.
 
 For many constants, this is the full symbol. However, initializers have an additional prefix
-(i.e., {lit}`_init_`) and boxed functions have an additional suffix (i.e., {lit}`___boxed`).
-Furthermore, some constants do not use this stem at all (e.g., {lit}`main` and definitions
-with {lit}`@[export]`).
+(i.e., {lit}`_init_`) and boxed functions have an additional suffix
+(see {name}`mkMangledBoxedName`). Furthermore, some constants do not use this stem at all
+(e.g., {lit}`main` and definitions with {lit}`@[export]`).
 -/
 @[export lean_get_symbol_stem]
 public def getSymbolStem (env : Environment) (declName : Name) : String :=