chore: missing @[grind] annotation for Array

This PR fixes the behavior of `simp_all?` and `simp_all?!`, aligning
them with `simp_all` and `simp_all!` respectively.

Closes #8490

.github/workflows/awaiting-mathlib.yml

@@ -10,11 +10,29 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check awaiting-mathlib label
+        id: check-awaiting-mathlib-label
         if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
           script: |
-            const { labels } = context.payload.pull_request;
-            if (labels.some(label => label.name == "awaiting-mathlib") && !labels.some(label => label.name == "builds-mathlib")) {
-              core.setFailed('PR is marked "awaiting-mathlib" but "builds-mathlib" label has not been applied yet by the bot');
+            const { labels, number: prNumber } = context.payload.pull_request;
+            const hasAwaiting = labels.some(label => label.name == "awaiting-mathlib");
+            const hasBreaks = labels.some(label => label.name == "breaks-mathlib");
+            const hasBuilds = labels.some(label => label.name == "builds-mathlib");
+
+            if (hasAwaiting && hasBreaks) {
+              core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
+            } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
+              core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
+              core.setOutput('awaiting', 'true');
             }
+      
+      - name: Wait for mathlib compatibility
+        if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
+        run: |
+          echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
+          echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
+          # Keep the job running indefinitely to show "in progress" status
+          while true; do
+            sleep 3600  # Sleep for 1 hour at a time
+          done

.github/workflows/update-stage0.yml

@@ -40,34 +40,24 @@ jobs:
       run: |
           git config --global user.name "Lean stage0 autoupdater"
           git config --global user.email "<>"
-    # Would be nice, but does not work yet:
-    # https://github.com/DeterminateSystems/magic-nix-cache/issues/39
-    # This action does not run that often and building runs in a few minutes, so ok for now
-    #- if: env.should_update_stage0 == 'yes'
-    #  uses: DeterminateSystems/magic-nix-cache-action@v2
-    - if: env.should_update_stage0 == 'yes'
-      name: Restore Build Cache
-      uses: actions/cache/restore@v4
-      with:
-        path: nix-store-cache
-        key: Nix Linux-nix-store-cache-${{ github.sha }}
-        # fall back to (latest) previous cache
-        restore-keys: |
-          Nix Linux-nix-store-cache
-    - if: env.should_update_stage0 == 'yes'
-      name: Further Set Up Nix Cache
-      shell: bash -euxo pipefail {0}
-      run: |
-        # Nix seems to mutate the cache, so make a copy
-        cp -r nix-store-cache nix-store-cache-copy || true
     - if: env.should_update_stage0 == 'yes'
       name: Install Nix
       uses: DeterminateSystems/nix-installer-action@main
-      with:
-        extra-conf: |
-          substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
+    - name: Open Nix shell once
+      if: env.should_update_stage0 == 'yes'
+      run: true
+      shell: 'nix develop -c bash -euxo pipefail {0}'
+    - name: Set up NPROC
+      if: env.should_update_stage0 == 'yes'
+      run: |
+        echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
+      shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
-      run: nix run .#update-stage0-commit
+      run: cmake --preset release
+      shell: 'nix develop -c bash -euxo pipefail {0}'
+    - if: env.should_update_stage0 == 'yes'
+      run: make -j$NPROC -C build/release  update-stage0-commit
+      shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: git show --stat
     - if: env.should_update_stage0 == 'yes' && github.event_name == 'push'

doc/std/README.md

