update expected output

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

.github/PULL_REQUEST_TEMPLATE.md

@@ -5,6 +5,10 @@
 * Include the link to your `RFC` or `bug` issue in the description.
 * If the issue does not already have approval from a developer, submit the PR as draft.
 * The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
+* For `feat/fix` PRs, the first paragraph starting with "This PR" must be present and will become a
+  changelog entry unless the PR is labeled with `no-changelog`. If the PR does not have this label,
+  it must instead be categorized with one of the `changelog-*` labels (which will be done by a
+  reviewer for external PRs).
 * A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
 * If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
 * You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
@@ -12,4 +16,6 @@
 
 ---
 
-Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)
+This PR <short changelog summary for feat/fix, see above>.
+
+Closes <`RFC` or `bug` issue number fixed by this PR, if any>

.github/dependabot.yml

@@ -0,0 +1,8 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "monthly"
+    commit-message:
+      prefix: "chore: CI"

.github/workflows/actionlint.yml

@@ -17,6 +17,6 @@ jobs:
     - name: Checkout
       uses: actions/checkout@v4
     - name: actionlint
-      uses: raven-actions/actionlint@v1
+      uses: raven-actions/actionlint@v2
       with:
         pyflakes: false # we do not use python scripts

.github/workflows/ci.yml

@@ -318,7 +318,7 @@ jobs:
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
       - name: Setup emsdk
-        uses: mymindstorm/setup-emsdk@v12
+        uses: mymindstorm/setup-emsdk@v14
         with:
           version: 3.1.44
           actions-cache-folder: emsdk
@@ -492,7 +492,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -536,7 +536,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/nix-ci.yml

@@ -110,14 +110,6 @@ jobs:
           # https://github.com/netlify/cli/issues/1809
           cp -r --dereference ./result ./dist
         if: matrix.name == 'Nix Linux'
-      - name: Check manual for broken links
-        id: lychee
-        uses: lycheeverse/lychee-action@v1.9.0
-        with:
-          fail: false  # report errors but do not block CI on temporary failures
-          # gmplib.org consistently times out from GH actions
-          # the GitHub token is to avoid rate limiting
-          args: --base './dist' --no-progress --github-token ${{ secrets.GITHUB_TOKEN }} --exclude 'gmplib.org' './dist/**/*.html'
       - name: Rebuild Nix Store Cache
         run: |
           rm -rf nix-store-cache || true
@@ -129,7 +121,7 @@ jobs:
           python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
           echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
       - name: Publish manual to Netlify
-        uses: nwtgck/actions-netlify@v2.0
+        uses: nwtgck/actions-netlify@v3.0
         id: publish-manual
         with:
           publish-dir: ./dist

.github/workflows/pr-body.yml

@@ -0,0 +1,23 @@
+name: Check PR body for changelog convention
+
+on:
+  pull_request:
+    types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
+
+jobs:
+  check-pr-body:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check PR body
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const { title, body, labels, draft } = context.payload.pull_request;
+            if (!draft && /^(feat|fix):/.test(title) && !labels.some(label => label.name == "changelog-no")) {
+              if (!labels.some(label => label.name.startsWith("changelog-"))) {
+                core.setFailed('feat/fix PR must have a `changelog-*` label');
+              }
+              if (!/^This PR [^<]/.test(body)) {
+                core.setFailed('feat/fix PR must have changelog summary starting with "This PR ..." as first line.');
+              }
+            }

.github/workflows/pr-release.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v2 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v6 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -60,7 +60,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -75,7 +75,7 @@ jobs:
 
       - name: Report release status
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v6
+        uses: actions/github-script@v7
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -111,7 +111,7 @@ jobs:
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD
@@ -208,7 +208,7 @@ jobs:
 
       - name: Report mathlib base
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
-        uses: actions/github-script@v6
+        uses: actions/github-script@v7
         with:
           script: |
             const description =

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v8
+      - uses: actions/stale@v9
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

doc/make/index.md

@@ -1,6 +1,6 @@
-These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](doc/dev/index.md).
+These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](../dev/index.md).
 
