one more

.github/PULL_REQUEST_TEMPLATE.md

@@ -5,10 +5,6 @@
 * 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.
@@ -16,6 +12,4 @@
 
 ---
 
-This PR <short changelog summary for feat/fix, see above>.
-
-Closes <`RFC` or `bug` issue number fixed by this PR, if any>
+Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)

.github/dependabot.yml

@@ -1,8 +0,0 @@
-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@v2
+      uses: raven-actions/actionlint@v1
       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@v14
+        uses: mymindstorm/setup-emsdk@v12
         with:
           version: 3.1.44
           actions-cache-folder: emsdk
@@ -492,7 +492,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@v1
         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@v2
+        uses: softprops/action-gh-release@v1
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/nix-ci.yml

@@ -110,6 +110,14 @@ 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
@@ -121,7 +129,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@v3.0
+        uses: nwtgck/actions-netlify@v2.0
         id: publish-manual
         with:
           publish-dir: ./dist

.github/workflows/pr-body.yml

@@ -1,23 +0,0 @@
-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@v6 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v2 # 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@v2
+        uses: softprops/action-gh-release@v1
         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@v7
+        uses: actions/github-script@v6
         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@v2.1.0
+        uses: dcarbone/install-jq-action@v1.0.1
 
       # 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@v7
+        uses: actions/github-script@v6
         with:
           script: |
             const description =

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v9
+      - uses: actions/stale@v8
         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](../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](doc/dev/index.md).
 
-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.
+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.
 
 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 -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 -lpthread -ldl -lrt -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,8 +17,6 @@ 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,4 +36,3 @@ import Init.Omega
 import Init.MacroTrace
 import Init.Grind
 import Init.While
-import Init.Syntax

src/Init/Control/Lawful/Instances.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Except
 import Init.Control.StateRef
-import Init.Ext
 
 open Function
 
@@ -15,7 +14,7 @@ open Function
 
 namespace ExceptT
 
-@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
   simp [run] at h
   assumption
 
@@ -106,7 +105,7 @@ instance : LawfulFunctor (Except ε) := inferInstance
 
 namespace ReaderT
 
-@[ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
+theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
   simp [run] at h
   exact funext h
 
@@ -168,7 +167,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
 
 namespace StateT
 
-@[ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
+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,21 +861,16 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
 
 /-! # Decidable -/
 
-@[simp] theorem decide_true (h : Decidable True) : @decide True h = true :=
+theorem decide_true_eq_true (h : Decidable True) : @decide True h = true :=
   match h with
   | isTrue _  => rfl
   | isFalse h => False.elim <| h ⟨⟩
 
-@[simp] theorem decide_false (h : Decidable False) : @decide False h = false :=
+theorem decide_false_eq_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,4 +17,3 @@ 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,7 +12,6 @@ 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 -/
@@ -30,8 +29,7 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp] theorem size_set (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    (set a i v h).size = a.size :=
+@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
   List.length_set ..
 
 @[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@@ -143,7 +141,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 v h
+  a.set ⟨i.toNat, h⟩ v
 
 @[extern "lean_array_pop"]
 def pop (a : Array α) : Array α where
@@ -166,14 +164,13 @@ count of 1 when called.
 -/
 @[extern "lean_array_fswap"]
 def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
-  let v₁ := a[i]
-  let v₂ := a[j]
+  let v₁ := a.get i
+  let v₂ := a.get j
   let a'  := a.set i v₂
-  a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
+  a'.set (size_set a i v₂ ▸ j) v₁
 
 @[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  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
+  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
   rw [size_set, size_set]
 
 /--
@@ -250,7 +247,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[i]
+  let e := a.get i
   let a := a.set i v
   (e, a)
 
@@ -274,22 +271,24 @@ 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 v                := a[i]
+    let idx : Fin a.size := ⟨i, h⟩
+    let v                := a.get idx
     -- 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 i (unsafeCast ())
+    let a'               := a.set idx (unsafeCast ())
     let v ← f v
-    pure <| a'.set i v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
+    pure <| a'.set (size_set a .. ▸ idx) v
   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 v   := a[i]
+    let idx := ⟨i, h⟩
+    let v   := a.get idx
     let v ← f v
-    pure <| a.set i v
+    pure <| a.set idx v
   else
     pure a
 
@@ -454,15 +453,15 @@ 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]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
   as.mapFinIdxM fun i a => f i a
 
 @[inline]
-def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
+def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
   for a in as do
     match (← f a) with
     | some b => return b
@@ -470,14 +469,14 @@ def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f
   return none
 
 @[inline]
-def findM? {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
+def findM? {α : Type} {m : Type → Type} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) := do
   for a in as do
     if (← p a) then
       return a
   return none
 
 @[inline]
-def findIdxM? [Monad m] (p : α → m Bool) (as : Array α) : m (Option Nat) := do
+def findIdxM? [Monad m] (as : Array α) (p : α → m Bool) : m (Option Nat) := do
   let mut i := 0
   for a in as do
     if (← p a) then
@@ -529,7 +528,7 @@ def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
   return !(← as.anyM (start := start) (stop := stop) fun v => return !(← p v))
 
 @[inline]
-def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) :=
+def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) :=
   let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
     | 0,   _ => pure none
     | i+1, h => do
@@ -543,7 +542,7 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
   find as.size (Nat.le_refl _)
 
 @[inline]
-def findRevM? {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) :=
+def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) :=
   as.findSomeRevM? fun a => return if (← p a) then some a else none
 
 @[inline]
@@ -572,7 +571,7 @@ def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size →
   Id.run <| as.mapFinIdxM f
 
 @[inline]
-def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β :=
+def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
@@ -580,29 +579,29 @@ def zipWithIndex (arr : Array α) : Array (α × Nat) :=
   arr.mapIdx fun i a => (a, i)
 
 @[inline]
-def find? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
+def find? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
   Id.run <| as.findM? p
 
 @[inline]
-def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
+def findSome? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
   Id.run <| as.findSomeM? f
 
 @[inline]
-def findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (a : Array α) : β :=
-  match a.findSome? f with
+def findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : α → Option β) : β :=
+  match findSome? a f with
   | some b => b
   | none   => panic! "failed to find element"
 
 @[inline]
-def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
+def findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
   Id.run <| as.findSomeRevM? f
 
 @[inline]
-def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
+def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
   Id.run <| as.findRevM? p
 
 @[inline]
-def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
+def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (j : Nat) :=
     if h : j < as.size then
@@ -617,7 +616,8 @@ 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
-    if a[i] == v then some ⟨i, h⟩
+    let idx : Fin a.size := ⟨i, h⟩;
+    if a.get idx == v then some idx
     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[as.size - 1]'(Nat.sub_lt h (by decide))) then
+    if p (as.get ⟨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[i]
+      let a := as.get ⟨i, h⟩
       if p a then
         go (i+1) (r.push a)
       else
@@ -866,7 +866,6 @@ 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 b h)
+        go (i+1) (as.set ⟨i, h⟩ b)
     else
       return as
 

src/Init/Data/Array/Bootstrap.lean

@@ -79,17 +79,6 @@ 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/Lemmas.lean

@@ -10,7 +10,6 @@ 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
@@ -190,151 +189,6 @@ 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 f l.toArray 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
@@ -450,7 +304,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 : Nat) (h) : a.get i h = a[i] := rfl
+@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
 
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
@@ -483,26 +337,25 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 
 /-! # set -/
 
-@[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) :
+@[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) :
     (a.set i v)[j]'p = v := by
   simp [set, getElem_eq_getElem_toList, ←eq]
 