@@ -0,0 +1,9 @@
+# The Lean standard library
+
+This directory contains development information about the Lean standard library. The user-facing documentation of the standard library
+is part of the [Lean Language Reference](https://lean-lang.org/doc/reference/latest/).
+
+Here you will find
+* the [standard library vision document](./vision.md), including the call for contributions,
+* the [standard library style guide](./style.md), and
+* the [standard library naming conventions](./naming.md).

doc/std/naming.md

@@ -0,0 +1,260 @@
+# Standard library naming conventions
+
+The easiest way to access a result in the standard library is to correctly guess the name of the declaration (possibly with the help of identifier autocompletion). This is faster and has lower friction than more sophisticated search tools, so easily guessable names (which are still reasonably short) make Lean users more productive.
+
+The guide that follows contains very few hard rules, many heuristics and a selection of examples. It cannot and does not present a deterministic algorithm for choosing good names in all situations. It is intended as a living document that gets clarified and expanded as situations arise during code reviews for the standard library. If applying one of the suggestions in this guide leads to nonsensical results in a certain situation, it is
+probably safe to ignore the suggestion (or even better, suggest a way to improve the suggestion).
+
+## Prelude
+
+Identifiers use a mix of `UpperCamelCase`, `lowerCamelCase` and `snake_case`, used for types, data, and theorems, respectively.
+
+Structure fields should be named such that the projections have the correct names.
+
+## Naming convention for types
+
+When defining a type, i.e., a (possibly 0-ary) function whose codomain is Sort u for some u, it should be named in UpperCamelCase. Examples include `List`, and `List.IsPrefix`.
+
+When defining a predicate, prefix the name by `Is`, like in `List.IsPrefix`. The `Is` prefix may be omitted if
+* the resulting name would be ungrammatical, or
+* the predicate depends on additional data in a way where the `Is` prefix would be confusing (like `List.Pairwise`), or
+* the name is an adjective (like `Std.Time.Month.Ordinal.Valid`)
+
+## Namespaces and generalized projection notation
+
+Almost always, definitions and theorems relating to a type should be placed in a namespace with the same name as the type. For example, operations and theorems about lists should be placed in the `List` namespace, and operations and theorems about `Std.Time.PlainDate` should be placed in the `Std.Time.PlainDate` namespace.
+
+Declarations in the root namespace will be relatively rare. The most common type of declaration in the root namespace are declarations about data and properties exported by notation type classes, as long as they are not about a specific type implementing that type class. For example, we have
+
+```lean
+theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b := sorry
+```
+
+in the root namespace, but
+
+```lean
+theorem List.cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
+    (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
+```
+
+belongs in the `List` namespace.
+
+Subtleties arise when multiple namespaces are in play. Generally, place your theorem in the most specific namespace that appears in one of the hypotheses of the theorem. The following names are both correct according to this convention:
+
+```lean
+theorem List.Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse := sorry
+theorem List.reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ := sorry
+```
+
+Notice that the second theorem does not have a hypothesis of type `List.Sublist l` for some `l`, so the name `List.Sublist.reverse_iff` would be incorrect.
+
+The advantage of placing results in a namespace like `List.Sublist` is that it enables generalized projection notation, i.e., given `h : l₁ <+ l₂`,
+one can write `h.reverse` to obtain a proof of `l₁.reverse <+ l₂.reverse`. Thinking about which dot notations are convenient can act as a guideline
+for deciding where to place a theorem, and is, on occasion, a good reason to duplicate a theorem into multiple namespaces.
+
+### The `Std` namespace
+
+New types that are added will usually be placed in the `Std` namespace and in the `Std/` source directory, unless there are good reasons to place
+them elsewhere.
+
+Inside the `Std` namespace, all internal declarations should be `private` or else have a name component that clearly marks them as internal, preferably
+`Internal`.
+
+
+## Naming convention for data
+
+When defining data, i.e., a (possibly 0-ary) function whose codomain is not Sort u, but has type Type u for some u, it should be named in lowerCamelCase. Examples include `List.append` and `List.isPrefixOf`.
+If your data is morally fully specified by its type, then use the naming procedure for theorems described below and convert the result to lower camel case.
+
+If your function returns an `Option`, consider adding `?` as a suffix. If your function may panic, consider adding `!` as a suffix. In many cases, there will be multiple variants of a function; one returning an option, one that may panic and possibly one that takes a proof argument.
+
+## Naming algorithm for theorems and some definitions
+
+There is, in principle, a general algorithm for naming a theorem. The problem with this algorithm is that it produces very long and unwieldy names which need to be shortened. So choosing a name for a declaration can be thought of as consisting of a mechanical part and a creative part.
+
+Usually the first part is to decide which namespace the result should live in, according to the guidelines described above.
+
+Next, consider the type of your declaration as a tree. Inner nodes of this tree are function types or function applications. Leaves of the tree are 0-ary functions or bound variables.
+
+As an example, consider the following result from the standard library:
+
+```lean
+example {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+    [Inhabited β] {m : Std.HashMap α β} {a : α} {h' : a ∈ m} : m[a]? = some (m[a]'h') :=
+  sorry
+```
+
+The correct namespace is clearly `Std.HashMap`. The corresponding tree looks like this:
+
+![](naming-tree.svg)
+
+The preferred spelling of a notation can be looked up by hovering over the notation.
+
+Now traverse the tree and build a name according to the following rules:
+
+* When encountering a function type, first turn the result type into a name, then all of the argument types from left to right, and join the names using `_of_`.
+* When encountering a function that is neither an infix notation nor a structure projection, first put the function name and then the arguments, joined by an underscore.
+* When encountering an infix notation, join the arguments using the name of the notation, separated by underscores.
+* When encountering a structure projection, proceed as for normal functions, but put the name of the projection last.
+* When encountering a name, put it in lower camel case.
+* Skip bound variables and proofs.
+* Type class arguments are also generally skipped.
+
+When encountering namespaces names, concatenate them in lower camel case.
+
+Applying this algorithm to our example yields the name `Std.HashMap.getElem?_eq_optionSome_getElem_of_mem`.
+
+From there, the name should be shortened, using the following heuristics:
+
+* The namespace of functions can be omitted if it is clear from context or if the namespace is the current one. This is almost always the case.
+* For infix operators, it is possible to leave out the RHS or the name of the notation and the RHS if they are clear from context.
+* Hypotheses can be left out if it is clear that they are required or if they appear in the conclusion.
+
+Based on this, here are some possible names for our example:
+
+1. `Std.HashMap.getElem?_eq`
+2. `Std.HashMap.getElem?_eq_of_mem`
+3. `Std.HashMap.getElem?_eq_some`
+4. `Std.HashMap.getElem?_eq_some_of_mem`
+5. `Std.HashMap.getElem?_eq_some_getElem`
+6. `Std.Hashmap.getElem?_eq_some_getElem_of_mem`
+
+Choosing a good name among these then requires considering the context of the lemma. In this case it turns out that the first four options are underspecified as there is also a lemma relating `m[a]?` and `m[a]!` which could have the same name. This leaves the last two options, the first of which is shorter, and this is how the lemma is called in the Lean standard library.
+
+Here are some additional examples:
+
+```lean
+example {x y : List α} (h : x <+: y) (hx : x ≠ []) :
+  x.head hx = y.head (h.ne_nil hx) := sorry
+```
+
+Since we have an `IsPrefix` parameter, this should live in the `List.IsPrefix` namespace, and the algorithm suggests `List.IsPrefix.head_eq_head_of_ne_nil`, which is shortened to `List.IsPrefix.head`. Note here the difference between the namespace name (`IsPrefix`) and the recommended spelling of the corresponding notation (`prefix`).
+
+```lean
+example : l₁ <+: l₂ → reverse l₁ <:+ reverse l₂ := sorry
+```
+
+Again, this result should be in the `List.IsPrefix` namespace; the algorithm suggests `List.IsPrefix.reverse_prefix_reverse`, which becomes `List.IsPrefix.reverse`.
+
+The following examples show how the traversal order often matters.
+
+```lean
+theorem Nat.mul_zero (n : Nat) : n * 0 = 0 := sorry
+theorem Nat.zero_mul (n : Nat) : 0 * n = 0 := sorry
+```
+
+Here we see that one name may be a prefix of another name:
+
+```lean
+theorem Int.mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 := sorry
+theorem Int.mul_ne_zero_iff {a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := sorry
+```
+
+It is usually a good idea to include the `iff` in a theorem name even if the name would still be unique without the name. For example,
+
+```lean
+theorem List.head?_eq_none_iff : l.head? = none ↔ l = [] := sorry
+```
+
+is a good name: if the lemma was simply called `List.head?_eq_none`, users might try to `apply` it when the goal is `l.head? = none`, leading
+to confusion.
+
+The more common you expect (or want) a theorem to be, the shorter you should try to make the name. For example, we have both
+
+```lean
+theorem Std.HashMap.getElem?_eq_none_of_contains_eq_false {a : α} : m.contains a = false → m[a]? = none := sorry
+theorem Std.HashMap.getElem?_eq_none {a : α} : ¬a ∈ m → m[a]? = none := sorry
+```
+
+As users of the hash map are encouraged to use ∈ rather than contains, the second lemma gets the shorter name.
+
+## Special cases
+
+There are certain special “keywords” that may appear in identifiers.
+
+| Keyword | Meaning | Example |
+| :---- | :---- | :---- |
+| `def` | Unfold a definition. Avoid this for public APIs. | `Nat.max_def` |
+| `refl` | Theorems of the form `a R a`, where R is a reflexive relation and `a` is an explicit parameter | `Nat.le_refl` |
+| `rfl` | Like `refl`, but with `a` implicit | `Nat.le_rfl` |
+| `irrefl` | Theorems of the form `¬a R a`, where R is an irreflexive relation | `Nat.lt_irrefl` |
+| `symm` | Theorems of the form `a R b → b R a`, where R is a symmetric relation (compare `comm` below) | `Eq.symm` |
+| `trans` | Theorems of the form `a R b → b R c → a R c`, where R is a transitive relation (R may carry data) | `Eq.trans` |
+| `antisymmm` | Theorems of the form `a R b → b R a → a = b`, where R is an antisymmetric relation | `Nat.le_antisymm` |
+| `congr` | Theorems of the form `a R b → f a S f b`, where R and S are usually equivalence relations | `Std.HashMap.mem_congr` |
+| `comm` | Theorems of the form `f a b = f b a` (compare `symm` above) | `Eq.comm`, `Nat.add_comm` |
+| `assoc` | Theorems of the form `g (f a b) c = f a (g b c)` (note the order! In most cases, we have f = g) | `Nat.add_sub_assoc` |
+| `distrib` | Theorems of the form `f (g a b) = g (f a) (f b)` | `Nat.add_left_distrib` |
+| `self` | May be used if a variable appears multiple times in the conclusion | `List.mem_cons_self` |
+| `inj` | Theorems of the form `f a = f b ↔ a = b`. | `Int.neg_inj`, `Nat.add_left_inj` |
+| `cancel` | Theorems which have one of the forms `f a = f b → a = b` or `g (f a) = a`, where `f` and `g` usually involve a binary operator | `Nat.add_sub_cancel` |
+| `cancel_iff` | Same as `inj`, but with different conventions for left and right (see below) | `Nat.add_right_cancel_iff` |
+| `ext` | Theorems of the form `f a = f b → a = b`, where `f` usually involves some kind of projection | `List.ext_getElem`
+| `mono` | Theorems of the form `a R b → f a R f b`, where `R` is a transitive relation | `List.countP_mono_left`
+
+### Left and right
+
+The keywords left and right are useful to disambiguate symmetric variants of theorems.
+
+```lean
+theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) := sorry
+theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) := sorry
+```
+
+It is not always obvious which version of a theorem should be “left” and which should be “right”.
+Heuristically, the theorem should name the side which is “more variable”, but there are exceptions. For some of the special keywords discussed in this section, there are conventions which should be followed, as laid out in the following examples:
+
+```lean
+theorem Nat.left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := sorry
+theorem Nat.right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k := sorry
+theorem Nat.add_left_cancel {n m k : Nat} : n + m = n + k → m = k := sorry
+theorem Nat.add_right_cancel {n m k : Nat} : n + m = k + m → n = k := sorry
+theorem Nat.add_left_cancel_iff {m k n : Nat} : n + m = n + k ↔ m = k := sorry
+theorem Nat.add_right_cancel_iff {m k n : Nat} : m + n = k + n ↔ m = k := sorry
+theorem Nat.add_left_inj {m k n : Nat} : m + n = k + n ↔ m = k := sorry
+theorem Nat.add_right_inj {m k n : Nat} : n + m = n + k ↔ m = k := sorry
+```
+
+Note in particular that the convention is opposite for `cancel_iff` and `inj`.
+
+```lean
+theorem Nat.add_sub_self_left (a b : Nat) : (a + b) - a = b := sorry
+theorem Nat.add_sub_self_right (a b : Nat) : (a + b) - b = a := sorry
+theorem Nat.add_sub_cancel (n m : Nat) : (n + m) - m = n := sorry
+```
+
+## Primed names
+
+Avoid disambiguating variants of a concept by appending the `'` character (e.g., introducing both `BitVec.sshiftRight` and `BitVec.sshiftRight'`), as it is impossible to tell the difference without looking at the type signature, the documentation or even the code, and even if you know what the two variants are there is no way to tell which is which. Prefer descriptive pairs `BitVec.sshiftRightNat`/`BitVec.sshiftRight`.
+
+## Acronyms
+
+For acronyms which are three letters or shorter, all letters should use the same case as dictated by the convention. For example, `IO` is a correct name for a type and the name `IO.Ref` may become `IORef` when used as part of a definition name and `ioRef` when used as part of a theorem name.
+
+For acronyms which are at least four letters long, switch to lower case starting from the second letter. For example, `Json` is a correct name for a type, as is `JsonRPC`.
+
+If an acronym is typically spelled using mixed case, this mixed spelling may be used in identifiers (for example `Std.Net.IPv4Addr`).
+
+## Simp sets
+
+Simp sets centered around a conversion function should be called `source_to_target`. For example, a simp set for the `BitVec.toNat` function, which goes from `BitVec` to
+`Nat`, should be called `bitvec_to_nat`.
+
+## Variable names
+
+We make the following recommendations for variable names, but without insisting on them:
+* Simple hypotheses should be named `h`, `h'`, or using a numerical sequence `h₁`, `h₂`, etc.
+* Another common name for a simple hypothesis is `w` (for "witness").
+* `List`s should be named `l`, `l'`, `l₁`, etc, or `as`, `bs`, etc.
+  (Use of `as`, `bs` is encouraged when the lists are of different types, e.g. `as : List α` and `bs : List β`.)
+  `xs`, `ys`, `zs` are allowed, but it is better if these are reserved for `Array` and `Vector`.
+  A list of lists may be named `L`.
+* `Array`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the arrays are of different types, e.g. `as : Array α` and `bs : Array β`.
+  An array of arrays may be named `xss`.
+* `Vector`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the vectors are of different types, e.g. `as : Vector α n` and `bs : Vector β n`.
+  A vector of vectors may be named `xss`.
+* A common exception for `List` / `Array` / `Vector` is to use `acc` for an accumulator in a recursive function.
+* `i`, `j`, `k` are preferred for numerical indices.
+  Descriptive names such as `start`, `stop`, `lo`, and `hi` are encouraged when they increase readability.
+* `n`, `m` are preferred for sizes, e.g. in `Vector α n` or `xs.size = n`.
+* `w` is preferred for the width of a `BitVec`.

doc/std/style.md

@@ -0,0 +1,522 @@
+# Standard library style
+
+Please take some time to familiarize yourself with the stylistic conventions of
+the project and the specific part of the library you are planning to contribute
+to. While the Lean compiler may not enforce strict formatting rules,
+consistently formatted code is much easier for others to read and maintain.
+Attention to formatting is more than a cosmetic concern—it reflects the same
+level of precision and care required to meet the deeper standards of the Lean 4
+standard library.
+
+Below we will give specific formatting prescriptions for various language constructs. Note that this style guide only applies to the Lean standard library, even though some examples in the guide are taken from other parts of the Lean code base.
+
+## Basic whitespace rules
+
+Syntactic elements (like `:`, `:=`, `|`, `::`) are surrounded by single spaces, with the exception of `,` and `;`, which are followed by a space but not preceded by one. Delimiters (like `()`, `{}`) do not have spaces on the inside, with the exceptions of subtype notation and structure instance notation.
+
+Examples of correctly formatted function parameters:
+
+* `{α : Type u}`
+* `[BEq α]`
+* `(cmp : α → α → Ordering)`
+* `(hab : a = b)`
+* `{d : { l : List ((n : Nat) × Vector Nat n) // l.length % 2 = 0 }}`
+
+Examples of correctly formatted terms:
+
+* `1 :: [2, 3]`
+* `letI : Ord α := ⟨cmp⟩; True`
+* `(⟨2, 3⟩ : Nat × Nat)`
+* `((2, 3) : Nat × Nat)`
+* `{ x with fst := f (4 + f 0), snd := 4, .. }`
+* `match 1 with | 0 => 0 | _ => 0`
+* `fun ⟨a, b⟩ _ _ => by cases hab <;> apply id; rw [hbc]`
+
+Configure your editor to remove trailing whitespace. If you have set up Visual Studio Code for Lean development in the recommended way then the correct setting is applied automatically.
+
+## Splitting terms across multiple lines
+
+When splitting a term across multiple lines, increase indentation by two spaces starting from the second line. When splitting a function application, try to split at argument boundaries. If an argument itself needs to be split, increase indentation further as appropriate.
+
+When splitting at an infix operator, the operator goes at the end of the first line, not at the beginning of the second line. When splitting at an infix operator, you may or may not increase indentation depth, depending on what is more readable.
+
+When splitting an `if`-`then`-`else` expression, the `then` keyword wants to stay with the condition and the `else` keyword wants to stay with the alternative term. Otherwise, indent as if the `if` and `else` keywords were arguments to the same function.
+
+When splitting a comma-separated bracketed sequence (i.e., anonymous constructor application, list/array/vector literal, tuple) it is allowed to indent subsequent lines for alignment, but indenting by two spaces is also allowed.
+
+Do not orphan parentheses.
+
+Correct:
+```lean
+def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
+  v₁.name.isPrefixOf v₂.name &&
+  v₁.scopes == v₂.scopes &&
+  v₁.mainModule == v₂.mainModule &&
+  v₁.imported == v₂.imported
+```
+
+Correct:
+```lean
+theorem eraseP_eq_iff {p} {l : List α} :
+    l.eraseP p = l' ↔
+      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
+        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧
+          l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ :=
+  sorry
+```
+
+Correct:
+```lean
+example : Nat :=
+  functionWithAVeryLongNameSoThatSomeArgumentsWillNotFit firstArgument secondArgument
+    (firstArgumentWithAnEquallyLongNameAndThatFunctionDoesHaveMoreArguments firstArgument
+      secondArgument)
+    secondArgument
+```
+
+Correct:
+```lean
+theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
+    (m.alter k f).size =
+      if m.contains k && (f (m.get? k)).isNone then
+        m.size - 1
+      else if !m.contains k && (f (m.get? k)).isSome then
+        m.size + 1
+      else
+        m.size := by
+ simp_to_raw using Raw₀.size_alter
+```
+
+Correct:
+```lean
+theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
+    (m.alter k f).get? k' =
+      if h : k == k' then
+        cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k))
+      else m.get? k' := by
+ simp_to_raw using Raw₀.get?_alter
+```
+
+Correct:
+```lean
+example : Nat × Nat :=
+  ⟨imagineThisWasALongTerm,
+   imagineThisWasAnotherLongTerm⟩
+```
+
+Correct:
+```lean
+example : Nat × Nat :=
+  ⟨imagineThisWasALongTerm,
+    imagineThisWasAnotherLongTerm⟩
+```
+
+Correct:
+```lean
+example : Vector Nat :=
+  #v[imagineThisWasALongTerm,
+     imagineThisWasAnotherLongTerm]
+```
+
+## Basic file structure
+
+Every file should start with a copyright header, imports (in the standard library, this always includes a `prelude` declaration) and a module documentation string. There should not be a blank line between the copyright header and the imports. There should be a blank line between the imports and the module documentation string.
+
+If you explicitly declare universe variables, do so at the top of the file, after the module documentation.
+
+Correct:
+```lean
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
+  Yury Kudryashov
+-/
+prelude
+import Init.Data.List.Pairwise
+import Init.Data.List.Find
+
+/-!
+**# Lemmas about `List.eraseP` and `List.erase`.**
+-/
+
+universe u u'
+```
+
+Syntax that is not supposed to be user-facing must be scoped. New public syntax must always be discussed explicitly in an RFC.
+
+## Top-level commands and declarations
+
+All top-level commands are unindented. Sectioning commands like `section` and `namespace` do not increase the indentation level.
+
+Attributes may be placed on the same line as the rest of the command or on a separate line.
+
+Multi-line declaration headers are indented by four spaces starting from the second line. The colon that indicates the type of a declaration may not be placed at the start of a line or on its own line.
+
+Declaration bodies are indented by two spaces. Short declaration bodies may be placed on the same line as the declaration type.
+
+Correct:
+```lean
+theorem eraseP_eq_iff {p} {l : List α} :
+    l.eraseP p = l' ↔
+      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
+        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧
+          l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ :=
+  sorry
+```
+
+Correct:
+```lean
+@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl
+```
+
+Correct:
+```lean
+@[simp]
+theorem eraseP_nil : [].eraseP p = [] := rfl
+```
+
+### Documentation comments
+
+Note to external contributors: this is a section where the Lean style and the mathlib style are different.
+
+Declarations should be documented as required by the `docBlame` linter, which may be activated in a file using
+`set_option linter.missingDocs true` (we allow these to stay in the file).
+
+Single-line documentation comments should go on the same line as `/--`/`-/`, while multi-line documentation strings
+should have these delimiters on their own line, with the documentation comment itself unindented.
+
+Documentation comments must be written in the indicative mood. Use American orthography.
+
+Correct:
+```lean
+/-- Carries out a monadic action on each mapping in the hash map in some order. -/
+@[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit :=
+  b.buckets.forM (AssocList.forM f)
+```
+
+Correct:
+```lean
+/--
+Monadically computes a value by folding the given function over the mappings in the hash
+map in some order.
+-/
+@[inline] def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ :=
+  b.buckets.foldlM (fun acc l => l.foldlM f acc) init
+```
+
+### Where clauses
+
+The `where` keyword should be unindented, and all declarations bound by it should be indented with two spaces.
+
+Blank lines before and after `where` and between declarations bound by `where` are optional and should be chosen
+to maximize readability.
+
+Correct:
+```lean
+@[simp] theorem partition_eq_filter_filter (p : α → Bool) (l : List α) :
+    partition p l = (filter p l, filter (not ∘ p) l) := by
+  simp [partition, aux]
+where
+  aux (l) {as bs} : partition.loop p l (as, bs) =
+      (as.reverse ++ filter p l, bs.reverse ++ filter (not ∘ p) l) :=
+    match l with
+    | [] => by simp [partition.loop, filter]
+    | a :: l => by cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]
+```
+
+### Termination arguments
+
+The `termination_by`, `decreasing_by`, `partial_fixpoint` keywords should be unindented. The associated terms should be indented like declaration bodies.
+
+Correct:
+```lean
+@[inline] def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do
+  let rec loop (p : String.Pos) := do
+    if h : opt.atEnd p then
+      return
+    else
+      handle (opt.get' p h)
+      loop (opt.next' p h)
+  termination_by opt.utf8ByteSize - p.byteIdx
+  decreasing_by
+    simp [String.atEnd] at h
+    apply Nat.sub_lt_sub_left h
+    simp [String.lt_next opt p]
+  loop ⟨1⟩
+```
+
+Correct:
+```lean
+def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) : Bool :=
+  off1.byteIdx + sz ≤ s1.endPos.byteIdx && off2.byteIdx + sz ≤ s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
+where
+  loop (off1 off2 stop1 : Pos) :=
+    if _h : off1.byteIdx < stop1.byteIdx then
+      let c₁ := s1.get off1
+      let c₂ := s2.get off2
+      c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
+    else true
+  termination_by stop1.1 - off1.1
+  decreasing_by
+    have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left c₁.utf8Size_pos off1.1)
+    decreasing_tactic
+```
+
+Correct:
+```lean
+theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
+  rw [div_eq, mod_eq]
+  have h : Decidable (0 < n ∧ n ≤ m) := inferInstance
+  cases h with
+  | isFalse h => simp [h]
+  | isTrue h =>
+    simp [h]
+    have ih := div_add_mod (m - n) n
+    rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
+decreasing_by apply div_rec_lemma; assumption
+```
+
+### Deriving
+
+The `deriving` clause should be unindented.
+
+Correct:
+```lean
+structure Iterator where
+  array : ByteArray
+  idx : Nat
+deriving Inhabited
+```
+
+## Notation and Unicode
+
+We generally prefer to use notation as available. We usually prefer the Unicode versions of notations over non-Unicode alternatives.
+
+There are some rules and exceptions regarding specific notations which are listed below:
+
+* Sigma types: use `(a : α) × β a` instead of `Σ a, β a` or `Sigma β`.
+* Function arrows: use `fun a => f x` instead of `fun x ↦ f x` or `λ x => f x` or any other variant.
+
+## Language constructs
+
+### Pattern matching, induction etc.
+
+Match arms are indented at the indentation level that the match statement would have if it was on its own line. If the match is implicit, then the arms should be indented as if the match was explicitly given. The content of match arms is indented two spaces, so that it appears on the same level as the match pattern.
+
+Correct:
+```lean
+def alter [BEq α] {β : Type v} (a : α) (f : Option β → Option β) :
+    AssocList α (fun _ => β) → AssocList α (fun _ => β)
+  | nil => match f none with
+    | none => nil
+    | some b => AssocList.cons a b nil
+  | cons k v l =>
+    if k == a then
+      match f v with
+      | none => l
+      | some b => cons a b l
+    else
+      cons k v (alter a f l)
+```
+
+Correct:
+```lean
+theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
+    ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as := by
+  induction xs with
+  | nil => cases h
+  | cons x xs ih =>
+    simp at h
+    cases h with
+    | inl h => exact ⟨[], xs, by simp_all⟩
+    | inr h =>
+      by_cases h' : a = x
+      · subst h'
+        exact ⟨[], xs, by simp⟩
+      · obtain ⟨as, bs, rfl, h⟩ := ih h
+        exact ⟨x :: as, bs, rfl, by simp_all⟩
+```
+
+Aligning match arms is allowed, but not required.
+
+Correct:
+```lean
+def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
+  match h₁?, h₂? with
+  | none, none       => return none
+  | none, some h     => return h
+  | some h, none     => return h
+  | some h₁, some h₂ => mkEqTrans h₁ h₂
+```
+
+Correct:
+```lean
+def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
+  match h₁?, h₂? with
+  | none, none => return none
+  | none, some h => return h
+  | some h, none => return h
+  | some h₁, some h₂ => mkEqTrans h₁ h₂
+```
+
+Correct:
+```lean
+def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
+  match h₁?, h₂? with
+  | none,    none    => return none
+  | none,    some h  => return h
+  | some h,  none    => return h
+  | some h₁, some h₂ => mkEqTrans h₁ h₂
+```
+
+### Structures
+
+Note to external contributors: this is a section where the Lean style and the mathlib style are different.
+
+When using structure instance syntax over multiple lines, the opening brace should go on the preceding line, while the closing brace should go on its own line. The rest of the syntax should be indented by one level. During structure updates, the `with` clause goes on the same line as the opening brace. Aligning at the assignment symbol is allowed but not required.
+
+Correct:
+```lean
+def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (reportExts := true) :
+    IO AddConstAsyncResult := do
+  let sigPromise ← IO.Promise.new
+  let infoPromise ← IO.Promise.new
+  let extensionsPromise ← IO.Promise.new
+  let checkedEnvPromise ← IO.Promise.new
+  let asyncConst := {
+    constInfo := {
+      name := constName
+      kind
+      sig := sigPromise.result
+      constInfo := infoPromise.result
+    }
+    exts? := guard reportExts *> some extensionsPromise.result
+  }
+  return {
+    constName, kind
+    mainEnv := { env with
+      asyncConsts := env.asyncConsts.add asyncConst
+      checked := checkedEnvPromise.result }
+    asyncEnv := { env with
+      asyncCtx? := some { declPrefix := privateToUserName constName.eraseMacroScopes }
+    }
+    sigPromise, infoPromise, extensionsPromise, checkedEnvPromise
+  }
+```
+
+Correct:
+```lean
+instance [Inhabited α] : Inhabited (Descr α β σ) where
+  default := {
+    name         := default
+    mkInitial    := default
+    ofOLeanEntry := default
+    toOLeanEntry := default
+    addEntry     := fun s _ => s
+  }
+```
+
+### Declaring structures
+
+When defining structure types, do not parenthesize structure fields.
+
+When declaring a structure type with a custom constructor name, put the custom name on its own line, indented like the
+structure fields, and add a documentation comment.
+
+Correct:
+
+```lean
+/--
+A bitvector of the specified width.
+
+This is represented as the underlying `Nat` number in both the runtime
+and the kernel, inheriting all the special support for `Nat`.
+-/
+structure BitVec (w : Nat) where
+  /--
+  Constructs a `BitVec w` from a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector.
+  -/
+  ofFin ::
+  /--
+  Interprets a bitvector as a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector.
+  -/
+  toFin : Fin (2 ^ w)
+```
+
+## Tactic proofs
+
+Tactic proofs are the most common thing to break during any kind of upgrade, so it is important to write them in a way that minimizes the likelihood of proofs breaking and that makes it easy to debug breakages if they do occur.
+
+If there are multiple goals, either use a tactic combinator (like `all_goals`) to operate on all of them or a clearly specified subset, or use focus dots to work on goals one at a time. Using structured proofs (e.g., `induction … with`) is encouraged but not mandatory.
+
+Squeeze non-terminal `simp`s (i.e., calls to `simp` which do not close the goal). Squeezing terminal `simp`s is generally discouraged, although there are exceptions (for example if squeezing yields a noticeable performance improvement).
+
+Do not over-golf proofs in ways that are likely to lead to hard-to-debug breakage. Examples of things to avoid include complex multi-goal manipulation using lots of tactic combinators, complex uses of the substitution operator (`▸`) and clever point-free expressions (possibly involving anonymous function notation for multiple arguments).
+
+Do not under-golf proofs: for routine tasks, use the most powerful tactics available.
+
+Do not use `erw`. Avoid using `rfl` after `simp` or `rw`, as this usually indicates a missing lemma that should be used instead of `rfl`.
+
+Use `(d)simp` or `rw` instead of `delta` or `unfold`. Use `refine` instead of `refine’`. Use `haveI` and `letI` only if they are actually required.
+
+Prefer highly automated tactics (like `grind` and `omega`) over low-level proofs, unless the automated tactic requires unacceptable additional imports or has bad performance. If you decide against using a highly automated tactic, leave a comment explaining the decision.
+
+## `do` notation
+
+The `do` keyword goes on the same line as the corresponding `:=` (or `=>`, or similar). `Id.run do` should be treated as if it was a bare `do`.
+
+Use early `return` statements to reduce nesting depth and make the non-exceptional control flow of a function easier to see.
+
+Alternatives for `let` matches may be placed in the same line or in the next line, indented by two spaces. If the term that is
+being matched on is itself more than one line and there is an alternative present, consider breaking immediately after `←` and indent
+as far as necessary to ensure readability.
+
+Correct:
+```lean
+def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
+  let some decl ← findFunDecl? fvarId | throwError "unknown local function {fvarId.name}"
+  return decl
+```
+
+Correct:
+```lean
+def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
+  let some decl ←
+        findFunDecl? fvarId
+    | throwError "unknown local function {fvarId.name}"
+  return decl
+```
+
+Correct:
+```lean
+def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
+  let some decl ← findFunDecl?
+      fvarId
+    | throwError "unknown local function {fvarId.name}"
+  return decl
+```
+
+Correct:
+```lean
+def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
+  let mctx ← getMCtx
+  let mut numAnonymous := 0
+  for g in newGoals do
+    if mctx.isAnonymousMVar g then
+      numAnonymous := numAnonymous + 1
+  modifyMCtx fun mctx => Id.run do
+    let mut mctx := mctx
+    let mut idx  := 1
+    for g in newGoals do
+      if mctx.isAnonymousMVar g then
+        if numAnonymous == 1 then
+          mctx := mctx.setMVarUserName g parentTag
+        else
+          mctx := mctx.setMVarUserName g (parentTag ++ newSuffix.appendIndexAfter idx)
+        idx := idx + 1
+    pure mctx
+```
+

doc/std/vision.md

@@ -0,0 +1,98 @@
+# The Lean 4 standard library
+
+Maintainer team (in alphabetical order): Henrik Böving, Markus Himmel
+(community contact & external contribution coordinator), Kim Morrison, Paul
+Reichert, Sofia Rodrigues.
+
+The Lean 4 standard library is a core part of the Lean distribution, providing
+essential building blocks for functional programming, verified software
+development, and software verification. Unlike the standard libraries of most
+other languages, many of its components are formally verified and can be used
+as part of verified applications.
+
+The standard library is a public API that contains the components listed in the
+standard library outline below. Not all public APIs in the Lean distribution
+are part of the standard library, and the standard library does not correspond
+to a certain directory within the Lean source repository (like `Std`). For
+example, the metaprogramming framework is not part of the standard library, but
+basic types like `True` and `Nat` are.
+
+The standard library is under active development. Our guiding principles are:
+
+* Provide comprehensive, verified building blocks for real-world software.
+* Build a public API of the highest quality with excellent internal consistency.
+* Carefully optimize components that may be used in performance-critical software.
+* Ensure smooth adoption and maintenance for users.
+* Offer excellent documentation, example projects, and guides.
+* Provide a reliable and extensible basis that libraries for software
+  development, software verification and mathematics can build on.
+
+The standard library is principally developed by the Lean FRO. Community
+contributions are welcome. If you would like to contribute, please refer to the
+call for contributions below.
+
+### Standard library outline
+
+1. Core types and operations
+   1. Basic types
+   2. Numeric types, including floating point numbers
+   3. Containers
+   4. Strings and formatting
+2. Language constructs
+   1. Ranges and iterators
+   2. Comparison, ordering, hashing and related type classes
+   3. Basic monad infrastructure
+3. Libraries
+   1. Random numbers
+   2. Dates and times
+4. Operating system abstractions
+   1. Concurrency and parallelism primitives
+   2. Asynchronous I/O
+   3. FFI helpers
+   4. Environment, file system, processes
+   5. Locales
+
+The material covered in the first three sections (core types and operations,
+language constructs and libraries) will be verified, with the exception of
+floating point numbers and the parts of the libraries that interface with the
+operating system (e.g., sources of operating system randomness or time zone
+database access).
+
+### Call for contributions
+
+Thank you for taking interest in contributing to the Lean standard library\!
+There are two main ways for community members to contribute to the Lean
+standard library: by contributing experience reports or by contributing code
+and lemmas.
+
+**If you are using Lean for software verification or verified software
+development:** hearing about your experiences using Lean and its standard
+library for software verification is extremely valuable to us. We are committed
+to building a standard library suitable for real-world applications and your
+input will directly influence the continued evolution of the Lean standard
+library. Please reach out to the standard library maintainer team via Zulip
+(either in a public thread in the \#lean4 channel or via direct message). Even
+just a link to your code helps. Thanks\!
+
+**If you have code that you believe could enhance the Lean 4 standard
+library:** we encourage you to initiate a discussion in the \#lean4 channel on
+Zulip. This is the most effective way to receive preliminary feedback on your
+contribution. The Lean standard library has a very precise scope and it has
+very high quality standards, so at the moment we are mostly interested in
+contributions that expand upon existing material rather than introducing novel
+concepts.
+
+**If you would like to contribute code to the standard library but don’t know
+what to work on:** we are always excited to meet motivated community members
+who would like to contribute, and there is always impactful work that is
+suitable for new contributors. Please reach out to Markus Himmel on Zulip to
+discuss possible contributions.
+
+As laid out in the [project-wide External Contribution
+Guidelines](../../CONTRIBUTING.md),
+PRs are much more likely to be merged if they are preceded by an RFC or if you
+discussed your planned contribution with a member of the standard library
+maintainer team. When in doubt, introducing yourself is always a good idea.
+
+All code in the standard library is expected to strictly adhere to the
+[standard library coding conventions](./style.md).

script/benchReelabRss.lean

@@ -8,12 +8,12 @@ open Lean.JsonRpc
 Tests language server memory use by repeatedly re-elaborate a given file.
 
 NOTE: only works on Linux for now.
-ot to touch the imports for usual files.
 -/
 
 def main (args : List String) : IO Unit := do
   let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
-  let uri := s!"file:///{file}"
+  let file ← IO.FS.realPath file
+  let uri := s!"file://{file}"
   Ipc.runWith leanCmd (#["--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
   -- for use with heaptrack:
   --Ipc.runWith "heaptrack" (#[leanCmd, "--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do

src/CMakeLists.txt

@@ -689,7 +689,7 @@ add_custom_target(make_stdlib ALL
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc
   VERBATIM)
 
 # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -768,7 +768,7 @@ if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_S
   add_custom_target(leanc ALL
     WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
     DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanc
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanc
     VERBATIM)
 endif()
 
@@ -823,7 +823,6 @@ endif()
 
 # Escape for `make`. Yes, twice.
 string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
-string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
 configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
 
 # hacky

src/Init/BinderNameHint.lean

@@ -40,5 +40,5 @@ This gadget is supported by
 It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics
 (e.g. `apply`).
 -/
-@[simp ↓]
+@[simp ↓, expose]
 def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e

src/Init/Classical.lean

@@ -107,8 +107,8 @@ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
   (strongIndefiniteDescription p h).property
 
-theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
-  epsilon_spec_aux (nonempty_of_exists hex) p hex
+theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α hex.nonempty p) :=
+  epsilon_spec_aux hex.nonempty p hex
 
 theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
   @epsilon_spec α (fun y => y = x) ⟨x, rfl⟩

src/Init/Control/Except.lean

@@ -127,7 +127,7 @@ end Except
 /--
 Adds exceptions of type `ε` to a monad `m`.
 -/
-def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
+@[expose] def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
   m (Except ε α)
 
 /--

src/Init/Control/ExceptCps.lean

@@ -18,7 +18,7 @@ Adds exceptions of type `ε` to a monad `m`.
 Instead of using `Except ε` to model exceptions, this implementation uses continuation passing
 style. This has different performance characteristics from `ExceptT ε`.
 -/
-def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
+@[expose] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
 
 namespace ExceptCpsT
 

src/Init/Control/Id.lean

@@ -34,7 +34,7 @@ def containsFive (xs : List Nat) : Bool := Id.run do
 true
 ```
 -/
-def Id (type : Type u) : Type u := type
+@[expose] def Id (type : Type u) : Type u := type
 
 namespace Id
 
@@ -56,7 +56,7 @@ Runs a computation in the identity monad.
 This function is the identity function. Because its parameter has type `Id α`, it causes
 `do`-notation in its arguments to use the `Monad Id` instance.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def run (x : Id α) : α := x
 
 instance [OfNat α n] : OfNat (Id α) n :=

src/Init/Control/Lawful/Basic.lean

@@ -6,6 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
+import Init.Ext
 import Init.SimpLemmas
 import Init.Meta
 
@@ -241,13 +242,23 @@ theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
 
 namespace Id
 
-@[simp] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
-@[simp] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
-@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+@[ext] theorem ext {x y : Id α} (h : x.run = y.run) : x = y := h
 
 instance : LawfulMonad Id := by
   refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
+@[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
+@[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
+@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
+@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
+@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
+@[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
+
+-- These lemmas are bad as they abuse the defeq of `Id α` and `α`
+@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
+@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
+@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+
 end Id
 
 /-! # Option -/

src/Init/Control/Lawful/Instances.lean

@@ -7,7 +7,8 @@ module
 
 prelude
 import Init.Control.Lawful.Basic
-import Init.Control.Except
+import all Init.Control.Except
+import all Init.Control.State
 import Init.Control.StateRef
 import Init.Ext
 
@@ -98,7 +99,7 @@ end ExceptT
 
 instance : LawfulMonad (Except ε) := LawfulMonad.mk'
   (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun _ _ => rfl)
+  (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun a _ _ => by cases a <;> rfl)
 
 instance : LawfulApplicative (Except ε) := inferInstance
@@ -247,7 +248,7 @@ instance : LawfulMonad (EStateM ε σ) := .mk'
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
-  (pure_bind := fun _ _ => rfl)
+  (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
     dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with

src/Init/Control/Option.lean

@@ -20,7 +20,7 @@ instance : ToBool (Option α) := ⟨Option.isSome⟩
 Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a
 failure occurred.
 -/
-def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
+@[expose] def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)
 
 /--

src/Init/Control/State.lean

@@ -22,7 +22,7 @@ Adds a mutable state of type `σ` to a monad.
 Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple
 of a value and a state.
 -/
-def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+@[expose] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)
 
 /--
@@ -47,7 +47,7 @@ A tuple-based state monad.
 Actions in `StateM σ` are functions that take an initial state and return a value paired with a
 final state.
 -/
-@[reducible]
+@[expose, reducible]
 def StateM (σ α : Type u) : Type u := StateT σ Id α
 
 instance {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) where

src/Init/Control/StateCps.lean

@@ -18,7 +18,7 @@ The State monad transformer using CPS style.
 An alternative implementation of a state monad transformer that internally uses continuation passing
 style instead of tuples.
 -/
-def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
+@[expose] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
 
 namespace StateCpsT
 

src/Init/Control/StateRef.lean

@@ -17,7 +17,7 @@ A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ`
 
 The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead.
 -/
-def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
+@[expose] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 
 /-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/
 

src/Init/Core.lean

@@ -12,6 +12,8 @@ import Init.Prelude
 import Init.SizeOf
 set_option linter.missingDocs true -- keep it documented
 
+@[expose] section
+
 universe u v w
 
 /--
@@ -1210,10 +1212,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
 instance : Inhabited Prop where
   default := True
 
-deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
-
-theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
-  | ⟨w, _⟩ => ⟨w⟩
+deriving instance Inhabited for NonScalar, PNonScalar, True
 
 /-! # Subsingleton -/
 
@@ -1387,16 +1386,7 @@ instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
 instance Sum.nonemptyRight [h : Nonempty β] : Nonempty (Sum α β) :=
   Nonempty.elim h (fun b => ⟨Sum.inr b⟩)
 
-instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
-  match a, b with
-  | Sum.inl a, Sum.inl b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr a, Sum.inr b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
-  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
+deriving instance DecidableEq for Sum
 
 end
 

src/Init/Data/Array/Attach.lean

@@ -9,7 +9,7 @@ prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Count
-import Init.Data.List.Attach
+import all Init.Data.List.Attach
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -69,11 +69,11 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 @[simp] theorem toList_attachWith {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs, P x} :
-   (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList] using H) := by
+   (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList_iff] using H) := by
   simp [attachWith]
 
 @[simp] theorem toList_attach {xs : Array α} :
-    xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList]) := by
+    xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList_iff]) := by
   simp [attach]
 
 @[simp] theorem toList_pmap {xs : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ xs, P a} :