-We strongly suggest that new users instead follow the [Quickstart](doc/quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
+We strongly suggest that new users instead follow the [Quickstart](../quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
 
 Requirements
 ------------

script/prepare-llvm-linux.sh

@@ -64,7 +64,7 @@ fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -lpthread -ldl -lrt -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests

src/CMakeLists.txt

@@ -17,6 +17,8 @@ set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description li
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)
   string(APPEND LEAN_VERSION_STRING "-${LEAN_SPECIAL_VERSION_DESC}")
+elseif (NOT LEAN_VERSION_IS_RELEASE)
+  string(APPEND LEAN_VERSION_STRING "-pre")
 endif()
 
 set(LEAN_PLATFORM_TARGET "" CACHE STRING "LLVM triple of the target platform")

src/Init.lean

@@ -36,3 +36,4 @@ import Init.Omega
 import Init.MacroTrace
 import Init.Grind
 import Init.While
+import Init.Syntax

src/Init/Control/Lawful/Instances.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Except
 import Init.Control.StateRef
+import Init.Ext
 
 open Function
 
@@ -14,7 +15,7 @@ open Function
 
 namespace ExceptT
 
-theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
   simp [run] at h
   assumption
 
@@ -105,7 +106,7 @@ instance : LawfulFunctor (Except ε) := inferInstance
 
 namespace ReaderT
 
-theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
+@[ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
   simp [run] at h
   exact funext h
 
@@ -167,7 +168,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
 
 namespace StateT
 
-theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
+@[ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   funext h
 
 @[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=

src/Init/Core.lean

@@ -861,16 +861,21 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
 
 /-! # Decidable -/
 
-theorem decide_true_eq_true (h : Decidable True) : @decide True h = true :=
+@[simp] theorem decide_true (h : Decidable True) : @decide True h = true :=
   match h with
   | isTrue _  => rfl
   | isFalse h => False.elim <| h ⟨⟩
 
-theorem decide_false_eq_false (h : Decidable False) : @decide False h = false :=
+@[simp] theorem decide_false (h : Decidable False) : @decide False h = false :=
   match h with
   | isFalse _ => rfl
   | isTrue h  => False.elim h
 
+set_option linter.missingDocs false in
+@[deprecated decide_true (since := "2024-11-05")] abbrev decide_true_eq_true := decide_true
+set_option linter.missingDocs false in
+@[deprecated decide_false (since := "2024-11-05")] abbrev decide_false_eq_false := decide_false
+
 /-- Similar to `decide`, but uses an explicit instance -/
 @[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
   decide (h := d)

src/Init/Data/Array.lean

@@ -17,3 +17,4 @@ import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
 import Init.Data.Array.MapIdx
+import Init.Data.Array.Set

src/Init/Data/Array/Basic.lean

@@ -12,6 +12,7 @@ import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
 import Init.Data.List.ToArray
+import Init.Data.Array.Set
 universe u v w
 
 /-! ### Array literal syntax -/
@@ -29,7 +30,8 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+@[simp] theorem size_set (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (set a i v h).size = a.size :=
   List.length_set ..
 
 @[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@@ -141,7 +143,7 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
    `fset` may be slightly slower than `uset`. -/
 @[extern "lean_array_uset"]
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
-  a.set ⟨i.toNat, h⟩ v
+  a.set i.toNat v h
 
 @[extern "lean_array_pop"]
 def pop (a : Array α) : Array α where
@@ -164,13 +166,14 @@ count of 1 when called.
 -/
 @[extern "lean_array_fswap"]
 def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
-  let v₁ := a.get i
-  let v₂ := a.get j
+  let v₁ := a[i]
+  let v₂ := a[j]
   let a'  := a.set i v₂
-  a'.set (size_set a i v₂ ▸ j) v₁
+  a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
 
 @[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
+  show ((a.set i a[j]).set j a[i]
+    (Nat.lt_of_lt_of_eq j.isLt (size_set a i a[j] _).symm)).size = a.size
   rw [size_set, size_set]
 
 /--
@@ -247,7 +250,7 @@ def back? (a : Array α) : Option α :=
   a.get? (a.size - 1)
 
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
-  let e := a.get i
+  let e := a[i]
   let a := a.set i v
   (e, a)
 
@@ -271,24 +274,22 @@ def take (a : Array α) (n : Nat) : Array α :=
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩
-    let v                := a.get idx
+    let v                := a[i]
     -- Replace a[i] by `box(0)`.  This ensures that `v` remains unshared if possible.
     -- Note: we assume that arrays have a uniform representation irrespective
     -- of the element type, and that it is valid to store `box(0)` in any array.
-    let a'               := a.set idx (unsafeCast ())
+    let a'               := a.set i (unsafeCast ())
     let v ← f v
-    pure <| a'.set (size_set a .. ▸ idx) v
+    pure <| a'.set i v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
   else
     pure a
 
 @[implemented_by modifyMUnsafe]
 def modifyM [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx := ⟨i, h⟩
-    let v   := a.get idx
+    let v   := a[i]
     let v ← f v
-    pure <| a.set idx v
+    pure <| a.set i v
   else
     pure a
 
@@ -453,7 +454,7 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt)))
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
@@ -616,8 +617,7 @@ def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
-    if a.get idx == v then some idx
+    if a[i] == v then some ⟨i, h⟩
     else indexOfAux a v (i+1)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
@@ -742,7 +742,7 @@ where
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
-    if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
+    if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
       popWhile p as.pop
     else
       as
@@ -754,7 +754,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
-      let a := as.get ⟨i, h⟩
+      let a := as[i]
       if p a then
         go (i+1) (r.push a)
       else
@@ -866,6 +866,7 @@ def zip (as : Array α) (bs : Array β) : Array (α × β) :=
 def unzip (as : Array (α × β)) : Array α × Array β :=
   as.foldl (init := (#[], #[])) fun (as, bs) (a, b) => (as.push a, bs.push b)
 
+@[deprecated partition (since := "2024-11-06")]
 def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)

src/Init/Data/Array/BasicAux.lean

@@ -60,7 +60,7 @@ where
       if ptrEq a b then
         go (i+1) as
       else
-        go (i+1) (as.set ⟨i, h⟩ b)
+        go (i+1) (as.set i b h)
     else
       return as
 

src/Init/Data/Array/Bootstrap.lean

@@ -23,7 +23,7 @@ theorem foldlM_eq_foldlM_toList.aux [Monad m]
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
-    rw (occs := .pos [2]) [← List.get_drop_eq_drop _ _ ‹_›]
+    rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
@@ -79,6 +79,17 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
   rw [foldl_eq_foldl_toList]
   induction arr'.toList generalizing arr <;> simp [*]
 
+@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
+
+@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
+  apply ext'; simp only [toList_append, toList_empty, List.append_nil]
+
+@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
+  apply ext'; simp only [toList_append, toList_empty, List.nil_append]
+
+@[simp] theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
+  apply ext'; simp only [toList_append, List.append_assoc]
+
 @[simp] theorem appendList_eq_append
     (arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
 

src/Init/Data/Array/GetLit.lean

@@ -41,6 +41,6 @@ where
   getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
     rfl
   go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop_succ_eq_drop, *]
 
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -10,6 +10,7 @@ import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
@@ -189,6 +190,151 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
   apply ext'
   simp
 
+@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by
+  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 findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeM? f = l.findSomeM? f := by
+  rw [Array.findSomeM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
+    (i : Nat) (h) :
+    findSomeRevM?.find l.toArray f i h = (l.take i).reverse.findSomeM? f := by
+  induction i generalizing l with
+  | zero => simp [Array.findSomeRevM?.find.eq_def]
+  | succ i ih =>
+    rw [size_toArray] at h
+    rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
+    simp only [ih, reverse_append]
+    congr
+    ext1 (_|_) <;> simp
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`.
+theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by
+  simp [Array.findSomeRevM?, findSomeRevM?_find_toArray]
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`.
+theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findRevM? f = l.reverse.findM? f := by
+  rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]
+
+@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findM? f = l.findM? f := by
+  rw [Array.findM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) :
+    l.toArray.findSome? f = l.findSome? f := by
+  rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
+
+@[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
+    l.toArray.find? f = l.find? f := by
+  rw [Array.find?, ← findM?_id, findM?_toArray, Id.run]
+
+theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
+      Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
+  rw [Array.isPrefixOfAux]
+  conv => rhs; rw [Array.isPrefixOfAux]
+  simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail]
+  split <;> rename_i h₁ <;> split <;> rename_i h₂
+  · rw [isPrefixOfAux_toArray_succ]
+  · omega
+  · omega
+  · rfl
+
+theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
+      Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0 := by
+  induction i generalizing l₁ l₂ with
+  | zero => simp [isPrefixOfAux_toArray_succ]
+  | succ i ih =>
+    rw [isPrefixOfAux_toArray_succ, ih]
+    simp
+
+theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 =
+      l₁.isPrefixOf l₂ := by
+  rw [Array.isPrefixOfAux]
+  match l₁, l₂ with
+  | [], _ => rw [dif_neg] <;> simp
+  | _::_, [] => simp at hle
+  | a::l₁, b::l₂ =>
+    simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]
+
+@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
+    l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by
+  rw [Array.isPrefixOf]
+  split <;> rename_i h
+  · simp [isPrefixOfAux_toArray_zero]
+  · simp only [Bool.false_eq]
+    induction l₁ generalizing l₂ with
+    | nil => simp at h
+    | cons a l₁ ih =>
+      cases l₂ with
+      | nil => simp
+      | cons b l₂ =>
+        simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]
+        intro w
+        rw [ih]
+        simp_all
+
+theorem zipWithAux_toArray_succ (f : α → β → γ) (as : List α) (bs : List β) (i : Nat) (cs : Array γ) :
+    zipWithAux f as.toArray bs.toArray (i + 1) cs = zipWithAux f as.tail.toArray bs.tail.toArray i cs := by
+  rw [zipWithAux]
+  conv => rhs; rw [zipWithAux]
+  simp only [size_toArray, getElem_toArray, length_tail, getElem_tail]
+  split <;> rename_i h₁
+  · split <;> rename_i h₂
+    · rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ]
+    · rw [dif_pos (by omega)]
+      rw [dif_neg (by omega)]
+  · rw [dif_neg (by omega)]
+
+theorem zipWithAux_toArray_succ' (f : α → β → γ) (as : List α) (bs : List β) (i : Nat) (cs : Array γ) :
+    zipWithAux f as.toArray bs.toArray (i + 1) cs = zipWithAux f (as.drop (i+1)).toArray (bs.drop (i+1)).toArray 0 cs := by
+  induction i generalizing as bs cs with
+  | zero => simp [zipWithAux_toArray_succ]
+  | succ i ih =>
+    rw [zipWithAux_toArray_succ, ih]
+    simp
+
+theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) :
+    zipWithAux f as.toArray bs.toArray 0 cs = cs ++ (List.zipWith f as bs).toArray := by
+  rw [Array.zipWithAux]
+  match as, bs with
+  | [], _ => simp
+  | _, [] => simp
+  | a :: as, b :: bs =>
+    simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]
+
+@[simp] theorem zipWith_toArray (f : α → β → γ) (as : List α) (bs : List β) :
+    Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by
+  rw [Array.zipWith]
+  simp [zipWithAux_toArray_zero]
+
+@[simp] theorem zip_toArray (as : List α) (bs : List β) :
+    Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by
+  simp [Array.zip, zipWith_toArray, zip]
+
 end List
 
 namespace Array
@@ -246,7 +392,7 @@ where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
     unfold mapM.map; split
-    · rw [← List.get_drop_eq_drop _ i ‹_›]
+    · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
       simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
@@ -304,7 +450,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
-@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
+@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
 
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
@@ -337,25 +483,26 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 
 /-! # set -/
 
-@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
-      (eq : i.val = j) (p : j < (a.set i v).size) :
+@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
+      (eq : i = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
   simp [set, getElem_eq_getElem_toList, ←eq]
 
-@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
-    (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
+@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
+    (pj : j < (a.set i v).size) (h : i ≠ j) :
+    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
-theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
+theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v ▸ h) := by
-  by_cases p : i.1 = j <;> simp [p]
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
+  by_cases p : i = j <;> simp [p]
 
-@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
+    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
 
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
+    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
 /-! # setD -/
@@ -372,7 +519,7 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
 @[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
     (setD a i v)[i]'h = v := by
   simp at h
-  simp only [setD, h, dite_true, getElem_set, ite_true]
+  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
 
 @[simp]
 theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
@@ -547,47 +694,47 @@ theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some
 
 @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
 
-@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
+@[simp] theorem toList_set (a : Array α) (i v h) : (a.set i v).toList = a.toList.set i v := rfl
 
-theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1] = v := by
+theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (a.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
 
-theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
+theorem get?_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (a.set i v)[i]? = v := by simp [getElem?_pos, h]
 
-@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (h : i.1 ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem get?_set_ne (a : Array α) (i : Nat) (h' : i < a.size) {j : Nat} (v : α)
+    (h : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
 
-theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
-    (a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
+theorem get?_set (a : Array α) (i : Nat) (h : i < a.size) (j : Nat) (v : α) :
+    (a.set i v)[j]? = if i = j then some v else a[j]? := by
+  if h : i = j then subst j; simp [*] else simp [*]
 
-theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
+theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) :
     (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
+  if h : i = j then subst j; simp [*] else simp [*]
 
-@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
-    (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
+@[simp] theorem get_set_ne (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size)
+    (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
     (setD a i v)[i] = v := by
   simp at h
-  simp only [setD, h, dite_true, get_set, ite_true]
+  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
 
-theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
-    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
+theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
+    (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
 
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Fin a.size) :
-    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
+    a.swap i j = (a.set i a[j]).set j a[i] := by
   simp [swap, fin_cast_val]
 
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
-    (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
+    (a.swap i j).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
 
 theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
     if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
@@ -601,7 +748,7 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
 
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
+    a.swapAt! i v = (a[i], a.set i v) := by simp [swapAt!, h]
 
 @[simp] theorem size_swapAt! (a : Array α) (i : Nat) (v : α) :
     (a.swapAt! i v).2.size = a.size := by
@@ -966,7 +1113,7 @@ theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
     (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
   simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
   split
-  · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
+  · simp only [Id.bind_eq, get_set _ _ _ _ (by simpa using h)]; split <;> simp [*]
   · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
 @[simp] theorem toList_modify (as : Array α) (f : α → α) :
@@ -1050,8 +1197,6 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
-
 /-! ### append -/
 
 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@@ -1101,15 +1246,6 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
   · exact getElem?_append_left h
   · exact getElem?_append_right (by simpa using h)
 
-@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
-  apply ext'; simp only [toList_append, toList_empty, List.append_nil]
-
-@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
-  apply ext'; simp only [toList_append, toList_empty, List.nil_append]
-
-@[simp] theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
-  apply ext'; simp only [toList_append, List.append_assoc]
-
 /-! ### flatten -/
 
 @[simp] theorem toList_flatten {l : Array (Array α)} :
@@ -1406,30 +1542,15 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
 
 open Fin
 
-@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
-  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
+@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.1] = a[i] := by
+  simp [swap_def, getElem_set]
 
-@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
-  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
-    simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
-  else by
-    apply Eq.trans
-    · apply Array.get_set_ne
-      · simp only [size_set, Fin.isLt]
-      · assumption
-    · simp [get_set_ne]
+@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.1] = a[j] := by
+  simp +contextual [swap_def, getElem_set]
 
 @[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
     (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
-  apply Eq.trans
-  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
-    apply Array.get_set_ne
-    · simp only [this]
-      apply Ne.symm
-      · assumption
-  · apply Array.get_set_ne
-    · apply Ne.symm
-      · assumption
+  simp [swap_def, getElem_set, hi.symm, hj.symm]
 
 theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
     (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
@@ -1460,6 +1581,54 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
+/-! ### eraseIdx -/
+
+theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
+    a.feraseIdx i = a.eraseIdx i.1 := by
+  simp [eraseIdx]
+
+/-! ### isPrefixOf -/
+
+@[simp] theorem isPrefixOf_toList [BEq α] {as bs : Array α} :
+    as.toList.isPrefixOf bs.toList = as.isPrefixOf bs := by
+  cases as
+  cases bs
+  simp
+
+/-! ### zipWith -/
+
+@[simp] theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
+    (Array.zipWith as bs f).toList = List.zipWith f as.toList bs.toList := by
+  cases as
+  cases bs
+  simp
+
+@[simp] theorem toList_zip (as : Array α) (bs : Array β) :
+    (Array.zip as bs).toList = List.zip as.toList bs.toList := by
+  simp [zip, toList_zipWith, List.zip]
+
+/-! ### findSomeM?, findM?, findSome?, find? -/
+
+@[simp] theorem findSomeM?_toList [Monad m] [LawfulMonad m] (p : α → m (Option β)) (as : Array α) :
+    as.toList.findSomeM? p = as.findSomeM? p := by
+  cases as
+  simp
+
+@[simp] theorem findM?_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    as.toList.findM? p = as.findM? p := by
+  cases as
+  simp
+
+@[simp] theorem findSome?_toList (p : α → Option β) (as : Array α) :
+    as.toList.findSome? p = as.findSome? p := by
+  cases as
+  simp
+
+@[simp] theorem find?_toList (p : α → Bool) (as : Array α) :
+    as.toList.find? p = as.find? p := by
+  cases as
+  simp
+
 end Array
 
 open Array
@@ -1475,11 +1644,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 @[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
   simp
 
-@[simp] theorem push_append_toArray (as : Array α) (a : α) (l : List α) :
-    as.push a ++ l.toArray = as ++ (a :: l).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
   apply ext'
   simp
@@ -1611,7 +1775,7 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
+@[simp] theorem extract_toArray (l : List α) (start stop : Nat) :
     l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
   apply ext'
   simp
@@ -1619,6 +1783,64 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
 @[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
   ext <;> simp
 
+theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
+    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
+  rw [takeWhile.go, takeWhile.go]
+  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+    getElem_toArray, getElem_cons_succ]
+  split
+  rw [takeWhile_go_succ]
+  rfl
+
+theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
+    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
+  induction l generalizing i r with
+  | nil => simp [takeWhile.go]
+  | cons a l ih =>
+    rw [takeWhile.go]
+    cases i with
+    | zero =>
+      simp [takeWhile_go_succ, ih, takeWhile_cons]
+      split <;> simp
+    | succ i =>
+      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+        getElem_toArray, getElem_cons_succ, drop_succ_cons]
+      split <;> rename_i h₁
+      · rw [takeWhile_go_succ, ih]
+        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
+        split <;> simp_all
+      · simp_all [drop_eq_nil_of_le]
+
+@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
+    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
+  simp [Array.takeWhile, takeWhile_go_toArray]
+
+@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
+    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
+  rw [feraseIdx]
+  split <;> rename_i h
+  · rw [feraseIdx_toArray]
+    simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
+    rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
+    simp
+  · rcases i with ⟨i, w⟩
+    simp at h w
+    have t : i = l.length - 1 := by omega
+    simp [t]
+termination_by l.length - i
+decreasing_by
+  rename_i h
+  simp at h
+  simp
+  omega
+
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
+  split
+  · simp
+  · simp_all [eraseIdx_eq_self.2]
+
 end List
 
 namespace Array
@@ -1629,6 +1851,84 @@ namespace Array
 @[simp] theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f := by
   apply List.ext_getElem <;> simp
 
+@[simp] theorem toList_takeWhile (p : α → Bool) (as : Array α) :
+    (as.takeWhile p).toList = as.toList.takeWhile p := by
+  induction as; simp
+
+@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
+    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
+  induction as
+  simp
+
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
+    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
+  induction as
+  simp
+
+/-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
+
+@[simp] theorem findSomeRevM?_eq_findSomeM?_reverse
+    [Monad m] [LawfulMonad m] (f : α → m (Option β)) (as : Array α) :
+    as.findSomeRevM? f = as.reverse.findSomeM? f := by
+  cases as
+  rw [List.findSomeRevM?_toArray]
+  simp
+
+@[simp] theorem findRevM?_eq_findM?_reverse
+    [Monad m] [LawfulMonad m] (f : α → m Bool) (as : Array α) :
+    as.findRevM? f = as.reverse.findM? f := by
+  cases as
+  rw [List.findRevM?_toArray]
+  simp
+
+@[simp] theorem findSomeRev?_eq_findSome?_reverse (f : α → Option β) (as : Array α) :
+    as.findSomeRev? f = as.reverse.findSome? f := by
+  cases as
+  simp [findSomeRev?, Id.run]
+
+@[simp] theorem findRev?_eq_find?_reverse (f : α → Bool) (as : Array α) :
+    as.findRev? f = as.reverse.find? f := by
+  cases as
+  simp [findRev?, Id.run]
+
+/-! ### unzip -/
+
+@[simp] theorem fst_unzip (as : Array (α × β)) : (Array.unzip as).fst = as.map Prod.fst := by
+  simp only [unzip]
+  rcases as with ⟨as⟩
+  simp only [List.foldl_toArray']
+  rw [← List.foldl_hom (f := Prod.fst) (g₂ := fun bs x => bs.push x.1) (H := by simp), ← List.foldl_map]
+  simp
+
+@[simp] theorem snd_unzip (as : Array (α × β)) : (Array.unzip as).snd = as.map Prod.snd := by
+  simp only [unzip]
+  rcases as with ⟨as⟩
+  simp only [List.foldl_toArray']
+  rw [← List.foldl_hom (f := Prod.snd) (g₂ := fun bs x => bs.push x.2) (H := by simp), ← List.foldl_map]
+  simp
+
+end Array
+
+namespace List
+
+@[simp] theorem unzip_toArray (as : List (α × β)) :
+    as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by
+  ext1 <;> simp
+
+end List
+
+namespace Array
+
+@[simp] theorem toList_fst_unzip (as : Array (α × β)) :
+    as.unzip.1.toList = as.toList.unzip.1 := by
+  cases as
+  simp
+
+@[simp] theorem toList_snd_unzip (as : Array (α × β)) :
+    as.unzip.2.toList = as.toList.unzip.2 := by
+  cases as
+  simp
+
 end Array
 
 /-! ### Deprecations -/
@@ -1737,8 +2037,8 @@ abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
 
 @[deprecated getElem_modify (since := "2024-08-08")]
 theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
-    (arr.modify x f).get ⟨i, h⟩ =
-    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
+    (arr.modify x f).get i h =
+    if x = i then f (arr.get i (by simpa using h)) else arr.get i (by simpa using h) := by
   simp [getElem_modify h]
 
 @[deprecated toList_filter (since := "2024-09-09")]

src/Init/Data/Array/Mem.lean

@@ -14,12 +14,12 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
 
-theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
   cases as with | _ as =>
-  exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
+  simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)
 
 @[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
-  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _ h
 
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions

src/Init/Data/Array/Set.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Tactics
+
+
+/--
+Set an element in an array, using a proof that the index is in bounds.
+(This proof can usually be omitted, and will be synthesized automatically.)
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
+@[extern "lean_array_fset"]
+def Array.set (a : Array α) (i : @& Nat) (v : α) (h : i < a.size := by get_elem_tactic) :
+    Array α where
+  toList := a.toList.set i v
+
+/--
+Set an element in an array, or do nothing if the index is out of bounds.
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
+@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=
+  dite (LT.lt i a.size) (fun h => a.set i v h) (fun _ => a)
+
+/--
+Set an element in an array, or panic if the index is out of bounds.
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
+@[extern "lean_array_set"]
+def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
+  Array.setD a i v

src/Init/Data/Array/Subarray.lean

@@ -48,7 +48,7 @@ instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
-  if h : i < s.size then s.get ⟨i, h⟩ else v₀
+  if h : i < s.size then s[i] else v₀
 
 abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
   getD s i default

src/Init/Data/BitVec/Bitblast.lean

@@ -76,7 +76,7 @@ to prove the correctness of the circuit that is built by `bv_decide`.
 def blastMul (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w
 theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment) :
    ...
-   ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
+   ⟦(blastMul aig input).aig, (blastMul aig input).vec[idx], assign.toAIGAssignment⟧
      =
    (lhs * rhs).getLsbD idx
 ```
@@ -180,7 +180,7 @@ theorem carry_succ_one (i : Nat) (x : BitVec w) (h : 0 < w) :
   | zero => simp [carry_succ, h]
   | succ i ih =>
     rw [carry_succ, ih]
-    simp only [getLsbD_one, add_one_ne_zero, decide_False, Bool.and_false, atLeastTwo_false_mid]
+    simp only [getLsbD_one, add_one_ne_zero, decide_false, Bool.and_false, atLeastTwo_false_mid]
     cases hx : x.getLsbD (i+1)
     case false =>
       have : ∃ j ≤ i + 1, x.getLsbD j = false :=
@@ -249,7 +249,7 @@ theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool
     [ Nat.testBit_mod_two_pow,
       Nat.testBit_mul_two_pow_add_eq,
       i_lt,
-      decide_True,
+      decide_true,
       Bool.true_and,
       Nat.add_assoc,
       Nat.add_left_comm (_%_) (_ * _) _,
@@ -392,7 +392,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} :
   by_cases hi : i < w
   · rw [getLsbD_add hi]
     have : 0 < w := by omega
-    simp only [getLsbD_not, hi, decide_True, Bool.true_and, getLsbD_one, this, not_bne,
+    simp only [getLsbD_not, hi, decide_true, Bool.true_and, getLsbD_one, this, not_bne,
       _root_.true_and, not_eq_eq_eq_not]
     cases i with
     | zero =>
@@ -401,7 +401,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} :
       simp [hi, carry_zero]
     | succ =>
       rw [carry_succ_one _ _ (by omega), ← Bool.xor_not, ← decide_not]
-      simp only [add_one_ne_zero, decide_False, getLsbD_not, and_eq_true, decide_eq_true_eq,
+      simp only [add_one_ne_zero, decide_false, getLsbD_not, and_eq_true, decide_eq_true_eq,
         not_eq_eq_eq_not, Bool.not_true, false_bne, not_exists, _root_.not_and, not_eq_true,
         bne_left_inj, decide_eq_decide]
       constructor
@@ -419,7 +419,7 @@ theorem getMsbD_neg {i : Nat} {x : BitVec w} :
     simp [hi]; omega
   case pos =>
     have h₁ : w - 1 - i < w := by omega
-    simp only [hi, decide_True, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide]
+    simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide]
     constructor
     · rintro ⟨j, hj, h⟩
       refine ⟨w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h⟩
@@ -455,7 +455,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
         apply hmin
         apply eq_of_getMsbD_eq
         rintro ⟨i, hi⟩
-        simp only [getMsbD_intMin, w_pos, decide_True, Bool.true_and]
+        simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and]
         cases i
         case zero => exact hmsb
         case succ => exact getMsbD_x _ hi (by omega)
@@ -476,7 +476,7 @@ theorem msb_abs {w : Nat} {x : BitVec w} :
   by_cases h₀ : 0 < w
   · by_cases h₁ : x = intMin w
     · simp [h₁, msb_intMin]
-    · simp only [neg_eq, h₁, decide_False]
+    · simp only [neg_eq, h₁, decide_false]
       by_cases h₂ : x.msb
       · simp [h₂, msb_neg]
         and_intros
@@ -566,18 +566,18 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
       setWidth w (x.setWidth i) + (x &&& twoPow w i) := by
   rw [add_eq_or_of_and_eq_zero]
   · ext k
-    simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
+    simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
     by_cases hik : i = k
     · subst hik
       simp
-    · simp only [getLsbD_twoPow, hik, decide_False, Bool.and_false, Bool.or_false]
+    · simp only [getLsbD_twoPow, hik, decide_false, Bool.and_false, Bool.or_false]
       by_cases hik' : k < (i + 1)
       · have hik'' : k < i := by omega
         simp [hik', hik'']
       · have hik'' : ¬ (k < i) := by omega
         simp [hik', hik'']
   · ext k
-    simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and,
+    simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and,
       getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]
     by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
 
@@ -1092,8 +1092,8 @@ def sshiftRightRec (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁ :
 
 @[simp]
 theorem sshiftRightRec_zero_eq (x : BitVec w₁) (y : BitVec w₂) :
-    sshiftRightRec x y 0 = x.sshiftRight' (y &&& 1#w₂) := by
-  simp only [sshiftRightRec, twoPow_zero]
+    sshiftRightRec x y 0 = x.sshiftRight' (y &&& twoPow w₂ 0) := by
+  simp only [sshiftRightRec]
 
 @[simp]
 theorem sshiftRightRec_succ_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :

src/Init/Data/BitVec/Folds.lean

@@ -65,7 +65,7 @@ theorem iunfoldr_getLsbD' {f : Fin w → α → α × Bool} (state : Nat → α)
     intro
     apply And.intro
     · intro i
-      have := Fin.size_pos i
+      have := Fin.pos i
       contradiction
     · rfl
   case step =>

src/Init/Data/BitVec/Lemmas.lean

@@ -123,7 +123,7 @@ theorem getMsbD_eq_getLsbD (x : BitVec w) (i : Nat) : x.getMsbD i = (decide (i <
 theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i)) := by
   rw [getMsbD]
   by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
-    simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
+    simp only [h₁, h₂] <;> simp only [decide_true, decide_false, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
   · congr
     omega
   all_goals
@@ -386,7 +386,7 @@ theorem msb_eq_getLsbD_last (x : BitVec w) :
     · simp [Nat.div_eq_of_lt h, h]
     · simp only [h]
       rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
-      · decide
+      · simp
       · omega
 
 @[bv_toNat] theorem getLsbD_succ_last (x : BitVec (w + 1)) :
@@ -512,6 +512,31 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
     subst h
     simp
 
+@[simp]
+theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
+  simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]
+
+/-! ### slt -/
+
+/--
+A bitvector, when interpreted as an integer, is less than zero iff
+its most significant bit is true.
+-/
+theorem slt_zero_iff_msb_cond (x : BitVec w) : x.slt 0#w ↔ x.msb = true := by
+  have := toInt_eq_msb_cond x
+  constructor
+  · intros h
+    apply Classical.byContradiction
+    intros hmsb
+    simp only [Bool.not_eq_true] at hmsb
+    simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this
+    simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h
+    omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
+  · intros h
+    simp only [h, ↓reduceIte] at this
+    simp [BitVec.slt, this]
+    omega
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]
@@ -633,7 +658,7 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
 @[simp] theorem setWidth_setWidth_of_le (x : BitVec w) (h : k ≤ l) :
     (x.setWidth l).setWidth k = x.setWidth k := by
   ext i
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and]
   have p := lt_of_getLsbD (x := x) (i := i)
   revert p
   cases getLsbD x i <;> simp; omega
@@ -663,7 +688,7 @@ theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
 theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
   ext ⟨i, hilt⟩
-  simp only [getLsbD_setWidth, hilt, decide_True, getLsbD_ofNat, Bool.true_and,
+  simp only [getLsbD_setWidth, hilt, decide_true, getLsbD_ofNat, Bool.true_and,
     Bool.and_iff_right_iff_imp, decide_eq_true_eq]
   intros hi₁
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
@@ -735,9 +760,9 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 
 @[simp] theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n := by
   ext
-  simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_True]
+  simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_true]
   rw [Fin.add_def]
-  simp only [Nat.testBit_mod_two_pow, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [Nat.testBit_mod_two_pow, Fin.is_lt, decide_true, Bool.true_and]
   have h : (x : Nat) + (2 ^ n - (x + 1)) = 2 ^ n - 1 := by omega
   rw [h, Nat.testBit_two_pow_sub_one]
   simp
@@ -1089,21 +1114,21 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
   ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_xor]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_xor]
   by_cases h : i < n
     <;> simp [h]
 
 theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
   ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_and]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_and]
   by_cases h : i < n
     <;> simp [h]
 
 theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
   ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or]
   by_cases h : i < n
     <;> simp [h]
 
@@ -1114,9 +1139,9 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
   · subst h; simp
   have t : w - 1 - k < w := by omega
   simp only [t]
-  simp only [decide_True, Nat.sub_sub, Bool.true_and, Nat.add_assoc]
+  simp only [decide_true, Nat.sub_sub, Bool.true_and, Nat.add_assoc]
   by_cases h₁ : k < w <;> by_cases h₂ : w - (1 + k) < i <;> by_cases h₃ : k + i < w
-    <;> simp only [h₁, h₂, h₃, decide_False, h₂, decide_True, Bool.not_true, Bool.false_and, Bool.and_self,
+    <;> simp only [h₁, h₂, h₃, decide_false, h₂, decide_true, Bool.not_true, Bool.false_and, Bool.and_self,
       Bool.true_and, Bool.false_eq, Bool.false_and, Bool.not_false]
     <;> (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
@@ -1160,7 +1185,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
 theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
     x <<< (n + m) = (x <<< n) <<< m := by
   ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and]
   rw [show i - (n + m) = (i - m - n) by omega]
   cases h₂ : decide (i < m) <;>
   cases h₃ : decide (i - m < w) <;>
@@ -1258,7 +1283,8 @@ theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
   · simp [getLsbD_ge, show w ≤ (n + (w - 1 - i)) by omega]
     omega
   · by_cases h₁ : i < w
-    · simp only [h, ushiftRight_eq, getLsbD_ushiftRight, show i - n < w by omega]
+    · simp only [h, decide_false, Bool.not_false, show i - n < w by omega, decide_true,
+        Bool.true_and]
       congr
       omega
     · simp [h, h₁]
@@ -1327,17 +1353,17 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
   rcases hmsb : x.msb with rfl | rfl
   · simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right]
     by_cases hi : i ≥ w
-    · simp only [hi, decide_True, Bool.not_true, Bool.false_and]
+    · simp only [hi, decide_true, Bool.not_true, Bool.false_and]
       apply getLsbD_ge
       omega
-    · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self,
+    · simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.iff_and_self,
         decide_eq_true_eq]
       intros hlsb
       apply BitVec.lt_of_getLsbD hlsb
   · by_cases hi : i ≥ w
     · simp [hi]
     · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and,
-        Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and,
+        Bool.not_not, hi, decide_false, Bool.not_false, Bool.if_true_right, Bool.true_and,
         Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
         Nat.not_lt, decide_eq_true_eq]
       omega
@@ -1382,7 +1408,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
   rw [msb_eq_getLsbD_last, getLsbD_sshiftRight, msb_eq_getLsbD_last]
   by_cases hw₀ : w = 0
   · simp [hw₀]
-  · simp only [show ¬(w ≤ w - 1) by omega, decide_False, Bool.not_false, Bool.true_and,
+  · simp only [show ¬(w ≤ w - 1) by omega, decide_false, Bool.not_false, Bool.true_and,
       ite_eq_right_iff]
     intros h
     simp [show n = 0 by omega]
@@ -1401,7 +1427,7 @@ theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
   simp only [getLsbD_sshiftRight, Nat.add_assoc]
   by_cases h₁ : w ≤ (i : Nat)
   · simp [h₁]
-  · simp only [h₁, decide_False, Bool.not_false, Bool.true_and]
+  · simp only [h₁, decide_false, Bool.not_false, Bool.true_and]
     by_cases h₂ : n + ↑i < w
     · simp [h₂]
     · simp only [h₂, ↓reduceIte]
@@ -1413,7 +1439,7 @@ theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
 theorem not_sshiftRight {b : BitVec w} :
     ~~~b.sshiftRight n = (~~~b).sshiftRight n := by
   ext i
-  simp only [getLsbD_not, Fin.is_lt, decide_True, getLsbD_sshiftRight, Bool.not_and, Bool.not_not,
+  simp only [getLsbD_not, Fin.is_lt, decide_true, getLsbD_sshiftRight, Bool.not_and, Bool.not_not,
     Bool.true_and, msb_not]
   by_cases h : w ≤ i
   <;> by_cases h' : n + i < w
@@ -1431,15 +1457,15 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
     getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by
   simp only [getMsbD, BitVec.getLsbD_sshiftRight]
   by_cases h : i < w
-  · simp only [h, decide_True, Bool.true_and]
+  · simp only [h, decide_true, Bool.true_and]
     by_cases h₁ : w ≤ w - 1 - i
     · simp [h₁]
       omega
-    · simp only [h₁, decide_False, Bool.not_false, Bool.true_and]
+    · simp only [h₁, decide_false, Bool.not_false, Bool.true_and]
       by_cases h₂ : i < n
       · simp only [h₂, ↓reduceIte, ite_eq_right_iff]
         omega
-      · simp only [show i - n < w by omega, h₂, ↓reduceIte, decide_True, Bool.true_and]
+      · simp only [show i - n < w by omega, h₂, ↓reduceIte, decide_true, Bool.true_and]
         by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega)
   · simp [h]
 
@@ -1459,15 +1485,15 @@ theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
     (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by
   simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight]
   by_cases h : i < w
-  · simp only [h, decide_True, Bool.true_and]
+  · simp only [h, decide_true, Bool.true_and]
     by_cases h₁ : w ≤ w - 1 - i
     · simp [h₁]
       omega
-    · simp only [h₁, decide_False, Bool.not_false, Bool.true_and]
+    · simp only [h₁, decide_false, Bool.not_false, Bool.true_and]
       by_cases h₂ : i < y.toNat
       · simp only [h₂, ↓reduceIte, ite_eq_right_iff]
         omega
-      · simp only [show i - y.toNat < w by omega, h₂, ↓reduceIte, decide_True, Bool.true_and]
+      · simp only [show i - y.toNat < w by omega, h₂, ↓reduceIte, decide_true, Bool.true_and]
         by_cases h₄ : y.toNat + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega)
   · simp [h]
 
@@ -1492,11 +1518,11 @@ theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hm
     x.signExtend v = x.setWidth v := by
   ext i
   by_cases hv : i < v
-  · simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_True, Bool.true_and, toNat_ofInt,
+  · simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_true, Bool.true_and, toNat_ofInt,
       BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]
     rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
     simp [BitVec.testBit_toNat]
-  · simp only [getLsbD_setWidth, hv, decide_False, Bool.false_and]
+  · simp only [getLsbD_setWidth, hv, decide_false, Bool.false_and]
     apply getLsbD_ge
     omega
 
@@ -1538,7 +1564,7 @@ theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
   ext i
-  simp only [getLsbD_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_setWidth,
+  simp only [getLsbD_signExtend, Fin.is_lt, decide_true, Bool.true_and, getLsbD_setWidth,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
@@ -1622,7 +1648,7 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
   apply eq_of_getLsbD_eq
   intro i
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_append, Bool.true_and]
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, Bool.true_and]
   split
   · have t : i < v := by omega
     simp [t]
@@ -1634,7 +1660,7 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
   subst h
   ext i
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_append, cond_eq_if,
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, cond_eq_if,
     decide_eq_true_eq, Bool.true_and, setWidth_eq]
   split
   · simp_all
@@ -1705,13 +1731,13 @@ theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
 
 theorem getLsbD_rev (x : BitVec w) (i : Fin w) :
     x.getLsbD i.rev = x.getMsbD i := by
-  simp only [getLsbD, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [getLsbD, Fin.val_rev, getMsbD, Fin.is_lt, decide_true, Bool.true_and]
   congr 1
   omega
 
 theorem getElem_rev {x : BitVec w} {i : Fin w}:
     x[i.rev] = x.getMsbD i := by
-  simp only [Fin.getElem_fin, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [Fin.getElem_fin, Fin.val_rev, getMsbD, Fin.is_lt, decide_true, Bool.true_and]
   congr 1
   omega
 
@@ -1741,7 +1767,7 @@ theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
   · have p1 : ¬(n ≤ i) := by omega
     have p2 : i ≠ n := by omega
     simp [p1, p2]
-  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero,
+  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
     Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte]
     cases b <;> trivial
   · have p1 : i ≠ n := by omega
@@ -1756,7 +1782,7 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
   · have p1 : ¬(n ≤ i) := by omega
     have p2 : i ≠ n := by omega
     simp [p1, p2]
-  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero,
+  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
     Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte]
     cases b <;> trivial
   · have p1 : i ≠ n := by omega
@@ -1776,7 +1802,7 @@ theorem setWidth_succ (x : BitVec w) :
     setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
   apply eq_of_getLsbD_eq
   intro j
-  simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_True, Bool.true_and]
+  simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_true, Bool.true_and]
   if j_eq : j.val = i then
     simp [j_eq]
   else
@@ -1884,7 +1910,7 @@ theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
 theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
     n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by
   ext i
-  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_true, Bool.true_and]
   split
   · simp [*]
   · congr 1; omega
@@ -1925,7 +1951,7 @@ theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} :
   · simp [h₀]
   · by_cases h₁ : i < w
     · simp [h₀, h₁, show ¬ w - i = 0 by omega, show i < w + 1 by omega, Nat.sub_sub, Nat.add_comm]
-    · simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_False, Bool.false_and,
+    · simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_false, Bool.false_and,
         Bool.and_eq_false_imp, decide_eq_true_eq]
       intro
       omega
@@ -1933,10 +1959,10 @@ theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} :
 @[simp]
 theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
     (x.concat b).msb = if 0 < w then x.msb else b := by
-  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_True, Nat.add_one_sub_one,
+  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_true, Nat.add_one_sub_one,
     Nat.sub_zero, Bool.true_and]
   by_cases h₀ : 0 < w
-  · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_True,
+  · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_true,
       Bool.true_and, ite_eq_right_iff]
     intro
     omega
@@ -2026,9 +2052,9 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
 
 @[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
 
-@[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
+theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
   rfl
-@[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
+theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
   rfl
 
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
@@ -2375,6 +2401,9 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
 theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
   simp [smtUDiv]
 
+@[simp]
+theorem smtUDiv_zero {x : BitVec n} : x.smtUDiv 0#n = allOnes n := rfl
+
 /-! ### sdiv -/
 
 /-- Equation theorem for `sdiv` in terms of `udiv`. -/
@@ -2442,6 +2471,10 @@ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
   rw [BitVec.smtSDiv]
   rcases x.msb <;> rcases y.msb <;> simp
 
+@[simp]
+theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by
+  rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond x, hx, ← negOne_eq_allOnes]
+
 /-! ### srem -/
 
 theorem srem_eq (x y : BitVec w) : srem x y =
@@ -2506,7 +2539,7 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
 @[simp] theorem getElem_ofBoolListBE (h : i < bs.length) :
     (ofBoolListBE bs)[i] = bs[bs.length - 1 - i] := by
   rw [← getLsbD_eq_getElem, getLsbD_ofBoolListBE]
-  simp only [h, decide_True, List.getD_eq_getElem?_getD, Bool.true_and]
+  simp only [h, decide_true, List.getD_eq_getElem?_getD, Bool.true_and]
   rw [List.getElem?_eq_getElem (by omega)]
   simp
 
@@ -2694,6 +2727,9 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
 
 /- ## twoPow -/
 
+theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by
+  dsimp [twoPow]
+
 @[simp, bv_toNat]
 theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
   rcases w with rfl | w
@@ -2708,7 +2744,7 @@ theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j
   · simp
   · simp only [twoPow, getLsbD_shiftLeft, getLsbD_ofNat]
     by_cases hj : j < i
-    · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
+    · simp only [hj, decide_true, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
       Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
       omega
     · by_cases hi : Nat.testBit 1 (j - i)
@@ -2771,7 +2807,15 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
 theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
     x <<< n = x * (BitVec.twoPow w n) := by
   ext i
-  simp [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, mul_twoPow_eq_shiftLeft]
+  simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
+
+/--
+The unsigned division of `x` by `2^k` equals shifting `x` right by `k`,
+when `k` is less than the bitwidth `w`.
+-/
+theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x / (twoPow w k) = x >>> k := by
+  have : 2^k < 2^w := Nat.pow_lt_pow_of_lt (by decide) hk
+  simp [bv_toNat, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt this]
 
 /- ### cons -/
 
@@ -2799,7 +2843,7 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) := by
   ext k
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -2815,7 +2859,7 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) ||| (twoPow w i) := by
   ext k
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -2825,7 +2869,7 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
 theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
     (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
   ext i
-  simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool,
+  simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_ofBool,
     Bool.true_and]
   by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
 
@@ -2862,13 +2906,13 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
   case succ n ih =>
     simp only [replicate_succ_eq, getLsbD_cast, getLsbD_append]
     by_cases hi : i < w * (n + 1)
-    · simp only [hi, decide_True, Bool.true_and]
+    · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
       · simp [hi', ih]
-      · simp only [hi', decide_False, cond_false]
+      · simp only [hi', decide_false, cond_false]
         rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
     · rw [Nat.mul_succ] at hi ⊢
-      simp only [show ¬i < w * n by omega, decide_False, cond_false, hi, Bool.false_and]
+      simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
       apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
 
 @[simp]
@@ -2929,7 +2973,7 @@ theorem toInt_intMin_le (x : BitVec w) :
     apply Int.le_bmod (by omega)
 
 theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by
-  simp only [BitVec.sle, toInt_intMin_le x, decide_True]
+  simp only [BitVec.sle, toInt_intMin_le x, decide_true]
 
 @[simp]
 theorem neg_intMin {w : Nat} : -intMin w = intMin w := by

src/Init/Data/ByteArray/Basic.lean

@@ -42,7 +42,7 @@ def usize (a : @& ByteArray) : USize :=
   a.size.toUSize
 
 @[extern "lean_byte_array_uget"]
-def uget : (a : @& ByteArray) → (i : USize) → i.toNat < a.size → UInt8
+def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, h => bs[i]
 
 @[extern "lean_byte_array_get"]
@@ -50,11 +50,11 @@ def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs.get! i
 
 @[extern "lean_byte_array_fget"]
-def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
-  | ⟨bs⟩, i => bs.get i
+def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
+  | ⟨bs⟩, i, _ => bs[i]
 
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i
 
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
@@ -64,11 +64,11 @@ def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
 @[extern "lean_byte_array_fset"]
-def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
-  | ⟨bs⟩, i, b => ⟨bs.set i b⟩
+def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
+  | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
 
 @[extern "lean_byte_array_uset"]
-def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray
+def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
 @[extern "lean_byte_array_hash"]
@@ -144,7 +144,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
       have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
       have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
       have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-      match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
+      match (← f as[as.size - 1 - i] b) with
       | ForInStep.done b  => pure b
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
@@ -178,7 +178,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
         match i with
         | 0    => pure b
         | i'+1 =>
-          loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
+          loop i' (j+1) (← f b as[j])
       else
         pure b
     loop (stop - start) start init

src/Init/Data/Fin/Basic.lean

@@ -165,6 +165,7 @@ theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (modn i m).val < m
 theorem val_lt_of_le (i : Fin b) (h : b ≤ n) : i.val < n :=
   Nat.lt_of_lt_of_le i.isLt h
 
+/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
 protected theorem pos (i : Fin n) : 0 < n :=
   Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
 

src/Init/Data/Fin/Lemmas.lean

@@ -13,17 +13,19 @@ import Init.Omega
 
 namespace Fin
 
-/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
-theorem size_pos (i : Fin n) : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
+@[deprecated Fin.pos (since := "2024-11-11")]
+theorem size_pos (i : Fin n) : 0 < n := i.pos
 
 theorem mod_def (a m : Fin n) : a % m = Fin.mk (a % m) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
   rfl
 
-theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % n) (Nat.mod_lt _ a.size_pos) := rfl
+theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % n) (Nat.mod_lt _ a.pos) := rfl
 
-theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b) + a) % n) (Nat.mod_lt _ a.size_pos) := rfl
+theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b) + a) % n) (Nat.mod_lt _ a.pos) := rfl
 
-theorem size_pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.size_pos
+theorem pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.pos
+
+@[deprecated pos' (since := "2024-11-11")] abbrev size_pos' := @pos'
 
 @[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
 
@@ -240,7 +242,7 @@ theorem fin_one_eq_zero (a : Fin 1) : a = 0 := Subsingleton.elim a 0
   rw [eq_comm]
   simp
 
-theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.size_pos) := rfl
+theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.pos) := rfl
 
 theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl
 

src/Init/Data/FloatArray/Basic.lean

@@ -46,8 +46,8 @@ def uget : (a : @& FloatArray) → (i : USize) → i.toNat < a.size → Float
   | ⟨ds⟩, i, h => ds[i]
 
 @[extern "lean_float_array_fget"]
-def get : (ds : @& FloatArray) → (@& Fin ds.size) → Float
-  | ⟨ds⟩, i => ds.get i
+def get : (ds : @& FloatArray) → (i : @& Nat) → (h : i < ds.size := by get_elem_tactic) → Float
+  | ⟨ds⟩, i, h => ds.get i h
 
 @[extern "lean_float_array_get"]
 def get! : (@& FloatArray) → (@& Nat) → Float
@@ -55,23 +55,23 @@ def get! : (@& FloatArray) → (@& Nat) → Float
 
 def get? (ds : FloatArray) (i : Nat) : Option Float :=
   if h : i < ds.size then
-    ds.get ⟨i, h⟩
+    some (ds.get i h)
   else
     none
 
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i h
 
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
 @[extern "lean_float_array_uset"]
-def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
+def uset : (a : FloatArray) → (i : USize) → Float → (h : i.toNat < a.size := by get_elem_tactic) → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩
 
 @[extern "lean_float_array_fset"]
-def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
-  | ⟨ds⟩, i, d => ⟨ds.set i d⟩
+def set : (ds : FloatArray) → (i : @& Nat) → Float → (h : i < ds.size := by get_elem_tactic) → FloatArray
+  | ⟨ds⟩, i, d, h => ⟨ds.set i d h⟩
 
 @[extern "lean_float_array_set"]
 def set! : FloatArray → (@& Nat) → Float → FloatArray
@@ -83,7 +83,7 @@ def isEmpty (s : FloatArray) : Bool :=
 partial def toList (ds : FloatArray) : List Float :=
   let rec loop (i r) :=
     if h : i < ds.size then
-      loop (i+1) (ds.get ⟨i, h⟩ :: r)
+      loop (i+1) (ds[i] :: r)
     else
       r.reverse
   loop 0 []
@@ -115,7 +115,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA
       have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
       have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
       have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-      match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
+      match (← f as[as.size - 1 - i] b) with
       | ForInStep.done b  => pure b
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
@@ -149,7 +149,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float →
         match i with
         | 0    => pure b
         | i'+1 =>
-          loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
+          loop i' (j+1) (← f b (as[j]'(Nat.lt_of_lt_of_le hlt h)))
       else
         pure b
     loop (stop - start) start init

src/Init/Data/List/Basic.lean

@@ -38,7 +38,7 @@ The operations are organized as follow:
 * Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
   `isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`,
   `rotateLeft` and `rotateRight`.
-* Manipulating elements: `replace`, `insert`, `modify`, `erase`, `eraseP`, `eraseIdx`.
+* Manipulating elements: `replace`, `modify`, `insert`, `insertIdx`, `erase`, `eraseP`, `eraseIdx`.
 * Finding elements: `find?`, `findSome?`, `findIdx`, `indexOf`, `findIdx?`, `indexOf?`,
  `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
@@ -1113,12 +1113,6 @@ theorem replace_cons [BEq α] {a : α} :
     (a::as).replace b c = match b == a with | true => c::as | false => a :: replace as b c :=
   rfl
 
-/-! ### insert -/
-
-/-- Inserts an element into a list without duplication. -/
-@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
-  if l.elem a then l else a :: l
-
 /-! ### modify -/
 
 /--
@@ -1148,6 +1142,21 @@ Apply `f` to the nth element of the list, if it exists, replacing that element w
 def modify (f : α → α) : Nat → List α → List α :=
   modifyTailIdx (modifyHead f)
 
+/-! ### insert -/
+
+/-- Inserts an element into a list without duplication. -/
+@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
+  if l.elem a then l else a :: l
+
+/--
+`insertIdx n a l` inserts `a` into the list `l` after the first `n` elements of `l`
+```
+insertIdx 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
+```
+-/
+def insertIdx (n : Nat) (a : α) : List α → List α :=
+  modifyTailIdx (cons a) n
+
 /-! ### erase -/
 
 /--

src/Init/Data/List/Control.lean

@@ -5,6 +5,8 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Control.Basic
+import Init.Control.Id
+import Init.Control.Lawful
 import Init.Data.List.Basic
 
 namespace List
@@ -207,6 +209,16 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
     | true  => pure (some a)
     | false => findM? p as
 
+@[simp]
+theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [findM?, find?]
+    cases p a with
+    | true  => rfl
+    | false => rw [ih]; rfl
+
 @[specialize]
 def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)
   | []    => pure none
@@ -215,6 +227,28 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
     | some b => pure (some b)
     | none   => findSomeM? f as
 
+@[simp]
+theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [findSomeM?, findSome?]
+    cases f a with
+    | some b => rfl
+    | none   => rw [ih]; rfl
+
+theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
+    as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [findM?, findSomeM?]
+    simp [ih]
+    congr
+    apply funext
+    intro b
+    cases b <;> simp
+
 @[inline] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
     | [], b, _    => pure b

src/Init/Data/List/Find.lean

@@ -206,7 +206,8 @@ theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (
 @[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
   induction l <;> simp [find?_cons]; split <;> simp [*]
 
-theorem find?_eq_some : xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ a ∈ as, !p a := by
+theorem find?_eq_some_iff_append :
+    xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ a ∈ as, !p a := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
@@ -242,6 +243,9 @@ theorem find?_eq_some : xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b
           cases h₁
           simp
 
+@[deprecated find?_eq_some_iff_append (since := "2024-11-06")]
+abbrev find?_eq_some := @find?_eq_some_iff_append
+
 @[simp]
 theorem find?_cons_eq_some : (a :: xs).find? p = some b ↔ (p a ∧ a = b) ∨ (!p a ∧ xs.find? p = some b) := by
   rw [find?_cons]
@@ -347,7 +351,7 @@ theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
     xs.flatten.find? p = some a ↔
       p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧
         (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
-  rw [find?_eq_some]
+  rw [find?_eq_some_iff_append]
   constructor
   · rintro ⟨h, ⟨ys, zs, h₁, h₂⟩⟩
     refine ⟨h, ?_⟩

src/Init/Data/List/Impl.lean

@@ -38,7 +38,7 @@ The following operations were already given `@[csimp]` replacements in `Init/Dat
 
 The following operations are given `@[csimp]` replacements below:
 `set`, `filterMap`, `foldr`, `append`, `bind`, `join`,
-`take`, `takeWhile`, `dropLast`, `replace`, `modify`, `erase`, `eraseIdx`, `zipWith`,
+`take`, `takeWhile`, `dropLast`, `replace`, `modify`, `insertIdx`, `erase`, `eraseIdx`, `zipWith`,
 `enumFrom`, and `intercalate`.
 
 -/
@@ -215,6 +215,23 @@ theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f
 @[csimp] theorem modify_eq_modifyTR : @modify = @modifyTR := by
   funext α f n l; simp [modifyTR, modifyTR_go_eq]
 
+/-! ### insertIdx -/
+
+/-- Tail-recursive version of `insertIdx`. -/
+@[inline] def insertIdxTR (n : Nat) (a : α) (l : List α) : List α := go n l #[] where
+  /-- Auxiliary for `insertIdxTR`: `insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l`. -/
+  go : Nat → List α → Array α → List α
+  | 0, l, acc => acc.toListAppend (a :: l)
+  | _, [], acc => acc.toList
+  | n+1, a :: l, acc => go n l (acc.push a)
+
+theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l
+  | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx]
+  | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l]
+
+@[csimp] theorem insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR := by
+  funext α f n l; simp [insertIdxTR, insertIdxTR_go_eq]
+
 /-! ### erase -/
 
 /-- Tail recursive version of `List.erase`. -/

src/Init/Data/List/Lemmas.lean

@@ -863,14 +863,30 @@ theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α
     (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
   induction l generalizing init <;> simp [*]
 
-theorem foldl_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
+theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldl_cons]
+    cases f a <;> simp [ih]
+
+theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldr_cons]
+    cases f a <;> simp [ih]
+
+theorem foldl_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
     (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
     (l.map g).foldl f' (g a) = g (l.foldl f a) := by
   induction l generalizing a
   · simp
   · simp [*, h]
 
-theorem foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
+theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
     (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
     (l.map g).foldr f' (g a) = g (l.foldr f a) := by
   induction l generalizing a
@@ -983,6 +999,21 @@ theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β →
     · simp
     · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
 
+@[simp] theorem foldl_add_const (l : List α) (a b : Nat) :
+    l.foldl (fun x _ => x + a) b = b + a * l.length := by
+  induction l generalizing b with
+  | nil => simp
+  | cons y l ih =>
+    simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
+      Nat.add_comm a]
+
+@[simp] theorem foldr_add_const (l : List α) (a b : Nat) :
+    l.foldr (fun _ x => x + a) b = b + a * l.length := by
+  induction l generalizing b with
+  | nil => simp
+  | cons y l ih =>
+    simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc]
+
 /-! ### getLast -/
 
 theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
@@ -1457,6 +1488,22 @@ theorem forall_mem_filter {l : List α} {p : α → Bool} {P : α → Prop} :
   | [] => rfl
   | a :: l => by by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]
 
+theorem foldl_filter (p : α → Bool) (f : β → α → β) (l : List α) (init : β) :
+    (l.filter p).foldl f init = l.foldl (fun x y => if p y then f x y else x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldl_cons]
+    split <;> simp [ih]
+
+theorem foldr_filter (p : α → Bool) (f : α → β → β) (l : List α) (init : β) :
+    (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldr_cons]
+    split <;> simp [ih]
+
 theorem filter_map (f : β → α) (l : List β) : filter p (map f l) = map f (filter (p ∘ f) l) := by
   induction l with
   | nil => rfl
@@ -2700,6 +2747,12 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla
     l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
   (foldl_reverse ..).symm.trans <| by simp
 
+theorem foldl_eq_foldr_reverse (l : List α) (f : β → α → β) (b) :
+    l.foldl f b = l.reverse.foldr (fun x y => f y x) b := by simp
+
+theorem foldr_eq_foldl_reverse (l : List α) (f : α → β → β) (b) :
+    l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by simp
+
 @[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
   eq_replicate_iff.2
     ⟨by rw [length_reverse, length_replicate],
@@ -2843,6 +2896,10 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
     l.contains a ↔ ∃ a' ∈ l, a == a' := by
   induction l <;> simp_all
 
+theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+    l.contains a ↔ a ∈ l := by
+  simp
+
 /-! ## Sublists -/
 
 /-! ### partition

src/Init/Data/List/Monadic.lean

@@ -86,6 +86,42 @@ theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂
     (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
   induction l generalizing g init <;> simp [*]
 
+theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldlM g init =
+      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldlM_cons]
+    cases f a <;> simp [ih]
+
+theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldrM g init =
+      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldrM_cons]
+    cases f a <;> simp [ih]
+
+theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : List α) (init : β) :
+    (l.filter p).foldlM g init =
+      l.foldlM (fun x y => if p y then g x y else pure x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldlM_cons]
+    split <;> simp [ih]
+
+theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : List α) (init : β) :
+    (l.filter p).foldrM g init =
+      l.foldrM (fun x y => if p x then g x y else pure y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldrM_cons]
+    split <;> simp [ih]
+
 /-! ### forM -/
 
 -- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
@@ -172,8 +208,8 @@ in which whenever we reach `.done b` we keep that value through the rest of the
 theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
     (l : List α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
     forIn' l init f = ForInStep.value <$>
-      l.attach.foldlM (fun b a => match b with
-        | .yield b => f a.1 a.2 b
+      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
+        | .yield b => f a m b
         | .done b => pure (.done b)) (ForInStep.yield init) := by
   induction l generalizing init with
   | nil => simp
@@ -198,6 +234,31 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
     | .yield b =>
       simp [ih, List.foldlM_map]
 
+/-- We can express a for loop over a list which always yields as a fold. -/
+@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : List α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
+    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
+      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
+  simp only [forIn'_eq_foldlM]
+  generalize l.attach = l'
+  induction l' generalizing init <;> simp_all
+
+theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : List α) (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' l init (fun a m b => pure (.yield (f a m b))) =
+      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
+  simp only [forIn'_eq_foldlM]
+  generalize l.attach = l'
+  induction l' generalizing init <;> simp_all
+
+@[simp] 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]
+  generalize l.attach = l'
+  induction l' generalizing init <;> simp_all
+
 /--
 We can express a for loop over a list as a fold,
 in which whenever we reach `.done b` we keep that value through the rest of the fold.
@@ -224,6 +285,28 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
     | .yield b =>
       simp [ih]
 
+/-- We can express a for loop over a list which always yields as a fold. -/
+@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : List α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
+    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
+      l.foldlM (fun b a => g a b <$> f a b) init := by
+  simp only [forIn_eq_foldlM]
+  induction l generalizing init <;> simp_all
+
+theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : List α) (f : α → β → β) (init : β) :
+    forIn l init (fun a b => pure (.yield (f a b))) =
+      pure (f := m) (l.foldl (fun b a => f a b) init) := by
+  simp only [forIn_eq_foldlM]
+  induction l generalizing init <;> simp_all
+
+@[simp] 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
+
 /-! ### allM -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :

src/Init/Data/List/Nat.lean

@@ -14,3 +14,4 @@ import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Find
 import Init.Data.List.Nat.BEq
 import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.InsertIdx

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

@@ -64,3 +64,82 @@ theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.era
     (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
   rw [getElem_eraseIdx, dif_neg]
   omega
+
+theorem eraseIdx_set_eq {l : List α} {i : Nat} {a : α} :
+    (l.set i a).eraseIdx i = l.eraseIdx i := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx, getElem_eraseIdx]
+    split <;>
+    · rw [getElem_set_ne]
+      omega
+
+theorem eraseIdx_set_lt {l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · split
+      · split
+        · rfl
+        · omega
+      · split
+        · omega
+        · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i - 1 ≠ n := by omega
+        simp [t]
+
+theorem eraseIdx_set_gt {l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i ≠ n := by omega
+        simp [t]
+
+@[simp] theorem set_getElem_succ_eraseIdx_succ
+    {l : List α} {i : Nat} (h : i + 1 < l.length) :
+    (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by
+  apply ext_getElem
+  · simp only [length_set, length_eraseIdx, h, ↓reduceIte]
+    rw [if_pos]
+    omega
+  · intro n h₁ h₂
+    simp [getElem_set, getElem_eraseIdx]
+    split
+    · split
+      · omega
+      · simp_all
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : ¬ n < i := by omega
+        simp [t]
+
+@[simp] theorem eraseIdx_length_sub_one (l : List α) :
+    (l.eraseIdx (l.length - 1)) = l.dropLast := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+    omega
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx_of_lt, getElem_dropLast]
+    simp_all
+
+end List

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

@@ -9,6 +9,32 @@ import Init.Data.List.Find
 
 namespace List
 
+open Nat
+
+theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
+    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j] := by
+  rw [find?_eq_some_iff_append]
+  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
+  intro w
+  constructor
+  · rintro ⟨as, ⟨bs, rfl⟩, h⟩
+    refine ⟨as.length, ⟨?_, ?_, ?_⟩⟩
+    · simp only [length_append, length_cons]
+      refine Nat.lt_add_of_pos_right (zero_lt_succ bs.length)
+    · rw [getElem_append_right (Nat.le_refl as.length)]
+      simp
+    · intro j h'
+      rw [getElem_append_left h']
+      exact h _ (getElem_mem h')
+  · rintro ⟨i, h, rfl, h'⟩
+    refine ⟨xs.take i, ⟨xs.drop (i+1), ?_⟩, ?_⟩
+    · rw [getElem_cons_drop, take_append_drop]
+    · intro a m
+      rw [mem_take_iff_getElem] at m
+      obtain ⟨j, h, rfl⟩ := m
+      apply h'
+      omega
+
 theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
     (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j := by
   simp only [findIdx?_eq_findSome?_enum] at h

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

@@ -0,0 +1,242 @@
+/-
+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
+-/
+prelude
+import Init.Data.List.Nat.Modify
+
+/-!
+# insertIdx
+
+Proves various lemmas about `List.insertIdx`.
+-/
+
+open Function
+
+open Nat
+
+namespace List
+
+universe u
+
+variable {α : Type u}
+
+section InsertIdx
+
+variable {a : α}
+
+@[simp]
+theorem insertIdx_zero (s : List α) (x : α) : insertIdx 0 x s = x :: s :=
+  rfl
+
+@[simp]
+theorem insertIdx_succ_nil (n : Nat) (a : α) : insertIdx (n + 1) a [] = [] :=
+  rfl
+
+@[simp]
+theorem insertIdx_succ_cons (s : List α) (hd x : α) (n : Nat) :
+    insertIdx (n + 1) x (hd :: s) = hd :: insertIdx n x s :=
+  rfl
+
+theorem length_insertIdx : ∀ n as, (insertIdx n a as).length = if n ≤ as.length then as.length + 1 else as.length
+  | 0, _ => by simp
+  | n + 1, [] => by simp
+  | n + 1, a :: as => by
+    simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_le_add_iff_right]
+    split <;> rfl
+
+theorem length_insertIdx_of_le_length (h : n ≤ length as) : length (insertIdx n a as) = length as + 1 := by
+  simp [length_insertIdx, h]
+
+theorem length_insertIdx_of_length_lt (h : length as < n) : length (insertIdx n a as) = length as := by
+  simp [length_insertIdx, h]
+
+theorem eraseIdx_insertIdx (n : Nat) (l : List α) : (l.insertIdx n a).eraseIdx n = l := by
+  rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
+  exact modifyTailIdx_id _ _
+
+theorem insertIdx_eraseIdx_of_ge :
+    ∀ n m as,
+      n < length as → n ≤ m → insertIdx m a (as.eraseIdx n) = (as.insertIdx (m + 1) a).eraseIdx n
+  | 0, 0, [], has, _ => (Nat.lt_irrefl _ has).elim
+  | 0, 0, _ :: as, _, _ => by simp [eraseIdx, insertIdx]
+  | 0, _ + 1, _ :: _, _, _ => rfl
+  | n + 1, m + 1, a :: as, has, hmn =>
+    congrArg (cons a) <|
+      insertIdx_eraseIdx_of_ge n m as (Nat.lt_of_succ_lt_succ has) (Nat.le_of_succ_le_succ hmn)
+
+theorem insertIdx_eraseIdx_of_le :
+    ∀ n m as,
+      n < length as → m ≤ n → insertIdx m a (as.eraseIdx n) = (as.insertIdx m a).eraseIdx (n + 1)
+  | _, 0, _ :: _, _, _ => rfl
+  | n + 1, m + 1, a :: as, has, hmn =>
+    congrArg (cons a) <|
+      insertIdx_eraseIdx_of_le n m as (Nat.lt_of_succ_lt_succ has) (Nat.le_of_succ_le_succ hmn)
+
+theorem insertIdx_comm (a b : α) :
+    ∀ (i j : Nat) (l : List α) (_ : i ≤ j) (_ : j ≤ length l),
+      (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a
+  | 0, j, l => by simp [insertIdx]
+  | _ + 1, 0, _ => fun h => (Nat.not_lt_zero _ h).elim
+  | i + 1, j + 1, [] => by simp
+  | i + 1, j + 1, c :: l => fun h₀ h₁ => by
+    simp only [insertIdx_succ_cons, cons.injEq, true_and]
+    exact insertIdx_comm a b i j l (Nat.le_of_succ_le_succ h₀) (Nat.le_of_succ_le_succ h₁)
+
+theorem mem_insertIdx {a b : α} :
+    ∀ {n : Nat} {l : List α} (_ : n ≤ l.length), a ∈ l.insertIdx n b ↔ a = b ∨ a ∈ l
+  | 0, as, _ => by simp
+  | _ + 1, [], h => (Nat.not_succ_le_zero _ h).elim
+  | n + 1, a' :: as, h => by
+    rw [List.insertIdx_succ_cons, mem_cons, mem_insertIdx (Nat.le_of_succ_le_succ h),
+      ← or_assoc, @or_comm (a = a'), or_assoc, mem_cons]
+
+theorem insertIdx_of_length_lt (l : List α) (x : α) (n : Nat) (h : l.length < n) :
+    insertIdx n x l = l := by
+  induction l generalizing n with
+  | nil =>
+    cases n
+    · simp at h
+    · simp
+  | cons x l ih =>
+    cases n
+    · simp at h
+    · simp only [Nat.succ_lt_succ_iff, length] at h
+      simpa using ih _ h
+
+@[simp]
+theorem insertIdx_length_self (l : List α) (x : α) : insertIdx l.length x l = l ++ [x] := by
+  induction l with
+  | nil => simp
+  | cons x l ih => simpa using ih
+
+theorem length_le_length_insertIdx (l : List α) (x : α) (n : Nat) :
+    l.length ≤ (insertIdx n x l).length := by
+  simp only [length_insertIdx]
+  split <;> simp
+
+theorem length_insertIdx_le_succ (l : List α) (x : α) (n : Nat) :
+    (insertIdx n x l).length ≤ l.length + 1 := by
+  simp only [length_insertIdx]
+  split <;> simp
+
+theorem getElem_insertIdx_of_lt {l : List α} {x : α} {n k : Nat} (hn : k < n)
+    (hk : k < (insertIdx n x l).length) :
+    (insertIdx n x l)[k] = l[k]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
+  induction n generalizing k l with
+  | zero => simp at hn
+  | succ n ih =>
+    cases l with
+    | nil => simp
+    | cons _ _=>
+      cases k
+      · simp [get]
+      · rw [Nat.succ_lt_succ_iff] at hn
+        simpa using ih hn _
+
+@[simp]
+theorem getElem_insertIdx_self {l : List α} {x : α} {n : Nat} (hn : n < (insertIdx n x l).length) :
+    (insertIdx n x l)[n] = x := by
+  induction l generalizing n with
+  | nil =>
+    simp [length_insertIdx] at hn
+    split at hn
+    · simp_all
+    · omega
+  | cons _ _ ih =>
+    cases n
+    · simp
+    · simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_lt_add_iff_right] at hn ih
+      simpa using ih hn
+
+theorem getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (hn : n + 1 ≤ k)
+    (hk : k < (insertIdx n x l).length) :
+    (insertIdx n x l)[k] = l[k - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
+  induction l generalizing n k with
+  | nil =>
+    cases n with
+    | zero =>
+      simp only [insertIdx_zero, length_singleton, lt_one_iff] at hk
+      omega
+    | succ n => simp at hk
+  | cons _ _ ih =>
+    cases n with
+    | zero =>
+      simp only [insertIdx_zero] at hk
+      cases k with
+      | zero => omega
+      | succ k => simp
+    | succ n =>
+      cases k with
+      | zero => simp
+      | succ k =>
+        simp only [insertIdx_succ_cons, getElem_cons_succ]
+        rw [ih (by omega)]
+        cases k with
+        | zero => omega
+        | succ k => simp
+
+theorem getElem_insertIdx {l : List α} {x : α} {n k : Nat} (h : k < (insertIdx n x l).length) :
+    (insertIdx n x l)[k] =
+      if h₁ : k < n then
+        l[k]'(by simp [length_insertIdx] at h; split at h <;> omega)
+      else
+        if h₂ : k = n then
+          x
+        else
+          l[k-1]'(by simp [length_insertIdx] at h; split at h <;> omega) := by
+  split <;> rename_i h₁
+  · rw [getElem_insertIdx_of_lt h₁]
+  · split <;> rename_i h₂
+    · subst h₂
+      rw [getElem_insertIdx_self h]
+    · rw [getElem_insertIdx_of_ge (by omega)]
+
+theorem getElem?_insertIdx {l : List α} {x : α} {n k : Nat} :
+    (insertIdx n x l)[k]? =
+      if k < n then
+        l[k]?
+      else
+        if k = n then
+          if k ≤ l.length then some x else none
+        else
+          l[k-1]? := by
+  rw [getElem?_def]
+  split <;> rename_i h
+  · rw [getElem_insertIdx h]
+    simp only [length_insertIdx] at h
+    split <;> rename_i h₁
+    · rw [getElem?_def, dif_pos]
+    · split <;> rename_i h₂
+      · rw [if_pos]
+        split at h <;> omega
+      · rw [getElem?_def]
+        simp only [Option.some_eq_dite_none_right, exists_prop, and_true]
+        split at h <;> omega
+  · simp only [length_insertIdx] at h
+    split <;> rename_i h₁
+    · rw [getElem?_eq_none]
+      split at h <;> omega
+    · split <;> rename_i h₂
+      · rw [if_neg]
+        split at h <;> omega
+      · rw [getElem?_eq_none]
+        split at h <;> omega
+
+theorem getElem?_insertIdx_of_lt {l : List α} {x : α} {n k : Nat} (h : k < n) :
+    (insertIdx n x l)[k]? = l[k]? := by
+  rw [getElem?_insertIdx, if_pos h]
+
+theorem getElem?_insertIdx_self {l : List α} {x : α} {n : Nat} :
+    (insertIdx n x l)[n]? = if n ≤ l.length then some x else none := by
+  rw [getElem?_insertIdx, if_neg (by omega)]
+  simp
+
+theorem getElem?_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (h : n + 1 ≤ k) :
+    (insertIdx n x l)[k]? = l[k - 1]? := by
+  rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
+
+end InsertIdx
+
+end List

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

@@ -110,6 +110,25 @@ theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h :
     ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
   ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
 
+theorem modifyTailIdx_modifyTailIdx {f g : List α → List α} (m : Nat) :
+    ∀ (n) (l : List α),
+      (l.modifyTailIdx f n).modifyTailIdx g (m + n) =
+        l.modifyTailIdx (fun l => (f l).modifyTailIdx g m) n
+  | 0, _ => rfl
+  | _ + 1, [] => rfl
+  | n + 1, a :: l => congrArg (List.cons a) (modifyTailIdx_modifyTailIdx m n l)
+
+theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (m n : Nat) (l : List α)
+    (h : n ≤ m) :
+    (l.modifyTailIdx f n).modifyTailIdx g m =
+      l.modifyTailIdx (fun l => (f l).modifyTailIdx g (m - n)) n := by
+  rcases Nat.exists_eq_add_of_le h with ⟨m, rfl⟩
+  rw [Nat.add_comm, modifyTailIdx_modifyTailIdx, Nat.add_sub_cancel]
+
+theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) (l : List α) :
+    (l.modifyTailIdx f n).modifyTailIdx g n = l.modifyTailIdx (g ∘ f) n := by
+  rw [modifyTailIdx_modifyTailIdx_le n n l (Nat.le_refl n), Nat.sub_self]; rfl
+
 /-! ### modify -/
 
 @[simp] theorem modify_nil (f : α → α) (n) : [].modify f n = [] := by cases n <;> rfl

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

@@ -108,7 +108,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
 
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
-  rw [find?_eq_some]
+  rw [find?_eq_some_iff_append]
   simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_range'_1,
     and_congr_right_iff]
   simp only [range'_eq_append_iff, eq_comm (a := i :: _), range'_eq_cons_iff]
@@ -282,7 +282,7 @@ theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
 
 @[simp] theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j := by
-  rw [find?_eq_some]
+  rw [find?_eq_some_iff_append]
   simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
     nil_append, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_reverse, mem_range'_1,
     and_congr_right_iff]

src/Init/Data/List/OfFn.lean

@@ -52,4 +52,29 @@ protected theorem getElem?_ofFn (f : Fin n → α) (i) : (ofFn f)[i]? = if h : i
     rw [dif_neg] <;>
     simpa using h
 
+/-- `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)
+
+@[simp]
+theorem ofFn_succ {n} (f : Fin (n + 1) → α) : ofFn f = f 0 :: ofFn fun i => f i.succ :=
+  ext_get (by simp) (fun i hi₁ hi₂ => by
+    cases i
+    · simp
+    · simp)
+
+@[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]
+
+theorem head_ofFn {n} (f : Fin n → α) (h : ofFn f ≠ []) :
+    (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by
+  rw [← getElem_zero (length_ofFn _ ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),
+    List.getElem_ofFn]
+
+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]
+
 end List

src/Init/Data/List/Perm.lean

@@ -114,6 +114,14 @@ theorem Perm.length_eq {l₁ l₂ : List α} (p : l₁ ~ l₂) : length l₁ = l
   | swap => rfl
   | trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]
 
+theorem Perm.contains_eq [BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) {a : α} :
+    l₁.contains a = l₂.contains a := by
+  induction h with
+  | nil => rfl
+  | cons => simp_all
+  | swap => simp only [contains_cons, ← Bool.or_assoc, Bool.or_comm]
+  | trans => simp_all
+
 theorem Perm.eq_nil {l : List α} (p : l ~ []) : l = [] := eq_nil_of_length_eq_zero p.length_eq
 
 theorem Perm.nil_eq {l : List α} (p : [] ~ l) : [] = l := p.symm.eq_nil.symm

src/Init/Data/List/TakeDrop.lean

@@ -190,7 +190,7 @@ theorem set_drop {l : List α} {n m : Nat} {a : α} :
 theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
     (l.take i).concat l[i] = l.take (i+1) :=
   Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
-    rw [concat_eq_append, append_assoc, singleton_append, get_drop_eq_drop, take_append_drop]
+    rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]
 
 @[deprecated take_succ_cons (since := "2024-07-25")]
 theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl

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

@@ -357,7 +357,7 @@ theorem testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : testBit (2 ^ n) m = f
   | zero => simp
   | succ n =>
     rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega)), mod_two_eq_one_iff_testBit_zero, testBit_two_pow_sub_one ]
-    simp only [zero_lt_succ, decide_True]
+    simp only [zero_lt_succ, decide_true]
 
 @[simp] theorem mod_two_pos_mod_two_eq_one : x % 2 ^ j % 2 = 1 ↔ (0 < j) ∧ x % 2 = 1 := by
   rw [mod_two_eq_one_iff_testBit_zero, testBit_mod_two_pow]

src/Init/Data/Repr.lean

@@ -162,7 +162,7 @@ private def reprArray : Array String := Id.run do
   List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
-  if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else
+  if h : n < 128 then Nat.reprArray.get n h else
   if h : n < USize.size then (USize.ofNatCore n h).repr
   else (toDigits 10 n).asString
 

src/Init/Data/SInt/Basic.lean

@@ -52,6 +52,18 @@ structure Int64 where
   -/
   toUInt64 : UInt64
 
+/--
+A `ISize` is a signed integer with the size of a word for the platform's architecture.
+
+For example, if running on a 32-bit machine, ISize is equivalent to `Int32`.
+Or on a 64-bit machine, `Int64`.
+-/
+structure ISize where
+  /--
+  Obtain the `USize` that is 2's complement equivalent to the `ISize`.
+  -/
+  toUSize : USize
+
 /-- The size of type `Int8`, that is, `2^8 = 256`. -/
 abbrev Int8.size : Nat := 256
 
@@ -463,3 +475,114 @@ instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
 instance (a b : Int64) : Decidable (a ≤ b) := Int64.decLe a b
 instance : Max Int64 := maxOfLe
 instance : Min Int64 := minOfLe
+
+/-- The size of type `ISize`, that is, `2^System.Platform.numBits`. -/
+abbrev ISize.size : Nat := 2^System.Platform.numBits
+
+/--
+Obtain the `BitVec` that contains the 2's complement representation of the `ISize`.
+-/
+@[inline] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
+
+@[extern "lean_isize_of_int"]
+def ISize.ofInt (i : @& Int) : ISize := ⟨⟨BitVec.ofInt System.Platform.numBits i⟩⟩
+@[extern "lean_isize_of_nat"]
+def ISize.ofNat (n : @& Nat) : ISize := ⟨⟨BitVec.ofNat System.Platform.numBits n⟩⟩
+abbrev Int.toISize := ISize.ofInt
+abbrev Nat.toISize := ISize.ofNat
+@[extern "lean_isize_to_int"]
+def ISize.toInt (i : ISize) : Int := i.toBitVec.toInt
+/--
+This function has the same behavior as `Int.toNat` for negative numbers.
+If you want to obtain the 2's complement representation use `toBitVec`.
+-/
+@[inline] def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
+@[extern "lean_isize_to_int32"]
+def ISize.toInt32 (a : ISize) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
+/--
+Upcast `ISize` to `Int64`. This function is losless as `ISize` is either `Int32` or `Int64`.
+-/
+@[extern "lean_isize_to_int64"]
+def ISize.toInt64 (a : ISize) : Int64 := ⟨⟨a.toBitVec.signExtend 64⟩⟩
+/--
+Upcast `Int32` to `ISize`. This function is losless as `ISize` is either `Int32` or `Int64`.
+-/
+@[extern "lean_int32_to_isize"]
+def Int32.toISize (a : Int32) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
+@[extern "lean_int64_to_isize"]
+def Int64.toISize (a : Int64) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
+@[extern "lean_isize_neg"]
+def ISize.neg (i : ISize) : ISize := ⟨⟨-i.toBitVec⟩⟩
+
+instance : ToString ISize where
+  toString i := toString i.toInt
+
+instance : OfNat ISize n := ⟨ISize.ofNat n⟩
+instance : Neg ISize where
+  neg := ISize.neg
+
+@[extern "lean_isize_add"]
+def ISize.add (a b : ISize) : ISize := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
+@[extern "lean_isize_sub"]
+def ISize.sub (a b : ISize) : ISize := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
+@[extern "lean_isize_mul"]
+def ISize.mul (a b : ISize) : ISize := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
+@[extern "lean_isize_div"]
+def ISize.div (a b : ISize) : ISize := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_isize_mod"]
+def ISize.mod (a b : ISize) : ISize := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_isize_land"]
+def ISize.land (a b : ISize) : ISize := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
+@[extern "lean_isize_lor"]
+def ISize.lor (a b : ISize) : ISize := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
+@[extern "lean_isize_xor"]
+def ISize.xor (a b : ISize) : ISize := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
+@[extern "lean_isize_shift_left"]
+def ISize.shiftLeft (a b : ISize) : ISize := ⟨⟨a.toBitVec <<< (b.toBitVec.smod System.Platform.numBits)⟩⟩
+@[extern "lean_isize_shift_right"]
+def ISize.shiftRight (a b : ISize) : ISize := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod System.Platform.numBits)⟩⟩
+@[extern "lean_isize_complement"]
+def ISize.complement (a : ISize) : ISize := ⟨⟨~~~a.toBitVec⟩⟩
+
+@[extern "lean_isize_dec_eq"]
+def ISize.decEq (a b : ISize) : Decidable (a = b) :=
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ =>
+    if h : n = m then
+      isTrue <| h ▸ rfl
+    else
+      isFalse (fun h' => ISize.noConfusion h' (fun h' => absurd h' h))
+
+def ISize.lt (a b : ISize) : Prop := a.toBitVec.slt b.toBitVec
+def ISize.le (a b : ISize) : Prop := a.toBitVec.sle b.toBitVec
+
+instance : Inhabited ISize where
+  default := 0
+
+instance : Add ISize         := ⟨ISize.add⟩
+instance : Sub ISize         := ⟨ISize.sub⟩
+instance : Mul ISize         := ⟨ISize.mul⟩
+instance : Mod ISize         := ⟨ISize.mod⟩
+instance : Div ISize         := ⟨ISize.div⟩
+instance : LT ISize          := ⟨ISize.lt⟩
+instance : LE ISize          := ⟨ISize.le⟩
+instance : Complement ISize  := ⟨ISize.complement⟩
+instance : AndOp ISize       := ⟨ISize.land⟩
+instance : OrOp ISize        := ⟨ISize.lor⟩
+instance : Xor ISize         := ⟨ISize.xor⟩
+instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
+instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
+instance : DecidableEq ISize := ISize.decEq
+
+@[extern "lean_isize_dec_lt"]
+def ISize.decLt (a b : ISize) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
+
+@[extern "lean_isize_dec_le"]
+def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
+
+instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
+instance (a b : ISize) : Decidable (a ≤ b) := ISize.decLe a b
+instance : Max ISize := maxOfLe
+instance : Min ISize := minOfLe

src/Init/Data/Stream.lean

@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.array.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+      some (s.array[s.start]'(Nat.lt_of_lt_of_le h s.stop_le_array_size),
         { s with start := s.start + 1, start_le_stop := this })
     else
       none

src/Init/Data/String/Extra.lean

@@ -134,7 +134,7 @@ def toUTF8 (a : @& String) : ByteArray :=
 /-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/
 @[extern "lean_string_get_byte_fast"]
 def getUtf8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8 :=
-  (toUTF8 s).get ⟨n, size_toUTF8 _ ▸ h⟩
+  (toUTF8 s)[n]'(size_toUTF8 _ ▸ h)
 
 theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h

src/Init/GetElem.lean

@@ -211,17 +211,20 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
+    as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
+  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _
+
+@[deprecated (since := "2024-11-05")] abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
 
 end List
 
 namespace Array
 
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i h
 
 end Array
 

src/Init/Meta.lean

@@ -7,6 +7,7 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
+import Init.Syntax
 import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
@@ -442,7 +443,7 @@ def unsetTrailing (stx : Syntax) : Syntax :=
   if h : i < a.size then
     let v := a[i]
     match f v with
-    | some v => some <| a.set ⟨i, h⟩ v
+    | some v => some <| a.set i v h
     | none   => updateFirst a f (i+1)
   else
     none

src/Init/Prelude.lean

@@ -938,8 +938,8 @@ and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypoth
 even though it has different types in the two cases.)
 
 We use this to be able to communicate the if-then-else condition to the branches.
-For example, `Array.get arr ⟨i, h⟩` expects a proof `h : i < arr.size` in order to
-avoid a bounds check, so you can write `if h : i < arr.size then arr.get ⟨i, h⟩ else ...`
+For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to
+avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...`
 to avoid the bounds check inside the if branch. (Of course in this case we have only
 lifted the check into an explicit `if`, but we could also use this proof multiple times
 or derive `i < arr.size` from some other proposition that we are checking in the `if`.)
@@ -1951,7 +1951,7 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
 instance : DecidableEq UInt8 := UInt8.decEq
 
 instance : Inhabited UInt8 where
-  default := UInt8.ofNatCore 0 (by decide)
+  default := UInt8.ofNatCore 0 (of_decide_eq_true rfl)
 
 /-- The size of type `UInt16`, that is, `2^16 = 65536`. -/
 abbrev UInt16.size : Nat := 65536
@@ -1992,7 +1992,7 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
 instance : DecidableEq UInt16 := UInt16.decEq
 
 instance : Inhabited UInt16 where
-  default := UInt16.ofNatCore 0 (by decide)
+  default := UInt16.ofNatCore 0 (of_decide_eq_true rfl)
 
 /-- The size of type `UInt32`, that is, `2^32 = 4294967296`. -/
 abbrev UInt32.size : Nat := 4294967296
@@ -2038,7 +2038,7 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
 instance : DecidableEq UInt32 := UInt32.decEq
 
 instance : Inhabited UInt32 where
-  default := UInt32.ofNatCore 0 (by decide)
+  default := UInt32.ofNatCore 0 (of_decide_eq_true rfl)
 
 instance : LT UInt32 where
   lt a b := LT.lt a.toBitVec b.toBitVec
@@ -2105,7 +2105,7 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
 instance : DecidableEq UInt64 := UInt64.decEq
 
 instance : Inhabited UInt64 where
-  default := UInt64.ofNatCore 0 (by decide)
+  default := UInt64.ofNatCore 0 (of_decide_eq_true rfl)
 
 /-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
 abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
@@ -2113,8 +2113,8 @@ abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
 theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
   show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
   match System.Platform.numBits, System.Platform.numBits_eq with
-  | _, Or.inl rfl => Or.inl (by decide)
-  | _, Or.inr rfl => Or.inr (by decide)
+  | _, Or.inl rfl => Or.inl (of_decide_eq_true rfl)
+  | _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)
 
 /--
 A `USize` is an unsigned integer with the size of a word
@@ -2156,8 +2156,8 @@ instance : DecidableEq USize := USize.decEq
 
 instance : Inhabited USize where
   default := USize.ofNatCore 0 (match USize.size, usize_size_eq with
-    | _, Or.inl rfl => by decide
-    | _, Or.inr rfl => by decide)
+    | _, Or.inl rfl => of_decide_eq_true rfl
+    | _, Or.inr rfl => of_decide_eq_true rfl)
 
 /--
 Upcast a `Nat` less than `2^32` to a `USize`.
@@ -2170,7 +2170,7 @@ def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
     BitVec.ofNatLt n (
       match System.Platform.numBits, System.Platform.numBits_eq with
       | _, Or.inl rfl => h
-      | _, Or.inr rfl => Nat.lt_trans h (by decide)
+      | _, Or.inr rfl => Nat.lt_trans h (of_decide_eq_true rfl)
     )
 
 /--
@@ -2197,8 +2197,8 @@ structure Char where
 
 private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
   match h with
-  | Or.inl h      => Nat.lt_trans h (by decide)
-  | Or.inr ⟨_, h⟩ => Nat.lt_trans h (by decide)
+  | Or.inl h      => Nat.lt_trans h (of_decide_eq_true rfl)
+  | Or.inr ⟨_, h⟩ => Nat.lt_trans h (of_decide_eq_true rfl)
 
 /--
 Pack a `Nat` encoding a valid codepoint into a `Char`.
@@ -2216,7 +2216,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
 def Char.ofNat (n : Nat) : Char :=
   dite (n.isValidChar)
     (fun h => Char.ofNatAux n h)
-    (fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) })
+    (fun _ => { val := ⟨BitVec.ofNatLt 0 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) })
 
 theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -2239,9 +2239,9 @@ instance : DecidableEq Char :=
 /-- Returns the number of bytes required to encode this `Char` in UTF-8. -/
 def Char.utf8Size (c : Char) : Nat :=
   let v := c.val
-  ite (LE.le v (UInt32.ofNatCore 0x7F (by decide))) 1
-    (ite (LE.le v (UInt32.ofNatCore 0x7FF (by decide))) 2
-      (ite (LE.le v (UInt32.ofNatCore 0xFFFF (by decide))) 3 4))
+  ite (LE.le v (UInt32.ofNatCore 0x7F (of_decide_eq_true rfl))) 1
+    (ite (LE.le v (UInt32.ofNatCore 0x7FF (of_decide_eq_true rfl))) 2
+      (ite (LE.le v (UInt32.ofNatCore 0xFFFF (of_decide_eq_true rfl))) 3 4))
 
 /--
 `Option α` is the type of values which are either `some a` for some `a : α`,
@@ -2630,14 +2630,21 @@ def Array.empty {α : Type u} : Array α := mkEmpty 0
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 
-/-- Access an element from an array without bounds checks, using a `Fin` index. -/
+/--
+Access an element from an array without needing a runtime bounds checks,
+using a `Nat` index and a proof that it is in bounds.
+
+This function does not use `get_elem_tactic` to automatically find the proof that
+the index is in bounds. This is because the tactic itself needs to look up values in
+arrays. Use the indexing notation `a[i]` instead.
+-/
 @[extern "lean_array_fget"]
-def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
-  a.toList.get i
+def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
+  a.toList.get ⟨i, h⟩
 
 /-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
-  dite (LT.lt i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => v₀)
+  dite (LT.lt i a.size) (fun h => a.get i h) (fun _ => v₀)
 
 /-- Access an element from an array, or panic if the index is out of bounds. -/
 @[extern "lean_array_get"]
@@ -2688,35 +2695,6 @@ def Array.mkArray7 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : α) : Arr
 def Array.mkArray8 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : α) : Array α :=
   ((((((((mkEmpty 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈
 
-/--
-Set an element in an array without bounds checks, using a `Fin` index.
-
-This will perform the update destructively provided that `a` has a reference
-count of 1 when called.
--/
-@[extern "lean_array_fset"]
-def Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α where
-  toList := a.toList.set i.val v
-
-/--
-Set an element in an array, or do nothing if the index is out of bounds.
-
-This will perform the update destructively provided that `a` has a reference
-count of 1 when called.
--/
-@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=
-  dite (LT.lt i a.size) (fun h => a.set ⟨i, h⟩ v) (fun _ => a)
-
-/--
-Set an element in an array, or panic if the index is out of bounds.
-
-This will perform the update destructively provided that `a` has a reference
-count of 1 when called.
--/
-@[extern "lean_array_set"]
-def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
-  Array.setD a i v
-
 /-- Slower `Array.append` used in quotations. -/
 protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) : Array α :=
   let rec loop (i : Nat) (j : Nat) (as : Array α) : Array α :=
@@ -2724,7 +2702,7 @@ protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) :
       (fun hlt =>
         match i with
         | 0           => as
-        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get ⟨j, hlt⟩)))
+        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get j hlt)))
       (fun _ => as)
   loop bs.size 0 as
 
@@ -2739,7 +2717,7 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
       (fun hlt =>
         match i with
         | 0           => bs
-        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.get ⟨j, hlt⟩)))
+        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.get j hlt)))
       (fun _ => bs)
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
@@ -2858,7 +2836,7 @@ def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       (fun hlt =>
         match i with
         | 0           => pure bs
-        | Nat.succ i' => Bind.bind (f (as.get ⟨j, hlt⟩)) fun b => loop i' (hAdd j 1) (bs.push b))
+        | Nat.succ i' => Bind.bind (f (as.get j hlt)) fun b => loop i' (hAdd j 1) (bs.push b))
       (fun _ => pure bs)
   loop as.size 0 (Array.mkEmpty as.size)
 
@@ -3480,7 +3458,7 @@ def USize.toUInt64 (u : USize) : UInt64 where
         let ⟨⟨n, h⟩⟩ := u
         show LT.lt n _ from
         match System.Platform.numBits, System.Platform.numBits_eq, h with
-        | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
+        | _, Or.inl rfl, h => Nat.lt_trans h (of_decide_eq_true rfl)
         | _, Or.inr rfl, h => h
       )
 
@@ -3549,9 +3527,9 @@ with
   /-- A hash function for names, which is stored inside the name itself as a
   computed field. -/
   @[computed_field] hash : Name → UInt64
-    | .anonymous => .ofNatCore 1723 (by decide)
+    | .anonymous => .ofNatCore 1723 (of_decide_eq_true rfl)
     | .str p s => mixHash p.hash s.hash
-    | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))
+    | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (of_decide_eq_true rfl)))
 
 instance : Inhabited Name where
   default := Name.anonymous
@@ -3637,6 +3615,13 @@ def appendCore : Name → Name → Name
 
 end Name
 
+/-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option. -/
+def defaultMaxRecDepth := 512
+
+/-- The message to display on stack overflow. -/
+def maxRecDepthErrorMessage : String :=
+  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
+
 /-! # Syntax -/
 
 /-- Source information of tokens. -/
@@ -3969,24 +3954,6 @@ def getId : Syntax → Name
   | ident _ _ val _ => val
   | _               => Name.anonymous
 
-/--
-Updates the argument list without changing the node kind.
-Does nothing for non-`node` nodes.
--/
-def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
-  match stx with
-  | node info k _ => node info k args
-  | stx           => stx
-
-/--
-Updates the `i`'th argument of the syntax.
-Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
--/
-def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
-  match stx with
-  | node info k args => node info k (args.setD i arg)
-  | stx              => stx
-
 /-- Retrieve the left-most node or leaf's info in the Syntax tree. -/
 partial def getHeadInfo? : Syntax → Option SourceInfo
   | atom info _   => some info
@@ -4423,13 +4390,6 @@ main module and current macro scope.
   bind getCurrMacroScope fun scp =>
   pure (Lean.addMacroScope mainModule n scp)
 
-/-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option. -/
-def defaultMaxRecDepth := 512
-
-/-- The message to display on stack overflow. -/
-def maxRecDepthErrorMessage : String :=
-  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
-
 namespace Syntax
 
 /-- Is this syntax a null `node`? -/

src/Init/SimpLemmas.lean

@@ -263,7 +263,7 @@ theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by simp
   ⟨of_decide_eq_false, decide_eq_false⟩
 
 @[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
-  cases g <;> (rename_i gp; simp [gp]; rfl)
+  cases g <;> (rename_i gp; simp [gp])
 theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp
 
 @[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
@@ -277,8 +277,10 @@ theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp
 @[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
 theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp
 
-@[simp] theorem decide_False : decide False = false := rfl
-@[simp] theorem decide_True  : decide True  = true := rfl
+set_option linter.missingDocs false in
+@[deprecated decide_false (since := "2024-11-05")] abbrev decide_False := decide_false
+set_option linter.missingDocs false in
+@[deprecated decide_true  (since := "2024-11-05")] abbrev decide_True  := decide_true
 
 @[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] {a b : α} : a != b ↔ a ≠ b := by
   simp [bne]; rw [← beq_iff_eq (a := a) (b := b)]; simp [-beq_iff_eq]

src/Init/SizeOf.lean

@@ -41,7 +41,11 @@ for every element of `α`.
 protected def default.sizeOf (α : Sort u) : α → Nat
   | _ => 0
 
-instance (priority := low) (α : Sort u) : SizeOf α where
+/--
+Every type `α` has a low priority default `SizeOf` instance that just returns `0`
+for every element of `α`.
+-/
+instance (priority := low) instSizeOfDefault (α : Sort u) : SizeOf α where
   sizeOf := default.sizeOf α
 
 @[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl

src/Init/Syntax.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+
+prelude
+import Init.Data.Array.Set
+
+/-!
+# Helper functions for `Syntax`.
+
+These are delayed here to allow some time to bootstrap `Array`.
+-/
+
+namespace Lean.Syntax
+
+/--
+Updates the argument list without changing the node kind.
+Does nothing for non-`node` nodes.
+-/
+def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
+  match stx with
+  | node info k _ => node info k args
+  | stx           => stx
+
+/--
+Updates the `i`'th argument of the syntax.
+Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
+-/
+def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
+  match stx with
+  | node info k args => node info k (args.setD i arg)
+  | stx              => stx
+
+end Lean.Syntax

src/Init/Tactics.lean

@@ -990,13 +990,6 @@ and tries to clear the previous one.
 -/
 syntax (name := specialize) "specialize " term : tactic
 
-macro_rules | `(tactic| trivial) => `(tactic| assumption)
-macro_rules | `(tactic| trivial) => `(tactic| rfl)
-macro_rules | `(tactic| trivial) => `(tactic| contradiction)
-macro_rules | `(tactic| trivial) => `(tactic| decide)
-macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
-macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
-
 /--
 `unhygienic tacs` runs `tacs` with name hygiene disabled.
 This means that tactics that would normally create inaccessible names will instead
@@ -1156,6 +1149,132 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
 macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
 
+/--
+Configuration for the `decide` tactic family.
+-/
+structure DecideConfig where
+  /-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
+  This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
+  however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/
+  kernel : Bool := false
+  /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
+  admitting the result via the axiom `Lean.ofReduceBool`.  This can be significantly more efficient,
+  but it is at the cost of increasing the trusted code base, namely the Lean compiler
+  and all definitions with an `@[implemented_by]` attribute.
+  The instance is only evaluated once. The `native_decide` tactic is a synonym for `decide +native`. -/
+  native : Bool := false
+  /-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/
+  zetaReduce : Bool := true
+  /-- If true (default: false), then when preprocessing reverts free variables. -/
+  revert : Bool := false
+
+/--
+`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
+and then reducing that instance to evaluate the truth value of `p`.
+If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
+
+The target is not allowed to contain local variables or metavariables.
+If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target,
+or you can use the `+revert` option, described below.
+
+Options:
+- `decide +revert` begins by reverting local variables that the target depends on,
+  after cleaning up the local context of irrelevant variables.
+  A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
+  or if it is a proposition that refers to a relevant variable.
+- `decide +kernel` uses kernel for reduction instead of the elaborator.
+  It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
+  and (2) it reduces the `Decidable` instance only once instead of twice.
+- `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance,
+  admitting the result via the `Lean.ofReduceBool` axiom.
+  This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
+  of the trusted code base.
+  Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.
+  Like with `+kernel`, the `Decidable` instance is evaluated only once.
+
+Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term,
+`Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs.
+Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms.
+These can appear in instances defined using tactics (such as `rw` and `simp`).
+To avoid this, create such instances using definitions such as `decidable_of_iff` instead.
+
+## Examples
+
+Proving inequalities:
+```lean
+example : 2 + 2 ≠ 5 := by decide
+```
+
+Trying to prove a false proposition:
+```lean
+example : 1 ≠ 1 := by decide
+/-
+tactic 'decide' proved that the proposition
+  1 ≠ 1
+is false
+-/
+```
+
+Trying to prove a proposition whose `Decidable` instance fails to reduce
+```lean
+opaque unknownProp : Prop
+
+open scoped Classical in
+example : unknownProp := by decide
+/-
+tactic 'decide' failed for proposition
+  unknownProp
+since its 'Decidable' instance reduced to
+  Classical.choice ⋯
+rather than to the 'isTrue' constructor.
+-/
+```
+
+## Properties and relations
+
+For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
+```lean
+example : 1 + 1 = 2 := by decide
+example : 1 + 1 = 2 := by rfl
+```
+-/
+syntax (name := decide) "decide" optConfig : tactic
+
+/--
+`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
+It has the following properties:
+- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
+- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
+  and once during kernel type checking), the `decide!` tactic reduces it exactly once.
+
+The `decide!` syntax is short for `decide +kernel`.
+-/
+syntax (name := decideBang) "decide!" optConfig : tactic
+
+/--
+`native_decide` is a synonym for `decide +native`.
+It will attempt to prove a goal of type `p` by synthesizing an instance
+of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
+uses `#eval` to evaluate the decidability instance.
+
+This should be used with care because it adds the entire lean compiler to the trusted
+part, and the axiom `Lean.ofReduceBool` will show up in `#print axioms` for theorems using
+this method or anything that transitively depends on them. Nevertheless, because it is
+compiled, this can be significantly more efficient than using `decide`, and for very
+large computations this is one way to run external programs and trust the result.
+```lean
+example : (List.range 1000).length = 1000 := by native_decide
+```
+-/
+syntax (name := nativeDecide) "native_decide" optConfig : tactic
+
+macro_rules | `(tactic| trivial) => `(tactic| assumption)
+macro_rules | `(tactic| trivial) => `(tactic| rfl)
+macro_rules | `(tactic| trivial) => `(tactic| contradiction)
+macro_rules | `(tactic| trivial) => `(tactic| decide)
+macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
+macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
+
 /--
 The `omega` tactic, for resolving integer and natural linear arithmetic problems.
 

src/Lean/Compiler/IR/Checker.lean

@@ -135,8 +135,8 @@ def checkExpr (ty : IRType) : Expr → M Unit
     match xType with
     | IRType.object       => checkObjType ty
     | IRType.tobject      => checkObjType ty
-    | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
-    | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
+    | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys[i]) ty else throw "invalid proj index"
+    | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys[i]) ty else throw "invalid proj index"
     | _                   => throw s!"unexpected IR type '{xType}'"
   | Expr.uproj _ x          => checkObjVar x *> checkType ty (fun t => t == IRType.usize)
   | Expr.sproj _ _ x        => checkObjVar x *> checkScalarType ty

src/Lean/Data/HashMap.lean

@@ -90,10 +90,9 @@ def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
 
 def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
   if h : i < source.size then
-     let idx : Fin source.size := ⟨i, h⟩
-     let es  : AssocList α β   := source.get idx
+     let es  : AssocList α β   := source[i]
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set idx AssocList.nil
+     let source                := source.set i AssocList.nil
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target

src/Lean/Data/HashSet.lean

@@ -80,10 +80,9 @@ def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
 
 def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
   if h : i < source.size then
-     let idx : Fin source.size := ⟨i, h⟩
-     let es  : List α   := source.get idx
+     let es  : List α   := source[i]
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set idx []
+     let source                := source.set i []
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else

src/Lean/Data/Lsp/Utf16.lean

@@ -66,7 +66,7 @@ namespace FileMap
 
 private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
   if h : line < text.positions.size then
-    text.positions.get ⟨line, h⟩
+    text.positions[line]
   else if text.positions.isEmpty then
     0
   else

src/Lean/Data/PersistentArray.lean

@@ -149,8 +149,8 @@ private def emptyArray {α : Type u} : Array (PersistentArrayNode α) :=
 partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (PersistentArrayNode α)
   | node cs =>
     if h : cs.size ≠ 0 then
-      let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.pred_lt h⟩
-      let last := cs.get idx
+      let idx := cs.size - 1
+      let last := cs[idx]
       let cs'  := cs.set idx default
       match popLeaf last with
       | (none,   _)       => (none, emptyArray)
@@ -159,7 +159,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
           let cs' := cs'.pop
           if cs'.isEmpty then (some l, emptyArray) else (some l, cs')
         else
-          (some l, cs'.set (Array.size_set cs idx _ ▸ idx) (node newLast))
+          (some l, cs'.set idx (node newLast) (by simp only [cs', Array.size_set]; omega))
     else
       (none, emptyArray)
   | leaf vs   => (some vs, emptyArray)

src/Lean/Data/PersistentHashMap.lean

@@ -84,11 +84,10 @@ private theorem size_push {ks : Array α} {vs : Array β} (h : ks.size = vs.size
 partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat → α → β → CollisionNode α β
   | n@⟨Node.collision keys vals heq, _⟩, i, k, v =>
     if h : i < keys.size then
-      let idx : Fin keys.size := ⟨i, h⟩;
-      let k' := keys.get idx;
+      let k' := keys[i];
       if k == k' then
          let j : Fin vals.size := ⟨i, by rw [←heq]; assumption⟩
-         ⟨Node.collision (keys.set idx k) (vals.set j v) (size_set heq idx j k v), IsCollisionNode.mk _ _ _⟩
+         ⟨Node.collision (keys.set i k) (vals.set j v) (size_set heq ⟨i, h⟩ j k v), IsCollisionNode.mk _ _ _⟩
       else insertAtCollisionNodeAux n (i+1) k v
     else
       ⟨Node.collision (keys.push k) (vals.push v) (size_push heq k v), IsCollisionNode.mk _ _ _⟩

src/Lean/Data/Position.lean

@@ -97,7 +97,7 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
   let colPos :=
     if h : pos.line - 1 < text.positions.size then
-      text.positions.get ⟨pos.line - 1, h⟩
+      text.positions[pos.line - 1]
     else if text.positions.isEmpty then
       0
     else
@@ -110,7 +110,7 @@ This gives the same result as `map.ofPosition ⟨line, 0⟩`, but is more effici
 -/
 def lineStart (map : FileMap) (line : Nat) : String.Pos :=
   if h : line - 1 < map.positions.size then
-    map.positions.get ⟨line - 1, h⟩
+    map.positions[line - 1]
   else map.positions.back?.getD 0
 
 end FileMap

src/Lean/Elab/App.lean

@@ -506,8 +506,7 @@ where
     if h : i < args.size then
       match (← whnf cType) with
       | .forallE _ d b _ =>
-        let arg := args.get ⟨i, h⟩
-        if arg == x && d.isOutParam then
+        if args[i] == x && d.isOutParam then
           return true
         isOutParamOf x (i+1) args b
       | _ => return false

src/Lean/Elab/BuiltinCommand.lean

@@ -111,9 +111,8 @@ private def checkEndHeader : Name → List Scope → Option Name
 
 private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM Unit :=
   if h : i < cmds.size then
-    let cmd := cmds.get ⟨i, h⟩;
     catchInternalId unsupportedSyntaxExceptionId
-      (elabCommand cmd)
+      (elabCommand cmds[i])
       (fun _ => elabChoiceAux cmds (i+1))
   else
     throwUnsupportedSyntax

src/Lean/Elab/BuiltinNotation.lean

@@ -322,7 +322,7 @@ def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
   let stx ← liftMacroM <| expandMacros stx
   match stx with
   | `(fun $binders* => $f $args*) =>
-    if binders == args then
+    if binders.raw.toList.isPerm args.raw.toList then
       try Term.resolveId? f catch _ => return none
     else
       return none
@@ -332,7 +332,7 @@ def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
   | `(fun $binders* => rightact% $f $a $b)
   | `(fun $binders* => binrel% $f $a $b)
   | `(fun $binders* => binrel_no_prop% $f $a $b) =>
-    if binders == #[a, b] then
+    if binders == #[a, b] || binders == #[b, a] then
       try Term.resolveId? f catch _ => return none
     else
       return none

src/Lean/Elab/Declaration.lean

@@ -192,8 +192,7 @@ private def isMutualPreambleCommand (stx : Syntax) : Bool :=
 private partial def splitMutualPreamble (elems : Array Syntax) : Option (Array Syntax × Array Syntax) :=
   let rec loop (i : Nat) : Option (Array Syntax × Array Syntax) :=
     if h : i < elems.size then
-      let elem := elems.get ⟨i, h⟩
-      if isMutualPreambleCommand elem then
+      if isMutualPreambleCommand elems[i] then
         loop (i+1)
       else if i == 0 then
         none -- `mutual` block does not contain any preamble commands

src/Lean/Elab/DefView.lean

@@ -11,19 +11,13 @@ import Lean.Elab.DeclUtil
 namespace Lean.Elab
 
 inductive DefKind where
-  | def | theorem | example | opaque | abbrev
+  | def | instance | theorem | example | opaque | abbrev
   deriving Inhabited, BEq
 
 def DefKind.isTheorem : DefKind → Bool
   | .theorem => true
   | _        => false
 
-def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool
-  | .def    => true
-  | .opaque => true
-  | .abbrev => true
-  | _       => false
-
 def DefKind.isExample : DefKind → Bool
   | .example => true
   | _        => false
@@ -171,7 +165,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
       trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}"
       pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
   return {
-    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.def, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.instance, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[5]
   }
 

src/Lean/Elab/Inductive.lean

@@ -133,7 +133,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
 private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) :=
   Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
     if h : i < views.size then
-      let view := views.get ⟨i, h⟩
+      let view := views[i]
       let acc ← Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
         match view.type? with
         | none         =>
@@ -250,7 +250,7 @@ private partial def withInductiveLocalDecls (rs : Array ElabHeaderResult) (x : A
   withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do
     let rec loop (i : Nat) (indFVars : Array Expr) := do
       if h : i < namesAndTypes.size then
-        let (declName, shortDeclName, type) := namesAndTypes.get ⟨i, h⟩
+        let (declName, shortDeclName, type) := namesAndTypes[i]
         Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
       else
         x params indFVars
@@ -740,10 +740,7 @@ private def getArity (indType : InductiveType) : MetaM Nat :=
   forallTelescopeReducing indType.type fun xs _ => return xs.size
 
 private def resetMaskAt (mask : Array Bool) (i : Nat) : Array Bool :=
-  if h : i < mask.size then
-    mask.set ⟨i, h⟩ false
-  else
-    mask
+  mask.setD i false
 
 /--
   Compute a bit-mask that for `indType`. The size of the resulting array `result` is the arity of `indType`.

src/Lean/Elab/LetRec.lean

@@ -77,7 +77,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
 private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : Array Expr → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
     if h : i < views.size then
-      let view := views.get ⟨i, h⟩
+      let view := views[i]
       withAuxDecl view.shortDeclName view.type view.declName fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars

src/Lean/Elab/Match.lean

@@ -108,7 +108,7 @@ where
   /-- Elaborate discriminants inferring the match-type -/
   elabDiscrs (i : Nat) (discrs : Array Discr) : TermElabM ElabMatchTypeAndDiscrsResult := do
     if h : i < discrStxs.size then
-      let discrStx := discrStxs.get ⟨i, h⟩
+      let discrStx := discrStxs[i]
       let discr     ← elabAtomicDiscr discrStx
       let discr     ← instantiateMVars discr
       let userName ← mkUserNameFor discr
@@ -176,9 +176,8 @@ structure PatternVarDecl where
 private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array PatternVarDecl → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (decls : Array PatternVarDecl) (userNames : Array Name) := do
     if h : i < pVars.size then
-      let var := pVars.get ⟨i, h⟩
       let type ← mkFreshTypeMVar
-      withLocalDecl var.getId BinderInfo.default type fun x =>
+      withLocalDecl pVars[i].getId BinderInfo.default type fun x =>
         loop (i+1) (decls.push { fvarId := x.fvarId! }) (userNames.push Name.anonymous)
     else
       k decls
@@ -760,7 +759,7 @@ where
     | [] => k eqs
     | p::ps =>
       if h : i < discrs.size then
-        let discr := discrs.get ⟨i, h⟩
+        let discr := discrs[i]
         if let some h := discr.h? then
           withLocalDeclD h.getId (← mkEqHEq discr.expr (← p.toExpr)) fun eq => do
             addTermInfo' h eq (isBinder := true)
@@ -957,7 +956,7 @@ where
     let mut s : CollectFVars.State := {}
     for discr in discrs do
       s := collectFVars s (← instantiateMVars (← inferType discr))
-    let (indicesFVar, indicesNonFVar) := indices.split Expr.isFVar
+    let (indicesFVar, indicesNonFVar) := indices.partition Expr.isFVar
     let indicesFVar := indicesFVar.map Expr.fvarId!
     let mut toAdd := #[]
     for fvarId in s.fvarSet.toList do

src/Lean/Elab/MutualDef.lean

@@ -22,6 +22,14 @@ open Lean.Parser.Term
 
 open Language
 
+builtin_initialize
+  registerTraceClass `Meta.instantiateMVars
+
+def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
+  profileitM Exception s!"instantiate metavars" (← getOptions) do
+  withTraceNode `Meta.instantiateMVars (fun _ => pure e) do
+    instantiateMVars e
+
 /-- `DefView` plus header elaboration data and snapshot. -/
 structure DefViewElabHeader extends DefView, DefViewElabHeaderData where
   /--
@@ -69,7 +77,7 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
   if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
     throwError "'unsafe' subsumes 'partial'"
   if h : 0 < prevHeaders.size then
-    let firstHeader := prevHeaders.get ⟨0, h⟩
+    let firstHeader := prevHeaders[0]
     try
       unless newHeader.levelNames == firstHeader.levelNames do
         throwError "universe parameters mismatch"
@@ -116,7 +124,7 @@ See issues #1389 and #875
 private def cleanupOfNat (type : Expr) : MetaM Expr := do
   Meta.transform type fun e => do
     if !e.isAppOfArity ``OfNat 2 then return .continue
-    let arg ← instantiateMVars e.appArg!
+    let arg ← instantiateMVarsProfiling e.appArg!
     if !arg.isAppOfArity ``OfNat.ofNat 3 then return .continue
     let argArgs := arg.getAppArgs
     if !argArgs[0]!.isConstOf ``Nat then return .continue
@@ -191,7 +199,7 @@ private def elabHeaders (views : Array DefView)
             -- TODO: add forbidden predicate using `shortDeclName` from `views`
             let xs ← addAutoBoundImplicits xs
             type ← mkForallFVars' xs type
-            type ← instantiateMVars type
+            type ← instantiateMVarsProfiling type
             let levelNames ← getLevelNames
             if view.type?.isSome then
               let pendingMVarIds ← getMVars type
@@ -265,7 +273,7 @@ where
 private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (k : Array Expr → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array Expr) := do
     if h : i < headers.size then
-      let header := headers.get ⟨i, h⟩
+      let header := headers[i]
       if header.modifiers.isNonrec then
         loop (i+1) fvars
       else
@@ -329,10 +337,6 @@ private def declValToTerminationHint (declVal : Syntax) : TermElabM TerminationH
   else
     return .none
 
-def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
-  profileitM Exception s!"instantiate metavars" (← getOptions) do
-    instantiateMVars e
-
 /--
 Runs `k` with a restricted local context where only section variables from `vars` are included that
 * are directly referenced in any `headers`,
@@ -474,11 +478,11 @@ private def isTheorem (views : Array DefView) : Bool :=
   views.any (·.kind.isTheorem)
 
 private def instantiateMVarsAtHeader (header : DefViewElabHeader) : TermElabM DefViewElabHeader := do
-  let type ← instantiateMVars header.type
+  let type ← instantiateMVarsProfiling header.type
   pure { header with type := type }
 
 private def instantiateMVarsAtLetRecToLift (toLift : LetRecToLift) : TermElabM LetRecToLift := do
-  let type ← instantiateMVars toLift.type
+  let type ← instantiateMVarsProfiling toLift.type
   let val ← instantiateMVarsProfiling toLift.val
   pure { toLift with type, val }
 
@@ -863,7 +867,7 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
   letRecClosures.foldlM (init := preDefs) fun preDefs c => do
     let type  := Closure.mkForall c.localDecls c.toLift.type
     let value := Closure.mkLambda c.localDecls c.toLift.val
-    let kind ← if kind.isDefOrAbbrevOrOpaque then
+    let kind ← if kind matches .def | .instance | .opaque | .abbrev then
       -- Convert any proof let recs inside a `def` to `theorem` kind
       withLCtx c.toLift.lctx c.toLift.localInstances do
         return if (← inferType c.toLift.type).isProp then .theorem else kind
@@ -911,7 +915,7 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai
     let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do
       Meta.check toLift.type
       Meta.check toLift.val
-      return { toLift with val := (← instantiateMVarsProfiling toLift.val), type := (← instantiateMVars toLift.type) }
+      return { toLift with val := (← instantiateMVarsProfiling toLift.val), type := (← instantiateMVarsProfiling toLift.type) }
     let letRecClosures ← mkLetRecClosures sectionVars mainFVarIds recFVarIds letRecsToLift
     -- mkLetRecClosures assign metavariables that were placeholders for the lifted declarations.
     let mainVals    ← mainVals.mapM (instantiateMVarsProfiling ·)
@@ -932,7 +936,7 @@ end MutualClosure
 private def getAllUserLevelNames (headers : Array DefViewElabHeader) : List Name :=
   if h : 0 < headers.size then
     -- Recall that all top-level functions must have the same levels. See `check` method above
-    (headers.get ⟨0, h⟩).levelNames
+    headers[0].levelNames
   else
     []
 
@@ -949,7 +953,7 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
         newHeaders := newHeaders.push header
     return newHeaders
   let newHeaders ← (process).run' 1
-  newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
+  newHeaders.mapM fun header => return { header with type := (← instantiateMVarsProfiling header.type) }
 
 def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then

src/Lean/Elab/PatternVar.lean

@@ -135,7 +135,7 @@ private def isNextArgAccessible (ctx : Context) : Bool :=
   | none =>
     if h : i < ctx.paramDecls.size then
       -- For `[match_pattern]` applications, only explicit parameters are accessible.
-      let d := ctx.paramDecls.get ⟨i, h⟩
+      let d := ctx.paramDecls[i]
       d.2.isExplicit
     else
       false

src/Lean/Elab/PreDefinition/Basic.lean

@@ -132,14 +132,21 @@ private def reportTheoremDiag (d : TheoremVal) : TermElabM Unit := do
 private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs preDef
+    let mkDefDecl : TermElabM Declaration :=
+      return Declaration.defnDecl {
+          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
+          hints := ReducibilityHints.regular (getMaxHeight (← getEnv) preDef.value + 1)
+          safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe,
+          all }
+    let mkThmDecl : TermElabM Declaration := do
+      let d := {
+        name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, all
+      }
+      reportTheoremDiag d
+      return Declaration.thmDecl d
     let decl ←
       match preDef.kind with
-      | DefKind.«theorem» =>
-        let d := {
-          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, all
-        }
-        reportTheoremDiag d
-        pure <| Declaration.thmDecl d
+      | DefKind.«theorem» => mkThmDecl
       | DefKind.«opaque»  =>
         pure <| Declaration.opaqueDecl {
           name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
@@ -151,12 +158,8 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
           hints := ReducibilityHints.«abbrev»
           safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe,
           all }
-      | _ => -- definitions and examples
-        pure <| Declaration.defnDecl {
-          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
-          hints := ReducibilityHints.regular (getMaxHeight (← getEnv) preDef.value + 1)
-          safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe,
-          all }
+      | DefKind.def | DefKind.example => mkDefDecl
+      | DefKind.«instance» => if ← Meta.isProp preDef.type then mkThmDecl else mkDefDecl
     addDecl decl
     withSaveInfoContext do  -- save new env
       addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)

src/Lean/Elab/PreDefinition/Main.lean

@@ -267,7 +267,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
             logException ex
             let s ← saveState
             try
-              if preDefs.all fun preDef => preDef.kind == DefKind.def || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
+              if preDefs.all fun preDef => (preDef.kind matches DefKind.def | DefKind.instance) || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
                 -- try to add as partial definition
                 try
                   addAndCompilePartial preDefs (useSorry := true)

src/Lean/Elab/StructInst.lean

@@ -885,7 +885,7 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
     if dist > maxDistance then
       return false
     else if h : i < structs.size then
-      let struct := structs.get ⟨i, h⟩
+      let struct := structs[i]
       match getDefaultFnForField? (← getEnv) struct.structName fieldName with
       | some defFn =>
         let cinfo ← getConstInfo defFn

src/Lean/Elab/Structure.lean

@@ -321,7 +321,7 @@ private partial def processSubfields (structDeclName : Name) (parentFVar : Expr)
 where
   go (i : Nat) (infos : Array StructFieldInfo) := do
     if h : i < subfieldNames.size then
-      let subfieldName := subfieldNames.get ⟨i, h⟩
+      let subfieldName := subfieldNames[i]
       if containsFieldName infos subfieldName then
         throwError "field '{subfieldName}' from '{.ofConstName parentStructName}' has already been declared"
       let val  ← mkProjection parentFVar subfieldName
@@ -463,7 +463,7 @@ where
     let fieldNames := getStructureFields (← getEnv) parentStructName
     let rec copy (i : Nat) (infos : Array StructFieldInfo) (fieldMap : FieldMap) (expandedStructNames : NameSet) : TermElabM α := do
       if h : i < fieldNames.size then
-        let fieldName := fieldNames.get ⟨i, h⟩
+        let fieldName := fieldNames[i]
         let fieldType ← getFieldType infos parentType fieldName
         match findFieldInfo? infos fieldName with
         | some existingFieldInfo =>

src/Lean/Elab/Tactic/BVDecide/External.lean

@@ -170,8 +170,8 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
   match out? with
   | .timeout =>
     let mut err := "The SAT solver timed out while solving the problem.\n"
-    err := err ++ "Consider increasing the timeout with `set_option sat.timeout <sec>`.\n"
-    err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option."
+    err := err ++ "Consider increasing the timeout with the `timeout` config option.\n"
+    err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option."
     throwError err
   | .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
     if exitCode == 255 then

src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison, Henrik Böving
 prelude
 import Lean.Util.Trace
 import Lean.Elab.Tactic.Simp
+import Std.Tactic.BVDecide.Syntax
 
 /-!
 Provides environment extensions around the `bv_decide` tactic frontends.
@@ -32,30 +33,7 @@ register_builtin_option sat.solver : String := {
         to use the one that ships with Lean."
 }
 
-register_builtin_option sat.timeout : Nat := {
-  defValue := 10
-  descr := "the number of seconds that the sat solver is run before aborting"
-}
-
-register_builtin_option sat.trimProofs : Bool := {
-  defValue := true
-  descr := "Whether to run the trimming algorithm on LRAT proofs"
-}
-
-register_builtin_option sat.binaryProofs : Bool := {
-  defValue := true
-  descr := "Whether to use the binary LRAT proof format. Currently set to false and ignored on Windows due to a bug in CaDiCal."
-}
-
-register_builtin_option debug.bv.graphviz : Bool := {
-  defValue := false
-  descr := "Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process."
-}
-
-register_builtin_option bv.ac_nf : Bool := {
-  defValue := false
-  descr := "Canonicalize with respect to associativity and commutativitiy."
-}
+declare_config_elab elabBVDecideConfig Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig
 
 builtin_initialize bvNormalizeExt : Meta.SimpExtension ←
   Meta.registerSimpAttr `bv_normalize "simp theorems used by bv_normalize"

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -28,22 +28,22 @@ def getSrcDir : TermElabM System.FilePath := do
     | throwError "cannot compute parent directory of '{srcPath}'"
   return srcDir
 
-def mkContext (lratPath : System.FilePath) : TermElabM TacticContext := do
+def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM TacticContext := do
   let lratPath := (← getSrcDir) / lratPath
-  TacticContext.new lratPath
+  TacticContext.new lratPath cfg
 
 /--
 Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
 -/
-def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
-  let cert ← LratCert.ofFile cfg.lratPath cfg.trimProofs
-  cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
+  let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs
+  cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
 
 @[inherit_doc Lean.Parser.Tactic.bvCheck]
-def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
+def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
   let unsatProver : UnsatProver := fun _ reflectionResult _ => do
     withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
-      let proof ← lratChecker cfg reflectionResult.bvExpr
+      let proof ← lratChecker ctx reflectionResult.bvExpr
       return .ok ⟨proof, ""⟩
   let _ ← closeWithBVReflection g unsatProver
   return ()
@@ -52,14 +52,15 @@ def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
 open Lean.Meta.Tactic in
 @[builtin_tactic Lean.Parser.Tactic.bvCheck]
 def evalBvCheck : Tactic := fun
-  | `(tactic| bv_check%$tk $path:str) => do
-    let cfg ← BVDecide.Frontend.BVCheck.mkContext path.getString
+  | `(tactic| bv_check%$tk $cfgStx:optConfig $path:str) => do
+    let cfg ← elabBVDecideConfig cfgStx
+    let ctx ← BVDecide.Frontend.BVCheck.mkContext path.getString cfg
     liftMetaFinishingTactic fun g => do
-      let g'? ← Normalize.bvNormalize g
+      let g'? ← Normalize.bvNormalize g cfg
       match g'? with
-      | some g' => bvCheck g' cfg
+      | some g' => bvCheck g' ctx
       | none =>
-        let bvNormalizeStx ← `(tactic| bv_normalize)
+        let bvNormalizeStx ← `(tactic| bv_normalize $cfgStx)
         logWarning m!"This goal can be closed by only applying bv_normalize, no need to keep the LRAT proof around."
         TryThis.addSuggestion tk bvNormalizeStx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -186,7 +186,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
     err := err ++ m!"Consider the following assignment:\n"
     return err
 
-def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
+def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
     MetaM (Except CounterExample UnsatProver.Result) := do
   let bvExpr := reflectionResult.bvExpr
@@ -197,7 +197,7 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref
   let aigSize := entry.aig.decls.size
   trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
 
-  if cfg.graphviz then
+  if ctx.config.graphviz then
     IO.FS.writeFile ("." / "aig.gv") <| AIG.toGraphviz entry
 
   let (cnf, map) ←
@@ -211,12 +211,12 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref
 
   let res ←
     withTraceNode `sat (fun _ => return "Obtaining external proof certificate") do
-      runExternal cnf cfg.solver cfg.lratPath cfg.trimProofs cfg.timeout cfg.binaryProofs
+      runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs
 
   match res with
   | .ok cert =>
     trace[Meta.Tactic.sat] "SAT solver found a proof."
-    let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+    let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
     return .ok ⟨proof, cert⟩
   | .error assignment =>
     trace[Meta.Tactic.sat] "SAT solver found a counter example."
@@ -267,10 +267,10 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
       return .ok cert
     | .error counterExample => return .error counterExample
 
-def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
+def bvUnsat (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
   let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
-      lratBitblaster g cfg reflectionResult atomsAssignment
+      lratBitblaster g ctx reflectionResult atomsAssignment
   closeWithBVReflection g unsatProver
 
 /--
@@ -287,18 +287,18 @@ structure Result where
 Try to close `g` using a bitblaster. Return either a `CounterExample` if one is found or a `Result`
 if `g` is proven.
 -/
-def bvDecide' (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Result) := do
-  let g? ← Normalize.bvNormalize g
+def bvDecide' (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample Result) := do
+  let g? ← Normalize.bvNormalize g ctx.config
   let some g := g? | return .ok ⟨none⟩
-  match ← bvUnsat g cfg with
+  match ← bvUnsat g ctx with
   | .ok lratCert => return .ok ⟨some lratCert⟩
   | .error counterExample => return .error counterExample
 
 /--
 Call `bvDecide'` and throw a pretty error if a counter example ends up being produced.
 -/
-def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
-  match ← bvDecide' g cfg with
+def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
+  match ← bvDecide' g ctx with
   | .ok result => return result
   | .error counterExample =>
     counterExample.goal.withContext do
@@ -309,9 +309,10 @@ def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
 def evalBvTrace : Tactic := fun
-  | `(tactic| bv_decide) => do
+  | `(tactic| bv_decide $cfg:optConfig) => do
+    let cfg ← elabBVDecideConfig cfg
     IO.FS.withTempFile fun _ lratFile => do
-      let cfg ← BVDecide.Frontend.TacticContext.new lratFile
+      let cfg ← BVDecide.Frontend.TacticContext.new lratFile cfg
       liftMetaFinishingTactic fun g => do
         discard <| bvDecide g cfg
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -65,6 +65,8 @@ where
     mkApp4 (mkConst ``BVExpr.shiftLeft) (toExpr m) (toExpr n) (go lhs) (go rhs)
   | .shiftRight (m := m) (n := n) lhs rhs =>
     mkApp4 (mkConst ``BVExpr.shiftRight) (toExpr m) (toExpr n) (go lhs) (go rhs)
+  | .arithShiftRight (m := m) (n := n) lhs rhs =>
+    mkApp4 (mkConst ``BVExpr.arithShiftRight) (toExpr m) (toExpr n) (go lhs) (go rhs)
 
 instance : ToExpr BVBinPred where
   toExpr x :=

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -60,8 +60,8 @@ where
           ``BVUnOp.shiftLeftConst
           ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
       else
+        let_expr BitVec _ := β | return none
         shiftReflection
-          β
           distanceExpr
           innerExpr
           .shiftLeft
@@ -78,8 +78,8 @@ where
           ``BVUnOp.shiftRightConst
           ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
       else
+        let_expr BitVec _ := β | return none
         shiftReflection
-          β
           distanceExpr
           innerExpr
           .shiftRight
@@ -92,6 +92,13 @@ where
         innerExpr
         .arithShiftRightConst
         ``BVUnOp.arithShiftRightConst
+        ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr
+    | BitVec.sshiftRight' _ _ innerExpr distanceExpr =>
+      shiftReflection
+        distanceExpr
+        innerExpr
+        .arithShiftRight
+        ``BVExpr.arithShiftRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
     | BitVec.zeroExtend _ newWidthExpr innerExpr =>
       let some newWidth ← getNatValue? newWidthExpr | return none
@@ -258,11 +265,10 @@ where
     let some distance ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr | return none
     shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
 
-  shiftReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr)
+  shiftReflection (distanceExpr : Expr) (innerExpr : Expr)
       (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
       (congrThm : Name) :
       LemmaM (Option ReifiedBVExpr) := do
-    let_expr BitVec _ ← β | return none
     let some inner ← goOrAtom innerExpr | return none
     let some distance ← goOrAtom distanceExpr | return none
     let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr

src/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean

@@ -34,12 +34,13 @@ open Lean.Meta.Tactic in
 open Lean.Elab.Tactic.BVDecide.LRAT in
 @[builtin_tactic Lean.Parser.Tactic.bvTrace]
 def evalBvTrace : Tactic := fun
-  | `(tactic| bv_decide?%$tk) => do
+  | `(tactic| bv_decide?%$tk $cfgStx:optConfig) => do
+    let cfg := { (← elabBVDecideConfig cfgStx) with trimProofs := false }
     let lratFile : System.FilePath ← BVTrace.getLratFileName
-    let cfg := { (← BVCheck.mkContext lratFile) with trimProofs := false }
+    let ctx ← BVCheck.mkContext lratFile cfg
     let g ← getMainGoal
     let trace ← g.withContext do
-      bvDecide g cfg
+      bvDecide g ctx
     /-
     Ideally trace.lratCert would be the `ByteArray` version of the proof already and we just write
     it. This isn't yet possible so instead we do the following:
@@ -57,12 +58,12 @@ def evalBvTrace : Tactic := fun
       let normalizeStx ← `(tactic| bv_normalize)
       TryThis.addSuggestion tk normalizeStx (origSpan? := ← getRef)
     | some .. =>
-      if sat.trimProofs.get (← getOptions) then
+      if ctx.config.trimProofs then
         let lratPath := (← BVCheck.getSrcDir) / lratFile
         let proof ← loadLRATProof lratPath
         let trimmed ← IO.ofExcept <| trim proof
         dumpLRATProof lratPath trimmed cfg.binaryProofs
-      let bvCheckStx ← `(tactic| bv_check $(quote lratFile.toString))
+      let bvCheckStx ← `(tactic| bv_check $cfgStx:optConfig $(quote lratFile.toString))
       TryThis.addSuggestion tk bvCheckStx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -30,37 +30,28 @@ structure TacticContext where
   reflectionDef : Name
   solver : System.FilePath
   lratPath : System.FilePath
-  graphviz : Bool
-  timeout : Nat
-  trimProofs : Bool
-  binaryProofs : Bool
+  config : BVDecideConfig
 
-def TacticContext.new (lratPath : System.FilePath) : Lean.Elab.TermElabM TacticContext := do
+def TacticContext.new (lratPath : System.FilePath) (config : BVDecideConfig) :
+    Lean.Elab.TermElabM TacticContext := do
+  -- Account for: https://github.com/arminbiere/cadical/issues/112
+  let config :=
+    if System.Platform.isWindows then
+      { config with binaryProofs := false }
+    else
+      config
   let exprDef ← Lean.Elab.Term.mkAuxName `_expr_def
   let certDef ← Lean.Elab.Term.mkAuxName `_cert_def
   let reflectionDef ← Lean.Elab.Term.mkAuxName `_reflection_def
-  let opts ← getOptions
   let solver ← determineSolver
   trace[Meta.Tactic.sat] m!"Using SAT solver at '{solver}'"
-  let timeout := sat.timeout.get opts
-  let graphviz := debug.bv.graphviz.get opts
-  let trimProofs := sat.trimProofs.get opts
-  let binaryProofs :=
-    -- Account for: https://github.com/arminbiere/cadical/issues/112
-    if System.Platform.isWindows then
-      false
-    else
-      sat.binaryProofs.get opts
   return {
     exprDef,
     certDef,
     reflectionDef,
     solver,
     lratPath,
-    graphviz,
-    timeout,
-    trimProofs,
-    binaryProofs
+    config
   }
 where
   determineSolver : Lean.Elab.TermElabM System.FilePath := do

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -129,6 +129,36 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
 
 attribute [builtin_bv_normalize_proc↓] reduceIte
 
+/-- Return a number `k` such that `2^k = n`. -/
+private def Nat.log2Exact (n : Nat) : Option Nat := do
+  guard <| n ≠ 0
+  let k := n.log2
+  guard <| Nat.pow 2 k == n
+  return k
+
+-- Build an expression for `x ^ y`.
+def mkPow (x y : Expr) : MetaM Expr := mkAppM ``HPow.hPow #[x, y]
+
+builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofNat _ _) : BitVec _)) := fun e => do
+  let_expr HDiv.hDiv _α _β _γ _self x y := e | return .continue
+  let some ⟨w, yVal⟩ ← getBitVecValue? y | return .continue
+  let n := yVal.toNat
+  -- BitVec.ofNat w n, where n =def= 2^k
+  let some k := Nat.log2Exact n | return .continue
+  -- check that k < w.
+  if k ≥ w then return .continue
+  let rhs ← mkAppM ``HShiftRight.hShiftRight #[x, mkNatLit k]
+  -- 2^k = n
+  let hk ← mkDecideProof (← mkEq (← mkPow (mkNatLit 2) (mkNatLit k)) (mkNatLit n))
+  -- k < w
+  let hlt ← mkDecideProof (← mkLt (mkNatLit k) (mkNatLit w))
+  let proof := mkAppN (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.udiv_ofNat_eq_of_lt)
+    #[mkNatLit w, x, mkNatLit n, mkNatLit k, hk, hlt]
+  return .done {
+      expr :=  rhs
+      proof? := some proof
+  }
+
 /--
 A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
 the goal fully, indicated by returning `none`.
@@ -157,14 +187,14 @@ partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Optio
 /--
 Responsible for applying the Bitwuzla style rewrite rules.
 -/
-def rewriteRulesPass : Pass := fun goal => do
+def rewriteRulesPass (maxSteps : Nat) : Pass := fun goal => do
   let bvThms ← bvNormalizeExt.getTheorems
   let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
   let sevalThms ← getSEvalTheorems
   let sevalSimprocs ← Simp.getSEvalSimprocs
 
   let simpCtx : Simp.Context := {
-    config := { failIfUnchanged := false, zetaDelta := true }
+    config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
     simpTheorems := #[bvThms, sevalThms]
     congrTheorems := (← getSimpCongrTheorems)
   }
@@ -181,7 +211,7 @@ def rewriteRulesPass : Pass := fun goal => do
 Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
 them to substitute occurences of `x` within other hypotheses
 -/
-def embeddedConstraintPass : Pass := fun goal =>
+def embeddedConstraintPass (maxSteps : Nat) : Pass := fun goal =>
   goal.withContext do
     let hyps ← goal.getNondepPropHyps
     let relevanceFilter acc hyp := do
@@ -195,7 +225,7 @@ def embeddedConstraintPass : Pass := fun goal =>
     let relevantHyps : SimpTheoremsArray ← hyps.foldlM (init := #[]) relevanceFilter
 
     let simpCtx : Simp.Context := {
-      config := { failIfUnchanged := false }
+      config := { failIfUnchanged := false, maxSteps }
       simpTheorems := relevantHyps
       congrTheorems := (← getSimpCongrTheorems)
     }
@@ -222,32 +252,35 @@ def acNormalizePass : Pass := fun goal => do
 /--
 The normalization passes used by `bv_normalize` and thus `bv_decide`.
 -/
-def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
+def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
+  [
+    rewriteRulesPass cfg.maxSteps,
+    embeddedConstraintPass cfg.maxSteps
+  ]
 
-def passPipeline : MetaM (List Pass) := do
-  let opts ← getOptions
+def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
+  let mut passPipeline := defaultPipeline cfg
 
-  let mut passPipeline := defaultPipeline
-
-  if bv.ac_nf.get opts then
+  if cfg.acNf then
     passPipeline := passPipeline ++ [acNormalizePass]
 
   return passPipeline
 
 end Pass
 
-def bvNormalize (g : MVarId) : MetaM (Option MVarId) := do
+def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := do
   withTraceNode `bv (fun _ => return "Normalizing goal") do
     -- Contradiction proof
     let some g ← g.falseOrByContra | return none
     trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}"
-    Pass.fixpointPipeline (← Pass.passPipeline) g
+    Pass.fixpointPipeline (Pass.passPipeline cfg) g
 
 @[builtin_tactic Lean.Parser.Tactic.bvNormalize]
 def evalBVNormalize : Tactic := fun
-  | `(tactic| bv_normalize) => do
+  | `(tactic| bv_normalize $cfg:optConfig) => do
+    let cfg ← elabBVDecideConfig cfg
     let g ← getMainGoal
-    match ← bvNormalize g with
+    match ← bvNormalize g cfg with
     | some newGoal => replaceMainGoal [newGoal]
     | none => replaceMainGoal []
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -308,7 +308,7 @@ def evalTacticSeq : Tactic :=
 
 partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   if h : i < tactics.size then
-    let tactic := tactics.get ⟨i, h⟩
+    let tactic := tactics[i]
     catchInternalId unsupportedSyntaxExceptionId
       (evalTactic tactic)
       (fun _ => evalChoiceAux tactics (i+1))

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -200,7 +200,7 @@ where
     if explicit then
       let i := if i > 0 then i - 1 else i + xs.size
       if i < 0 || i ≥ xs.size then
-        throwError "invalid '{tacticName}' tactic, application has {xs.size} arguments but the index is out of bounds"
+        throwError "invalid '{tacticName}' tactic, application has {xs.size} argument(s) but the index is out of bounds"
       let idx := i.natAbs
       return (mkAppN f xs[0:idx], xs[idx:])
     else
@@ -217,7 +217,7 @@ where
           explicitIdxs := explicitIdxs.push k
       let i := if i > 0 then i - 1 else i + explicitIdxs.size
       if i < 0 || i ≥ explicitIdxs.size then
-        throwError "invalid '{tacticName}' tactic, application has {xs.size} explicit argument(s) but the index is out of bounds"
+        throwError "invalid '{tacticName}' tactic, application has {explicitIdxs.size} explicit argument(s) but the index is out of bounds"
       let idx := explicitIdxs[i.natAbs]!
       return (mkAppN f xs[0:idx], xs[idx:])
 

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -7,9 +7,11 @@ prelude
 import Lean.Meta.Tactic.Constructor
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.AuxLemma
+import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Clear
 import Lean.Meta.Tactic.Rename
 import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Config
 import Lean.Elab.SyntheticMVars
 
 namespace Lean.Elab.Tactic
@@ -347,6 +349,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
       replaceMainGoal [← (← getMainGoal).rename fvarId h.getId]
   | _ => throwUnsupportedSyntax
 
+
 /--
 Make sure `expectedType` does not contain free and metavariables.
 It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
@@ -355,8 +358,11 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
   let mut expectedType ← instantiateMVars expectedType
   if expectedType.hasFVar then
     expectedType ← zetaReduce expectedType
-  if expectedType.hasFVar || expectedType.hasMVar then
-    throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
+  if expectedType.hasMVar then
+    throwError "expected type must not contain meta variables{indentExpr expectedType}"
+  if expectedType.hasFVar then
+    throwError "expected type must not contain free variables{indentExpr expectedType}\n\
+      Use the '+revert' option to automatically cleanup and revert free variables."
   return expectedType
 
 /--
@@ -381,36 +387,96 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
               return ← blameDecideReductionFailure inst''
   return inst
 
-def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
+private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType : Expr) : TacticM Expr := do
+  let d ← mkDecide expectedType
+  let levels := (collectLevelParams {} expectedType).params.toList
+  let auxDeclName ← Term.mkAuxName `_nativeDecide
+  let decl := Declaration.defnDecl {
+    name := auxDeclName
+    levelParams := levels
+    type := mkConst ``Bool
+    value := d
+    hints := .abbrev
+    safety := .safe
+  }
+  addAndCompile decl
+  -- get instance from `d`
+  let s := d.appArg!
+  let rflPrf ← mkEqRefl (toExpr true)
+  let levelParams := levels.map .param
+  let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <|
+    mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName levelParams) (toExpr true) rflPrf
+  try
+    let lemmaName ← mkAuxLemma levels expectedType pf
+    return .const lemmaName levelParams
+  catch ex =>
+    -- Diagnose error
+    throwError MessageData.ofLazyM (es := #[expectedType]) do
+      let r ←
+        try
+          evalConst Bool auxDeclName
+        catch ex =>
+          return m!"\
+            tactic '{tacticName}' failed, could not evaluate decidable instance. \
+            Error: {ex.toMessageData}"
+      if !r then
+        return m!"\
+          tactic '{tacticName}' evaluated that the proposition\
+          {indentExpr expectedType}\n\
+          is false"
+      else
+        return m!"tactic '{tacticName}' failed. Error: {ex.toMessageData}"
+
+@[implemented_by elabNativeDecideCoreUnsafe]
+private opaque elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr
+
+def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do
+  if cfg.revert then
+    -- In revert mode: clean up the local context and then revert everything that is left.
+    liftMetaTactic1 fun g => do
+      let g ← g.cleanup
+      let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
+      return g
   closeMainGoalUsing tacticName fun expectedType _ => do
+    if cfg.kernel && cfg.native then
+      throwError "tactic '{tacticName}' failed, cannot simultaneously set both '+kernel' and '+native'"
     let expectedType ← preprocessPropToDecide expectedType
+    if cfg.native then
+      elabNativeDecideCore tacticName expectedType
+    else if cfg.kernel then
+      doKernel expectedType
+    else
+      doElab expectedType
+where
+  doElab (expectedType : Expr) : TacticM Expr := do
     let pf ← mkDecideProof expectedType
     -- Get instance from `pf`
     let s := pf.appFn!.appArg!
-    if kernelOnly then
-      -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
-      -- The `mkAuxLemma` function caches the result in two ways:
-      -- 1. First, the function makes use of a `type`-indexed cache per module.
-      -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
-      let levelsInType := (collectLevelParams {} expectedType).params
-      -- Level variables occurring in `expectedType`, in ambient order
-      let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
-      try
-        let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
-        return mkConst lemmaName (lemmaLevels.map .param)
-      catch _ =>
-        diagnose expectedType s none
+    let r ← withAtLeastTransparency .default <| whnf s
+    if r.isAppOf ``isTrue then
+      -- Success!
+      -- While we have a proof from reduction, we do not embed it in the proof term,
+      -- and instead we let the kernel recompute it during type checking from the following more
+      -- efficient term. The kernel handles the unification `e =?= true` specially.
+      return pf
     else
-      let r ← withAtLeastTransparency .default <| whnf s
-      if r.isAppOf ``isTrue then
-        -- Success!
-        -- While we have a proof from reduction, we do not embed it in the proof term,
-        -- and instead we let the kernel recompute it during type checking from the following more
-        -- efficient term. The kernel handles the unification `e =?= true` specially.
-        return pf
-      else
-        diagnose expectedType s r
-where
+      diagnose expectedType s r
+  doKernel (expectedType : Expr) : TacticM Expr := do
+    let pf ← mkDecideProof expectedType
+    -- Get instance from `pf`
+    let s := pf.appFn!.appArg!
+    -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
+    -- The `mkAuxLemma` function caches the result in two ways:
+    -- 1. First, the function makes use of a `type`-indexed cache per module.
+    -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
+    let levelsInType := (collectLevelParams {} expectedType).params
+    -- Level variables occurring in `expectedType`, in ambient order
+    let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
+    try
+      let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
+      return mkConst lemmaName (lemmaLevels.map .param)
+    catch _ =>
+      diagnose expectedType s none
   diagnose {α : Type} (expectedType s : Expr) (r? : Option Expr) : TacticM α :=
     -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
     throwError MessageData.ofLazyM (es := #[expectedType]) do
@@ -470,30 +536,20 @@ where
         did not reduce to '{.ofConstName ``isTrue}' or '{.ofConstName ``isFalse}'.\n\n\
         {stuckMsg}{hint}"
 
-@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
-  evalDecideCore `decide false
+declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
 
-@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun _ =>
-  evalDecideCore `decide! true
+@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  evalDecideCore `decide cfg
 
-private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do
-  let auxName ← Term.mkAuxName baseName
-  let decl := Declaration.defnDecl {
-    name := auxName, levelParams := [], type, value
-    hints := .abbrev
-    safety := .safe
-  }
-  addDecl decl
-  compileDecl decl
-  pure auxName
+@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  let cfg := { cfg with kernel := true }
+  evalDecideCore `decide! cfg
 
-@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
-  closeMainGoalUsing `nativeDecide fun expectedType _ => do
-    let expectedType ← preprocessPropToDecide expectedType
-    let d ← mkDecide expectedType
-    let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d
-    let rflPrf ← mkEqRefl (toExpr true)
-    let s := d.appArg! -- get instance from `d`
-    return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s <| mkApp3 (Lean.mkConst ``Lean.ofReduceBool) (Lean.mkConst auxDeclName) (toExpr true) rflPrf
+@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  let cfg := { cfg with native := true }
+  evalDecideCore `native_decide cfg
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/RCases.lean

@@ -526,7 +526,7 @@ where
   /-- Runs `rintroContinue` on `pats[i:]` -/
   loop i g fs clears a := do
     if h : i < pats.size then
-      rintroCore g fs clears a ref (pats.get ⟨i, h⟩) ty? (loop (i+1))
+      rintroCore g fs clears a ref pats[i] ty? (loop (i+1))
     else cont g fs clears a
 
 end

src/Lean/Elab/Tactic/Simpa.lean

@@ -95,7 +95,8 @@ deriving instance Repr for UseImplicitLambdaResult
       else
         g.assumption; pure stats
       if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
-        let stx ← match ← mkSimpOnly stx stats.usedTheorems with
+        let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩)
+        let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with
           | `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
             if unfold.isSome then
               `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)

src/Lean/Environment.lean

@@ -328,7 +328,7 @@ private def invalidExtMsg := "invalid environment extension has been accessed"
 
 unsafe def setState {σ} (ext : Ext σ) (exts : Array EnvExtensionState) (s : σ) : Array EnvExtensionState :=
   if h : ext.idx < exts.size then
-    exts.set ⟨ext.idx, h⟩ (unsafeCast s)
+    exts.set ext.idx (unsafeCast s)
   else
     have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
     panic! invalidExtMsg
@@ -345,7 +345,7 @@ unsafe def setState {σ} (ext : Ext σ) (exts : Array EnvExtensionState) (s : σ
 
 unsafe def getState {σ} [Inhabited σ] (ext : Ext σ) (exts : Array EnvExtensionState) : σ :=
   if h : ext.idx < exts.size then
-    let s : EnvExtensionState := exts.get ⟨ext.idx, h⟩
+    let s : EnvExtensionState := exts[ext.idx]
     unsafeCast s
   else
     panic! invalidExtMsg

src/Lean/InternalExceptionId.lean

@@ -37,7 +37,7 @@ def InternalExceptionId.getName (id : InternalExceptionId) : IO Name :=  do
   let exs ← internalExceptionsRef.get
   let i := id.idx;
   if h : i < exs.size then
-    return exs.get ⟨i, h⟩
+    return exs[i]
   else
     throw <| IO.userError "invalid internal exception id"
 

src/Lean/Level.lean

@@ -320,7 +320,7 @@ private def accMax (result : Level) (prev : Level) (offset : Nat) : Level :=
  -/
 private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev : Level) (prevK : Nat) (result : Level) : Level :=
   if h : i < lvls.size then
-    let lvl   := lvls.get ⟨i, h⟩
+    let lvl   := lvls[i]
     let curr  := lvl.getLevelOffset
     let currK := lvl.getOffset
     if curr == prev then
@@ -335,7 +335,7 @@ private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev
   It finds the first position that is not an explicit universe. -/
 private partial def skipExplicit (lvls : Array Level) (i : Nat) : Nat :=
   if h : i < lvls.size then
-    let lvl := lvls.get ⟨i, h⟩
+    let lvl := lvls[i]
     if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i
   else
     i
@@ -349,7 +349,7 @@ It assumes `lvls` has been sorted using `normLt`.
 -/
 private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Nat) (i : Nat) : Bool :=
   if h : i < lvls.size then
-    let lvl := lvls.get ⟨i, h⟩
+    let lvl := lvls[i]
     if lvl.getOffset ≥ maxExplicit then true
     else isExplicitSubsumedAux lvls maxExplicit (i+1)
   else

src/Lean/Message.lean

@@ -250,7 +250,7 @@ instance : Coe (Option Expr) MessageData := ⟨fun o => match o with | none => "
 
 partial def arrayExpr.toMessageData (es : Array Expr) (i : Nat) (acc : MessageData) : MessageData :=
   if h : i < es.size then
-    let e   := es.get ⟨i, h⟩;
+    let e   := es[i];
     let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e;
     toMessageData es (i+1) acc
   else

src/Lean/Meta/AppBuilder.lean

@@ -352,7 +352,7 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat →
   | i, args, j, instMVars, Expr.forallE n d b bi => do
     let d  := d.instantiateRevRange j args.size args
     if h : i < xs.size then
-      match xs.get ⟨i, h⟩ with
+      match xs[i] with
       | none =>
         match bi with
         | BinderInfo.instImplicit => do

src/Lean/Meta/Basic.lean

@@ -953,7 +953,7 @@ Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x
 
 @[inline] def withTransparency (mode : TransparencyMode) : n α → n α :=
-  mapMetaM <| withConfig (fun config => { config with transparency := mode })
+  withConfig (fun config => { config with transparency := mode })
 
 /-- `withDefault x` executes `x` using the default transparency setting. -/
 @[inline] def withDefault (x : n α) : n α :=
@@ -1081,7 +1081,7 @@ mutual
   private partial def withNewLocalInstancesImp
       (fvars : Array Expr) (i : Nat) (k : MetaM α) : MetaM α := do
     if h : i < fvars.size then
-      let fvar := fvars.get ⟨i, h⟩
+      let fvar := fvars[i]
       let decl ← getFVarLocalDecl fvar
       match (← isClassQuick? decl.type) with
       | .none   => withNewLocalInstancesImp fvars (i+1) k
@@ -1650,7 +1650,7 @@ def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.i
 
 private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do
   if h : i < ps.size then
-    let p := ps.get ⟨i, h⟩
+    let p := ps[i]
     match (← whnf e) with
     | .forallE _ _ b _ => instantiateForallAux ps (i+1) (b.instantiate1 p)
     | _                => throwError "invalid instantiateForall, too many parameters"
@@ -1663,7 +1663,7 @@ def instantiateForall (e : Expr) (ps : Array Expr) : MetaM Expr :=
 
 private partial def instantiateLambdaAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do
   if h : i < ps.size then
-    let p := ps.get ⟨i, h⟩
+    let p := ps[i]
     match (← whnf e) with
     | .lam _ _ b _ => instantiateLambdaAux ps (i+1) (b.instantiate1 p)
     | _            => throwError "invalid instantiateLambda, too many parameters"

src/Lean/Meta/Closure.lean

@@ -224,9 +224,9 @@ def collectExpr (e : Expr) : ClosureM Expr := do
 partial def pickNextToProcessAux (lctx : LocalContext) (i : Nat) (toProcess : Array ToProcessElement) (elem : ToProcessElement)
     : ToProcessElement × Array ToProcessElement :=
   if h : i < toProcess.size then
-    let elem' := toProcess.get ⟨i, h⟩
+    let elem' := toProcess[i]
     if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then
-      pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ elem) elem'
+      pickNextToProcessAux lctx (i+1) (toProcess.set i elem) elem'
     else
       pickNextToProcessAux lctx (i+1) toProcess elem
   else

src/Lean/Meta/CollectFVars.lean

@@ -29,7 +29,7 @@ where
     let s ← getThe CollectFVars.State
     let i ← get
     if h : i < s.fvarIds.size then
-      let r := s.fvarIds.get ⟨i, h⟩
+      let r := s.fvarIds[i]
       modify (· + 1)
       return some r
     else