-@[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] 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 only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
-theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
+theorem getElem_set (a : Array α) (i : Fin 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 = 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.1 = j <;> simp [p]
 
-@[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_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_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
-    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[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
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
 /-! # setD -/
@@ -519,7 +372,7 @@ theorem getElem_set (a : Array α) (i : Nat) (h' : i < 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, ↓reduceDIte, getElem_set_eq]
+  simp only [setD, h, dite_true, getElem_set, ite_true]
 
 @[simp]
 theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
@@ -694,47 +547,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 h) : (a.set i v).toList = a.toList.set i v := rfl
+@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
-theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    (a.set i v h)[i]'(by simp [h]) = v := by
+theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1] = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
 
-theorem get?_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    (a.set i v)[i]? = v := by simp [getElem?_pos, h]
+theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
 
-@[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
+@[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
   by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
 
-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) (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) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) :
+theorem get_set (a : Array α) (i : Fin 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 = j then subst j; simp [*] else simp [*]
+  if h : i.1 = j then subst j; simp [*] else simp [*]
 
-@[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] 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 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, ↓reduceDIte, getElem_set_eq]
+  simp only [setD, h, dite_true, get_set, ite_true]
 
-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]
+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]
 
 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[j]).set j a[i] := by
+    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get 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[j]).set j a[i] := by simp [swap_def]
+    (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get 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
@@ -748,7 +601,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 v) := by simp [swapAt!, h]
+    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
 
 @[simp] theorem size_swapAt! (a : Array α) (i : Nat) (v : α) :
     (a.swapAt! i v).2.size = a.size := by
@@ -1113,7 +966,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 : α → α) :
@@ -1197,6 +1050,8 @@ 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
@@ -1246,6 +1101,15 @@ 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 α)} :
@@ -1470,7 +1334,7 @@ termination_by stop - start
 
 -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
 theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
-    as.any p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
+    any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
   dsimp [any, anyM, Id.run]
   split
   · rw [anyM_loop_iff_exists]; rfl
@@ -1482,7 +1346,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
       exact ⟨i, by omega, by omega, h⟩
 
 theorem any_eq_true {p : α → Bool} {as : Array α} :
-    as.any p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
+    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
 
 theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
@@ -1502,20 +1366,20 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
   rw [List.allM_eq_not_anyM_not]
 
 theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
-    as.all p start stop = !(as.any (!p ·) start stop) := by
+    all as p start stop = !(any as (!p ·) start stop) := by
   dsimp [all, allM]
   rfl
 
 theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
-    as.all p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
+    all as p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
   rw [all_eq_not_any_not]
-  suffices ¬(as.any (!p ·) start stop = true) ↔
+  suffices ¬(any as (!p ·) start stop = true) ↔
       ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] by
     simp_all
   rw [any_iff_exists]
   simp
 
-theorem all_eq_true {p : α → Bool} {as : Array α} : as.all p ↔ ∀ i : Fin as.size, p as[i] := by
+theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
   simp [all_iff_forall, Fin.isLt]
 
 theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
@@ -1542,15 +1406,30 @@ 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.1] = a[i] := by
-  simp [swap_def, getElem_set]
+@[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_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_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_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
-  simp [swap_def, getElem_set, hi.symm, hj.symm]
+  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
 
 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
@@ -1581,54 +1460,6 @@ 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
@@ -1644,6 +1475,11 @@ 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
@@ -1775,7 +1611,7 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[simp] theorem extract_toArray (l : List α) (start stop : Nat) :
+@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
     l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
   apply ext'
   simp
@@ -1815,32 +1651,6 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     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
@@ -1855,80 +1665,6 @@ namespace 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 -/
@@ -2037,8 +1773,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/MapIdx.lean

@@ -66,35 +66,35 @@ theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
 
 /-! ### mapIdx -/
 
-theorem mapIdx_induction (f : Nat → α → β) (as : Array α)
+theorem mapIdx_induction (as : Array α) (f : Nat → α → β)
     (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (as.mapIdx f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
+    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
   mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
 
-theorem mapIdx_spec (f : Nat → α → β) (as : Array α)
+theorem mapIdx_spec (as : Array α) (f : Nat → α → β)
     (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
-    ∃ eq : (as.mapIdx f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
+    ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
   (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
 
-@[simp] theorem size_mapIdx (f : Nat → α → β) (as : Array α) : (as.mapIdx f).size = as.size :=
+@[simp] theorem size_mapIdx (a : Array α) (f : Nat → α → β) : (a.mapIdx f).size = a.size :=
   (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
 
-@[simp] theorem getElem_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat)
-    (h : i < (as.mapIdx f).size) :
-    (as.mapIdx f)[i] = f i (as[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b => b = f i as[i]) fun _ => rfl).2 i (by simp_all)
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
+    (a.mapIdx f)[i] = f i (a[i]'(by simp_all)) :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i (by simp_all)
 
-@[simp] theorem getElem?_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat) :
-    (as.mapIdx f)[i]? =
-      as[i]?.map (f i) := by
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat) :
+    (a.mapIdx f)[i]? =
+      a[i]?.map (f i) := by
   simp [getElem?_def, size_mapIdx, getElem_mapIdx]
 
-@[simp] theorem toList_mapIdx (f : Nat → α → β) (as : Array α) :
-    (as.mapIdx f).toList = as.toList.mapIdx (fun i a => f i a) := by
+@[simp] theorem toList_mapIdx (a : Array α) (f : Nat → α → β) :
+    (a.mapIdx f).toList = a.toList.mapIdx (fun i a => f i a) := by
   apply List.ext_getElem <;> simp
 
 end Array
@@ -105,7 +105,7 @@ namespace List
     l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
   ext <;> simp
 
-@[simp] theorem mapIdx_toArray (f : Nat → α → β) (l : List α) :
+@[simp] theorem mapIdx_toArray (l : List α) (f : Nat → α → β) :
     l.toArray.mapIdx f = (l.mapIdx f).toArray := by
   ext <;> simp
 

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 : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
   cases as with | _ as =>
-  simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)
+  exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 
 @[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
-  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _ h
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
 
 /-- 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

@@ -1,39 +0,0 @@
-/-
-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[i] else v₀
+  if h : i < s.size then s.get ⟨i, h⟩ 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[idx], assign.toAIGAssignment⟧
+   ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, 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 &&& twoPow w₂ 0) := by
-  simp only [sshiftRightRec]
+    sshiftRightRec x y 0 = x.sshiftRight' (y &&& 1#w₂) := by
+  simp only [sshiftRightRec, twoPow_zero]
 
 @[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.pos i
+      have := Fin.size_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]
-      · simp
+      · decide
       · omega
 
 @[bv_toNat] theorem getLsbD_succ_last (x : BitVec (w + 1)) :
@@ -512,31 +512,6 @@ 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]
@@ -658,7 +633,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
@@ -688,7 +663,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₁
@@ -760,9 +735,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
@@ -1114,21 +1089,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]
 
@@ -1139,9 +1114,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
@@ -1185,7 +1160,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) <;>
@@ -1283,8 +1258,7 @@ 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, decide_false, Bool.not_false, show i - n < w by omega, decide_true,
-        Bool.true_and]
+    · simp only [h, ushiftRight_eq, getLsbD_ushiftRight, show i - n < w by omega]
       congr
       omega
     · simp [h, h₁]
@@ -1353,17 +1327,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
@@ -1408,7 +1382,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]
@@ -1427,7 +1401,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]
@@ -1439,7 +1413,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
@@ -1457,15 +1431,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]
 
@@ -1485,15 +1459,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]
 
@@ -1518,11 +1492,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
 
@@ -1564,7 +1538,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
 
@@ -1648,7 +1622,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]
@@ -1660,7 +1634,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
@@ -1731,13 +1705,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
 