@@ -574,9 +574,12 @@ state, the right approach is usually the tactic `simp [Array.unattach, -Array.ma
 -/
 def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array α := xs.map (·.val)
 
-@[simp] theorem unattach_nil {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := by
+@[simp] theorem unattach_empty {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := by
   simp [unattach]
 
+@[deprecated unattach_empty (since := "2025-05-26")]
+abbrev unattach_nil := @unattach_empty
+
 @[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {xs : Array { x // p x }} :
     (xs.push a).unattach = xs.unattach.push a.1 := by
   simp only [unattach, Array.map_push]

src/Init/Data/Array/Basic.lean

@@ -13,8 +13,8 @@ import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
-import Init.Data.List.ToArrayImpl
-import Init.Data.Array.Set
+import all Init.Data.List.ToArrayImpl
+import all Init.Data.Array.Set
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -112,6 +112,10 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
+@[simp, grind =] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
+
+@[simp] theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
+
 end Array
 
 namespace List
@@ -334,6 +338,8 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
   decreasing_by simp_wf; decreasing_trivial_pre_omega
 
+-- See also `Array.ofFnM` defined in `Init.Data.Array.OfFn`.
+
 /--
 Constructs an array that contains all the numbers from `0` to `n`, exclusive.
 
@@ -538,7 +544,7 @@ Examples:
 -/
 @[inline]
 def modify (xs : Array α) (i : Nat) (f : α → α) : Array α :=
-  Id.run <| modifyM xs i f
+  Id.run <| modifyM xs i (pure <| f ·)
 
 set_option linter.indexVariables false in -- Changing `idx` causes bootstrapping issues, haven't investigated.
 /--
@@ -1053,7 +1059,7 @@ Examples:
 -/
 @[inline]
 def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 /--
 Folds a function over an array from the right, accumulating a value starting with `init`. The
@@ -1070,7 +1076,7 @@ Examples:
 -/
 @[inline]
 def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β :=
-  Id.run <| as.foldrM f init start stop
+  Id.run <| as.foldrM (pure <| f · ·) init start stop
 
 /--
 Computes the sum of the elements of an array.
@@ -1118,7 +1124,7 @@ Examples:
 -/
 @[inline]
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
-  Id.run <| as.mapM f
+  Id.run <| as.mapM (pure <| f ·)
 
 instance : Functor Array where
   map := map
@@ -1133,7 +1139,7 @@ valid.
 -/
 @[inline]
 def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β :=
-  Id.run <| as.mapFinIdxM f
+  Id.run <| as.mapFinIdxM (pure <| f · · ·)
 
 /--
 Applies a function to each element of the array along with the index at which that element is found,
@@ -1144,7 +1150,7 @@ is valid.
 -/
 @[inline]
 def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β :=
-  Id.run <| as.mapIdxM f
+  Id.run <| as.mapIdxM (pure <| f · ·)
 
 /--
 Pairs each element of an array with its index, optionally starting from an index other than `0`.
@@ -1192,7 +1198,7 @@ some 10
 -/
 @[inline]
 def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
-  Id.run <| as.findSomeM? f
+  Id.run <| as.findSomeM? (pure <| f ·)
 
 /--
 Returns the first non-`none` result of applying the function `f` to each element of the
@@ -1226,7 +1232,7 @@ Examples:
 -/
 @[inline]
 def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
-  Id.run <| as.findSomeRevM? f
+  Id.run <| as.findSomeRevM? (pure <| f ·)
 
 /--
 Returns the last element of the array for which the predicate `p` returns `true`, or `none` if no
@@ -1238,7 +1244,7 @@ Examples:
 -/
 @[inline]
 def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
-  Id.run <| as.findRevM? p
+  Id.run <| as.findRevM? (pure <| p ·)
 
 /--
 Returns the index of the first element for which `p` returns `true`, or `none` if there is no such
@@ -1377,7 +1383,7 @@ Examples:
 -/
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
-  Id.run <| as.anyM p start stop
+  Id.run <| as.anyM (pure <| p ·) start stop
 
 /--
 Returns `true` if `p` returns `true` for every element of `as`.
@@ -1395,7 +1401,7 @@ Examples:
 -/
 @[inline]
 def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
-  Id.run <| as.allM p start stop
+  Id.run <| as.allM (pure <| p ·) start stop
 
 /--
 Checks whether `a` is an element of `as`, using `==` to compare elements.
@@ -1664,7 +1670,7 @@ Example:
 -/
 @[inline]
 def filterMap (f : α → Option β) (as : Array α) (start := 0) (stop := as.size) : Array β :=
-  Id.run <| as.filterMapM f (start := start) (stop := stop)
+  Id.run <| as.filterMapM (pure <| f ·) (start := start) (stop := stop)
 
 /--
 Returns the largest element of the array, as determined by the comparison `lt`, or `none` if

src/Init/Data/Array/BasicAux.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.NotationExtra
 
@@ -88,4 +88,4 @@ pointer equality, and does not allocate a new array if the result of each functi
 pointer-equal to its argument.
 -/
 @[inline] def Array.mapMono (as : Array α) (f : α → α) : Array α :=
-  Id.run <| as.mapMonoM f
+  Id.run <| as.mapMonoM (pure <| f ·)

src/Init/Data/Array/BinSearch.lean

@@ -129,6 +129,6 @@ Examples:
 * `#[].binInsert (· < ·) 1 = #[1]`
 -/
 @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=
-  Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k
+  Id.run <| binInsertM lt (fun _ => pure k) (fun _ => pure k) as k
 
 end Array

src/Init/Data/Array/Bootstrap.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 import Init.Data.List.TakeDrop
+import all Init.Data.Array.Basic
 
 /-!
 ## Bootstrapping theorems about arrays
@@ -52,8 +53,8 @@ theorem foldlM_toList.aux [Monad m]
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_toList.aux (j := j+1) H]
     rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
-    rfl
-  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
+    simp
+  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; simp
 
 @[simp, grind =] theorem foldlM_toList [Monad m]
     {f : β → α → m β} {init : β} {xs : Array α} :