@@ -1767,7 +1741,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
@@ -1782,7 +1756,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
@@ -1802,7 +1776,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
@@ -1910,7 +1884,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
@@ -1951,7 +1925,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
@@ -1959,10 +1933,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
@@ -2052,9 +2026,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
 
-theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
+@[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
   rfl
-theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
+@[simp] 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.
@@ -2401,9 +2375,6 @@ 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`. -/
@@ -2471,10 +2442,6 @@ 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 =
@@ -2539,7 +2506,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
 
@@ -2727,9 +2694,6 @@ 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
@@ -2744,7 +2708,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)
@@ -2807,15 +2771,7 @@ 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]
-
-/--
-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]
+  simp [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /- ### cons -/
 
@@ -2843,7 +2799,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]
@@ -2859,7 +2815,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]
@@ -2869,7 +2825,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
 
@@ -2906,13 +2862,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]
@@ -2973,7 +2929,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) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
+def uget : (a : @& ByteArray) → (i : USize) → i.toNat < a.size → 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) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
-  | ⟨bs⟩, i, _ => bs[i]
+def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
+  | ⟨bs⟩, i => bs.get i
 
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-  getElem xs i h := xs.get i
+  getElem xs i h := xs.get ⟨i, h⟩
 
 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) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
-  | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
+def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
+  | ⟨bs⟩, i, b => ⟨bs.set i b⟩
 
 @[extern "lean_byte_array_uset"]
-def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
+def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → 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[as.size - 1 - i] b) with
+      match (← f (as.get ⟨as.size - 1 - i, this⟩) 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[j])
+          loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
       else
         pure b
     loop (stop - start) start init

src/Init/Data/Fin/Basic.lean

@@ -165,7 +165,6 @@ 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,19 +13,17 @@ import Init.Omega
 
 namespace Fin
 
-@[deprecated Fin.pos (since := "2024-11-11")]
-theorem size_pos (i : Fin n) : 0 < n := i.pos
+/-- 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
 
 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.pos) := rfl
+theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % 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 sub_def (a b : Fin n) : a - b = Fin.mk (((n - b) + a) % n) (Nat.mod_lt _ a.size_pos) := rfl
 
-theorem pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.pos
-
-@[deprecated pos' (since := "2024-11-11")] abbrev size_pos' := @pos'
+theorem size_pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.size_pos
 
 @[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
 
@@ -242,7 +240,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.pos) := rfl
+theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.size_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) → (i : @& Nat) → (h : i < ds.size := by get_elem_tactic) → Float
-  | ⟨ds⟩, i, h => ds.get i h
+def get : (ds : @& FloatArray) → (@& Fin ds.size) → Float
+  | ⟨ds⟩, i => ds.get i
 
 @[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
-    some (ds.get i h)
+    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 → (h : i.toNat < a.size := by get_elem_tactic) → FloatArray
+def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩
 
 @[extern "lean_float_array_fset"]
-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⟩
+def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
+  | ⟨ds⟩, i, d => ⟨ds.set i d⟩
 
 @[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[i] :: r)
+      loop (i+1) (ds.get ⟨i, h⟩ :: 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[as.size - 1 - i] b) with
+      match (← f (as.get ⟨as.size - 1 - i, this⟩) 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[j]'(Nat.lt_of_lt_of_le hlt h)))
+          loop i' (j+1) (← f b (as.get ⟨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`, `modify`, `insert`, `insertIdx`, `erase`, `eraseP`, `eraseIdx`.
+* Manipulating elements: `replace`, `insert`, `modify`, `erase`, `eraseP`, `eraseIdx`.
 * Finding elements: `find?`, `findSome?`, `findIdx`, `indexOf`, `findIdx?`, `indexOf?`,
  `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
@@ -1113,6 +1113,12 @@ 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 -/
 
 /--
@@ -1142,21 +1148,6 @@ 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,8 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Control.Basic
-import Init.Control.Id
-import Init.Control.Lawful
 import Init.Data.List.Basic
 
 namespace List
@@ -209,16 +207,6 @@ 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
@@ -227,28 +215,6 @@ 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,8 +206,7 @@ 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_iff_append :
-    xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ a ∈ as, !p a := by
+theorem find?_eq_some : 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 =>
@@ -243,9 +242,6 @@ theorem find?_eq_some_iff_append :
           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]
@@ -351,7 +347,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_iff_append]
+  rw [find?_eq_some]
   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`, `insertIdx`, `erase`, `eraseIdx`, `zipWith`,
+`take`, `takeWhile`, `dropLast`, `replace`, `modify`, `erase`, `eraseIdx`, `zipWith`,
 `enumFrom`, and `intercalate`.
 
 -/
@@ -215,23 +215,6 @@ 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,30 +863,14 @@ 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_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 α)
+theorem foldl_map' {α β : Type u} (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' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
+theorem foldr_map' {α β : Type u} (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
@@ -999,21 +983,6 @@ 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 ≠ []),
@@ -1488,22 +1457,6 @@ 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
@@ -2747,12 +2700,6 @@ 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],
@@ -2896,10 +2843,6 @@ 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,42 +86,6 @@ 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`.
@@ -208,8 +172,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, m⟩ => match b with
-        | .yield b => f a m b
+      l.attach.foldlM (fun b a => match b with
+        | .yield b => f a.1 a.2 b
         | .done b => pure (.done b)) (ForInStep.yield init) := by
   induction l generalizing init with
   | nil => simp
@@ -234,31 +198,6 @@ 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.
@@ -285,28 +224,6 @@ 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,4 +14,3 @@ 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,82 +64,3 @@ 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,32 +9,6 @@ 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

@@ -1,242 +0,0 @@
-/-
-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,25 +110,6 @@ 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_iff_append]
+  rw [find?_eq_some]
   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_iff_append]
+  rw [find?_eq_some]
   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,29 +52,4 @@ 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,14 +114,6 @@ 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/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,18 +52,6 @@ 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
 
@@ -475,114 +463,3 @@ 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[s.start]'(Nat.lt_of_lt_of_le h s.stop_le_array_size),
+      some (s.array.get ⟨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)[n]'(size_toUTF8 _ ▸ h)
+  (toUTF8 s).get ⟨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

@@ -224,7 +224,7 @@ 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,7 +7,6 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
-import Init.Syntax
 import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
@@ -443,7 +442,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 v h
+    | some v => some <| a.set ⟨i, h⟩ v
     | 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 (of_decide_eq_true rfl)
+  default := UInt8.ofNatCore 0 (by decide)
 
 /-- 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 (of_decide_eq_true rfl)
+  default := UInt16.ofNatCore 0 (by decide)
 
 /-- 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 (of_decide_eq_true rfl)
+  default := UInt32.ofNatCore 0 (by decide)
 
 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 (of_decide_eq_true rfl)
+  default := UInt64.ofNatCore 0 (by decide)
 
 /-- 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 (of_decide_eq_true rfl)
-  | _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)
+  | _, Or.inl rfl => Or.inl (by decide)
+  | _, Or.inr rfl => Or.inr (by decide)
 
 /--
 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 => of_decide_eq_true rfl
-    | _, Or.inr rfl => of_decide_eq_true rfl)
+    | _, Or.inl rfl => by decide
+    | _, Or.inr rfl => by decide)
 
 /--
 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 (of_decide_eq_true rfl)
+      | _, Or.inr rfl => Nat.lt_trans h (by decide)
     )
 
 /--
@@ -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 (of_decide_eq_true rfl)
-  | Or.inr ⟨_, h⟩ => Nat.lt_trans h (of_decide_eq_true rfl)
+  | Or.inl h      => Nat.lt_trans h (by decide)
+  | Or.inr ⟨_, h⟩ => Nat.lt_trans h (by decide)
 
 /--
 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 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) })
+    (fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) })
 
 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 (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))
+  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))
 
 /--
 `Option α` is the type of values which are either `some a` for some `a : α`,
@@ -2630,21 +2630,14 @@ 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 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.
--/
+/-- Access an element from an array without bounds checks, using a `Fin` index. -/
 @[extern "lean_array_fget"]
-def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
-  a.toList.get ⟨i, h⟩
+def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
+  a.toList.get i
 
 /-- 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"]
@@ -2695,6 +2688,35 @@ 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 α :=
@@ -2702,7 +2724,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
 
@@ -2717,7 +2739,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')
@@ -2836,7 +2858,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)
 
@@ -3458,7 +3480,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 (of_decide_eq_true rfl)
+        | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
         | _, Or.inr rfl, h => h
       )
 
@@ -3527,9 +3549,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 (of_decide_eq_true rfl)
+    | .anonymous => .ofNatCore 1723 (by decide)
     | .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 (of_decide_eq_true rfl)))
+    | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))
 
 instance : Inhabited Name where
   default := Name.anonymous
@@ -3615,13 +3637,6 @@ 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. -/
@@ -3954,6 +3969,24 @@ 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
@@ -4390,6 +4423,13 @@ 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])
+  cases g <;> (rename_i gp; simp [gp]; rfl)
 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,10 +277,8 @@ 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
 
-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 decide_False : decide False = false := rfl
+@[simp] theorem decide_True  : decide True  = true := rfl
 
 @[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,11 +41,7 @@ for every element of `α`.
 protected def default.sizeOf (α : Sort u) : α → Nat
   | _ => 0
 
-/--
-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
+instance (priority := low) (α : Sort u) : SizeOf α where
   sizeOf := default.sizeOf α
 
 @[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl

src/Init/Syntax.lean

@@ -1,36 +0,0 @@
-/-
-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,6 +990,13 @@ 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
@@ -1149,132 +1156,6 @@ 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[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"
+    | 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"
     | _                   => 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,9 +90,10 @@ 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 es  : AssocList α β   := source[i]
+     let idx : Fin source.size := ⟨i, h⟩
+     let es  : AssocList α β   := source.get idx
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set i AssocList.nil
+     let source                := source.set idx AssocList.nil
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target

src/Lean/Data/HashSet.lean

@@ -80,9 +80,10 @@ 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 es  : List α   := source[i]
+     let idx : Fin source.size := ⟨i, h⟩
+     let es  : List α   := source.get idx
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set i []
+     let source                := source.set idx []
      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[line]
+    text.positions.get ⟨line, h⟩
   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 := cs.size - 1
-      let last := cs[idx]
+      let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.pred_lt h⟩
+      let last := cs.get 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 idx (node newLast) (by simp only [cs', Array.size_set]; omega))
+          (some l, cs'.set (Array.size_set cs idx _ ▸ idx) (node newLast))
     else
       (none, emptyArray)
   | leaf vs   => (some vs, emptyArray)

src/Lean/Data/PersistentHashMap.lean

@@ -84,10 +84,11 @@ 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 k' := keys[i];
+      let idx : Fin keys.size := ⟨i, h⟩;
+      let k' := keys.get idx;
       if k == k' then
          let j : Fin vals.size := ⟨i, by rw [←heq]; assumption⟩
-         ⟨Node.collision (keys.set i k) (vals.set j v) (size_set heq ⟨i, h⟩ j k v), IsCollisionNode.mk _ _ _⟩
+         ⟨Node.collision (keys.set idx k) (vals.set j v) (size_set heq idx 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[pos.line - 1]
+      text.positions.get ⟨pos.line - 1, h⟩
     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[line - 1]
+    map.positions.get ⟨line - 1, h⟩
   else map.positions.back?.getD 0
 
 end FileMap

src/Lean/Elab/App.lean

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

src/Lean/Elab/BuiltinCommand.lean

@@ -111,8 +111,9 @@ 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 cmds[i])
+      (elabCommand cmd)
       (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.raw.toList.isPerm args.raw.toList then
+    if binders == args 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] || binders == #[b, a] then
+    if binders == #[a, b] then
       try Term.resolveId? f catch _ => return none
     else
       return none

src/Lean/Elab/Declaration.lean

@@ -192,7 +192,8 @@ 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
-      if isMutualPreambleCommand elems[i] then
+      let elem := elems.get ⟨i, h⟩
+      if isMutualPreambleCommand elem then
         loop (i+1)
       else if i == 0 then
         none -- `mutual` block does not contain any preamble commands

src/Lean/Elab/DefView.lean

@@ -11,13 +11,19 @@ import Lean.Elab.DeclUtil
 namespace Lean.Elab
 
 inductive DefKind where
-  | def | instance | theorem | example | opaque | abbrev
+  | def | 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
@@ -165,7 +171,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.instance, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.def, 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[i]
+      let view := views.get ⟨i, h⟩
       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[i]
+        let (declName, shortDeclName, type) := namesAndTypes.get ⟨i, h⟩
         Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
       else
         x params indFVars
@@ -740,7 +740,10 @@ 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 :=
-  mask.setD i false
+  if h : i < mask.size then
+    mask.set ⟨i, h⟩ false
+  else
+    mask
 
 /--
   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[i]
+      let view := views.get ⟨i, h⟩
       withAuxDecl view.shortDeclName view.type view.declName fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars
@@ -90,9 +90,9 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       for i in [0:view.binderIds.size] do
         addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
-        withInfoContext' view.valStx (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·)) do
-          let value ← elabTermEnsuringType view.valStx type
-          mkLambdaFVars xs value
+        withInfoContext' view.valStx (mkInfo := mkTermInfo `MutualDef.body view.valStx) do
+         let value ← elabTermEnsuringType view.valStx type
+         mkLambdaFVars xs value
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
   let letRecsToLiftCurr := (← get).letRecsToLift

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[i]
+      let discrStx := discrStxs.get ⟨i, h⟩
       let discr     ← elabAtomicDiscr discrStx
       let discr     ← instantiateMVars discr
       let userName ← mkUserNameFor discr
@@ -176,8 +176,9 @@ 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 pVars[i].getId BinderInfo.default type fun x =>
+      withLocalDecl var.getId BinderInfo.default type fun x =>
         loop (i+1) (decls.push { fvarId := x.fvarId! }) (userNames.push Name.anonymous)
     else
       k decls
@@ -759,7 +760,7 @@ where
     | [] => k eqs
     | p::ps =>
       if h : i < discrs.size then
-        let discr := discrs[i]
+        let discr := discrs.get ⟨i, h⟩
         if let some h := discr.h? then
           withLocalDeclD h.getId (← mkEqHEq discr.expr (← p.toExpr)) fun eq => do
             addTermInfo' h eq (isBinder := true)
@@ -956,7 +957,7 @@ where
     let mut s : CollectFVars.State := {}
     for discr in discrs do
       s := collectFVars s (← instantiateMVars (← inferType discr))
-    let (indicesFVar, indicesNonFVar) := indices.partition Expr.isFVar
+    let (indicesFVar, indicesNonFVar) := indices.split Expr.isFVar
     let indicesFVar := indicesFVar.map Expr.fvarId!
     let mut toAdd := #[]
     for fvarId in s.fvarSet.toList do

src/Lean/Elab/MutualDef.lean

@@ -22,14 +22,6 @@ 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
   /--
@@ -77,7 +69,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[0]
+    let firstHeader := prevHeaders.get ⟨0, h⟩
     try
       unless newHeader.levelNames == firstHeader.levelNames do
         throwError "universe parameters mismatch"
@@ -124,7 +116,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 ← instantiateMVarsProfiling e.appArg!
+    let arg ← instantiateMVars e.appArg!
     if !arg.isAppOfArity ``OfNat.ofNat 3 then return .continue
     let argArgs := arg.getAppArgs
     if !argArgs[0]!.isConstOf ``Nat then return .continue