@@ -69,14 +70,14 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (xs.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f xs 0 i h init := by
   unfold foldrM.fold
   match i with
-  | 0 => simp [List.foldlM, List.take]
+  | 0 => simp
   | i+1 => rw [← List.take_concat_get h]; simp [← aux]
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
     xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by
   have : xs = #[] ∨ 0 < xs.size :=
     match xs with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
-  match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_
+  match xs, this with | _, .inl rfl => simp [foldrM] | xs, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
 @[simp, grind =] theorem foldrM_toList [Monad m]
@@ -88,9 +89,13 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
     xs.toList.foldr f init = xs.foldr f init :=
   List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
-@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
+@[simp, grind =] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
+  rcases xs with ⟨xs⟩
   simp [push, List.concat_eq_append]
 
+@[deprecated toList_push (since := "2025-05-26")]
+abbrev push_toList := @toList_push
+
 @[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
   simp [toListAppend, ← foldr_toList]
 

src/Init/Data/Array/Count.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Count
 
@@ -51,8 +52,8 @@ theorem countP_push {a : α} {xs : Array α} : countP p (xs.push a) = countP p x
   rcases xs with ⟨xs⟩
   simp_all
 
-@[simp] theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
-  simp [countP_push]
+theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
+  simp
 
 theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + countP (fun a => ¬p a) xs := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/DecidableEq.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 import Init.Data.BEq
 import Init.Data.List.Nat.BEq
 import Init.ByCases

src/Init/Data/Array/Erase.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Basic
@@ -23,7 +24,7 @@ open Nat
 
 /-! ### eraseP -/
 
-@[simp] theorem eraseP_empty : #[].eraseP p = #[] := by simp
+theorem eraseP_empty : #[].eraseP p = #[] := by simp
 
 theorem eraseP_of_forall_mem_not {xs : Array α} (h : ∀ a, a ∈ xs → ¬p a) : xs.eraseP p = xs := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Extract.lean

@@ -238,11 +238,9 @@ theorem extract_append_left {as bs : Array α} :
     (as ++ bs).extract 0 as.size = as.extract 0 as.size := by
   simp
 
-@[simp] theorem extract_append_right {as bs : Array α} :
+theorem extract_append_right {as bs : Array α} :
     (as ++ bs).extract as.size (as.size + i) = bs.extract 0 i := by
-  simp only [extract_append, extract_size_left, Nat.sub_self, empty_append]
-  congr 1
-  omega
+  simp
 
 @[simp] theorem map_extract {as : Array α} {i j : Nat} :
     (as.extract i j).map f = (as.map f).extract i j := by

src/Init/Data/Array/Find.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.List.Nat.Find
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.Array.Range
@@ -141,9 +142,9 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 @[simp] theorem find?_empty : find? p #[] = none := rfl
 
-@[simp] theorem find?_singleton {a : α} {p : α → Bool} :
+theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
-  simp [singleton_eq_toArray_singleton]
+  simp
 
 @[simp] theorem findRev?_push_of_pos {xs : Array α} (h : p a) :
     findRev? p (xs.push a) = some a := by
@@ -346,7 +347,8 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
-@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
+theorem findIdx_empty : findIdx p #[] = 0 := rfl
+
 theorem findIdx_singleton {a : α} {p : α → Bool} :
     #[a].findIdx p = if p a then 0 else 1 := by
   simp
@@ -599,7 +601,8 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 
 /-! ### findFinIdx? -/
 
-@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
   simp
@@ -698,7 +701,7 @@ The verification API for `idxOf?` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx?` (and proved using them).
 -/
 
-@[simp] theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
+theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
 
 @[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = none ↔ a ∉ xs := by
@@ -711,14 +714,10 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp
 
-@[simp]
 theorem isNone_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.idxOf? a).isNone = ¬ a ∈ xs := by
-  rcases xs with ⟨xs⟩
   simp
 
-
-
 /-! ### finIdxOf?
 
 The verification API for `finIdxOf?` is still incomplete.
@@ -729,7 +728,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
-@[simp] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
+theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
 
 @[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by
@@ -747,10 +746,8 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp
 
-@[simp]
 theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by
-  rcases xs with ⟨xs⟩
   simp
 
 end Array

src/Init/Data/Array/GetLit.lean

@@ -27,11 +27,13 @@ theorem extLit {n : Nat}
     (h : (i : Nat) → (hi : i < n) → xs.getLit i hsz₁ hi = ys.getLit i hsz₂ hi) : xs = ys :=
   Array.ext (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
 
-def toListLitAux (xs : Array α) (n : Nat) (hsz : xs.size = n) : ∀ (i : Nat), i ≤ xs.size → List α → List α
+-- has to be expose for array literal support
+@[expose] def toListLitAux (xs : Array α) (n : Nat) (hsz : xs.size = n) : ∀ (i : Nat), i ≤ xs.size → List α → List α
   | 0,     _,  acc => acc
   | (i+1), hi, acc => toListLitAux xs n hsz i (Nat.le_of_succ_le hi) (xs.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
 
-def toArrayLit (xs : Array α) (n : Nat) (hsz : xs.size = n) : Array α :=
+-- has to be expose for array literal support
+@[expose] def toArrayLit (xs : Array α) (n : Nat) (hsz : xs.size = n) : Array α :=
   List.toArray <| toListLitAux xs n hsz n (hsz ▸ Nat.le_refl _) []
 
 theorem toArrayLit_eq (xs : Array α) (n : Nat) (hsz : xs.size = n) : xs = toArrayLit xs n hsz := by

src/Init/Data/Array/Lemmas.lean

@@ -8,11 +8,13 @@ module
 prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Range
+import all Init.Data.List.Control
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
 import Init.Data.List.Nat.Basic
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
+import all Init.Data.Array.Bootstrap
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
 import Init.Data.Array.Lex.Basic
@@ -59,14 +61,9 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
 
 @[grind] theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-@[simp] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
-
-@[deprecated emptyWithCapacity_eq (since := "2025-03-12")]
-theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
-
 /-! ### size -/
 
-@[grind →] theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
+theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
   cases xs
   simp_all
 
@@ -78,7 +75,6 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
   cases xs
   simpa using List.ne_nil_of_length_pos h
 
-@[grind]
 theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
@@ -120,14 +116,11 @@ abbrev size_eq_one := @size_eq_one_iff
 
 /-! ## L[i] and L[i]? -/
 
-@[simp] theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
-  by_cases h : i < xs.size
-  · simp [getElem?_pos, h]
-  · rw [getElem?_neg xs i h]
-    simp_all
+theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
+  simp
 
-@[simp] theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.size ≤ i := by
-  simp [eq_comm (a := none)]
+theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.size ≤ i := by
+  simp
 
 theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by
   simp [getElem?_eq_none_iff, h]
@@ -137,8 +130,8 @@ grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]?
 @[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
   getElem?_pos ..
 
-theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b := by
-  simp [getElem?_def]
+theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b :=
+  _root_.getElem?_eq_some_iff
 
 @[grind →]
 theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs.size, xs[i] = a :=
@@ -147,13 +140,13 @@ theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs
 theorem some_eq_getElem?_iff {xs : Array α} : some b = xs[i]? ↔ ∃ h : i < xs.size, xs[i] = b := by
   rw [eq_comm, getElem?_eq_some_iff]
 
-@[simp] theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
+theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
     (some xs[i] = xs[i]?) ↔ True := by
-  simp [h]
+  simp
 
-@[simp] theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
+theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
     (xs[i]? = some xs[i]) ↔ True := by
-  simp [h]
+  simp
 
 theorem getElem_eq_iff {xs : Array α} {i : Nat} {h : i < xs.size} : xs[i] = x ↔ xs[i]? = some x := by
   simp only [getElem?_eq_some_iff]
@@ -189,16 +182,15 @@ theorem getElem_push {xs : Array α} {x : α} {i : Nat} (h : i < (xs.push x).siz
   · simp at h
     simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
 
-theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]? := by
+@[grind =] theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]? := by
   simp [getElem?_def, getElem_push]
   (repeat' split) <;> first | rfl | omega
 
-@[simp] theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
-  simp [getElem?_push]
+theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
+  simp
 
-@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a :=
-  match i, h with
-  | 0, _ => rfl
+theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a := by
+  simp
 
 @[grind]
 theorem getElem?_singleton {a : α} {i : Nat} : #[a][i]? = if i = 0 then some a else none := by
@@ -245,6 +237,8 @@ theorem back?_pop {xs : Array α} :
 
 /-! ### push -/
 
+@[simp] theorem push_empty : #[].push x = #[x] := rfl
+
 @[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by
   cases xs
   simp
@@ -424,8 +418,7 @@ theorem eq_empty_iff_forall_not_mem {xs : Array α} : xs = #[] ↔ ∀ a, a ∉
 theorem eq_of_mem_singleton (h : a ∈ #[b]) : a = b := by
   simpa using h
 
-@[simp] theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b :=
-  ⟨eq_of_mem_singleton, (by simp [·])⟩
+theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b := by simp
 
 theorem forall_mem_push {p : α → Prop} {xs : Array α} {a : α} :
     (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by
@@ -610,13 +603,13 @@ theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {st
 
 -- Auxiliary for `any_iff_exists`.
 theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
-    anyM.loop (m := Id) p as stop h start = true ↔
+    (anyM.loop (m := Id) (pure <| p ·) as stop h start).run = true ↔
       ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true := by
   unfold anyM.loop
   split <;> rename_i h₁
   · dsimp
     split <;> rename_i h₂
-    · simp only [true_iff]
+    · simp only [true_iff, Id.run_pure]
       refine ⟨start, by omega, by omega, by omega, h₂⟩
     · rw [anyM_loop_iff_exists]
       constructor
@@ -633,9 +626,9 @@ termination_by stop - start
 -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
 theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
     as.any p start stop ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] := by
-  dsimp [any, anyM, Id.run]
+  dsimp [any, anyM]
   split
-  · rw [anyM_loop_iff_exists]
+  · rw [anyM_loop_iff_exists (p := p)]
   · rw [anyM_loop_iff_exists]
     constructor
     · rintro ⟨i, hi, ge, _, h⟩
@@ -852,7 +845,7 @@ abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
     elem a xs = xs.contains a := by
   simp [elem]
 
-@[grind] theorem contains_empty [BEq α] : (#[] : Array α).contains a = false := rfl
+@[grind] theorem contains_empty [BEq α] : (#[] : Array α).contains a = false := by simp
 
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     elem a xs = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
@@ -869,8 +862,8 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
 @[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = decide (a ∈ xs) := by rw [← elem_eq_contains, elem_eq_mem]
 
-@[simp, grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := rfl
-@[simp, grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := rfl
+@[grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp
+@[grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp
 
 /-- Variant of `any_push` with a side condition on `stop`. -/
 @[simp, grind] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
@@ -1229,7 +1222,7 @@ where
 @[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
   rw [mapM, mapM.map]; rfl
 
-@[simp, grind] theorem map_empty {f : α → β} : map f #[] = #[] := mapM_empty f
+@[grind] theorem map_empty {f : α → β} : map f #[] = #[] := by simp
 
 @[simp, grind] theorem map_push {f : α → β} {as : Array α} {x : α} :
     (as.push x).map f = (as.map f).push (f x) := by
@@ -1367,17 +1360,17 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar
 
 @[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
 theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} :
-    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun acc a => acc.push (f a)) b := by
+    mapM.map (m := Id) (pure <| f ·) as i b = pure (as.foldl (start := i) (fun acc a => acc.push (f a)) b) := by
   unfold mapM.map
   split <;> rename_i h
-  · simp only [Id.bind_eq]
-    dsimp [foldl, Id.run, foldlM]
+  · ext : 1
+    dsimp [foldl, foldlM]
     rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
     -- Calling `split` here gives a bad goal.
     have : size as - i = Nat.succ (size as - i - 1) := by omega
     rw [this]
-    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
-  · dsimp [foldl, Id.run, foldlM]
+    simp [foldl, foldlM, Nat.sub_add_eq]
+  · dsimp [foldl, foldlM]
     rw [dif_pos (by omega), foldlM.loop, dif_neg h]
     rfl
 termination_by as.size - i
@@ -1599,8 +1592,8 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
     as.toList ++ List.filterMap f xs := ?_
   exact this #[]
   induction xs
-  · simp_all [Id.run]
-  · simp_all [Id.run, List.filterMap_cons]
+  · simp_all
+  · simp_all [List.filterMap_cons]
     split <;> simp_all
 
 @[grind] theorem toList_filterMap {f : α → Option β} {xs : Array α} :
@@ -1814,7 +1807,8 @@ theorem toArray_append {xs : List α} {ys : Array α} :
 
 theorem singleton_eq_toArray_singleton {a : α} : #[a] = [a].toArray := rfl
 
-@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
+@[deprecated empty_append (since := "2025-05-26")]
+theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
   funext ⟨l⟩
   simp
 
@@ -1965,8 +1959,8 @@ theorem append_left_inj {xs₁ xs₂ : Array α} (ys) : xs₁ ++ ys = xs₂ ++ y
 theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ∧ ys = #[] :=
   append_eq_empty_iff.mp h
 
-@[simp] theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by
-  rw [eq_comm, append_eq_empty_iff]
+theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by
+  simp
 
 theorem append_ne_empty_of_left_ne_empty {xs ys : Array α} (h : xs ≠ #[]) : xs ++ ys ≠ #[] := by
   simp_all
@@ -2034,7 +2028,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
   simp only [List.append_toArray, List.set_toArray, List.set_append]
   split <;> simp
 
-@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) :
+@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size)  :
     (xs ++ ys).set i x (by simp; omega) = xs.set i x ++ ys := by
   simp [set_append, h]
 
@@ -2109,14 +2103,13 @@ theorem append_eq_map_iff {f : α → β} :
   | nil => simp
   | cons as => induction as.toList <;> simp [*]
 
-@[simp] theorem flatten_map_toArray {L : List (List α)} :
-    (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
+@[simp] theorem flatten_toArray_map {L : List (List α)} :
+    (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
   apply ext'
   simp [Function.comp_def]
 
-@[simp] theorem flatten_toArray_map {L : List (List α)} :
-    (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
-  rw [← flatten_map_toArray]
+theorem flatten_map_toArray {L : List (List α)} :
+    (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   simp
 
 -- We set this to lower priority so that `flatten_toArray_map` is applied first when relevant.
@@ -2144,8 +2137,8 @@ theorem mem_flatten : ∀ {xss : Array (Array α)}, a ∈ xss.flatten ↔ ∃ xs
   induction xss using array₂_induction
   simp
 
-@[simp] theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by
-  rw [eq_comm, flatten_eq_empty_iff]
+theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by
+  simp
 
 theorem flatten_ne_empty_iff {xss : Array (Array α)} : xss.flatten ≠ #[] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ #[] := by
   simp
@@ -2285,15 +2278,9 @@ theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
       rw [List.map_inj_right]
       simp +contextual
 
-@[simp] theorem flatten_toArray_map_toArray {xss : List (List α)} :
+theorem flatten_toArray_map_toArray {xss : List (List α)} :
     (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
-  simp [flatten]
-  suffices ∀ as, List.foldl (fun acc bs => acc ++ bs) as (List.map List.toArray xss) = as ++ xss.flatten.toArray by
-    simpa using this #[]
-  intro as
-  induction xss generalizing as with
-  | nil => simp
-  | cons xs xss ih => simp [ih]
+  simp
 
 /-! ### flatMap -/
 
@@ -2323,13 +2310,9 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α}
   intro cs
   induction as generalizing cs <;> simp_all
 
-@[simp, grind =] theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
+theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
-  induction as with
-  | nil => simp
-  | cons a as ih =>
-    apply ext'
-    simp [ih, flatMap_toArray_cons]
+  simp
 
 @[simp] theorem flatMap_id {xss : Array (Array α)} : xss.flatMap id = xss.flatten := by simp [flatMap_def]
 
@@ -2795,7 +2778,7 @@ theorem reverse_eq_iff {xs ys : Array α} : xs.reverse = ys ↔ xs = ys.reverse
   cases xs
   simp
 
-@[grind _=_]theorem filterMap_reverse {f : α → Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
+@[grind _=_] theorem filterMap_reverse {f : α → Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
   cases xs
   simp
 
@@ -3031,19 +3014,21 @@ theorem take_size {xs : Array α} : xs.take xs.size = xs := by
   | succ n ih =>
     simp [shrink.loop, ih]
 
-@[simp] theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by
+-- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`.
+theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by
   simp [shrink]
   omega
 
-@[simp] theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) :
-    (xs.shrink i)[j] = xs[j]'(by simp at h; omega) := by
+-- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`.
+theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) :
+    (xs.shrink i)[j] = xs[j]'(by simp [size_shrink] at h; omega) := by
   simp [shrink]
 
-@[simp] theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
-  apply List.ext_getElem <;> simp
-
 @[simp] theorem shrink_eq_take {xs : Array α} {i : Nat} : xs.shrink i = xs.take i := by
-  ext <;> simp
+  ext <;> simp [size_shrink, getElem_shrink]
+
+theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
+  simp
 
 /-! ### foldlM and foldrM -/
 
@@ -3212,18 +3197,16 @@ theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Array α} {a : α} {f : β
   rw [foldr, foldrM_start_stop, ← foldrM_toList, List.foldrM_pure, foldr_toList, foldr, ← foldrM_start_stop]
 
 theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop : Nat} :
-    xs.foldl f b start stop = xs.foldlM (m := Id) f b start stop := by
-  simp [foldl, Id.run]
+    xs.foldl f b start stop = (xs.foldlM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} :
-    xs.foldr f b start stop = xs.foldrM (m := Id) f b start stop := by
-  simp [foldr, Id.run]
+    xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
 @[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Array α} {start stop : Nat} :
-    Id.run (xs.foldlM f b start stop) = xs.foldl f b start stop := foldl_eq_foldlM.symm
+    Id.run (xs.foldlM f b start stop) = xs.foldl (f · · |>.run) b start stop := rfl
 
 @[simp] theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Array α} {start stop : Nat} :
-    Id.run (xs.foldrM f b start stop) = xs.foldr f b start stop := foldr_eq_foldrM.symm
+    Id.run (xs.foldrM f b start stop) = xs.foldr (f · · |>.run) b start stop := rfl
 
 /-- Variant of `foldlM_reverse` with a side condition for the `stop` argument. -/
 @[simp] theorem foldlM_reverse' [Monad m] {xs : Array α} {f : β → α → m β} {b} {stop : Nat}
@@ -3252,7 +3235,7 @@ theorem foldrM_reverse [Monad m] {xs : Array α} {f : α → β → m β} {b} :
 
 theorem foldrM_push [Monad m] {f : α → β → m β} {init : β} {xs : Array α} {a : α} :
     (xs.push a).foldrM f init = f a init >>= xs.foldrM f := by
-  simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
+  simp only [foldrM_eq_reverse_foldlM_toList, toList_push, List.reverse_append, List.reverse_cons,
     List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
 
 /--
@@ -3264,6 +3247,22 @@ rather than `(arr.push a).size` as the argument.
     (xs.push a).foldrM f init start = f a init >>= xs.foldrM f := by
   simp [← foldrM_push, h]
 
+@[simp, grind] theorem _root_.List.foldrM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
+    l.foldrM (fun x xs => xs.push <$> f x) xs = do return xs ++ (← l.reverse.mapM f).toArray := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [ih]
+    congr 1
+    funext l'
+    congr 1
+    funext x
+    simp
+
+@[simp, grind] theorem _root_.List.foldlM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
+    l.foldlM (fun xs x => xs.push <$> f x) xs = do return xs ++ (← l.mapM f).toArray := by
+  induction l generalizing xs <;> simp [*]
+
 /-! ### foldl / foldr -/
 
 @[grind] theorem foldl_empty {f : β → α → β} {init : β} : (#[].foldl f init) = init := rfl
@@ -3360,6 +3359,32 @@ rather than `(arr.push a).size` as the argument.
   rcases as with ⟨as⟩
   simp
 
+@[simp, grind] theorem _root_.List.foldr_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
+    l.foldr (fun x xs => xs.push (f x)) xs = xs ++ (l.reverse.map f).toArray := by
+  induction l <;> simp [*]
+
+/-- Variant of `List.foldr_push_eq_append` specialized to `f = id`. -/
+@[simp, grind] theorem _root_.List.foldr_push_eq_append' {l : List α} {xs : Array α} :
+    l.foldr (fun x xs => xs.push x) xs = xs ++ l.reverse.toArray := by
+  induction l <;> simp [*]
+
+@[simp, grind] theorem _root_.List.foldl_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
+    l.foldl (fun xs x => xs.push (f x)) xs = xs ++ (l.map f).toArray := by
+  induction l generalizing xs <;> simp [*]
+
+/-- Variant of `List.foldl_push_eq_append` specialized to `f = id`. -/
+@[simp, grind] theorem _root_.List.foldl_push_eq_append' {l : List α} {xs : Array α} :
+    l.foldl (fun xs x => xs.push x) xs = xs ++ l.toArray := by
+  simpa using List.foldl_push_eq_append (f := id)
+
+@[deprecated _root_.List.foldl_push_eq_append' (since := "2025-05-18")]
+theorem _root_.List.foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
+  induction l generalizing as <;> simp [*]
+
+@[deprecated _root_.List.foldr_push_eq_append' (since := "2025-05-18")]
+theorem _root_.List.foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
+  rw [List.foldr_eq_foldl_reverse, List.foldl_push_eq_append']
+
 @[simp, grind] theorem foldr_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldr (f · ++ ·) ys = (xs.map f).flatten ++ ys := by
   rcases xs with ⟨xs⟩
@@ -3481,17 +3506,16 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
 
 @[simp] theorem foldr_append' {f : α → β → β} {b} {xs ys : Array α} {start : Nat}
     (w : start = xs.size + ys.size) :
-    (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) := by
-  subst w
-  simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) :=
+  foldrM_append' w
 
-@[grind _=_]theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
-    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by
-  simp [foldl_eq_foldlM]
+@[grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
+    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) :=
+  foldlM_append
 
 @[grind _=_] theorem foldr_append {f : α → β → β} {b} {xs ys : Array α} :
-    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by
-  simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) :=
+  foldrM_append
 
 @[simp] theorem foldl_flatten' {f : β → α → β} {b} {xss : Array (Array α)} {stop : Nat}
     (w : stop = xss.flatten.size) :
@@ -3520,21 +3544,22 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
 /-- Variant of `foldl_reverse` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_reverse' {xs : Array α} {f : β → α → β} {b} {stop : Nat}
     (w : stop = xs.size) :
-    xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b := by
-  simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b :=
+  foldlM_reverse' w
 
 /-- Variant of `foldr_reverse` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_reverse' {xs : Array α} {f : α → β → β} {b} {start : Nat}
     (w : start = xs.size) :
-    xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b := by
-  simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b :=
+  foldrM_reverse' w
 
 @[grind] theorem foldl_reverse {xs : Array α} {f : β → α → β} {b} :
-    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b :=
+  foldlM_reverse
 
 @[grind] theorem foldr_reverse {xs : Array α} {f : α → β → β} {b} :
     xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
-  (foldl_reverse ..).symm.trans <| by simp
+  foldrM_reverse
 
 theorem foldl_eq_foldr_reverse {xs : Array α} {f : β → α → β} {b} :
     xs.foldl f b = xs.reverse.foldr (fun x y => f y x) b := by simp
@@ -3615,7 +3640,7 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} {r : β
 theorem back?_eq_some_iff {xs : Array α} {a : α} :
     xs.back? = some a ↔ ∃ ys : Array α, xs = ys.push a := by
   rcases xs with ⟨xs⟩
-  simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, push_toList]
+  simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, toList_push]
   constructor
   · rintro ⟨ys, rfl⟩
     exact ⟨ys.toArray, by simp⟩
@@ -3740,7 +3765,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp [List.contains_iff_exists_mem_beq]
 
-@[grind]
+@[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp
@@ -4049,15 +4074,16 @@ abbrev all_mkArray := @all_replicate
 /-! ### modify -/
 
 @[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
-  unfold modify modifyM Id.run
+  unfold modify modifyM
   split <;> simp
 
 theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
     (xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
-  simp only [modify, modifyM, Id.run, Id.pure_eq]
+  simp only [modify, modifyM]
   split
-  · simp only [Id.bind_eq, getElem_set]; split <;> simp [*]
-  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
+  · simp only [getElem_set, Id.run_pure, Id.run_bind]; split <;> simp [*]
+  · simp only [Id.run_pure]
+    rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
 @[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
     (xs.modify i f).toList = xs.toList.modify i f := by
@@ -4152,7 +4178,7 @@ theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
 section replace
 variable [BEq α]
 
-@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by rfl
+@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by simp [replace]
 
 @[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
   simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]
@@ -4385,7 +4411,8 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
 
 /-! # mem -/
 
-@[simp, grind =] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
+@[deprecated mem_toList_iff (since := "2025-05-26")]
+theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
 
 @[deprecated not_mem_empty (since := "2025-03-25")]
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
@@ -4434,7 +4461,7 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
   simp
 
 @[simp, grind =] theorem forIn'_toList [Monad m] {xs : Array α} {b : β} {f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)} :
-    forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList.mpr m) b) := by
+    forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList_iff.mpr m) b) := by
   cases xs
   simp
 
@@ -4531,8 +4558,8 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 
 theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by simp
 
-@[simp, grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
-  apply Array.ext <;> simp
+@[grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
+  simp
 
 @[simp, grind =] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by
@@ -4598,12 +4625,12 @@ namespace Array
 @[simp] theorem findSomeRev?_eq_findSome?_reverse {f : α → Option β} {xs : Array α} :
     xs.findSomeRev? f = xs.reverse.findSome? f := by
   cases xs
-  simp [findSomeRev?, Id.run]
+  simp [findSomeRev?]
 
 @[simp] theorem findRev?_eq_find?_reverse {f : α → Bool} {xs : Array α} :
     xs.findRev? f = xs.reverse.find? f := by
   cases xs
-  simp [findRev?, Id.run]
+  simp [findRev?]
 
 /-! ### unzip -/
 

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

@@ -6,6 +6,7 @@ Author: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Lex.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
 
@@ -22,22 +23,18 @@ namespace Array
 @[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
-protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
-    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
+    ¬ xs ≤ ys ↔ ys < xs :=
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  simp [lex, Id.run]
-
-@[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
-  simp only [lex, List.getElem_toArray, List.getElem_singleton]
-  cases lt a b <;> cases a != b <;> simp [Id.run]
+  simp [lex]
 
 private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
-  simp only [lex, Id.run]
+  simp only [lex]
   simp only [Std.Range.forIn'_eq_forIn'_range', size_append, List.size_toArray, List.length_singleton,
     Nat.add_comm 1]
   simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left,
@@ -50,13 +47,16 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
 @[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
-  | nil => cases l₂ <;> simp [lex, Id.run]
+  | nil => cases l₂ <;> simp [lex]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Id.run]
+    | nil => simp [lex]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
+theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
+  simp
+
 @[simp, grind =] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
     xs.toList.lex ys.toList lt = xs.lex ys lt := by
   cases xs <;> cases ys <;> simp

src/Init/Data/Array/MapIdx.lean

@@ -6,10 +6,11 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.Array.OfFn
-import Init.Data.List.MapIdx
+import all Init.Data.List.MapIdx
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -26,7 +27,7 @@ theorem mapFinIdx_induction (xs : Array α) (f : (i : Nat) → α → (h : i < x
     motive xs.size ∧ ∃ eq : (Array.mapFinIdx xs f).size = xs.size,
       ∀ i h, p i ((Array.mapFinIdx xs f)[i]) h := by
   let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) :
-    let as : Array β := Array.mapFinIdxM.map (m := Id) xs f i j h bs
+    let as : Array β := Id.run <| Array.mapFinIdxM.map xs (pure <| f · · ·) i j h bs
     motive xs.size ∧ ∃ eq : as.size = xs.size, ∀ i h, p i as[i] h := by
     induction i generalizing j bs with simp [mapFinIdxM.map]
     | zero =>

src/Init/Data/Array/Monadic.lean

@@ -6,6 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.List.Control
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.List.Monadic
@@ -23,15 +25,29 @@ open Nat
 
 /-! ## Monadic operations -/
 
+theorem map_toList_inj [Monad m] [LawfulMonad m]
+    {xs : m (Array α)} {ys : m (Array α)} :
+   toList <$> xs = toList <$> ys ↔ xs = ys := by
+  simp
+
 /-! ### mapM -/
 
 @[simp] theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Array α} {f : α → β} :
     xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
   induction xs; simp_all
 
-@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
+@[simp] theorem idRun_mapM {xs : Array α} {f : α → Id β} : (xs.mapM f).run = xs.map (f · |>.run) :=
   mapM_pure
 
+@[deprecated idRun_mapM (since := "2025-05-21")]
+theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
+  mapM_pure
+
+@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {xs : Array α} :
+    (xs.map f).mapM g = xs.mapM (g ∘ f) := by
+  rcases xs with ⟨xs⟩
+  simp
+
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {xs ys : Array α} :
     (xs ++ ys).mapM f = (return (← xs.mapM f) ++ (← ys.mapM f)) := by
   rcases xs with ⟨xs⟩
@@ -179,12 +195,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
 
-@[simp] theorem forIn'_yield_eq_foldl
+theorem idRun_forIn'_yield_eq_foldl
+    {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
+    (forIn' xs init (fun a m b => .yield <$> f a m b)).run =
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := by
+  simp
+
+@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
     {xs : Array α} (f : (a : α) → a ∈ xs → β → β) (init : β) :
     forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
-      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
-  rcases xs with ⟨xs⟩
-  simp [List.foldl_map]
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {xs : Array α} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
@@ -221,12 +243,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
 
-@[simp] theorem forIn_yield_eq_foldl
+theorem idRun_forIn_yield_eq_foldl
+    {xs : Array α} (f : α → β → Id β) (init : β) :
+    (forIn xs init (fun a b => .yield <$> f a b)).run =
+      xs.foldl (fun b a => f a b |>.run) init := by
+  simp
+
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
     {xs : Array α} (f : α → β → β) (init : β) :
     forIn (m := Id) xs init (fun a b => .yield (f a b)) =
-      xs.foldl (fun b a => f a b) init := by
-  rcases xs with ⟨xs⟩
-  simp [List.foldl_map]
+      xs.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)} :

src/Init/Data/Array/OfFn.lean

@@ -6,8 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
+import Init.Data.Array.Monadic
 import Init.Data.List.OfFn
+import Init.Data.List.FinRange
 
 /-!
 # Theorems about `Array.ofFn`
@@ -18,6 +21,8 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
+/-! ### ofFn -/
+
 @[simp] theorem ofFn_zero {f : Fin 0 → α} : ofFn f = #[] := by
   simp [ofFn, ofFn.go]
 
@@ -25,12 +30,17 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
   ext i h₁ h₂
   · simp
-  · simp [getElem_push]
-    split <;> rename_i h₃
-    · rfl
-    · congr
-      simp at h₁ h₂
-      omega
+  · simp only [getElem_ofFn, getElem_push, size_ofFn, Fin.castSucc_mk, left_eq_dite_iff,
+      Nat.not_lt]
+    simp only [size_ofFn] at h₁
+    intro h₃
+    simp only [show i = n by omega]
+
+theorem ofFn_add {n m} {f : Fin (n + m) → α} :
+    ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
+  induction m with
+  | zero => simp
+  | succ m ih => simp [ofFn_succ, ih]
 
 @[simp] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
   ext <;> simp
@@ -38,6 +48,11 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
 @[simp] theorem toList_ofFn {f : Fin n → α} : (Array.ofFn f).toList = List.ofFn f := by
   apply List.ext_getElem <;> simp
 
+theorem ofFn_succ' {f : Fin (n+1) → α} :
+    ofFn f = #[f 0] ++ ofFn (fun i => f i.succ) := by
+  apply Array.toList_inj.mp
+  simp [List.ofFn_succ]
+
 @[simp]
 theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
   rw [← Array.toList_inj]
@@ -52,4 +67,70 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
+/-! ### ofFnM -/
+
+/-- Construct (in a monadic context) an array by applying a monadic function to each index. -/
+def ofFnM {n} [Monad m] (f : Fin n → m α) : m (Array α) :=
+  Fin.foldlM n (fun xs i => xs.push <$> f i) (Array.emptyWithCapacity n)
+
+@[simp]
+theorem ofFnM_zero [Monad m] {f : Fin 0 → m α} : ofFnM f = pure #[] := by
+  simp [ofFnM]
+
+theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
+    ofFnM f = (do
+      let a ← f 0
+      let as ← ofFnM fun i => f i.succ
+      pure (#[a] ++ as)) := by
+  simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
+
+theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
+    ofFnM f = (do
+      let as ← ofFnM fun i => f i.castSucc
+      let a  ← f (Fin.last n)
+      pure (as.push a)) := by
+  simp [ofFnM, Fin.foldlM_succ_last]
+
+theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
+    ofFnM f = (do
+      let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))
+      let bs ← ofFnM fun i : Fin k => f (i.natAdd n)
+      pure (as ++ bs)) := by
+  induction k with
+  | zero => simp
+  | succ k ih =>
+    simp only [ofFnM_succ, Nat.add_eq, ih, Fin.castSucc_castLE, Fin.castSucc_natAdd, bind_pure_comp,
+      bind_assoc, bind_map_left, Fin.natAdd_last, map_bind, Functor.map_map]
+    congr 1
+    funext xs
+    congr 1
+    funext ys
+    congr 1
+    funext x
+    simp
+
+@[simp] theorem toList_ofFnM [Monad m] [LawfulMonad m] {f : Fin n → m α} :
+    toList <$> ofFnM f = List.ofFnM f := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp [ofFnM_succ, List.ofFnM_succ_last, ← ih]
+
+@[simp]
+theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
+    ofFnM (pure ∘ f) = (pure (ofFn f) : m (Array α)) := by
+  apply Array.map_toList_inj.mp
+  simp
+
+-- Variant of `ofFnM_pure_comp` using a lambda.
+-- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
+theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
+    ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (Array α)) :=
+  ofFnM_pure_comp
+
+@[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
+    Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp [ofFnM_succ', ofFn_succ', ih]
+
 end Array

src/Init/Data/Array/Perm.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.List.Nat.Perm
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.

src/Init/Data/Array/QSort/Basic.lean

@@ -27,23 +27,27 @@ Internal implementation of `Array.qsort`.
 
 It does so by first swapping the elements at indices `lo`, `mid := (lo + hi) / 2`, and `hi`
 if necessary so that the middle (pivot) element is at index `hi`.
-We then iterate from `j = lo` to `j = hi`, with a pointer `i` starting at `lo`, and
+We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
 swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
 -/
-def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
-    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m < n} × Vector α n :=
+def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w : lo ≤ hi := by omega)
+    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m ≤ hi} × Vector α n :=
   let mid := (lo + hi) / 2
   let as  := if lt as[mid] as[lo] then as.swap lo mid else as
   let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
   let as  := if lt as[mid] as[hi] then as.swap mid hi else as
   let pivot := as[hi]
-  let rec loop (as : Vector α n) (i j : Nat)
-      (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
-    if h : j < hi then
-      if lt as[j] pivot then
-        loop (as.swap i j) (i+1) (j+1)
+  -- During this loop, elements below in `[lo, i)` are less than `pivot`,
+  -- elements in `[i, k)` are greater than or equal to `pivot`,
+  -- elements in `[k, hi)` are unexamined,
+  -- while `as[hi]` is (by definition) the pivot.
+  let rec loop (as : Vector α n) (i k : Nat)
+      (ilo : lo ≤ i := by omega) (ik : i ≤ k := by omega) (w : k ≤ hi := by omega) :=
+    if h : k < hi then
+      if lt as[k] pivot then
+        loop (as.swap i k) (i+1) (k+1)
       else
-        loop as i (j+1)
+        loop as i (k+1)
     else
       (⟨i, ilo, by omega⟩, as.swap i hi)
   loop as lo lo
@@ -51,25 +55,28 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
 /--
 In-place quicksort.
 
-`qsort as lt low high` sorts the subarray `as[low:high+1]` in-place using `lt` to compare elements.
+`qsort as lt lo hi` sorts the subarray `as[lo:hi+1]` in-place using `lt` to compare elements.
 -/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
-    (low := 0) (high := as.size - 1) : Array α :=
-  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
+    (lo := 0) (hi := as.size - 1) : Array α :=
+  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat) (w : lo ≤ hi := by omega)
       (hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
     if h₁ : lo < hi then
       let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
       if h₂ : mid ≥ hi then
+        -- This only occurs when `hi ≤ lo`,
+        -- and thus `as[lo:hi+1]` is trivially already sorted.
         as
       else
+        -- Otherwise, we recursively sort the two subarrays.
         sort (sort as lo mid) (mid+1) hi
     else as
   if h : as.size = 0 then
     as
   else
-    let low := min low (as.size - 1)
-    let high := min high (as.size - 1)
-    sort as.toVector low high |>.toArray
+    let lo := min lo (as.size - 1)
+    let hi := max lo (min hi (as.size - 1))
+    sort as.toVector lo hi |>.toArray
 
 set_option linter.unusedVariables.funArgs false in
 /--

src/Init/Data/Array/Range.lean

@@ -7,7 +7,8 @@ module
 
 prelude
 import Init.Data.Array.Lemmas
-import Init.Data.Array.OfFn
+import all Init.Data.Array.Basic
+import all Init.Data.Array.OfFn
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Zip
 import Init.Data.List.Nat.Range
@@ -80,7 +81,7 @@ theorem range'_append {s m n step : Nat} :
     range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
 
 theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ #[s + step * n] := by
-  simpa using range'_append.symm
+  simp [← range'_append]
 
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #[s + n] := by
   simp [range'_concat]

src/Init/Data/Array/Subarray.lean

@@ -290,7 +290,7 @@ Examples:
 -/
 @[inline]
 def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
-  Id.run <| as.foldlM f (init := init)
+  Id.run <| as.foldlM (pure <| f · ·) (init := init)
 
 /--
 Folds an operation from right to left over the elements in a subarray.
@@ -304,7 +304,7 @@ Examples:
 -/
 @[inline]
 def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β :=
-  Id.run <| as.foldrM f (init := init)
+  Id.run <| as.foldrM (pure <| f · ·) (init := init)
 
 /--
 Checks whether any of the elements in a subarray satisfy a Boolean predicate.
@@ -314,7 +314,7 @@ an element that satisfies the predicate is found.
 -/
 @[inline]
 def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
-  Id.run <| as.anyM p
+  Id.run <| as.anyM (pure <| p ·)
 
 /--
 Checks whether all of the elements in a subarray satisfy a Boolean predicate.
@@ -324,7 +324,7 @@ an element that does not satisfy the predicate is found.
 -/
 @[inline]
 def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
-  Id.run <| as.allM p
+  Id.run <| as.allM (pure <| p ·)
 
 /--
 Applies a monadic function to each element in a subarray in reverse order, stopping at the first
@@ -394,7 +394,7 @@ Examples:
 -/
 @[inline]
 def findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α :=
-  Id.run <| as.findRevM? p
+  Id.run <| as.findRevM? (pure <| p ·)
 
 end Subarray
 

src/Init/Data/Array/Subarray/Split.lean

@@ -8,7 +8,7 @@ module
 
 prelude
 import Init.Data.Array.Basic
-import Init.Data.Array.Subarray
+import all Init.Data.Array.Subarray
 import Init.Omega
 
 /-

src/Init/Data/Array/TakeDrop.lean

@@ -6,6 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop
 

src/Init/Data/Array/Zip.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.TakeDrop
 import Init.Data.List.Zip
 
@@ -333,11 +334,13 @@ abbrev zipWithAll_mkArray := @zipWithAll_replicate
 
 /-! ### unzip -/
 
-@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
-  induction l <;> simp_all
+@[deprecated fst_unzip (since := "2025-05-26")]
+theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
+  simp
 
-@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
-  induction l <;> simp_all
+@[deprecated snd_unzip (since := "2025-05-26")]
+theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
+  simp
 
 theorem unzip_eq_map {xs : Array (α × β)} : unzip xs = (xs.map Prod.fst, xs.map Prod.snd) := by
   cases xs
@@ -370,7 +373,7 @@ theorem unzip_zip {as : Array α} {bs : Array β} (h : as.size = bs.size) :
 
 theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl : xs.map Prod.fst = as)
     (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
-  rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
+  rw [← hl, ← hr, ← zip_unzip xs, ← fst_unzip, ← snd_unzip, zip_unzip, zip_unzip]
 
 @[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by

src/Init/Data/BitVec/BasicAux.lean

@@ -22,7 +22,7 @@ section Nat
 /--
 The bitvector with value `i mod 2^n`.
 -/
-@[match_pattern]
+@[expose, match_pattern]
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
   toFin := Fin.ofNat' (2^n) i
 

src/Init/Data/BitVec/Bitblast.lean

@@ -7,9 +7,11 @@ module
 
 prelude
 import Init.Data.BitVec.Folds
+import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Mod
+import all Init.Data.Int.DivMod
 import Init.Data.Int.LemmasAux
-import Init.Data.BitVec.Lemmas
+import all Init.Data.BitVec.Lemmas
 
 /-!
 # Bit blasting of bitvectors

src/Init/Data/BitVec/Folds.lean

@@ -6,6 +6,7 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
+import all Init.Data.BitVec.Basic
 import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate

src/Init/Data/BitVec/Lemmas.lean

@@ -8,7 +8,8 @@ module
 
 prelude
 import Init.Data.Bool
-import Init.Data.BitVec.Basic
+import all Init.Data.BitVec.Basic
+import all Init.Data.BitVec.BasicAux
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Div.Lemmas
@@ -67,11 +68,11 @@ theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w :=
 @[simp] theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n] := by
   simp only [getElem?_def, h, ↓reduceDIte]
 
-theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a := by
-  simp only [getElem?_def]
-  split
-  · simp_all
-  · simp; omega
+theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a :=
+  _root_.getElem?_eq_some_iff
+
+theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? ↔ ∃ h : n < w, l[n] = a :=
+  _root_.some_eq_getElem?_iff
 
 theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
   getElem?_eq_some_iff.mp
@@ -80,11 +81,11 @@ set_option linter.missingDocs false in
 @[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
 abbrev getElem?_eq_some := @getElem?_eq_some_iff
 
-@[simp] theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
-  simp only [getElem?_def]
-  split
-  · simp_all
-  · simp; omega
+theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
+  simp
+
+theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by
+  simp
 
 theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
@@ -92,13 +93,13 @@ theorem getElem?_eq (l : BitVec w) (i : Nat) :
     l[i]? = if h : i < w then some l[i] else none := by
   split <;> simp_all
 
-@[simp] theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
+theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
     (some l[i] = l[i]?) ↔ True := by
-  simp [h]
+  simp
 
-@[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
+theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
     (l[i]? = some l[i]) ↔ True := by
-  simp [h]
+  simp
 
 theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x := by
   simp only [getElem?_eq_some_iff]
@@ -343,7 +344,7 @@ theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
   cases b <;> rfl
 
 @[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
-  cases b <;> rfl
+  cases b <;> simp
 
 @[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
   cases b <;> rfl
@@ -504,7 +505,7 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-@[simp] theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
+theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
 
 @[simp]
 theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
@@ -1972,7 +1973,7 @@ theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
 /-! ### shiftLeft reductions from BitVec to Nat -/
 
 @[simp]
-theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := by rfl
+theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := rfl
 
 theorem shiftLeft_zero' {x : BitVec w₁} : x <<< 0#w₂ = x := by simp
 
@@ -2132,7 +2133,7 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
 
 @[simp]
 theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :
-    x >>> y = x >>> y.toNat := by rfl
+    x >>> y = x >>> y.toNat := rfl
 
 theorem ushiftRight_ofNat_eq {x : BitVec w} {k : Nat} : x >>> (BitVec.ofNat w k) = x >>> (k % 2^w) := rfl
 
@@ -2260,7 +2261,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
-  simp [getElem_sshiftRight, getLsbD_sshiftRight, Nat.add_assoc]
+  simp only [getElem_sshiftRight, Nat.add_assoc, msb_sshiftRight, dite_eq_ite]
   by_cases h₂ : n + i < w
   · simp [h₂]
   · simp only [h₂, ↓reduceIte]
@@ -3178,12 +3179,12 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
   · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
-@[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
-  simp [getElem_concat]
-
 @[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
   simp [getElem_concat]
 
+theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
+  simp
+
 @[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by
   simp [getLsbD_concat]
 
@@ -3372,7 +3373,7 @@ theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b := by
 
 /-! ### sub/neg -/
 
-theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
+theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := rfl
 
 @[simp] theorem toNat_sub {n} (x y : BitVec n) :
     (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
@@ -3683,7 +3684,7 @@ theorem fill_false {w : Nat} : fill w false = 0#w := by
 
 /-! ### mul -/
 
-theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
+theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := rfl
 
 @[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
 @[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
@@ -3731,6 +3732,10 @@ theorem mul_add {x y z : BitVec w} :
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
+theorem add_mul {x y z : BitVec w} :
+    (x + y) * z = x * z + y * z := by
+  rw [BitVec.mul_comm, mul_add, BitVec.mul_comm z, BitVec.mul_comm z]
+
 theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add]
 theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
 
@@ -4162,7 +4167,7 @@ theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
   have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
   rcases hx with rfl | rfl <;>
     rcases hy with rfl | rfl <;>
-      rfl
+      simp
 
 @[simp]
 theorem sdiv_self {x : BitVec w} :
@@ -5345,7 +5350,7 @@ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
 
 /-! ### abs -/
 
-theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
+theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := rfl
 
 @[simp, bitvec_to_nat]
 theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by

src/Init/Data/Bool.lean

@@ -432,7 +432,7 @@ theorem and_or_inj_left_iff :
 /--
 Converts `true` to `1` and `false` to `0`.
 -/
-def toNat (b : Bool) : Nat := cond b 1 0
+@[expose] def toNat (b : Bool) : Nat := cond b 1 0
 
 @[simp, bitvec_to_nat] theorem toNat_false : false.toNat = 0 := rfl
 
@@ -687,7 +687,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/ByteArray/Basic.lean

@@ -9,6 +9,7 @@ prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.Subarray
 import Init.Data.UInt.Basic
+import all Init.Data.UInt.BasicAux
 import Init.Data.Option.Basic
 universe u
 
@@ -204,7 +205,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
 
 @[inline]
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 /-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
 

src/Init/Data/Cast.lean

@@ -64,7 +64,7 @@ class NatCast (R : Type u) where
 
 instance : NatCast Nat where natCast n := n
 
-@[coe, reducible, match_pattern, inherit_doc NatCast]
+@[coe, expose, reducible, match_pattern, inherit_doc NatCast]
 protected def Nat.cast {R : Type u} [NatCast R] : Nat → R :=
   NatCast.natCast
 

src/Init/Data/Char/Basic.lean

@@ -20,13 +20,13 @@ namespace Char
 /--
 One character is less than another if its code point is strictly less than the other's.
 -/
-protected def lt (a b : Char) : Prop := a.val < b.val
+@[expose] protected def lt (a b : Char) : Prop := a.val < b.val
 
 /--
 One character is less than or equal to another if its code point is less than or equal to the
 other's.
 -/
-protected def le (a b : Char) : Prop := a.val ≤ b.val
+@[expose] protected def le (a b : Char) : Prop := a.val ≤ b.val
 
 instance : LT Char := ⟨Char.lt⟩
 instance : LE Char := ⟨Char.le⟩

src/Init/Data/Char/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Char.Basic
+import all Init.Data.Char.Basic
 import Init.Data.UInt.Lemmas
 
 namespace Char

src/Init/Data/Fin/Basic.lean

@@ -8,6 +8,8 @@ module
 prelude
 import Init.Data.Nat.Bitwise.Basic
 
+@[expose] section
+
 open Nat
 
 namespace Fin
@@ -44,7 +46,7 @@ Returns `a` modulo `n` as a `Fin n`.
 
 The assumption `NeZero n` ensures that `Fin n` is nonempty.
 -/
-protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
+@[expose] protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
 
 /--

src/Init/Data/Fin/Fold.lean

@@ -100,6 +100,11 @@ Fin.foldrM n f xₙ = do
 
 /-! ### foldlM -/
 
+@[congr] theorem foldlM_congr [Monad m] {n k : Nat} (w : n = k) (f : α → Fin n → m α) :
+    foldlM n f = foldlM k (fun x i => f x (i.cast w.symm)) := by
+  subst w
+  rfl
+
 theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
     foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by
   rw [foldlM.loop, dif_pos h]
@@ -120,14 +125,49 @@ theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1)
     rw [foldlM_loop_eq, foldlM_loop_eq]
 termination_by n - i
 
-@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x :=
-  foldlM_loop_eq ..
+@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) : foldlM 0 f = pure := by
+  funext x
+  exact foldlM_loop_eq ..
 
-theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) :
-    foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
+theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) :
+    foldlM (n+1) f = fun x => f x 0 >>= foldlM n (fun x j => f x j.succ) := by
+  funext x
+  exact foldlM_loop ..
+
+/-- Variant of `foldlM_succ` that splits off `Fin.last n` rather than `0`. -/
+theorem foldlM_succ_last [Monad m] [LawfulMonad m] (f : α → Fin (n+1) → m α) :
+    foldlM (n+1) f = fun x => foldlM n (fun x j => f x j.castSucc) x >>= (f · (Fin.last n)) := by
+  funext x
+  induction n generalizing x with
+  | zero =>
+    simp [foldlM_succ]
+  | succ n ih =>
+    rw [foldlM_succ]
+    conv => rhs; rw [foldlM_succ]
+    simp only [castSucc_zero, castSucc_succ, bind_assoc]
+    congr 1
+    funext x
+    rw [ih]
+    simp
+
+theorem foldlM_add [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) :
+    foldlM (n + k) f =
+      fun x => foldlM n (fun x i => f x (i.castLE (Nat.le_add_right n k))) x >>= foldlM k (fun x i => f x (i.natAdd n)) := by
+  induction k with
+  | zero =>
+    funext x
+    simp
+  | succ k ih =>
+    funext x
+    simp [foldlM_succ_last, ← Nat.add_assoc, ih]
 
 /-! ### foldrM -/
 
+@[congr] theorem foldrM_congr [Monad m] {n k : Nat} (w : n = k) (f : Fin n → α → m α) :
+    foldrM n f = foldrM k (fun i => f (i.cast w.symm)) := by
+  subst w
+  rfl
+
 theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) :
     foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by
   rw [foldrM.loop]
@@ -145,19 +185,47 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
     conv => rhs; rw [←bind_pure (f 0 x)]
     congr
     funext
-    try simp only [foldrM.loop] -- the try makes this proof work with and without opaque wf rec
+    simp [foldrM_loop_zero]
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..
 
-@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x :=
-  foldrM_loop_zero ..
+@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) : foldrM 0 f = pure := by
+  funext x
+  exact foldrM_loop_zero ..
 
-theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
-    foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
+theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) :
+    foldrM (n+1) f = fun x => foldrM n (fun i => f i.succ) x >>= f 0 := by
+  funext x
+  exact foldrM_loop ..
+
+theorem foldrM_succ_last [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) :
+    foldrM (n+1) f = fun x => f (Fin.last n) x >>= foldrM n (fun i => f i.castSucc) := by
+  funext x
+  induction n generalizing x with
+  | zero => simp [foldrM_succ]
+  | succ n ih =>
+    rw [foldrM_succ]
+    conv => rhs; rw [foldrM_succ]
+    simp [ih]
+
+theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) :
+    foldrM (n + k) f =
+      fun x => foldrM k (fun i => f (i.natAdd n)) x >>= foldrM n (fun i => f (i.castLE (Nat.le_add_right n k))) := by
+  induction k with
+  | zero =>
+    simp
+  | succ k ih =>
+    funext x
+    simp [foldrM_succ_last, ← Nat.add_assoc, ih]
 
 /-! ### foldl -/
 
+@[congr] theorem foldl_congr {n k : Nat} (w : n = k) (f : α → Fin n → α) :
+    foldl n f = foldl k (fun x i => f x (i.cast w.symm)) := by
+  subst w
+  rfl
+
 theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) :
     foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by
   rw [foldl.loop, dif_pos h]
@@ -187,14 +255,34 @@ theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
   rw [foldl_succ]
   induction n generalizing x with
   | zero => simp [foldl_succ, Fin.last]
-  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
+  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp
+
+theorem foldl_add (f : α → Fin (n + m) → α) (x) :
+    foldl (n + m) f x =
+      foldl m (fun x i => f x (i.natAdd n))
+        (foldl n (fun x i => f x (i.castLE (Nat.le_add_right n m))) x):= by
+  induction m with
+  | zero => simp
+  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
-    foldl n f x = foldlM (m:=Id) n f x := by
+    foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by
   induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
 
+-- This is not marked `@[simp]` as it would match on every occurrence of `foldlM`.
+theorem foldlM_pure [Monad m] [LawfulMonad m] {n} {f : α → Fin n → α} :
+    foldlM n (fun x i => pure (f x i)) x = (pure (foldl n f x) : m α) := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih => simp [foldlM_succ, foldl_succ, ih]
+
 /-! ### foldr -/
 
+@[congr] theorem foldr_congr {n k : Nat} (w : n = k) (f : Fin n → α → α) :
+    foldr n f = foldr k (fun i => f (i.cast w.symm)) := by
+  subst w
+  rfl
+
 theorem foldr_loop_zero (f : Fin n → α → α) (x) :
     foldr.loop n f 0 (Nat.zero_le _) x = x := by
   rw [foldr.loop]
@@ -220,10 +308,18 @@ theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
     foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
   induction n generalizing x with
   | zero => simp [foldr_succ, Fin.last]
-  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
+  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp
+
+theorem foldr_add (f : Fin (n + m) → α → α) (x) :
+    foldr (n + m) f x =
+      foldr n (fun i => f (i.castLE (Nat.le_add_right n m)))
+        (foldr m (fun i => f (i.natAdd n)) x) := by
+  induction m generalizing x with
+  | zero => simp
+  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
-    foldr n f x = foldrM (m:=Id) n f x := by
+    foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by
   induction n <;> simp [foldr_succ, foldrM_succ, *]
 
 theorem foldl_rev (f : Fin n → α → α) (x) :
@@ -238,4 +334,11 @@ theorem foldr_rev (f : α → Fin n → α) (x) :
   | zero => simp
   | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]
 
+-- This is not marked `@[simp]` as it would match on every occurrence of `foldrM`.
+theorem foldrM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α → α} :
+    foldrM n (fun i x => pure (f i x)) x = (pure (foldr n f x) : m α) := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih => simp [foldrM_succ, foldr_succ, ih]
+
 end Fin

src/Init/Data/Fin/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Mario Carneiro, Leonardo de Moura
 module
 
 prelude
-import Init.Data.Fin.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Int.DivMod.Lemmas
 import Init.Ext
@@ -647,6 +646,20 @@ theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := k.rev_cast
 
 theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := k.rev_addNat 1
 
+@[simp, grind _=_]
+theorem castSucc_succ (i : Fin n) : i.succ.castSucc = i.castSucc.succ := rfl
+
+@[simp, grind =]
+theorem castLE_refl (h : n ≤ n) (i : Fin n) : i.castLE h = i := rfl
+
+@[simp, grind =]
+theorem castSucc_castLE (h : n ≤ m) (i : Fin n) :
+    (i.castLE h).castSucc = i.castLE (by omega) := rfl
+
+@[simp, grind =]
+theorem castSucc_natAdd (n : Nat) (i : Fin k) :
+    (i.natAdd n).castSucc = (i.castSucc).natAdd n := rfl
+
 /-! ### pred -/
 
 @[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl

src/Init/Data/Float.lean

@@ -161,8 +161,7 @@ This function does not reduce in the kernel. It is compiled to the C inequality
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
-instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
-instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
+attribute [instance] Float.decLt Float.decLe
 
 /--
 Converts a floating-point number to a string.

src/Init/Data/Float32.lean

@@ -145,7 +145,7 @@ Compares two floating point numbers for strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
+@[extern "lean_float32_decLt", instance] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLt a b
 
@@ -154,13 +154,10 @@ Compares two floating point numbers for non-strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
+@[extern "lean_float32_decLe", instance] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
 
-instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
-instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
-
 /--
 Converts a floating-point number to a string.
 

src/Init/Data/FloatArray/Basic.lean

@@ -165,7 +165,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float →
 
 @[inline]
 def foldl {β : Type v} (f : β → Float → β) (init : β) (as : FloatArray) (start := 0) (stop := as.size) : β :=
-  Id.run <| as.foldlM f init start stop
+  Id.run <| as.foldlM (pure <| f · ·) init start stop
 
 end FloatArray
 

src/Init/Data/Function.lean

@@ -18,7 +18,7 @@ Examples:
  * `Function.curry (fun (x, y) => x + y) 3 5 = 8`
  * `Function.curry Prod.swap 3 "five" = ("five", 3)`
 -/
-@[inline]
+@[inline, expose]
 def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
 
 /--
@@ -28,7 +28,7 @@ Examples:
  * `Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]`
  * `[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]`
 -/
-@[inline]
+@[inline, expose]
 def uncurry : (α → β → φ) → α × β → φ := fun f a => f a.1 a.2
 
 @[simp]

src/Init/Data/Hashable.lean

@@ -57,9 +57,6 @@ instance : Hashable UInt64 where
 instance : Hashable USize where
   hash n := n.toUInt64
 
-instance : Hashable ByteArray where
-  hash as := as.foldl (fun r a => mixHash r (hash a)) 7
-
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 

src/Init/Data/Int/Basic.lean

@@ -11,6 +11,8 @@ prelude
 import Init.Data.Cast
 import Init.Data.Nat.Div.Basic
 
+@[expose] section
+
 set_option linter.missingDocs true -- keep it documented
 open Nat
 

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

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Int.Bitwise.Basic
+import all Init.Data.Int.Bitwise.Basic
 import Init.Data.Int.DivMod.Lemmas
 
 namespace Int

src/Init/Data/Int/Compare.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
 module
 
 prelude
-import Init.Data.Ord
+import all Init.Data.Ord
 import Init.Data.Int.Order
 
 /-! # Basic lemmas about comparing integers

src/Init/Data/Int/DivMod/Basic.lean

@@ -8,6 +8,8 @@ module
 prelude
 import Init.Data.Int.Basic
 
+@[expose] section
+
 open Nat
 
 namespace Int

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -264,8 +264,8 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
 
-@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
-  conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]
+theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
+  simp
 
 theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
   apply (emod_add_cancel_right b).mp

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -1410,8 +1410,7 @@ theorem mul_tmod (a b n : Int) : (a * b).tmod n = (a.tmod n * b.tmod n).tmod n :
   norm_cast at h
   rw [Nat.mod_mod_of_dvd _ h]
 
-@[simp] theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b :=
-  tmod_tmod_of_dvd a (Int.dvd_refl b)
+theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b := by simp
 
 theorem tmod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → tmod b a = 0
   | _, _, ⟨_, rfl⟩ => mul_tmod_right ..
@@ -1469,9 +1468,8 @@ protected theorem tdiv_mul_cancel {a b : Int} (H : b ∣ a) : a.tdiv b * b = a :
 protected theorem mul_tdiv_cancel' {a b : Int} (H : a ∣ b) : a * b.tdiv a = b := by
   rw [Int.mul_comm, Int.tdiv_mul_cancel H]
 
-@[simp] theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
-  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
-  exact Int.dvd_refl a
+theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
+  simp
 
 theorem lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.tdiv b + 1) * b := by
   rw [Int.add_mul, Int.one_mul, Int.mul_comm]
@@ -1568,13 +1566,11 @@ theorem dvd_tmod_sub_self {x m : Int} : m ∣ x.tmod m - x := by
 theorem dvd_self_sub_tmod {x m : Int} : m ∣ x - x.tmod m :=
   Int.dvd_neg.1 (by simpa only [Int.neg_sub] using dvd_tmod_sub_self)
 
-@[simp] theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
-  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
-  exact Int.dvd_mul_right a b
+theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
+  simp
 
-@[simp] theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
-  rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]
-  exact Int.dvd_mul_left a b
+theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
+  simp
 
 @[simp] protected theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
@@ -2193,8 +2189,8 @@ theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n :
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_fmod_self_left]
 
-@[simp] theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b :=
-  fmod_fmod_of_dvd _ (Int.dvd_refl b)
+theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b := by
+  simp
 
 theorem sub_fmod (a b n : Int) : (a - b).fmod n = (a.fmod n - b.fmod n).fmod n := by
   apply (fmod_add_cancel_right b).mp

src/Init/Data/Int/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module
 
 prelude
-import Init.Data.Int.Basic
 import Init.Conv
 import Init.NotationExtra
 import Init.PropLemmas

src/Init/Data/Int/LemmasAux.lean

@@ -121,7 +121,7 @@ theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m :=
 /-! ### min and max -/
 
 @[simp] protected theorem min_assoc : ∀ (a b c : Int), min (min a b) c = min a (min b c) := by omega
-instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
+instance : Std.Associative (α := Int) min := ⟨Int.min_assoc⟩
 
 @[simp] protected theorem min_self_assoc {m n : Int} : min m (min m n) = min m n := by
   rw [← Int.min_assoc, Int.min_self]
@@ -130,7 +130,7 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
   rw [Int.min_comm m n, ← Int.min_assoc, Int.min_self]
 
 @[simp] protected theorem max_assoc (a b c : Int) : max (max a b) c = max a (max b c) := by omega
-instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
+instance : Std.Associative (α := Int) max := ⟨Int.max_assoc⟩
 
 @[simp] protected theorem max_self_assoc {m n : Int} : max m (max m n) = max m n := by
   rw [← Int.max_assoc, Int.max_self]

src/Init/Data/Int/Linear.lean

@@ -12,9 +12,9 @@ import Init.Data.Int.Lemmas
 import Init.Data.Int.LemmasAux
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.Cooper
-import Init.Data.Int.Gcd
+import all Init.Data.Int.Gcd
 import Init.Data.RArray
-import Init.Data.AC
+import all Init.Data.AC
 
 namespace Int.Linear
 

src/Init/Data/Int/Order.lean

@@ -166,6 +166,9 @@ protected theorem lt_or_le (a b : Int) : a < b ∨ b ≤ a := by rw [← Int.not
 protected theorem le_of_not_gt {a b : Int} (h : ¬ a > b) : a ≤ b :=
   Int.not_lt.mp h
 
+protected theorem not_lt_of_ge {a b : Int} (h : b ≤ a) : ¬a < b :=
+  Int.not_lt.mpr h
+
 protected theorem lt_trichotomy (a b : Int) : a < b ∨ a = b ∨ b < a :=
   if eq : a = b then .inr <| .inl eq else
   if le : a ≤ b then .inl <| Int.lt_iff_le_and_ne.2 ⟨le, eq⟩ else
@@ -1181,6 +1184,54 @@ protected theorem nonpos_of_mul_nonpos_right {a b : Int}
     (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 :=
   Int.le_of_not_gt fun hb : b > 0 => Int.not_le_of_gt (Int.mul_pos ha hb) h
 
+protected theorem nonneg_of_mul_nonpos_left {a b : Int}
+    (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a :=
+  Int.le_of_not_gt fun ha => Int.not_le_of_gt (Int.mul_pos_of_neg_of_neg ha hb) h
+
+protected theorem nonneg_of_mul_nonpos_right {a b : Int}
+    (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b :=
+  Int.le_of_not_gt fun hb => Int.not_le_of_gt (Int.mul_pos_of_neg_of_neg ha hb) h
+
+protected theorem nonpos_of_mul_nonneg_left {a b : Int}
+    (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0 :=
+  Int.le_of_not_gt fun ha : a > 0 => Int.not_le_of_gt (Int.mul_neg_of_pos_of_neg ha hb) h
+
+protected theorem nonpos_of_mul_nonneg_right {a b : Int}
+    (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0 :=
+  Int.le_of_not_gt fun hb : b > 0 => Int.not_le_of_gt (Int.mul_neg_of_neg_of_pos ha hb) h
+
+protected theorem pos_of_mul_pos_left {a b : Int}
+    (h : 0 < a * b) (hb : 0 < b) : 0 < a :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonpos_of_nonpos_of_nonneg ha (Int.le_of_lt hb)) h
+
+protected theorem pos_of_mul_pos_right {a b : Int}
+    (h : 0 < a * b) (ha : 0 < a) : 0 < b :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonpos_of_nonneg_of_nonpos (Int.le_of_lt ha) hb) h
+
+protected theorem neg_of_mul_neg_left {a b : Int}
+    (h : a * b < 0) (hb : 0 < b) : a < 0 :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonneg ha (Int.le_of_lt hb)) h
+
+protected theorem neg_of_mul_neg_right {a b : Int}
+    (h : a * b < 0) (ha : 0 < a) : b < 0 :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonneg (Int.le_of_lt ha) hb) h
+
+protected theorem pos_of_mul_neg_left {a b : Int}
+    (h : a * b < 0) (hb : b < 0) : 0 < a :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonneg_of_nonpos_of_nonpos ha (Int.le_of_lt hb)) h
+
+protected theorem pos_of_mul_neg_right {a b : Int}
+    (h : a * b < 0) (ha : a < 0) : 0 < b :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonneg_of_nonpos_of_nonpos (Int.le_of_lt ha) hb) h
+
+protected theorem neg_of_mul_pos_left {a b : Int}
+    (h : 0 < a * b) (hb : b < 0) : a < 0 :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonpos_of_nonneg_of_nonpos ha (Int.le_of_lt hb)) h
+
+protected theorem neg_of_mul_pos_right {a b : Int}
+    (h : 0 < a * b) (ha : a < 0) : b < 0 :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonpos_of_nonpos_of_nonneg (Int.le_of_lt ha) hb) h
+
 /- ## sign -/
 
 @[simp] theorem sign_zero : sign 0 = 0 := rfl

src/Init/Data/List/Attach.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 module
 
 prelude
+import all Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
 import Init.Data.List.Count
 import Init.Data.Subtype
 import Init.BinderNameHint
@@ -242,9 +243,8 @@ theorem getElem?_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} (h
   | nil => simp
   | cons hd tl hl =>
     rcases i with ⟨i⟩
-    · simp only [Option.pmap]
-      split <;> simp_all
-    · simp only [pmap, getElem?_cons_succ, hl, Option.pmap]
+    · simp
+    · simp only [pmap, getElem?_cons_succ, hl]
 
 set_option linter.deprecated false in
 @[deprecated List.getElem?_pmap (since := "2025-02-12")]

src/Init/Data/List/Basic.lean

@@ -10,6 +10,8 @@ import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.List.Notation
 
+@[expose] section
+
 /-!
 # Basic operations on `List`.
 

src/Init/Data/List/BasicAux.lean

@@ -254,7 +254,7 @@ pointer-equal to its argument.
 For verification purposes, `List.mapMono = List.map`.
 -/
 def mapMono (as : List α) (f : α → α) : List α :=
-  Id.run <| as.mapMonoM f
+  Id.run <| as.mapMonoM (pure <| f ·)
 
 /-! ## Additional lemmas required for bootstrapping `Array`. -/
 

src/Init/Data/List/Control.lean

@@ -9,7 +9,6 @@ prelude
 import Init.Control.Basic
 import Init.Control.Id
 import Init.Control.Lawful
-import Init.Data.List.Basic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -341,17 +340,24 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
 theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
     findM? (m := m) (pure <| p ·) as = pure (as.find? p) := by
   induction as with
-  | nil => rfl
+  | nil => simp [findM?, find?_nil]
   | cons a as ih =>
-    simp only [findM?, find?]
+    simp only [findM?, find?_cons]
     cases p a with
     | true  => simp
     | false => simp [ih]
 
 @[simp]
-theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p :=
+theorem idRun_findM? (p : α → Id Bool) (as : List α) :
+    (findM? p as).run = as.find? (p · |>.run) :=
   findM?_pure _ _
 
+@[deprecated idRun_findM? (since := "2025-05-21")]
+theorem findM?_id (p : α → Id Bool) (as : List α) :
+    findM? (m := Id) p as = as.find? p :=
+  findM?_pure _ _
+
+
 /--
 Returns the first non-`none` result of applying the monadic function `f` to each element of the
 list, in order. Returns `none` if `f` returns `none` for all elements.
@@ -395,7 +401,13 @@ theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : L
     | none   => simp [ih]
 
 @[simp]
-theorem findSomeM?_id {f : α → Option β} {as : List α} : findSomeM? (m := Id) f as = as.findSome? f :=
+theorem idRun_findSomeM? (f : α → Id (Option β)) (as : List α) :
+    (findSomeM? f as).run = as.findSome? (f · |>.run) :=
+  findSomeM?_pure
+
+@[deprecated idRun_findSomeM? (since := "2025-05-21")]
+theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) :
+    findSomeM? (m := Id) f as = as.findSome? f :=
   findSomeM?_pure
 
 theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} :

src/Init/Data/List/FinRange.lean

@@ -6,7 +6,8 @@ Authors: François G. Dorais
 module
 
 prelude
-import Init.Data.List.OfFn
+import all Init.Data.List.OfFn
+import Init.Data.List.Monadic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -29,7 +30,7 @@ def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
     (finRange n)[i] = Fin.cast length_finRange ⟨i, h⟩ := by
   simp [List.finRange]
 
-@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]
+@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange]
 
 theorem finRange_succ {n} : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
   apply List.ext_getElem; simp; intro i; cases i <;> simp
@@ -57,3 +58,50 @@ theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev :
     simp [Fin.rev_succ]
 
 end List
+
+namespace Fin
+
+theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x : α) :
+    foldlM n f x = (List.finRange n).foldlM f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih =>
+    simp [foldlM_succ, List.finRange_succ, List.foldlM_cons]
+    congr 1
+    funext y
+    simp [ih, List.foldlM_map]
+
+theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
+    foldrM n f x = (List.finRange n).foldrM f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih =>
+    simp [foldrM_succ, List.finRange_succ, ih, List.foldrM_map]
+
+theorem foldl_eq_finRange_foldl (f : α → Fin n → α) (x : α) :
+    foldl n f x = (List.finRange n).foldl f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih =>
+    simp [foldl_succ, List.finRange_succ, ih, List.foldl_map]
+
+theorem foldr_eq_finRange_foldr (f : Fin n → α → α) (x : α) :
+    foldr n f x = (List.finRange n).foldr f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih =>
+    simp [foldr_succ, List.finRange_succ, ih, List.foldr_map]
+
+end Fin
+
+namespace List
+
+theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
+    ofFnM f = (do
+      let a ← f 0
+      let as ← ofFnM fun i => f i.succ
+      pure (a :: as)) := by
+  simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.finRange_succ, List.foldlM_cons_eq_append,
+    List.foldlM_map]
+
+end List

src/Init/Data/List/Find.lean

@@ -11,6 +11,7 @@ import Init.Data.List.Lemmas
 import Init.Data.List.Sublist
 import Init.Data.List.Range
 import Init.Data.List.Impl
+import all Init.Data.List.Attach
 import Init.Data.Fin.Lemmas
 
 /-!
@@ -94,7 +95,7 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
   induction l with
   | nil => simp
   | cons x xs ih =>
-    simp [guard, findSome?, find?]
+    simp [findSome?, find?]
     split <;> rename_i h
     · simp only [Option.guard_eq_some_iff] at h
       obtain ⟨rfl, h⟩ := h
@@ -1002,9 +1003,8 @@ theorem isNone_findFinIdx? {l : List α} {p : α → Bool} :
 @[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
-  unfold unattach
   induction l with
-  | nil => simp
+  | nil => simp [unattach]
   | cons a l ih =>
     simp [hf, findFinIdx?_cons]
     split <;> simp [ih, Function.comp_def]
@@ -1108,14 +1108,9 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     simp only [finIdxOf?_cons]
     split <;> simp_all [@eq_comm _ x a]
 
-@[simp]
 theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.finIdxOf? a).isNone = ¬ a ∈ l := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [finIdxOf?_cons]
-    split <;> simp_all [@eq_comm _ x a]
+  simp
 
 /-! ### idxOf?
 
@@ -1154,15 +1149,9 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     simp only [idxOf?_cons]
     split <;> simp_all [@eq_comm _ x a]
 
-@[simp]
 theorem isNone_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.idxOf? a).isNone = ¬ a ∈ l := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [idxOf?_cons]
-    split <;> simp_all [@eq_comm _ x a]
-
+  simp
 
 /-! ### lookup -/
 

src/Init/Data/List/Impl.lean

@@ -109,7 +109,7 @@ Example:
   let rec go : ∀ as acc, filterMapTR.go f as acc = acc.toList ++ as.filterMap f
     | [], acc => by simp [filterMapTR.go, filterMap]
     | a::as, acc => by
-      simp only [filterMapTR.go, go as, Array.push_toList, append_assoc, singleton_append,
+      simp only [filterMapTR.go, go as, Array.toList_push, append_assoc, singleton_append,
         filterMap]
       split <;> simp [*]
   exact (go l #[]).symm

src/Init/Data/List/Lemmas.lean

@@ -9,8 +9,8 @@ module
 prelude
 import Init.Data.Bool
 import Init.Data.Option.Lemmas
-import Init.Data.List.BasicAux
-import Init.Data.List.Control
+import all Init.Data.List.BasicAux
+import all Init.Data.List.Control
 import Init.Control.Lawful.Basic
 import Init.BinderPredicates
 
@@ -272,13 +272,13 @@ theorem getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.len
 theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.length, l[i] = a := by
   rw [eq_comm, getElem?_eq_some_iff]
 
-@[simp] theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
+theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
     (some xs[i] = xs[i]?) ↔ True := by
-  simp [h]
+  simp
 
-@[simp] theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
+theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
     (xs[i]? = some xs[i]) ↔ True := by
-  simp [h]
+  simp
 
 theorem getElem_eq_iff {l : List α} {i : Nat} (h : i < l.length) : l[i] = x ↔ l[i]? = some x := by
   simp only [getElem?_eq_some_iff]
@@ -296,7 +296,7 @@ theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
     have p : i ≥ l.length := Nat.le_of_not_gt h
     simp [getElem?_eq_none p, h]
 
-@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a :=
+@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a := by
   match i, h with
   | 0, _ => rfl
 
@@ -434,8 +434,8 @@ theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := b
 theorem eq_of_mem_singleton : a ∈ [b] → a = b
   | .head .. => rfl
 
-@[simp] theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b :=
-  ⟨eq_of_mem_singleton, (by simp [·])⟩
+theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b := by
+  simp
 
 theorem forall_mem_cons {p : α → Prop} {a : α} {l : List α} :
     (∀ x, x ∈ a :: l → p x) ↔ p a ∧ ∀ x, x ∈ l → p x :=
@@ -1685,8 +1685,8 @@ theorem getLast_concat {a : α} : ∀ {l : List α}, getLast (l ++ [a]) (by simp
 
 @[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff
 
-@[simp] theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
-  rw [eq_comm, append_eq_nil_iff]
+theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
+  simp
 
 @[grind →]
 theorem eq_nil_of_append_eq_nil {l₁ l₂ : List α} (h : l₁ ++ l₂ = []) : l₁ = [] ∧ l₂ = [] :=
@@ -1745,7 +1745,7 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
   rw [head_append, dif_pos (by simp_all)]
 
 @[simp, grind] theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head? := by
-  cases l <;> rfl
+  cases l <;> simp
 
 -- Note:
 -- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
@@ -1897,8 +1897,8 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ l' b, l = concat l' b
 @[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = [] := by
   induction L <;> simp_all
 
-@[simp] theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by
-  rw [eq_comm, flatten_eq_nil_iff]
+theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by
+  simp
 
 theorem flatten_ne_nil_iff {xss : List (List α)} : xss.flatten ≠ [] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ [] := by
   simp
@@ -2052,7 +2052,7 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
 
 /-! ### flatMap -/
 
-theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := by rfl
+theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := rfl
 
 @[simp] theorem flatMap_id {L : List (List α)} : L.flatMap id = L.flatten := by simp [flatMap_def]
 
@@ -2541,17 +2541,25 @@ theorem flatten_reverse {L : List (List α)} :
   induction l generalizing b <;> simp [*]
 
 theorem foldl_eq_foldlM {f : β → α → β} {b : β} {l : List α} :
-    l.foldl f b = l.foldlM (m := Id) f b := by
-  induction l generalizing b <;> simp [*, foldl]
+    l.foldl f b = (l.foldlM (m := Id) (pure <| f · ·) b).run := by
+  simp
 
 theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
-    l.foldr f b = l.foldrM (m := Id) f b := by
-  induction l <;> simp [*, foldr]
+    l.foldr f b = (l.foldrM (m := Id) (pure <| f · ·) b).run := by
+  simp
 
-@[simp] theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
+theorem idRun_foldlM {f : β → α → Id β} {b : β} {l : List α} :
+    Id.run (l.foldlM f b) = l.foldl (f · · |>.run) b := foldl_eq_foldlM.symm
+
+@[deprecated idRun_foldlM (since := "2025-05-21")]
+theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
     Id.run (l.foldlM f b) = l.foldl f b := foldl_eq_foldlM.symm
 
-@[simp] theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
+theorem idRun_foldrM {f : α → β → Id β} {b : β} {l : List α} :
+    Id.run (l.foldrM f b) = l.foldr (f · · |>.run) b := foldr_eq_foldrM.symm
+
+@[deprecated idRun_foldrM (since := "2025-05-21")]
+theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
     Id.run (l.foldrM f b) = l.foldr f b := foldr_eq_foldrM.symm
 
 @[simp] theorem foldlM_reverse [Monad m] {l : List α} {f : β → α → m β} {b : β} :
@@ -2576,6 +2584,11 @@ theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
     l.foldl (fun xs y => f y :: xs) l' = (l.map f).reverse ++ l' := by
   induction l generalizing l' <;> simp [*]
 
+/-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`. -/
+@[grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
+    l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by
+  simp
+
 @[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
   induction l <;> simp [*]
@@ -2641,10 +2654,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   induction l <;> simp [*]
 
 @[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b : β} {l l' : List α} :
-    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
+    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM, -foldlM_pure]
 
 @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} :
-    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
+    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM, -foldrM_pure]
 
 @[grind] theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} :
     (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
@@ -2655,7 +2668,8 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   induction L <;> simp_all
 
 @[simp, grind] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} :