@@ -199,7 +191,7 @@ private def elabHeaders (views : Array DefView)
             -- TODO: add forbidden predicate using `shortDeclName` from `views`
             let xs ← addAutoBoundImplicits xs
             type ← mkForallFVars' xs type
-            type ← instantiateMVarsProfiling type
+            type ← instantiateMVars type
             let levelNames ← getLevelNames
             if view.type?.isSome then
               let pendingMVarIds ← getMVars type
@@ -273,7 +265,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[i]
+      let header := headers.get ⟨i, h⟩
       if header.modifiers.isNonrec then
         loop (i+1) fvars
       else
@@ -337,6 +329,10 @@ 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`,
@@ -417,7 +413,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- Store instantiated body in info tree for the benefit of the unused variables linter
           -- and other metaprograms that may want to inspect it without paying for the instantiation
           -- again
-          withInfoContext' valStx (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·)) do
+          withInfoContext' valStx (mkInfo := mkTermInfo `MutualDef.body valStx) do
             -- synthesize mvars here to force the top-level tactic block (if any) to run
             let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
             -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
@@ -478,11 +474,11 @@ private def isTheorem (views : Array DefView) : Bool :=
   views.any (·.kind.isTheorem)
 
 private def instantiateMVarsAtHeader (header : DefViewElabHeader) : TermElabM DefViewElabHeader := do
-  let type ← instantiateMVarsProfiling header.type
+  let type ← instantiateMVars header.type
   pure { header with type := type }
 
 private def instantiateMVarsAtLetRecToLift (toLift : LetRecToLift) : TermElabM LetRecToLift := do
-  let type ← instantiateMVarsProfiling toLift.type
+  let type ← instantiateMVars toLift.type
   let val ← instantiateMVarsProfiling toLift.val
   pure { toLift with type, val }
 
@@ -867,7 +863,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 matches .def | .instance | .opaque | .abbrev then
+    let kind ← if kind.isDefOrAbbrevOrOpaque 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
@@ -915,7 +911,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 := (← instantiateMVarsProfiling toLift.type) }
+      return { toLift with val := (← instantiateMVarsProfiling toLift.val), type := (← instantiateMVars toLift.type) }
     let letRecClosures ← mkLetRecClosures sectionVars mainFVarIds recFVarIds letRecsToLift
     -- mkLetRecClosures assign metavariables that were placeholders for the lifted declarations.
     let mainVals    ← mainVals.mapM (instantiateMVarsProfiling ·)
@@ -936,7 +932,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[0].levelNames
+    (headers.get ⟨0, h⟩).levelNames
   else
     []
 
@@ -953,7 +949,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 := (← instantiateMVarsProfiling header.type) }
+  newHeaders.mapM fun header => return { header with type := (← instantiateMVars 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[i]
+      let d := ctx.paramDecls.get ⟨i, h⟩
       d.2.isExplicit
     else
       false

src/Lean/Elab/PreDefinition/Basic.lean

@@ -132,21 +132,14 @@ 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» => mkThmDecl
+      | DefKind.«theorem» =>
+        let d := {
+          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, all
+        }
+        reportTheoremDiag d
+        pure <| Declaration.thmDecl d
       | DefKind.«opaque»  =>
         pure <| Declaration.opaqueDecl {
           name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
@@ -158,8 +151,12 @@ 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 }
-      | DefKind.def | DefKind.example => mkDefDecl
-      | DefKind.«instance» => if ← Meta.isProp preDef.type then mkThmDecl else mkDefDecl
+      | _ => -- 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 }
     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 matches DefKind.def | DefKind.instance) || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
+              if preDefs.all fun preDef => preDef.kind == DefKind.def || 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[i]
+      let struct := structs.get ⟨i, h⟩
       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[i]
+      let subfieldName := subfieldNames.get ⟨i, h⟩
       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[i]
+        let fieldName := fieldNames.get ⟨i, h⟩
         let fieldType ← getFieldType infos parentType fieldName
         match findFieldInfo? infos fieldName with
         | some existingFieldInfo =>
@@ -548,9 +548,8 @@ where
       let parentType ← whnf type
       let parentStructName ← getStructureName parentType
       if parents.any (fun info => info.structName == parentStructName) then
-        logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}', skipping"
-        go (i + 1) infos parents
-      else if let some existingFieldName ← findExistingField? infos parentStructName then
+        logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}'"
+      if let some existingFieldName ← findExistingField? infos parentStructName then
         if structureDiamondWarning.get (← getOptions) then
           logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared"
         let parents := parents.push { ref := parent, fvar? := none, subobject := false, structName := parentStructName, type := parentType }
@@ -855,7 +854,6 @@ private def setSourceInstImplicit (type : Expr) : Expr :=
 Creates a projection function to a non-subobject parent.
 -/
 private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentStructName : Name) (parentType : Expr) : MetaM StructureParentInfo := do
-  let isProp ← Meta.isProp parentType
   let env ← getEnv
   let structName := view.declName
   let sourceFieldNames := getStructureFieldsFlattened env structName
@@ -885,24 +883,17 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
       return result
     let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType)))
     let declName := structName ++ mkToParentName (← getStructureName parentType) fun n => !env.contains (structName ++ n)
-    -- Logic from `mk_projections`: prop-valued projections are theorems (or at least opaque)
-    let cval : ConstantVal := { name := declName, levelParams, type := declType }
-    if isProp then
-      addDecl <|
-        if view.modifiers.isUnsafe then
-          -- Theorems cannot be unsafe.
-          Declaration.opaqueDecl { cval with value := declVal, isUnsafe := true }
-        else
-          Declaration.thmDecl { cval with value := declVal }
+    addAndCompile <| Declaration.defnDecl {
+      name        := declName
+      levelParams := levelParams
+      type        := declType
+      value       := declVal
+      hints       := ReducibilityHints.abbrev
+      safety      := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
+    }
+    if binfo.isInstImplicit then
+      addInstance declName AttributeKind.global (eval_prio default)
     else
-      addAndCompile <| Declaration.defnDecl { cval with
-        value       := declVal
-        hints       := ReducibilityHints.abbrev
-        safety      := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
-      }
-    -- Logic from `mk_projections`: non-instance-implicits that aren't props become reducible.
-    -- (Instances will get instance reducibility in `Lean.Elab.Command.addParentInstances`.)
-    if !binfo.isInstImplicit && !(← Meta.isProp parentType) then
       setReducibleAttribute declName
     return { structName := parentStructName, subobject := false, projFn := declName }
 
@@ -974,19 +965,6 @@ private def checkResolutionOrder (structName : Name) : TermElabM Unit := do
         must come after {MessageData.andList conflicts.toList}" :: defects
     logWarning m!"failed to compute strict resolution order:\n{MessageData.joinSep defects.reverse "\n"}"
 
-/--
-Adds each direct parent projection to a class as an instance, so long as the parent isn't an ancestor of the others.
--/
-private def addParentInstances (parents : Array StructureParentInfo) : MetaM Unit := do
-  let env ← getEnv
-  let instParents := parents.filter fun parent => isClass env parent.structName
-  -- A parent is an ancestor of the others if it appears with index ≥ 1 in one of the resolution orders.
-  let resOrders : Array (Array Name) ← instParents.mapM fun parent => getStructureResolutionOrder parent.structName
-  let instParents := instParents.filter fun parent =>
-    !resOrders.any (fun resOrder => resOrder[1:].any (· == parent.structName))
-  for instParent in instParents do
-    addInstance instParent.projFn AttributeKind.global (eval_prio default)
-
 def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
   let scopeLevelNames ← Term.getLevelNames
   let isUnsafe := view.modifiers.isUnsafe
@@ -1030,6 +1008,9 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
           addProjections r fieldInfos
           registerStructure view.declName fieldInfos
           mkAuxConstructions view.declName
+          let instParents ← fieldInfos.filterM fun info => do
+            let decl ← Term.getFVarLocalDecl! info.fvar
+            pure (info.isSubobject && decl.binderInfo.isInstImplicit)
           withSaveInfoContext do  -- save new env
             Term.addLocalVarInfo view.ref[1] (← mkConstWithLevelParams view.declName)
             if let some _ := view.ctor.ref.getPos? (canonicalOnly := true) then
@@ -1040,6 +1021,8 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
                 Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
           withRef view.declId do
             Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
+          let projInstances := instParents.toList.map fun info => info.declName
+          projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default)
           let parentInfos ← r.parents.mapM fun parent => do
             if parent.subobject then
               let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable!
@@ -1048,8 +1031,6 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
               mkCoercionToCopiedParent levelParams params view parent.structName parent.type
           setStructureParents view.declName parentInfos
           checkResolutionOrder view.declName
-          if view.isClass then
-            addParentInstances parentInfos
 
           let lctx ← getLCtx
           /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations

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 the `timeout` config option.\n"
-    err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option."
+    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."
     throwError err
   | .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
     if exitCode == 255 then

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

@@ -6,7 +6,6 @@ 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.
@@ -33,7 +32,30 @@ register_builtin_option sat.solver : String := {
         to use the one that ships with Lean."
 }
 
-declare_config_elab elabBVDecideConfig Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig
+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."
+}
 
 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) (cfg : BVDecideConfig) : TermElabM TacticContext := do
+def mkContext (lratPath : System.FilePath) : TermElabM TacticContext := do
   let lratPath := (← getSrcDir) / lratPath
-  TacticContext.new lratPath cfg
+  TacticContext.new lratPath
 
 /--
 Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
 -/
-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
+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
 
 @[inherit_doc Lean.Parser.Tactic.bvCheck]
-def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
+def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
   let unsatProver : UnsatProver := fun _ reflectionResult _ => do
     withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
-      let proof ← lratChecker ctx reflectionResult.bvExpr
+      let proof ← lratChecker cfg reflectionResult.bvExpr
       return .ok ⟨proof, ""⟩
   let _ ← closeWithBVReflection g unsatProver
   return ()
@@ -52,15 +52,14 @@ def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
 open Lean.Meta.Tactic in
 @[builtin_tactic Lean.Parser.Tactic.bvCheck]
 def evalBvCheck : Tactic := fun
-  | `(tactic| bv_check%$tk $cfgStx:optConfig $path:str) => do
-    let cfg ← elabBVDecideConfig cfgStx
-    let ctx ← BVDecide.Frontend.BVCheck.mkContext path.getString cfg
+  | `(tactic| bv_check%$tk $path:str) => do
+    let cfg ← BVDecide.Frontend.BVCheck.mkContext path.getString
     liftMetaFinishingTactic fun g => do
-      let g'? ← Normalize.bvNormalize g cfg
+      let g'? ← Normalize.bvNormalize g
       match g'? with
-      | some g' => bvCheck g' ctx
+      | some g' => bvCheck g' cfg
       | none =>
-        let bvNormalizeStx ← `(tactic| bv_normalize $cfgStx)
+        let bvNormalizeStx ← `(tactic| bv_normalize)
         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) (ctx : TacticContext) (reflectionResult : ReflectionResult)
+def lratBitblaster (goal : MVarId) (cfg : 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) (ctx : TacticContext) (reflectionResult : Ref
   let aigSize := entry.aig.decls.size
   trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
 
-  if ctx.config.graphviz then
+  if cfg.graphviz then
     IO.FS.writeFile ("." / "aig.gv") <| AIG.toGraphviz entry
 
   let (cnf, map) ←
@@ -211,12 +211,12 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref
 
   let res ←
     withTraceNode `sat (fun _ => return "Obtaining external proof certificate") do
-      runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs
+      runExternal cnf cfg.solver cfg.lratPath cfg.trimProofs cfg.timeout cfg.binaryProofs
 
   match res with
   | .ok cert =>
     trace[Meta.Tactic.sat] "SAT solver found a proof."
-    let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+    let proof ← cert.toReflectionProof cfg 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) (ctx : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
+def bvUnsat (g : MVarId) (cfg : 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 ctx reflectionResult atomsAssignment
+      lratBitblaster g cfg 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) (ctx : TacticContext) : MetaM (Except CounterExample Result) := do
-  let g? ← Normalize.bvNormalize g ctx.config
+def bvDecide' (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Result) := do
+  let g? ← Normalize.bvNormalize g
   let some g := g? | return .ok ⟨none⟩
-  match ← bvUnsat g ctx with
+  match ← bvUnsat g cfg 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) (ctx : TacticContext) : MetaM Result := do
-  match ← bvDecide' g ctx with
+def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
+  match ← bvDecide' g cfg with
   | .ok result => return result
   | .error counterExample =>
     counterExample.goal.withContext do
@@ -309,10 +309,9 @@ def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
 def evalBvTrace : Tactic := fun
-  | `(tactic| bv_decide $cfg:optConfig) => do
-    let cfg ← elabBVDecideConfig cfg
+  | `(tactic| bv_decide) => do
     IO.FS.withTempFile fun _ lratFile => do
-      let cfg ← BVDecide.Frontend.TacticContext.new lratFile cfg
+      let cfg ← BVDecide.Frontend.TacticContext.new lratFile
       liftMetaFinishingTactic fun g => do
         discard <| bvDecide g cfg
   | _ => throwUnsupportedSyntax

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

@@ -65,8 +65,6 @@ 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,13 +92,6 @@ 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
@@ -265,10 +258,11 @@ where
     let some distance ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr | return none
     shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
 
-  shiftReflection (distanceExpr : Expr) (innerExpr : Expr)
+  shiftReflection (β : Expr) (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,13 +34,12 @@ 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 $cfgStx:optConfig) => do
-    let cfg := { (← elabBVDecideConfig cfgStx) with trimProofs := false }
+  | `(tactic| bv_decide?%$tk) => do
     let lratFile : System.FilePath ← BVTrace.getLratFileName
-    let ctx ← BVCheck.mkContext lratFile cfg
+    let cfg := { (← BVCheck.mkContext lratFile) with trimProofs := false }
     let g ← getMainGoal
     let trace ← g.withContext do
-      bvDecide g ctx
+      bvDecide g cfg
     /-
     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:
@@ -58,12 +57,12 @@ def evalBvTrace : Tactic := fun
       let normalizeStx ← `(tactic| bv_normalize)
       TryThis.addSuggestion tk normalizeStx (origSpan? := ← getRef)
     | some .. =>
-      if ctx.config.trimProofs then
+      if sat.trimProofs.get (← getOptions) 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 $cfgStx:optConfig $(quote lratFile.toString))
+      let bvCheckStx ← `(tactic| bv_check $(quote lratFile.toString))
       TryThis.addSuggestion tk bvCheckStx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax
 

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

@@ -30,28 +30,37 @@ structure TacticContext where
   reflectionDef : Name
   solver : System.FilePath
   lratPath : System.FilePath
-  config : BVDecideConfig
+  graphviz : Bool
+  timeout : Nat
+  trimProofs : Bool
+  binaryProofs : Bool
 
-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
+def TacticContext.new (lratPath : System.FilePath) : Lean.Elab.TermElabM TacticContext := do
   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,
-    config
+    graphviz,
+    timeout,
+    trimProofs,
+    binaryProofs
   }
 where
   determineSolver : Lean.Elab.TermElabM System.FilePath := do

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