-    l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+    l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by
+  simp [foldl_eq_foldlM, foldr_eq_foldrM, -foldrM_pure]
 
 @[simp, grind] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} :
     l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
@@ -2938,7 +2952,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
     l.contains a ↔ ∃ a' ∈ l, a == a' := by
   induction l <;> simp_all
 
-@[grind]
+@[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.contains a ↔ a ∈ l := by
   simp
@@ -3054,7 +3068,7 @@ theorem head?_dropLast {xs : List α} : xs.dropLast.head? = if 1 < xs.length the
 
 theorem getLast_dropLast {xs : List α} (h) :
    xs.dropLast.getLast h =
-     xs[xs.length - 2]'(match xs, h with | (_ :: _ :: _), _ => Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
+     xs[xs.length - 2]'(by match xs, h with | (_ :: _ :: _), _ => exact Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
   rw [getLast_eq_getElem, getElem_dropLast]
   congr 1
   simp; rfl
@@ -3413,8 +3427,8 @@ variable [LawfulBEq α]
     | Or.inr h' => exact h'
   else rw [insert_of_not_mem h, mem_cons]
 
-@[simp] theorem mem_insert_self {a : α} {l : List α} : a ∈ l.insert a :=
-  mem_insert_iff.2 (Or.inl rfl)
+theorem mem_insert_self {a : α} {l : List α} : a ∈ l.insert a := by
+  simp
 
 theorem mem_insert_of_mem {l : List α} (h : a ∈ l) : a ∈ l.insert b :=
   mem_insert_iff.2 (Or.inr h)

src/Init/Data/List/MapIdx.lean

@@ -348,7 +348,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
     split <;> split
     · simp only [Option.some.injEq]
       rw [← Array.getElem_toList]
-      simp only [Array.push_toList]
+      simp only [Array.toList_push]
       rw [getElem_append_left, ← Array.getElem_toList]
     · have : i = acc.size := by omega
       simp_all

src/Init/Data/List/Monadic.lean

@@ -8,6 +8,9 @@ module
 prelude
 import Init.Data.List.TakeDrop
 import Init.Data.List.Attach
+import Init.Data.List.OfFn
+import Init.Data.Array.Bootstrap
+import all Init.Data.List.Control
 
 /-!
 # Lemmas about `List.mapM` and `List.forM`.
@@ -65,16 +68,24 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α}
     l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by
   induction l <;> simp_all
 