@@ -129,43 +129,11 @@ 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`.
 -/
-structure Pass where
-  name : Name
-  run : MVarId → MetaM (Option MVarId)
+abbrev Pass := MVarId → MetaM (Option MVarId)
 
 namespace Pass
 
@@ -176,8 +144,7 @@ the goal anymore.
 partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Option MVarId) := do
   let runPass (goal? : Option MVarId) (pass : Pass) : MetaM (Option MVarId) := do
     let some goal := goal? | return none
-    withTraceNode `bv (fun _ => return s!"Running pass: {pass.name}") do
-      pass.run goal
+    pass goal
 
   let some newGoal := ← passes.foldlM (init := some goal) runPass | return none
   if goal != newGoal then
@@ -190,159 +157,97 @@ partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Optio
 /--
 Responsible for applying the Bitwuzla style rewrite rules.
 -/
-def rewriteRulesPass (maxSteps : Nat) : Pass where
-  name := `rewriteRules
-  run goal := do
-    let bvThms ← bvNormalizeExt.getTheorems
-    let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
-    let sevalThms ← getSEvalTheorems
-    let sevalSimprocs ← Simp.getSEvalSimprocs
+def rewriteRulesPass : 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 }
+    simpTheorems := #[bvThms, sevalThms]
+    congrTheorems := (← getSimpCongrTheorems)
+  }
+
+  let hyps ← goal.getNondepPropHyps
+  let ⟨result?, _⟩ ← simpGoal goal
+    (ctx := simpCtx)
+    (simprocs := #[bvSimprocs, sevalSimprocs])
+    (fvarIdsToSimp := hyps)
+  let some (_, newGoal) := result? | return none
+  return newGoal
+
+/--
+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 =>
+  goal.withContext do
+    let hyps ← goal.getNondepPropHyps
+    let relevanceFilter acc hyp := do
+      let typ ← hyp.getType
+      let_expr Eq α _ rhs := typ | return acc
+      let_expr Bool := α | return acc
+      let_expr Bool.true := rhs | return acc
+      let localDecl ← hyp.getDecl
+      let proof  := localDecl.toExpr
+      acc.addTheorem (.fvar hyp) proof
+    let relevantHyps : SimpTheoremsArray ← hyps.foldlM (init := #[]) relevanceFilter
 
     let simpCtx : Simp.Context := {
-      config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
-      simpTheorems := #[bvThms, sevalThms]
+      config := { failIfUnchanged := false }
+      simpTheorems := relevantHyps
       congrTheorems := (← getSimpCongrTheorems)
     }
 
-    let hyps ← goal.getNondepPropHyps
-    let ⟨result?, _⟩ ← simpGoal goal
-      (ctx := simpCtx)
-      (simprocs := #[bvSimprocs, sevalSimprocs])
-      (fvarIdsToSimp := hyps)
+    let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps)
     let some (_, newGoal) := result? | return none
     return newGoal
 
-/--
-Flatten out ands. That is look for hypotheses of the form `h : (x && y) = true` and replace them
-with `h.left : x = true` and `h.right : y = true`. This can enable more fine grained substitutions
-in embedded constraint substitution.
--/
-def andFlatteningPass : Pass where
-  name := `andFlattening
-  run goal := do
-    goal.withContext do
-      let hyps ← goal.getNondepPropHyps
-      let mut newHyps := #[]
-      let mut oldHyps := #[]
-      for hyp in hyps do
-        let typ ← hyp.getType
-        let_expr Eq α eqLhs eqRhs := typ | continue
-        let_expr Bool.and lhs rhs := eqLhs | continue
-        let_expr Bool := α | continue
-        let_expr Bool.true := eqRhs | continue
-        let mkEqTrue (lhs : Expr) : Expr :=
-          mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) lhs (mkConst ``Bool.true)
-        let hypExpr := (← hyp.getDecl).toExpr
-        let leftHyp : Hypothesis := {
-          userName := (← hyp.getUserName) ++ `left,
-          type := mkEqTrue lhs,
-          value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_left) lhs rhs hypExpr
-        }
-        let rightHyp : Hypothesis := {
-          userName := (← hyp.getUserName) ++ `right,
-          type := mkEqTrue rhs,
-          value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_right) lhs rhs hypExpr
-        }
-        newHyps := newHyps.push leftHyp
-        newHyps := newHyps.push rightHyp
-        oldHyps := oldHyps.push hyp
-      if newHyps.size == 0 then
-        return goal
-      else
-        let (_, goal) ← goal.assertHypotheses newHyps
-        -- Given that we collected the hypotheses in the correct order above the invariant is given
-        let goal ← goal.tryClearMany oldHyps
-        return goal
-
-/--
-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. Additionally this drops all
-redundant top level hypotheses.
--/
-def embeddedConstraintPass (maxSteps : Nat) : Pass where
-  name := `embeddedConstraintSubsitution
-  run goal := do
-    goal.withContext do
-      let hyps ← goal.getNondepPropHyps
-      let mut relevantHyps : SimpTheoremsArray := #[]
-      let mut seen : Std.HashSet Expr := {}
-      let mut duplicates : Array FVarId := #[]
-      for hyp in hyps do
-        let typ ← hyp.getType
-        let_expr Eq α lhs rhs := typ | continue
-        let_expr Bool.true := rhs | continue
-        let_expr Bool := α | continue
-        if seen.contains lhs then
-          -- collect and later remove duplicates on the fly
-          duplicates := duplicates.push hyp
-        else
-          seen := seen.insert lhs
-          let localDecl ← hyp.getDecl
-          let proof  := localDecl.toExpr
-          relevantHyps ← relevantHyps.addTheorem (.fvar hyp) proof
-
-      let goal ← goal.tryClearMany duplicates
-
-      let simpCtx : Simp.Context := {
-        config := { failIfUnchanged := false, maxSteps }
-        simpTheorems := relevantHyps
-        congrTheorems := (← getSimpCongrTheorems)
-      }
-
-      let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := ← goal.getNondepPropHyps)
-      let some (_, newGoal) := result? | return none
-      return newGoal
-
 /--
 Normalize with respect to Associativity and Commutativity.
 -/
-def acNormalizePass : Pass where
-  name := `ac_nf
-  run goal := do
-    let mut newGoal := goal
-    for hyp in (← goal.getNondepPropHyps) do
-      let result ← Lean.Meta.AC.acNfHypMeta newGoal hyp
+def acNormalizePass : Pass := fun goal => do
+  let mut newGoal := goal
+  for hyp in (← goal.getNondepPropHyps) do
+    let result ← Lean.Meta.AC.acNfHypMeta newGoal hyp
 
-      if let .some nextGoal := result then
-        newGoal := nextGoal
-      else
-        return none
+    if let .some nextGoal := result then
+      newGoal := nextGoal
+    else
+      return none
 
-    return newGoal
+  return newGoal
 
 /--
 The normalization passes used by `bv_normalize` and thus `bv_decide`.
 -/
-def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
-  [
-    rewriteRulesPass cfg.maxSteps,
-    andFlatteningPass,
-    embeddedConstraintPass cfg.maxSteps
-  ]
+def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
 
-def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
-  let mut passPipeline := defaultPipeline cfg
+def passPipeline : MetaM (List Pass) := do
+  let opts ← getOptions
 
-  if cfg.acNf then
+  let mut passPipeline := defaultPipeline
+
+  if bv.ac_nf.get opts then
     passPipeline := passPipeline ++ [acNormalizePass]
 
   return passPipeline
 
 end Pass
 
-def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := do
+def bvNormalize (g : MVarId) : 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 cfg) g
+    Pass.fixpointPipeline (← Pass.passPipeline) g
 
 @[builtin_tactic Lean.Parser.Tactic.bvNormalize]
 def evalBVNormalize : Tactic := fun
-  | `(tactic| bv_normalize $cfg:optConfig) => do
-    let cfg ← elabBVDecideConfig cfg
+  | `(tactic| bv_normalize) => do
     let g ← getMainGoal
-    match ← bvNormalize g cfg with
+    match ← bvNormalize g 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[i]
+    let tactic := tactics.get ⟨i, h⟩
     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} argument(s) but the index is out of bounds"
+        throwError "invalid '{tacticName}' tactic, application has {xs.size} arguments 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 {explicitIdxs.size} explicit argument(s) but the index is out of bounds"
+        throwError "invalid '{tacticName}' tactic, application has {xs.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,11 +7,9 @@ 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
@@ -349,7 +347,6 @@ 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.
@@ -358,11 +355,8 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
   let mut expectedType ← instantiateMVars expectedType
   if expectedType.hasFVar then
     expectedType ← zetaReduce 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."
+  if expectedType.hasFVar || expectedType.hasMVar then
+    throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
   return expectedType
 
 /--
@@ -387,96 +381,36 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
               return ← blameDecideReductionFailure inst''
   return inst
 
-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
+def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
   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
+    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
     else
-      doElab expectedType
+      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
-  doElab (expectedType : Expr) : TacticM Expr := do
-    let pf ← mkDecideProof expectedType
-    -- Get instance from `pf`
-    let s := pf.appFn!.appArg!
-    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
-  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
@@ -536,20 +470,30 @@ where
         did not reduce to '{.ofConstName ``isTrue}' or '{.ofConstName ``isFalse}'.\n\n\
         {stuckMsg}{hint}"
 
-declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
+@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
+  evalDecideCore `decide false
 
-@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  evalDecideCore `decide cfg
+@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun _ =>
+  evalDecideCore `decide! true
 
-@[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
+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.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  let cfg := { cfg with native := true }
-  evalDecideCore `native_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
 
 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[i] ty? (loop (i+1))
+      rintroCore g fs clears a ref (pats.get ⟨i, h⟩) ty? (loop (i+1))
     else cont g fs clears a
 
 end

src/Lean/Elab/Tactic/Simpa.lean

@@ -95,8 +95,7 @@ deriving instance Repr for UseImplicitLambdaResult
       else
         g.assumption; pure stats
       if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
-        let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩)
-        let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with
+        let stx ← match ← mkSimpOnly stx 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/Elab/Term.lean

@@ -1339,21 +1339,6 @@ def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → Term
   else
     Elab.withInfoContext' x mkInfo
 
-/-- Info node capturing `def/let rec` bodies, used by the unused variables linter. -/
-structure BodyInfo where
-  /-- The body as a fully elaborated term. -/
-  value : Expr
-deriving TypeName
-
-/-- Creates an `Info.ofCustomInfo` node backed by a `BodyInfo`. -/
-def mkBodyInfo (stx : Syntax) (value : Expr) : Info :=
-  .ofCustomInfo { stx, value := .mk { value : BodyInfo } }
-
-/-- Extracts a `BodyInfo` custom info. -/
-def getBodyInfo? : Info → Option BodyInfo
-  | .ofCustomInfo { value, .. } => value.get? BodyInfo
-  | _ => none
-
 /--
 Postpone the elaboration of `stx`, return a metavariable that acts as a placeholder, and
 ensures the info tree is updated and a hole id is introduced.

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 (unsafeCast s)
+    exts.set ⟨ext.idx, h⟩ (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[ext.idx]
+    let s : EnvExtensionState := exts.get ⟨ext.idx, h⟩
     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[i]
+    return exs.get ⟨i, h⟩
   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[i]
+    let lvl   := lvls.get ⟨i, h⟩
     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[i]
+    let lvl := lvls.get ⟨i, h⟩
     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[i]
+    let lvl := lvls.get ⟨i, h⟩
     if lvl.getOffset ≥ maxExplicit then true
     else isExplicitSubsumedAux lvls maxExplicit (i+1)
   else

src/Lean/Linter/UnusedVariables.lean

@@ -18,7 +18,7 @@ It is not immediately obvious but this is a surprisingly expensive check without
 some optimizations.  The main complication is that it can be difficult to
 determine what constitutes a "use" apart from direct references to a variable
 that we can easily find in the info tree.  For example, we would like this to be
-considered a use of `x`:
+considered a use of `x`: 
 ```
 def foo (x : Nat) : Nat := by assumption
 ```
@@ -390,20 +390,22 @@ where
         -- set if `analyzeTactics` is unset, tactic infos are present, and we're inside the body
         let ignored ← read
         match info with
-        | .ofCustomInfo ti =>
-          if !linter.unusedVariables.analyzeTactics.get ci.options then
-            if let some bodyInfo := ti.value.get? Elab.Term.BodyInfo then
-              -- the body is the only `Expr` we will analyze in this case
-              -- NOTE: we include it even if no tactics are present as at least for parameters we want
-              -- to lint only truly unused binders
-              let (e, _) := instantiateMVarsCore ci.mctx bodyInfo.value
-              modify fun s => { s with
-                assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
-              let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
-              withReader (· || tacticsPresent) do
-                go children.toArray ci
-              return false
         | .ofTermInfo ti =>
+          -- NOTE: we have to do this check *before* `ignored` because nested bodies (e.g. from
+          -- nested `let rec`s) do need to be included to find all `Expr` uses of the top-level
+          -- parameters
+          if ti.elaborator == `MutualDef.body &&
+              !linter.unusedVariables.analyzeTactics.get ci.options then
+            -- the body is the only `Expr` we will analyze in this case
+            -- NOTE: we include it even if no tactics are present as at least for parameters we want
+            -- to lint only truly unused binders
+            let (e, _) := instantiateMVarsCore ci.mctx ti.expr
+            modify fun s => { s with
+              assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
+            let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
+            withReader (· || tacticsPresent) do
+              go children.toArray ci
+            return false
           if ignored then return true
           match ti.expr with
           | .const .. =>
@@ -439,20 +441,22 @@ where
               -- Found a direct use, keep track of it
               modify fun s => { s with fvarUses := s.fvarUses.insert id }
           | _ => pure ()
+          return true
         | .ofTacticInfo ti =>
           -- When ignoring new binders, no need to look at intermediate tactic states either as
           -- references to binders outside the body will be covered by the body `Expr`
           if ignored then return true
           -- Keep track of the `MetavarContext` after a tactic for later
           modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
+          return true
         | .ofFVarAliasInfo i =>
           if ignored then return true
           -- record any aliases we find
           modify fun s =>
             let id := followAliases s.fvarAliases i.baseId
             { s with fvarAliases := s.fvarAliases.insert i.id id }
-        | _ => pure ()
-        return true)
+          return true
+        | _ => return true)
   /-- Since declarations attach the declaration info to the `declId`,
   we skip that to get to the `.ident` if possible. -/
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=

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[i];
+    let e   := es.get ⟨i, h⟩;
     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[i] with
+      match xs.get ⟨i, h⟩ 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 α :=
-  withConfig (fun config => { config with transparency := mode })
+  mapMetaM <| 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[i]
+      let fvar := fvars.get ⟨i, h⟩
       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[i]
+    let p := ps.get ⟨i, h⟩
     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[i]
+    let p := ps.get ⟨i, h⟩
     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[i]
+    let elem' := toProcess.get ⟨i, h⟩
     if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then
-      pickNextToProcessAux lctx (i+1) (toProcess.set i elem) elem'
+      pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ elem) elem'
     else
       pickNextToProcessAux lctx (i+1) toProcess elem
   else