-@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f :=
+@[simp] theorem idRun_mapM {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) :=
   mapM_pure
 
+@[deprecated idRun_mapM (since := "2025-05-21")]
+theorem mapM_id {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) :=
+  mapM_pure
+
+@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {l : List α} :
+    (l.map f).mapM g = l.mapM (g ∘ f) := by
+  induction l <;> simp_all
+
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {l₁ l₂ : List α} :
     (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
 
 /-- Auxiliary lemma for `mapM_eq_reverse_foldlM_cons`. -/
 theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] {f : α → m β} {as : List α} {b : β} {bs : List β} :
-    (as.foldlM (init := b :: bs) fun acc a => return ((← f a) :: acc)) =
-      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return ((← f a) :: acc) := by
+    (as.foldlM (init := b :: bs) fun acc a => (· :: acc) <$> f a) =
+      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => (· :: acc) <$> f a := by
   induction as generalizing b bs with
   | nil => simp
   | cons a as ih =>
@@ -82,7 +93,7 @@ theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] {f : α → m β} {as :
     simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]
 
 theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
-    mapM f l = reverse <$> (l.foldlM (fun acc a => return ((← f a) :: acc)) []) := by
+    mapM f l = reverse <$> (l.foldlM (fun acc a => (· :: acc) <$> f a) []) := by
   rw [← mapM'_eq_mapM]
   induction l with
   | nil => simp
@@ -338,12 +349,18 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   simp only [forIn'_eq_foldlM]
   induction l.attach generalizing init <;> simp_all
 
-@[simp] theorem forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
+    (l : List α) (f : (a : α) → a ∈ l → β → Id β) (init : β) :
+    (forIn' l init (fun a m b => .yield <$> f a m b)).run =
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
+  forIn'_pure_yield_eq_foldl _ _
+
+@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
     {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) :
     forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
-      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
-  simp only [forIn'_eq_foldlM]
-  induction l.attach generalizing init <;> simp_all
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
@@ -391,12 +408,18 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   simp only [forIn_eq_foldlM]
   induction l generalizing init <;> simp_all
 
-@[simp] theorem forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
+    (l : List α) (f : α → β → Id β) (init : β) :
+    (forIn l init (fun a b => .yield <$> f a b)).run =
+      l.foldl (fun b a => f a b |>.run) init :=
+  forIn_pure_yield_eq_foldl _ _
+
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
     {l : List α} (f : α → β → β) (init : β) :
     forIn (m := Id) l init (fun a b => .yield (f a b)) =
-      l.foldl (fun b a => f a b) init := by
-  simp only [forIn_eq_foldlM]
-  induction l generalizing init <;> simp_all
+      l.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} :
@@ -437,7 +460,6 @@ and simplifies these to the function directly taking the value.
     {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
     (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
     l.foldlM f x = l.unattach.foldlM g x := by
-  unfold unattach
   induction l generalizing x with
   | nil => simp
   | cons a l ih => simp [ih, hf]
@@ -460,7 +482,6 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
     (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
     l.foldrM f x = l.unattach.foldrM g x := by
-  unfold unattach
   induction l generalizing x with
   | nil => simp
   | cons a l ih =>
@@ -486,7 +507,6 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.mapM f = l.unattach.mapM g := by
-  unfold unattach
   simp [← List.mapM'_eq_mapM]
   induction l with
   | nil => simp
@@ -504,7 +524,6 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m (Option β)} {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.filterMapM f = l.unattach.filterMapM g := by
-  unfold unattach
   induction l with
   | nil => simp
   | cons a l ih => simp [ih, hf, filterMapM_cons]
@@ -523,10 +542,9 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m (List β)} {g : α → m (List β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (l.flatMapM f) = l.unattach.flatMapM g := by
-  unfold unattach
   induction l with
-  | nil => simp
-  | cons a l ih => simp [ih, hf]
+  | nil => simp [flatMapM_nil]
+  | cons a l ih => simp only [flatMapM_cons, hf, ih, bind_pure_comp, unattach_cons]
 
 @[wf_preprocess] theorem flatMapM_wfParam [Monad m] [LawfulMonad m]
     {xs : List α} {f : α → m (List β)} :

src/Init/Data/List/Nat/Modify.lean

@@ -148,7 +148,7 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (i : Nat) (
     (a :: l).modify 0 f = f a :: l := rfl
 
 @[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (i) :
-    (a :: l).modify (i + 1) f = a :: l.modify i f := by rfl
+    (a :: l).modify (i + 1) f = a :: l.modify i f := rfl
 
 theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
     l.modifyHead f = l.modify 0 f := by cases l <;> simp

src/Init/Data/List/Nat/TakeDrop.lean

@@ -56,7 +56,7 @@ theorem getElem?_take_eq_none {l : List α} {i j : Nat} (h : i ≤ j) :
     (l.take i)[j]? = none :=
   getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
-@[grind =]theorem getElem?_take {l : List α} {i j : Nat} :
+@[grind =] theorem getElem?_take {l : List α} {i j : Nat} :
     (l.take i)[j]? = if j < i then l[j]? else none := by
   split
   · next h => exact getElem?_take_of_lt h

src/Init/Data/List/OfFn.lean

@@ -27,6 +27,13 @@ Examples:
 -/
 def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []
 
+/--
+Creates a list wrapped in a monad by applying the monadic function `f : Fin n → m α`
+to each potential index in order, starting at `0`.
+-/
+def ofFnM {n} [Monad m] (f : Fin n → m α) : m (List α) :=
+  List.reverse <$> Fin.foldlM n (fun xs i => (· :: xs) <$> f i) []
+
 @[simp]
 theorem length_ofFn {f : Fin n → α} : (ofFn f).length = n := by
   simp only [ofFn]
@@ -49,7 +56,8 @@ protected theorem getElem_ofFn {f : Fin n → α} (h : i < (ofFn f).length) :
       simp_all
 
 @[simp]
-protected theorem getElem?_ofFn {f : Fin n → α} : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
+protected theorem getElem?_ofFn {f : Fin n → α} :
+    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
   if h : i < (ofFn f).length
   then by
     rw [getElem?_eq_getElem h, List.getElem_ofFn]
@@ -60,8 +68,8 @@ protected theorem getElem?_ofFn {f : Fin n → α} : (ofFn f)[i]? = if h : i < n
 
 /-- `ofFn` on an empty domain is the empty list. -/
 @[simp]
-theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] :=
-  ext_get (by simp) (fun i hi₁ hi₂ => by contradiction)
+theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] := by
+  rw [ofFn, Fin.foldr_zero]
 
 @[simp]
 theorem ofFn_succ {n} {f : Fin (n + 1) → α} : ofFn f = f 0 :: ofFn fun i => f i.succ :=
@@ -70,6 +78,22 @@ theorem ofFn_succ {n} {f : Fin (n + 1) → α} : ofFn f = f 0 :: ofFn fun i => f
     · simp
     · simp)
 
+theorem ofFn_succ_last {n} {f : Fin (n + 1) → α} :
+    ofFn f = (ofFn fun i => f i.castSucc) ++ [f (Fin.last n)] := by
+  induction n with
+  | zero => simp [ofFn_succ]
+  | succ n ih =>
+    rw [ofFn_succ]
+    conv => rhs; rw [ofFn_succ]
+    rw [ih]
+    simp
+
+theorem ofFn_add {n m} {f : Fin (n + m) → α} :
+    ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
+  induction m with
+  | zero => simp
+  | succ m ih => simp [-ofFn_succ, ofFn_succ_last, ih]
+
 @[simp]
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
   cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]
@@ -92,4 +116,65 @@ theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFn f ≠ []) :
     (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩ := by
   simp [getLast_eq_getElem, length_ofFn, List.getElem_ofFn]
 
+/-- `ofFnM` on an empty domain is the empty list. -/
+@[simp]
+theorem ofFnM_zero [Monad m] [LawfulMonad m] {f : Fin 0 → m α} : ofFnM f = pure [] := by
+  simp [ofFnM]
+
+/-! See `Init.Data.List.FinRange` for the `ofFnM_succ` variant. -/
+
+theorem ofFnM_succ_last {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
+    ofFnM f = (do
+      let as ← ofFnM fun i => f i.castSucc
+      let a  ← f (Fin.last n)
+      pure (as ++ [a])) := by
+  simp [ofFnM, Fin.foldlM_succ_last]
+
+theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
+    ofFnM f = (do
+      let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))
+      let bs ← ofFnM fun i : Fin k => f (i.natAdd n)
+      pure (as ++ bs)) := by
+  induction k with
+  | zero => simp
+  | succ k ih => simp [ofFnM_succ_last, ih]
+
+
+end List
+
+namespace Fin
+
+theorem foldl_cons_eq_append {f : Fin n → α} {xs : List α} :
+    Fin.foldl n (fun xs i => f i :: xs) xs = (List.ofFn f).reverse ++ xs := by
+  induction n generalizing xs with
+  | zero => simp
+  | succ n ih => simp [Fin.foldl_succ, List.ofFn_succ, ih]
+
+theorem foldr_cons_eq_append {f : Fin n → α} {xs : List α} :
+    Fin.foldr n (fun i xs => f i :: xs) xs = List.ofFn f ++ xs:= by
+  induction n generalizing xs with
+  | zero => simp
+  | succ n ih => simp [Fin.foldr_succ, List.ofFn_succ, ih]
+
+end Fin
+
+namespace List
+
+@[simp]
+theorem ofFnM_pure_comp [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
+    ofFnM (pure ∘ f) = (pure (ofFn f) : m (List α)) := by
+  simp [ofFnM, Fin.foldlM_pure, Fin.foldl_cons_eq_append]
+
+-- Variant of `ofFnM_pure_comp` using a lambda.
+-- This is not marked a `@[simp]` as it would match on every occurrence of `ofFnM`.
+theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
+    ofFnM (fun i => pure (f i)) = (pure (ofFn f) : m (List α)) :=
+  ofFnM_pure_comp
+
+@[simp, grind =] theorem idRun_ofFnM {f : Fin n → Id α} :
+    Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp [-ofFn_succ, ofFnM_succ_last, ofFn_succ_last, ih]
+
 end List

src/Init/Data/List/Pairwise.lean

@@ -24,7 +24,7 @@ open Nat
 
 /-! ### Pairwise -/
 
-theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
+@[grind →] theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
   | .slnil, h => h
   | .cons _ s, .cons _ h₂ => h₂.sublist s
   | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h)
@@ -37,11 +37,11 @@ theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) :
 theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : ∀ {a'}, a' ∈ l → R a a' :=
   (pairwise_cons.1 p).1 _
 
-theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
+@[grind →] theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
   (pairwise_cons.1 p).2
 
 set_option linter.unusedVariables false in
-theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
+@[grind] theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
   | [], h => h
   | _ :: _, h => h.of_cons
 
@@ -101,11 +101,11 @@ theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pa
     · exact h₃.1 _ hx
     · exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
 
-theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
+@[grind] theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
 
-theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
+@[grind =] theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
 
-theorem pairwise_map {l : List α} :
+@[grind =] theorem pairwise_map {l : List α} :
     (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b) := by
   induction l
   · simp
@@ -115,11 +115,11 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
     (p : Pairwise S (map f l)) : Pairwise R l :=
   (pairwise_map.1 p).imp (H _ _)
 
-theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
+@[grind] theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
     (p : Pairwise R l) : Pairwise S (map f l) :=
   pairwise_map.2 <| p.imp (H _ _)
 
-theorem pairwise_filterMap {f : β → Option α} {l : List β} :
+@[grind =] theorem pairwise_filterMap {f : β → Option α} {l : List β} :
     Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b, f a = some b → ∀ b', f a' = some b' → R b b') l := by
   let _S (a a' : β) := ∀ b, f a = some b → ∀ b', f a' = some b' → R b b'
   induction l with
@@ -134,20 +134,20 @@ theorem pairwise_filterMap {f : β → Option α} {l : List β} :
     simpa [IH, e] using fun _ =>
       ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
 
-theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
+@[grind] theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
     (H : ∀ a a' : α, R a a' → ∀ b, f a = some b → ∀ b', f a' = some b' → S b b') {l : List α} (p : Pairwise R l) :
     Pairwise S (filterMap f l) :=
   pairwise_filterMap.2 <| p.imp (H _ _)
 
-theorem pairwise_filter {p : α → Prop} [DecidablePred p] {l : List α} :
+@[grind =] theorem pairwise_filter {p : α → Bool} {l : List α} :
     Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l := by
   rw [← filterMap_eq_filter, pairwise_filterMap]
   simp
 
-theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
+@[grind] theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
   Pairwise.sublist filter_sublist
 
-theorem pairwise_append {l₁ l₂ : List α} :
+@[grind =] theorem pairwise_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b := by
   induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]
 
@@ -157,13 +157,13 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
     (x : α) (xm : x ∈ l₂) (y : α) (ym : y ∈ l₁) : R x y := s (H y ym x xm)
   simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
 
-theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
+@[grind =] theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) := by
   show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
   rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
   simp only [mem_append, or_comm]
 
-theorem pairwise_flatten {L : List (List α)} :
+@[grind =] theorem pairwise_flatten {L : List (List α)} :
     Pairwise R (flatten L) ↔
       (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L := by
   induction L with
@@ -174,16 +174,16 @@ theorem pairwise_flatten {L : List (List α)} :
     rw [and_comm, and_congr_left_iff]
     intros; exact ⟨fun h l' b c d e => h c d e l' b, fun h c d e l' b => h l' b c d e⟩
 
-theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
+@[grind =] theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
     List.Pairwise R (l.flatMap f) ↔
       (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
   simp [List.flatMap, pairwise_flatten, pairwise_map]
 
-theorem pairwise_reverse {l : List α} :
+@[grind =] theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by
   induction l <;> simp [*, pairwise_append, and_comm]
 
-@[simp] theorem pairwise_replicate {n : Nat} {a : α} :
+@[simp, grind =] theorem pairwise_replicate {n : Nat} {a : α} :
     (replicate n a).Pairwise R ↔ n ≤ 1 ∨ R a a := by
   induction n with
   | zero => simp
@@ -205,10 +205,10 @@ theorem pairwise_reverse {l : List α} :
         simp
       · exact ⟨fun _ => h, Or.inr h⟩
 
-theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
+@[grind] theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
   h.sublist (drop_sublist _ _)
 
-theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
+@[grind] theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
   h.sublist (take_sublist _ _)
 
 theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by
@@ -247,19 +247,19 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
   intro a b hab
   apply h <;> (apply hab.subset; simp)
 
-theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
+@[grind =] theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
     Pairwise R (l.pmap f h) ↔
       Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l := by
   induction l with
   | nil => simp
   | cons a l ihl =>
     obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
-    simp only [ihl hl, pairwise_cons, exists₂_imp, pmap, and_congr_left_iff, mem_pmap]
+    simp only [pmap_cons, pairwise_cons, mem_pmap, forall_exists_index, ihl hl, and_congr_left_iff]
     refine fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, ?_⟩
     rintro H _ b hb rfl
     exact H b hb _ _
 
-theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
+@[grind] theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
     (h : ∀ x ∈ l, p x) {S : β → β → Prop}
     (hS : ∀ ⦃x⦄ (hx : p x) ⦃y⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
     Pairwise S (l.pmap f h) := by
@@ -268,15 +268,15 @@ theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f :
 
 /-! ### Nodup -/
 
-@[simp]
+@[simp, grind]
 theorem nodup_nil : @Nodup α [] :=
   Pairwise.nil
 
-@[simp]
+@[simp, grind =]
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]
 
-theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Pairwise.sublist
 
 theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
@@ -303,7 +303,7 @@ theorem getElem?_inj {xs : List α}
       rw [mem_iff_getElem?]
     exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
 
-@[simp] theorem nodup_replicate {n : Nat} {a : α} :
+@[simp, grind =] theorem nodup_replicate {n : Nat} {a : α} :
     (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
 
 end List

src/Init/Data/List/Perm.lean

@@ -9,6 +9,7 @@ prelude
 import Init.Data.List.Pairwise
 import Init.Data.List.Erase
 import Init.Data.List.Find
+import all Init.Data.List.Attach
 
 /-!
 # List Permutations

src/Init/Data/List/Sort/Impl.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.List.Sort.Basic
 import Init.Data.List.Sort.Lemmas
 
 /-!

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

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.List.Perm
-import Init.Data.List.Sort.Basic
+import all Init.Data.List.Sort.Basic
 import Init.Data.List.Nat.Range
 import Init.Data.Bool
 

src/Init/Data/List/TakeDrop.lean

@@ -6,6 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module
 
 prelude
+import all Init.Data.List.Basic
 import Init.Data.List.Lemmas
 
 /-!
@@ -30,6 +31,11 @@ theorem take_cons {l : List α} (h : 0 < i) : (a :: l).take i = a :: l.take (i -
   | zero => exact absurd h (Nat.lt_irrefl _)
   | succ i => rfl
 
+theorem drop_cons {l : List α} (h : 0 < i) : (a :: l).drop i = l.drop (i - 1) := by
+  cases i with
+  | zero => exact absurd h (Nat.lt_irrefl _)
+  | succ i => rfl
+
 @[simp]
 theorem drop_one : ∀ {l : List α}, l.drop 1 = l.tail
   | [] | _ :: _ => rfl
@@ -241,7 +247,7 @@ theorem dropLast_eq_take {l : List α} : l.dropLast = l.take (l.length - 1) := b
     ∀ {l : List α} {i : Nat}, (l.take i).map f = (l.map f).take i
   | [], i => by simp
   | _, 0 => by simp
-  | _ :: tl, n + 1 => by dsimp; rw [map_take]
+  | _ :: tl, n + 1 => by simp [map_take]
 
 @[simp] theorem map_drop {f : α → β} :
     ∀ {l : List α} {i : Nat}, (l.drop i).map f = (l.map f).drop i

src/Init/Data/List/ToArray.lean

@@ -6,11 +6,14 @@ Authors: Mario Carneiro
 module
 
 prelude
+import all Init.Data.List.Control
 import Init.Data.List.Impl
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.Nat.InsertIdx
 import Init.Data.Array.Lex.Basic
+import all Init.Data.Array.Basic
+import all Init.Data.Array.Set
 
 /-! ### Lemmas about `List.toArray`.
 
@@ -207,12 +210,6 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
   cases as
   simp
 
-@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
-  induction l generalizing as <;> simp [*]
-
-@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
-  rw [foldr_eq_foldl_reverse, foldl_push]
-
 @[simp, grind =] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
@@ -259,16 +256,16 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
 
 @[simp, grind =] theorem findSome?_toArray (f : α → Option β) (l : List α) :
     l.toArray.findSome? f = l.findSome? f := by
-  rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
+  rw [Array.findSome?, findSomeM?_toArray, findSomeM?_pure, Id.run_pure]
 
 @[simp, grind =] theorem find?_toArray (f : α → Bool) (l : List α) :
     l.toArray.find? f = l.find? f := by
   rw [Array.find?]
-  simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
+  simp only [forIn_toArray]
   induction l with
   | nil => simp
   | cons a l ih =>
-    simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
+    simp only [forIn_cons, find?]
     by_cases f a <;> simp_all
 
 private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :

src/Init/Data/Nat/Basic.lean

@@ -57,7 +57,7 @@ Examples:
 * `Nat.repeat f 3 a = f <| f <| f <| a`
 * `Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"`
 -/
-@[specialize] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
+@[specialize, expose] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
   | 0,      a => a
   | succ n, a => f (repeat f n a)
 
@@ -89,7 +89,7 @@ Examples:
  * `Nat.blt 5 2 = false`
  * `Nat.blt 5 5 = false`
 -/
-def blt (a b : Nat) : Bool :=
+@[expose] def blt (a b : Nat) : Bool :=
   ble a.succ b
 
 attribute [simp] Nat.zero_le
@@ -150,7 +150,7 @@ theorem add_one (n : Nat) : n + 1 = succ n :=
 @[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
   rfl
 
-@[simp] theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun
+theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun
 theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := by simp
 
 protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
@@ -731,13 +731,12 @@ theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n =
 theorem ctor_eq_zero : Nat.zero = 0 :=
   rfl
 
-@[simp] protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
-  fun h => Nat.noConfusion h
+protected theorem one_ne_zero : 1 ≠ (0 : Nat) := by simp
 
 @[simp] protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
   fun h => Nat.noConfusion h
 
-@[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
+theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
 instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := ⟨succ_ne_zero n⟩
 

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

@@ -9,7 +9,7 @@ module
 prelude
 import Init.Data.Bool
 import Init.Data.Int.Pow
-import Init.Data.Nat.Bitwise.Basic
+import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Simproc
 import Init.TacticsExtra

src/Init/Data/Nat/Compare.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 module
 
 prelude
-import Init.Data.Ord
+import all Init.Data.Ord
 
 /-! # Basic lemmas about comparing natural numbers
 

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

@@ -10,6 +10,8 @@ import Init.WF
 import Init.WFTactics
 import Init.Data.Nat.Basic
 
+@[expose] section
+
 namespace Nat
 
 /--

src/Init/Data/Nat/Fold.lean

@@ -197,6 +197,8 @@ theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bo
       omega
   go n 0 f
 
+/-! ### `fold` -/
+
 @[simp] theorem fold_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
     fold 0 f init = init := by simp [fold]
 
@@ -210,6 +212,8 @@ theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n
   | succ n ih =>
     simp [ih, List.finRange_succ_last, List.foldl_map]
 
+/-! ### `foldRev` -/
+
 @[simp] theorem foldRev_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
     foldRev 0 f init = init := by simp [foldRev]
 
@@ -223,10 +227,12 @@ theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i <
   | zero => simp
   | succ n ih => simp [ih, List.finRange_succ_last, List.foldr_map]
 
+/-! ### `any` -/
+
 @[simp] theorem any_zero {f : (i : Nat) → i < 0 → Bool} : any 0 f = false := by simp [any]
 
 @[simp] theorem any_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
-  any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
+    any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
 
 theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
     any n f = (List.finRange n).any (fun ⟨i, h⟩ => f i h) := by
@@ -234,10 +240,12 @@ theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
   | zero => simp
   | succ n ih => simp [ih, List.finRange_succ_last, List.any_map, Function.comp_def]
 
+/-! ### `all` -/
+
 @[simp] theorem all_zero {f : (i : Nat) → i < 0 → Bool} : all 0 f = true := by simp [all]
 
 @[simp] theorem all_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
-  all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
+    all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
 
 theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
     all n f = (List.finRange n).all (fun ⟨i, h⟩ => f i h) := by
@@ -250,7 +258,7 @@ end Nat
 namespace Prod
 
 /--
-Combines an initial value with each natural number from in a range, in increasing order.
+Combines an initial value with each natural number from a range, in increasing order.
 
 In particular, `(start, stop).foldI f init` applies `f`on all the numbers
 from `start` (inclusive) to `stop` (exclusive) in increasing order:
@@ -260,7 +268,7 @@ Examples:
 * `(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]`
 * `(5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]`
 -/
-@[inline] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → α → α) (init : α) : α :=
+@[inline, simp] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → α → α) (init : α) : α :=
   (i.2 - i.1).fold (fun j _ => f (i.1 + j) (by omega) (by omega)) init
 
 /--
@@ -274,7 +282,7 @@ Examples:
  * `(5, 8).anyI (fun j _ _ => j % 2 = 0) = true`
  * `(6, 6).anyI (fun j _ _ => j % 2 = 0) = false`
 -/
-@[inline] def anyI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
+@[inline, simp] def anyI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
   (i.2 - i.1).any (fun j _ => f (i.1 + j) (by omega) (by omega))
 
 /--
@@ -288,7 +296,7 @@ Examples:
  * `(5, 8).allI (fun j _ _ => j % 2 = 0) = false`
  * `(6, 7).allI (fun j _ _ => j % 2 = 0) = true`
 -/
-@[inline] def allI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
+@[inline, simp] def allI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
   (i.2 - i.1).all (fun j _ => f (i.1 + j) (by omega) (by omega))
 
 end Prod

src/Init/Data/Nat/Lemmas.lean

@@ -6,8 +6,9 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn
 module
 
 prelude
+import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.MinMax
-import Init.Data.Nat.Log2
+import all Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
 import Init.Data.Nat.Mod
 
@@ -414,7 +415,7 @@ theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
   | inl h => rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
   | inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]
 
-@[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _)
+protected theorem min_self (a : Nat) : min a a = a := by simp
 instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
@@ -430,16 +431,14 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 @[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
   rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
 
-@[simp] theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by
-  rw [Nat.min_def]
+theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by
   simp
-@[simp] theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by
-  rw [Nat.min_def]
+theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by
+  simp
+theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by
+  simp
+theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by
   simp
-@[simp] theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by
-  rw [Nat.min_comm, min_add_left_self]
-@[simp] theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by
-  rw [Nat.min_comm, min_add_right_self]
 
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
@@ -461,7 +460,7 @@ protected theorem succ_max_succ (x y) : max (succ x) (succ y) = succ (max x y) :
   | inl h => rw [Nat.max_eq_right h, Nat.max_eq_right (Nat.succ_le_succ h)]
   | inr h => rw [Nat.max_eq_left h, Nat.max_eq_left (Nat.succ_le_succ h)]
 
-@[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _)
+protected theorem max_self (a : Nat) : max a a = a := by simp
 instance : Std.IdempotentOp (α := Nat) max := ⟨Nat.max_self⟩
 
 instance : Std.LawfulIdentity (α := Nat) max 0 where
@@ -475,16 +474,14 @@ instance : Std.LawfulIdentity (α := Nat) max 0 where
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
 instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
-@[simp] theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by
-  rw [Nat.max_def]
+theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by
   simp
-@[simp] theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by
-  rw [Nat.max_def]
+theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by
+  simp
+theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by
+  simp
+theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by
   simp
-@[simp] theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by
-  rw [Nat.max_comm, max_add_left_self]
-@[simp] theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by
-  rw [Nat.max_comm, max_add_right_self]
 
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with
@@ -813,10 +810,8 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
       simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
     rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂]
 
-@[simp] theorem mod_mod (a n : Nat) : (a % n) % n = a % n :=
-  match eq_zero_or_pos n with
-  | .inl n0 => by simp [n0, mod_zero]
-  | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
+theorem mod_mod (a n : Nat) : (a % n) % n = a % n := by
+  simp
 
 theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
   rw (occs := [1]) [← mod_add_div a n]

src/Init/Data/Nat/Linear.lean

@@ -10,6 +10,8 @@ import Init.ByCases
 import Init.Data.Prod
 import Init.Data.RArray
 
+@[expose] section
+
 namespace Nat.Linear
 
 /-!
@@ -255,15 +257,8 @@ theorem Poly.denote_cons (ctx : Context) (k : Nat) (v : Var) (p : Poly) : denote
 
 attribute [local simp] Poly.denote_cons
 
-theorem Poly.denote_reverseAux (ctx : Context) (p q : Poly) : denote ctx (List.reverseAux p q) = denote ctx (p ++ q) := by
-  match p with
-  | [] => simp [List.reverseAux]
-  | (k, v) :: p => simp [List.reverseAux, denote_reverseAux]
-
-attribute [local simp] Poly.denote_reverseAux
-
 theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.reverse p) = denote ctx p := by
-  simp [List.reverse]
+  induction p <;> simp [*]
 
 attribute [local simp] Poly.denote_reverse
 

src/Init/Data/Option/Array.lean

@@ -8,14 +8,42 @@ module
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Option.List
+import all Init.Data.Option.Instances
 
 namespace Option
 
-@[simp]
+@[simp, grind] theorem mem_toArray {a : α} {o : Option α} : a ∈ o.toArray ↔ o = some a := by
+  cases o <;> simp [eq_comm]
+
+@[simp, grind] theorem forIn'_toArray [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toArray → β → m (ForInStep β)) :
+    forIn' o.toArray b f = forIn' o b fun a m b => f a (by simpa using m) b := by
+  cases o <;> simp <;> rfl
+
+@[simp, grind] theorem forIn_toArray [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
+    forIn o.toArray b f = forIn o b f := by
+  cases o <;> simp <;> rfl
+
+@[simp, grind] theorem foldlM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
+    o.toArray.foldlM f a = o.elim (pure a) (fun b => f a b) := by
+  cases o <;> simp
+
+@[simp, grind] theorem foldrM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
+    o.toArray.foldrM f a = o.elim (pure a) (fun b => f b a) := by
+  cases o <;> simp
+
+@[simp, grind] theorem foldl_toArray (o : Option β) (a : α) (f : α → β → α) :
+    o.toArray.foldl f a = o.elim a (fun b => f a b) := by
+  cases o <;> simp
+
+@[simp, grind] theorem foldr_toArray (o : Option β) (a : α) (f : β → α → α) :
+    o.toArray.foldr f a = o.elim a (fun b => f b a) := by
+  cases o <;> simp
+
+@[simp, grind =]
 theorem toList_toArray {o : Option α} : o.toArray.toList = o.toList := by
   cases o <;> simp
 
-@[simp]
+@[simp, grind =]
 theorem toArray_toList {o : Option α} : o.toList.toArray = o.toArray := by
   cases o <;> simp
 
@@ -23,4 +51,47 @@ theorem toArray_filter {o : Option α} {p : α → Bool} :
     (o.filter p).toArray = o.toArray.filter p := by
   rw [← toArray_toList, toList_filter, ← List.filter_toArray, toArray_toList]
 
+theorem toArray_bind {o : Option α} {f : α → Option β} :
+    (o.bind f).toArray = o.toArray.flatMap (Option.toArray ∘ f) := by
+  cases o <;> simp
+
+theorem toArray_join {o : Option (Option α)} : o.join.toArray = o.toArray.flatMap Option.toArray := by
+  simp [toArray_bind, ← bind_id_eq_join]
+
+theorem toArray_map {o : Option α} {f : α → β} : (o.map f).toArray = o.toArray.map f := by
+  cases o <;> simp
+
+theorem toArray_min [Min α] {o o' : Option α} :
+    (min o o').toArray = o.toArray.zipWith min o'.toArray := by
+  cases o <;> cases o' <;> simp
+
+@[simp]
+theorem size_toArray_le {o : Option α} : o.toArray.size ≤ 1 := by
+  cases o <;> simp
+
+@[grind =]
+theorem size_toArray {o : Option α} :
+    o.toArray.size = if o.isSome then 1 else 0 := by
+  cases o <;> simp
+
+@[simp]
+theorem toArray_eq_empty_iff {o : Option α} : o.toArray = #[] ↔ o = none := by
+  cases o <;> simp
+
+@[simp]
+theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] ↔ o = some a := by
+  cases o <;> simp
+
+theorem size_toArray_eq_zero_iff {o : Option α} :
+    o.toArray.size = 0 ↔ o = none := by
+  simp
+
+@[simp]
+theorem size_toArray_eq_one_iff {o : Option α} :
+    o.toArray.size = 1 ↔ o.isSome := by
+  cases o <;> simp
+
+theorem size_toArray_choice_eq_one [Nonempty α] : (choice α).toArray.size = 1 := by
+  simp
+
 end Option

src/Init/Data/Option/Attach.lean

@@ -8,11 +8,16 @@ module
 prelude
 import Init.Data.Option.Basic
 import Init.Data.Option.List
+import Init.Data.Option.Array
+import Init.Data.Array.Attach
 import Init.Data.List.Attach
 import Init.BinderPredicates
 
 namespace Option
 
+instance {o : Option α} : Subsingleton { x // o = some x } where
+  allEq a b := Subtype.ext (Option.some.inj (a.property.symm.trans b.property))
+
 /--
 Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
 `Option {x // P x}` is the same as the input `Option α`.
@@ -46,12 +51,12 @@ terminates.
 -/
 @[inline] def attach (xs : Option α) : Option {x // xs = some x} := xs.attachWith _ fun _ => id
 
-@[simp] theorem attach_none : (none : Option α).attach = none := rfl
-@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
+@[simp, grind =] theorem attach_none : (none : Option α).attach = none := rfl
+@[simp, grind =] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
 
-@[simp] theorem attach_some {x : α} :
+@[simp, grind =] theorem attach_some {x : α} :
     (some x).attach = some ⟨x, rfl⟩ := rfl
-@[simp] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), some x = some b → P b) :
+@[simp, grind =] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), some x = some b → P b) :
     (some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl
 
 theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
@@ -71,7 +76,7 @@ theorem attach_map_val (o : Option α) (f : α → β) :
 @[deprecated attach_map_val (since := "2025-02-17")]
 abbrev attach_map_coe := @attach_map_val
 
-theorem attach_map_subtype_val (o : Option α) :
+@[simp, grind =]theorem attach_map_subtype_val (o : Option α) :
     o.attach.map Subtype.val = o :=
   (attach_map_val _ _).trans (congrFun Option.map_id _)
 
@@ -82,28 +87,28 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H
 @[deprecated attachWith_map_val (since := "2025-02-17")]
 abbrev attachWith_map_coe := @attachWith_map_val
 
-theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
+@[simp, grind =] theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).map Subtype.val = o :=
   (attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
 
-theorem attach_eq_some : ∀ (o : Option a) (x : {x // o = some x}), o.attach = some x
+theorem attach_eq_some : ∀ (o : Option α) (x : {x // o = some x}), o.attach = some x
   | none, ⟨x, h⟩ => by simp at h
   | some a, ⟨x, h⟩ => by simpa using h
 
 theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach :=
   attach_eq_some
 
-@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
+@[simp, grind =] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
   cases o <;> simp
 
-@[simp] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
+@[simp, grind =] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).isNone = o.isNone := by
   cases o <;> simp
 
-@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
+@[simp, grind =] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
   cases o <;> simp
 
-@[simp] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
+@[simp, grind =] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).isSome = o.isSome := by
   cases o <;> simp
 
@@ -122,43 +127,67 @@ theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach
     o.attachWith p H = some x ↔ o = some x.val := by
   cases o <;> cases x <;> simp
 
-@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
-    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ := by
-  cases o
-  · simp at h
-  · simp [get_some]
+@[simp, grind =] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
+    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ :=
+  Subsingleton.elim _ _
 
-@[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a, o = some a → p a) (h : (o.attachWith p H).isSome) :
+@[simp, grind =] theorem getD_attach {o : Option α} {fallback} :
+    o.attach.getD fallback = fallback :=
+  Subsingleton.elim _ _
+
+@[simp, grind =] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
+    o.attach.get! = default :=
+  Subsingleton.elim _ _
+
+@[simp, grind =] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a, o = some a → p a) (h : (o.attachWith p H).isSome) :
     (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
-  cases o
-  · simp at h
-  · simp [get_some]
+  cases o <;> simp
+
+@[simp, grind =] theorem getD_attachWith {p : α → Prop} {o : Option α} {h} {fallback} :
+    (o.attachWith p h).getD fallback =
+      ⟨o.getD fallback.val, by
+        cases o
+        · exact fallback.property
+        · exact h _ (by simp)⟩ := by
+  cases o <;> simp
 
 theorem toList_attach (o : Option α) :
-    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+    o.attach.toList = o.toList.attach.map fun x => ⟨x.1, by simpa using x.2⟩ := by
+  cases o <;> simp
+
+theorem toList_attachWith {p : α → Prop} {o : Option α} {h} :
+    (o.attachWith p h).toList = o.toList.attach.map fun x => ⟨x.1, h _ (by simpa using x.2)⟩ := by
+  cases o <;> simp
+
+theorem toArray_attach (o : Option α) :
+    o.attach.toArray = o.toArray.attach.map fun x => ⟨x.1, by simpa using x.2⟩ := by
+  cases o <;> simp
+
+theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
+    (o.attachWith p h).toArray = o.toArray.attach.map fun x => ⟨x.1, h _ (by simpa using x.2)⟩ := by
   cases o <;> simp
 
 @[simp, grind =] theorem attach_toList (o : Option α) :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
-  cases o <;> simp
+  cases o <;> simp [toList]
 
-theorem attach_map {o : Option α} (f : α → β) :
+@[grind =] theorem attach_map {o : Option α} (f : α → β) :
     (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by
   cases o <;> simp
 
-theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
+@[grind =] theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
     (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some_iff.2 ⟨_, h, rfl⟩))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
-theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
+@[grind =] theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
     o.attach.map f = o.pmap (fun a (h : o = some a) => f ⟨a, h⟩) (fun _ h => h) := by
   cases o <;> simp
 
 @[deprecated map_attach_eq_pmap (since := "2025-02-09")]
 abbrev map_attach := @map_attach_eq_pmap
 
-@[simp] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a}
+@[simp, grind =] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a}
     (f : { x // P x } → β) :
     (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases l <;> simp_all
@@ -174,12 +203,12 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o
     o.attach.map (fun x => ⟨x.1, f x.1 x.2⟩) = o.attachWith p f := by
   cases o <;> simp_all [Function.comp_def]
 
-theorem attach_bind {o : Option α} {f : α → Option β} :
+@[grind =] theorem attach_bind {o : Option α} {f : α → Option β} :
     (o.bind f).attach =
       o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some_iff.2 ⟨_, h, h'⟩⟩ := by
   cases o <;> simp
 
-theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
+@[grind =] theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
     o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
   cases o <;> simp
 
@@ -187,13 +216,13 @@ theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → o = some a → Op
     o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
   cases o <;> simp
 
-theorem attach_filter {o : Option α} {p : α → Bool} :
+@[grind =] theorem attach_filter {o : Option α} {p : α → Bool} :
     (o.filter p).attach =
       o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
   cases o with
   | none => simp
   | some a =>
-    simp only [filter_some, attach_some]
+    simp only [Option.filter, attach_some]
     ext
     simp only [attach_eq_some_iff, ite_none_right_eq_some, some.injEq, bind_some,
       dite_none_right_eq_some]
@@ -203,7 +232,12 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
     · rintro ⟨h, rfl⟩
       simp [h]
 
-theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
+@[grind =] theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
+    (o.attachWith P h).filter q =
+      (o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
+  cases o <;> simp [filter_some] <;> split <;> simp
+
+@[grind =] theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
     o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
   cases o <;> simp [filter_some]
 
@@ -211,6 +245,64 @@ theorem toList_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
     (o.pbind f).toList = o.attach.toList.flatMap (fun ⟨x, h⟩ => (f x h).toList) := by
   cases o <;> simp
 
+theorem toArray_pbind {o : Option α} {f : (a : α) → o = some a → Option β} :
+    (o.pbind f).toArray = o.attach.toArray.flatMap (fun ⟨x, h⟩ => (f x h).toArray) := by
+  cases o <;> simp
+
+theorem toList_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+    (o.pfilter p).toList = (o.toList.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pfilter_some, toList_some, List.attach_cons, List.attach_nil, List.map_nil]
+    split <;> rename_i h
+    · rw [List.filter_cons_of_pos h]; simp
+    · rw [List.filter_cons_of_neg h]; simp
+
+theorem toArray_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+    (o.pfilter p).toArray = (o.toArray.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pfilter_some, toArray_some, List.attach_toArray, List.attachWith_mem_toArray,
+      List.attach_cons, List.attach_nil, List.map_nil, List.map_cons, List.size_toArray,
+      List.length_cons, List.length_nil, Nat.zero_add, List.filter_toArray', List.unattach_toArray]
+    split <;> rename_i h
+    · rw [List.filter_cons_of_pos h]; simp
+    · rw [List.filter_cons_of_neg h]; simp
+
+theorem toList_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a → β}
+    (h : ∀ a, o = some a → p a) :
+    (o.pmap f h).toList = o.attach.toList.map (fun x => f x.1 (h _ x.2)) := by
+  cases o <;> simp
+
+theorem toArray_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a → β}
+    (h : ∀ a, o = some a → p a) :
+    (o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
+  cases o <;> simp
+
+@[grind =] theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+    (o.pfilter p).attach =
+      o.attach.pbind fun x h => if h' : p x (by simp_all) then
+        some ⟨x.1, by simpa [pfilter_eq_some_iff] using ⟨_, h'⟩⟩ else none := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [attach_some, eq_mp_eq_cast, id_eq, pbind_some]
+    rw [attach_congr pfilter_some]
+    split <;> simp [*]
+
+theorem attach_guard {p : α → Bool} {x : α} :
+    (guard p x).attach = if h : p x then some ⟨x, by simp_all⟩ else none := by
+  simp only [guard_eq_ite]
+  split <;> simp [*]
+
+theorem attachWith_guard {q : α → Bool} {x : α} {P : α → Prop}
+    {h : ∀ a, guard q x = some a → P a} :
+    (guard q x).attachWith P h = if h' : q x then some ⟨x, h _ (by simp_all)⟩ else none := by
+  simp only [guard_eq_ite]
+  split <;> simp [*]
+
 /-! ## unattach
 
 `Option.unattach` is the (one-sided) inverse of `Option.attach`. It is a synonym for `Option.map Subtype.val`.
@@ -255,6 +347,29 @@ def unattach {α : Type _} {p : α → Prop} (o : Option { x // p x }) := o.map
     (o.attachWith p H).unattach = o := by
   cases o <;> simp
 
+theorem unattach_eq_some_iff {p : α → Prop} {o : Option { x // p x }} {x : α} :
+    o.unattach = some x ↔ ∃ h, o = some ⟨x, h⟩ :=
+  match o with
+  | none => by simp
+  | some ⟨y, h⟩ => by simpa using fun h' => h' ▸ h
+
+@[simp]
+theorem unattach_eq_none_iff {p : α → Prop} {o : Option { x // p x }} :
+    o.unattach = none ↔ o = none := by
+  cases o <;> simp
+
+theorem get_unattach {p : α → Prop} {o : Option { x // p x }} {h} :
+    o.unattach.get h = (o.get (by simpa using h)).1 := by
+  cases o <;> simp
+
+theorem toList_unattach {p : α → Prop} {o : Option { x // p x }} :
+    o.unattach.toList = o.toList.unattach := by
+  cases o <;> simp
+
+theorem toArray_unattach {p : α → Prop} {o : Option { x // p x }} :
+    o.unattach.toArray = o.toArray.unattach := by
+  cases o <;> simp
+
 /-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
 
 /--
@@ -279,4 +394,51 @@ and simplifies these to the function directly taking the value.
   · simp only [filter_some, hf, unattach_some]
     split <;> simp
 
+@[simp] theorem unattach_guard {p : α → Prop} {q : { x // p x } → Bool} {r : α → Bool}
+    (hq : ∀ x h, q ⟨x, h⟩ = r x) {x : { x // p x }} :
+    (guard q x).unattach = guard r x.1 := by
+  simp only [guard]
+  split <;> simp_all
+
+@[simp] theorem unattach_pfilter {p : α → Prop} {o : Option { x // p x }}
+    {f : (a : { x // p x }) → o = some a → Bool}
+    {g : (a : α) → o.unattach = some a → Bool} (hf : ∀ x h h', f ⟨x, h⟩ h' = g x (by simp_all)) :
+    (o.pfilter f).unattach = o.unattach.pfilter g := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [hf, pfilter_some, unattach_some]
+    split <;> simp
+
+@[simp] theorem unattach_merge {p : α → Prop} {f : { x // p x } → { x // p x } → { x // p x }}
+    {g : α → α → α} (hf : ∀ x h y h', (f ⟨x, h⟩ ⟨y, h'⟩).1 = g x y) {o o' : Option { x // p x }} :
+    (o.merge f o').unattach = o.unattach.merge g o'.unattach := by
+  cases o <;> cases o' <;> simp [*]
+
+theorem any_attach {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : o.attach.any q = o.any p := by
+  cases o <;> simp [*]
+
+theorem any_attachWith {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ x, o = some x → r x)
+    {q : { x // r x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : (o.attachWith r hr).any q = o.any p := by
+  cases o <;> simp [*]
+
+theorem any_unattach {p : α → Prop} {o : Option { x // p x }} {q : α → Bool} :
+    o.unattach.any q = o.any (q ∘ Subtype.val) := by
+  cases o <;> simp
+
+theorem all_attach {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : o.attach.all q = o.all p := by
+  cases o <;> simp [*]
+
+theorem all_attachWith {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ x, o = some x → r x)
+    {q : { x // r x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : (o.attachWith r hr).all q = o.all p := by
+  cases o <;> simp [*]
+
+theorem all_unattach {p : α → Prop} {o : Option { x // p x }} {q : α → Bool} :
+    o.unattach.all q = o.all (q ∘ Subtype.val) := by
+  cases o <;> simp
+
 end Option

src/Init/Data/Option/Basic.lean

@@ -8,6 +8,8 @@ module
 prelude
 import Init.Control.Basic
 
+@[expose] section
+
 namespace Option
 
 deriving instance DecidableEq for Option
@@ -100,11 +102,9 @@ From the perspective of `Option` as a collection with at most one element, the m
 is applied to the element if present, and the final result is empty if either the initial or the
 resulting collections are empty.
 -/
-@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
-  if let some a := o then
-    return (← f a)
-  else
-    return none
+@[inline] protected def bindM [Pure m] (f : α → m (Option β)) : Option α → m (Option β)
+  | none => pure none
+  | some a => f a
 
 /--
 Applies a function in some applicative functor to an optional value, returning `none` with no