fixes

.github/workflows/check-prelude.yml

@@ -11,9 +11,7 @@ jobs:
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
-          sparse-checkout: |
-            src/Lean
-            src/Std
+          sparse-checkout: src/Lean
       - name: Check Prelude
         run: |
           failed_files=""
@@ -21,8 +19,8 @@ jobs:
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean src/Std -name '*.lean' -print0)
+          done < <(find src/Lean -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1
-          fi
+          fi

.github/workflows/nix-ci.yml

@@ -96,7 +96,7 @@ jobs:
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/build/source/src/build ./push-test; false)
+          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
       - name: Test Summary
         uses: test-summary/action@v2
         with:

CODEOWNERS

@@ -4,14 +4,14 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @Kha @kim-em
-/RELEASES.md @kim-em
+/.github/ @Kha @semorrison
+/RELEASES.md @semorrison
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
 /src/Lean/Compiler/ @leodemoura
 /src/Lean/Data/Lsp/ @mhuisi
-/src/Lean/Elab/Deriving/ @kim-em
-/src/Lean/Elab/Tactic/ @kim-em
+/src/Lean/Elab/Deriving/ @semorrison
+/src/Lean/Elab/Tactic/ @semorrison
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
 /src/Lean/Parser/ @Kha
@@ -19,7 +19,7 @@
 /src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
-/src/Init/Data/ @kim-em
+/src/Init/Data/ @semorrison
 /src/Init/Data/Array/Lemmas.lean @digama0
 /src/Init/Data/List/Lemmas.lean @digama0
 /src/Init/Data/List/BasicAux.lean @digama0
@@ -45,4 +45,3 @@
 /src/Std/ @TwoFX
 /src/Std/Tactic/BVDecide/ @hargoniX
 /src/Lean/Elab/Tactic/BVDecide/ @hargoniX
-/src/Std/Sat/ @hargoniX

doc/make/msys2.md

@@ -15,13 +15,6 @@ Mode](https://docs.microsoft.com/en-us/windows/apps/get-started/enable-your-devi
 which will allow Lean to create symlinks that e.g. enable go-to-definition in
 the stdlib.
 
-## Installing the Windows SDK
-
-Install the Windows SDK from [Microsoft](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
-The oldest supported version is 10.0.18362.0. If you installed the Windows SDK to the default location,
-then there should be a directory with the version number at `C:\Program Files (x86)\Windows Kits\10\Include`.
-If there are multiple directories, only the highest version number matters.
-
 ## Installing dependencies
 
 [The official webpage of MSYS2][msys2] provides one-click installers.

doc/setup.md

@@ -7,7 +7,7 @@ Platforms built & tested by our CI, available as binary releases via elan (see b
 * x86-64 Linux with glibc 2.27+
 * x86-64 macOS 10.15+
 * aarch64 (Apple Silicon) macOS 10.15+
-* x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022
+* x86-64 Windows 10+
 
 ### Tier 2
 

script/prepare-llvm-mingw.sh

@@ -31,20 +31,14 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # runtime
 (cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
 # further dependencies
-# Note: even though we're linking against libraries like `libbcrypt.a` which appear to be static libraries from the file name,
-# we're not actually linking statically against the code.
-# Rather, `libbcrypt.a` is an import library (see https://en.wikipedia.org/wiki/Dynamic-link_library#Import_libraries) that just
-# tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
-# This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
-# be delivered to users via Windows Update without having to recompile Lean or Lean programs.
-cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
+cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
 echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
-# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
+# when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
 # do not set `LEAN_CC` for tests
 echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"

src/CMakeLists.txt

@@ -297,23 +297,6 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LIBRARIES}")
 endif()
 
-# Windows SDK (for ICU)
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  # Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
-  find_package(WindowsSDK REQUIRED COMPONENTS tools)
-
-  # This will give a semicolon-separated list of include directories
-  get_windowssdk_include_dirs(${WINDOWSSDK_LATEST_DIR} WINDOWSSDK_INCLUDE_DIRS)
-
-  # To successfully build against Windows SDK headers, the Windows SDK headers must have lower
-  # priority than other system headers, so use `-idirafter`. Unfortunately, CMake does not
-  # support this using `include_directories`.
-  string(REPLACE ";" "\" -idirafter \"" WINDOWSSDK_INCLUDE_DIRS "${WINDOWSSDK_INCLUDE_DIRS}")
-  string(APPEND CMAKE_CXX_FLAGS " -idirafter \"${WINDOWSSDK_INCLUDE_DIRS}\"")
-
-  string(APPEND LEAN_EXTRA_LINKER_FLAGS " -licu")
-endif()
-
 # ccache
 if(CCACHE AND NOT CMAKE_CXX_COMPILER_LAUNCHER AND NOT CMAKE_C_COMPILER_LAUNCHER)
   find_program(CCACHE_PATH ccache)
@@ -497,7 +480,7 @@ endif()
 # Git HASH
 if(USE_GITHASH)
   include(GetGitRevisionDescription)
-  get_git_head_revision(GIT_REFSPEC GIT_SHA1 ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
+  get_git_head_revision(GIT_REFSPEC GIT_SHA1)
   if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
     message(STATUS "Failed to read git_sha1")
     set(GIT_SHA1 "")

src/Init.lean

@@ -35,4 +35,3 @@ import Init.Ext
 import Init.Omega
 import Init.MacroTrace
 import Init.Grind
-import Init.While

src/Init/Control/StateRef.lean

@@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 The State monad transformer using IO references.
 -/
 prelude
-import Init.System.ST
+import Init.System.IO
+import Init.Control.State
 
 def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 

src/Init/Core.lean

@@ -1937,6 +1937,15 @@ instance : Subsingleton (Squash α) where
     apply Quot.sound
     trivial
 
+/-! # Relations -/
+
+/--
+`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
+-/
+class Antisymm {α : Sort u} (r : α → α → Prop) : Prop where
+  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
+  antisymm {a b : α} : r a b → r b a → a = b
+
 namespace Lean
 /-! # Kernel reduction hints -/
 
@@ -2112,14 +2121,4 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
 instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
 instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
 
-/--
-`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
--/
-class Antisymm (r : α → α → Prop) : Prop where
-  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
-  antisymm {a b : α} : r a b → r b a → a = b
-
-@[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
-abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
-
 end Std

src/Init/Data/Array.lean

@@ -16,4 +16,3 @@ import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
-import Init.Data.Array.MapIdx

src/Init/Data/Array/Basic.lean

@@ -25,8 +25,6 @@ variable {α : Type u}
 
 namespace Array
 
-@[deprecated size (since := "2024-10-13")] abbrev data := @toList
-
 /-! ### Preliminary theorems -/
 
 @[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
@@ -80,26 +78,6 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
 
-@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
-
-end Array
-
-namespace List
-
-@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
-
-@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
-    a.toArray[i] = a[i]'(by simpa using h) := rfl
-
-@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
-
-@[simp] theorem getElem!_toArray [Inhabited α] {a : List α} {i : Nat} :
-    a.toArray[i]! = a[i]! := rfl
-
-end List
-
-namespace Array
-
 @[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
 
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@@ -241,15 +219,12 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited (α × Array α) := ⟨(v, a)⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
-/-- `take a n` returns the first `n` elements of `a`. -/
-def take (a : Array α) (n : Nat) : Array α :=
+def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
     | 0,   a => a
     | n+1, a => loop n a.pop
   loop (a.size - n) a
 
-@[deprecated take (since := "2024-10-22")] abbrev shrink := @take
-
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
@@ -421,25 +396,20 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
-/-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
-    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
     match i, inv with
     | 0,    _  => pure bs
     | i+1, inv =>
-      have j_lt : j < as.size := by
+      have : j < as.size := by
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
+      let idx : Fin as.size := ⟨j, this⟩
       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 idx (as.get idx)))
   map as.size 0 rfl (mkEmpty as.size)
 
-@[inline]
-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] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
   for a in as do
@@ -545,13 +515,8 @@ def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : A
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
   Id.run <| as.mapM f
 
-/-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
-  Id.run <| as.mapFinIdxM f
-
-@[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
+def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
@@ -852,15 +817,9 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
 
 /-! ## Auxiliary functions used in metaprogramming.
 
-We do not currently intend to provide verification theorems for these functions.
+We do not intend to provide verification theorems for these functions.
 -/
 
-/- ### reduceOption -/
-
-/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
-@[inline] def reduceOption (as : Array (Option α)) : Array α :=
-  as.filterMap id
-
 /-! ### eraseReps -/
 
 /--

src/Init/Data/Array/Bootstrap.lean

@@ -42,7 +42,7 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
   unfold foldrM.fold
   match i with
   | 0 => simp [List.foldlM, List.take]
-  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]
+  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
     arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by

src/Init/Data/Array/DecidableEq.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.Data.BEq
-import Init.Data.Nat.Lemmas
-import Init.Data.List.Nat.BEq
 import Init.ByCases
 
 namespace Array
@@ -28,14 +26,6 @@ theorem rel_of_isEqvAux
       subst hj'
       exact heqv.left
 
-theorem isEqvAux_of_rel (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
-    (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
-  induction i with
-  | zero => simp [Array.isEqvAux]
-  | succ i ih =>
-    simp only [isEqvAux, Bool.and_eq_true]
-    exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
-
 theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
     Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
   simp only [isEqv]
@@ -43,29 +33,6 @@ theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
   · exact fun h' => ⟨h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
-theorem isEqv_iff_rel (a b : Array α) (r) :
-    Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
-  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
-    simp only [isEqv, ← h, ↓reduceDIte]
-    exact isEqvAux_of_rel r a b h a.size (by simp [h]) w⟩
-
-theorem isEqv_eq_decide (a b : Array α) (r) :
-    Array.isEqv a b r =
-      if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h'))) else false := by
-  by_cases h : Array.isEqv a b r
-  · simp only [h, Bool.true_eq]
-    simp only [isEqv_iff_rel] at h
-    obtain ⟨h, w⟩ := h
-    simp [h, w]
-  · let h' := h
-    simp only [Bool.not_eq_true] at h
-    simp only [h, Bool.false_eq, dite_eq_right_iff, decide_eq_false_iff_not, Classical.not_forall,
-      Bool.not_eq_true]
-    simpa [isEqv_iff_rel] using h'
-
-@[simp] theorem isEqv_toList [BEq α] (a b : Array α) : (a.toList.isEqv b.toList r) = (a.isEqv b r) := by
-  simp [isEqv_eq_decide, List.isEqv_eq_decide]
-
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
   have ⟨h, h'⟩ := rel_of_isEqv (fun x y => x = y) a b h
   exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
@@ -89,22 +56,4 @@ instance [DecidableEq α] : DecidableEq (Array α) :=
     | true  => isTrue (eq_of_isEqv a b h)
     | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
 
-theorem beq_eq_decide [BEq α] (a b : Array α) :
-    (a == b) = if h : a.size = b.size then
-      decide (∀ (i : Nat) (h' : i < a.size), a[i] == b[i]'(h ▸ h')) else false := by
-  simp [BEq.beq, isEqv_eq_decide]
-
-@[simp] theorem beq_toList [BEq α] (a b : Array α) : (a.toList == b.toList) = (a == b) := by
-  simp [beq_eq_decide, List.beq_eq_decide]
-
 end Array
-
-namespace List
-
-@[simp] theorem isEqv_toArray [BEq α] (a b : List α) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
-  simp [isEqv_eq_decide, Array.isEqv_eq_decide]
-
-@[simp] theorem beq_toArray [BEq α] (a b : List α) : (a.toArray == b.toArray) = (a == b) := by
-  simp [beq_eq_decide, Array.beq_eq_decide]
-
-end List

src/Init/Data/Array/GetLit.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -8,17 +8,19 @@ import Init.Data.Nat.Lemmas
 import Init.Data.List.Impl
 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.Array.Mem
 import Init.TacticsExtra
 
 /-!
-## Theorems about `Array`.
+## Bootstrapping theorems about arrays
+
+This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`.
 -/
 
 namespace Array
 
+@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
+
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
 theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
@@ -43,32 +45,21 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
   rw [getElem?_eq]
   split <;> simp_all
 
-theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
   simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
 
-@[simp] theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
+@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
   simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
   rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
 
-theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
+theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
   by_cases h' : i < a.size
-  · simp [getElem_push_lt, h']
+  · simp [get_push_lt, h']
   · simp at h
-    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
-
-@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
-@[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
-@[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
-
-@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
-  simp [getElem!_def, get!, getD]
-  split <;> rename_i h
-  · simp [getElem?_eq_getElem h]
-    rfl
-  · simp [getElem?_eq_none_iff.2 (by simpa using h)]
+    simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
 
 end Array
 
@@ -85,6 +76,13 @@ We prefer to pull `List.toArray` outwards.
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+
+@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
+    a.toArray[i] = a[i]'(by simpa using h) := rfl
+
+@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
+
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -94,33 +92,6 @@ We prefer to pull `List.toArray` outwards.
   funext a
   simp
 
-@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
-  cases l <;> simp
-
-@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
-
-@[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
-  simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
-
-@[simp] theorem forIn_loop_toArray [Monad m] (l : List α) (f : α → β → m (ForInStep β)) (i : Nat)
-    (h : i ≤ l.length) (b : β) :
-    Array.forIn.loop l.toArray f i h b = (l.drop (l.length - i)).forIn b f := by
-  induction i generalizing l b with
-  | zero => simp [Array.forIn.loop]
-  | succ i ih =>
-    simp only [Array.forIn.loop, size_toArray, getElem_toArray, ih, forIn_eq_forIn]
-    rw [Nat.sub_add_eq, List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
-    simp only [Option.toList_some, singleton_append, forIn_cons]
-    have t : l.length - 1 - i = l.length - i - 1 := by omega
-    simp only [t]
-    congr
-
-@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn l.toArray b f = forIn l b f := by
-  change l.toArray.forIn b f = l.forIn b f
-  rw [Array.forIn, forIn_loop_toArray]
-  simp
-
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList]
@@ -178,9 +149,6 @@ namespace Array
 
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
--- This is a duplicate of `List.toArray_toList`.
--- It's confusing to guess which namespace this theorem should live in,
--- so we provide both.
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
 @[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
@@ -189,9 +157,6 @@ namespace Array
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
-@[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
-  rcases l with ⟨_ | _⟩ <;> simp
-
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
   simp [foldrM_eq_reverse_foldlM_toList, -size_push]
@@ -285,7 +250,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 @[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
+    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
 
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
@@ -308,10 +273,8 @@ theorem getD_get? (a : Array α) (i : Nat) (d : α) :
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
-@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
-    a.get! i = (a.get? i).getD default := by
-  by_cases p : i < a.size <;>
-  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
+@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
+  by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
 
 /-! # set -/
 
@@ -391,8 +354,8 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
     simp only [dif_pos hin]
     rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
     cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
-    | inl hj => simp [getElem_push, hj, hacc j hj]
-    | inr hj => simp [getElem_push, *]
+    | inl hj => simp [get_push, hj, hacc j hj]
+    | inr hj => simp [get_push, *]
   else
     simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
 termination_by n - i
@@ -460,7 +423,7 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
-@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
+theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
@@ -469,11 +432,9 @@ theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
 
-theorem getElem?_size_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
+theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
   simp [getElem?_neg, h]
 
-@[deprecated getElem?_size_le (since := "2024-10-21")] abbrev get?_len_le := @getElem?_size_le
-
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
   simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
@@ -481,39 +442,35 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
   simp [getElem?_eq_getElem?_toList]
 
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
-  simp only [get!_eq_getElem?, get?_eq_getElem?]
+  simp [get!_eq_getD]
 
 theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
   cases as
   simp [List.getElem?_eq_some_iff]
 
 @[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]
+  simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
   simp [back?, getElem?_eq_getElem?_toList]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
-theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
-  rw [getElem?_pos, getElem_push_lt]
+  rw [getElem?_pos, get_push_lt]
 
-@[deprecated getElem?_push_lt (since := "2024-10-21")] abbrev get?_push_lt := @getElem?_push_lt
+theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
+  rw [getElem?_pos, get_push_eq]
 
-theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
-  rw [getElem?_pos, getElem_push_eq]
-
-@[deprecated getElem?_push_eq (since := "2024-10-21")] abbrev get?_push_eq := @getElem?_push_eq
-
-theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
+theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
   match Nat.lt_trichotomy i a.size with
   | Or.inl g =>
     have h1 : i < a.size + 1 := by omega
     have h2 : i ≠ a.size := by omega
-    simp [getElem?_def, size_push, g, h1, h2, getElem_push_lt]
+    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
   | Or.inr (Or.inl heq) =>
-    simp [heq, getElem?_pos, getElem_push_eq]
+    simp [heq, getElem?_pos, get_push_eq]
   | Or.inr (Or.inr g) =>
     simp only [getElem?_def, size_push]
     have h1 : ¬ (i < a.size) := by omega
@@ -521,13 +478,9 @@ theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some
     have h3 : i ≠ a.size := by omega
     simp [h1, h2, h3]
 
-@[deprecated getElem?_push (since := "2024-10-21")] abbrev get?_push := @getElem?_push
-
-@[simp] theorem getElem?_size {a : Array α} : a[a.size]? = none := by
+@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
   simp only [getElem?_def, Nat.lt_irrefl, dite_false]
 
-@[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
-
 @[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
@@ -577,9 +530,6 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
 
-@[simp] theorem size_swapAt (a : Array α) (i : Fin a.size) (v : α) :
-    (a.swapAt i v).2.size = a.size := by simp [swapAt_def]
-
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
@@ -612,11 +562,11 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
   · intros i h h'
     if hlt : i < as.pop.size then
-      rw [getElem_push_lt (h:=hlt), getElem_pop]
+      rw [get_push_lt (h:=hlt), getElem_pop]
     else
       have heq : i = as.pop.size :=
         Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [getElem_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+      cases heq; rw [get_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
 
 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
     ∃ (bs : Array α) (c : α), as = bs.push c :=
@@ -694,40 +644,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
 
-/-! ### take -/
-
-@[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
-  induction n generalizing a with
-  | zero => simp [take.loop]
-  | succ n ih =>
-    simp [take.loop, ih]
-    omega
-
-@[simp] theorem getElem_take_loop (a : Array α) (n : Nat) (i : Nat) (h : i < (take.loop n a).size) :
-    (take.loop n a)[i] = a[i]'(by simp at h; omega) := by
-  induction n generalizing a i with
-  | zero => simp [take.loop]
-  | succ n ih =>
-    simp [take.loop, ih]
-
-@[simp] theorem size_take (a : Array α) (n : Nat) : (a.take n).size = min n a.size  := by
-  simp [take]
-  omega
-
-@[simp] theorem getElem_take (a : Array α) (n : Nat) (i : Nat) (h : i < (a.take n).size) :
-    (a.take n)[i] = a[i]'(by simp at h; omega) := by
-  simp [take]
-
-@[simp] theorem toList_take (a : Array α) (n : Nat) : (a.take n).toList = a.toList.take n := by
-  apply List.ext_getElem <;> simp
-
-/-! ### forIn -/
-
-@[simp] theorem forIn_toList [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn as.toList b f = forIn as b f := by
-  cases as
-  simp
-
 /-! ### foldl / foldr -/
 
 @[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -859,9 +775,9 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
     · intro j h
       simp at h ⊢
       by_cases h' : j < size b
-      · rw [getElem_push]
+      · rw [get_push]
         simp_all
-      · rw [getElem_push, dif_neg h']
+      · rw [get_push, dif_neg h']
         simp only [show j = i by omega]
         exact (hs _ m).1
 
@@ -886,7 +802,7 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
     (as.push x).map f = (as.map f).push (f x) := by
   ext
   · simp
-  · simp only [getElem_map, getElem_push, size_map]
+  · simp only [getElem_map, get_push, size_map]
     split <;> rfl
 
 @[simp] theorem map_pop {f : α → β} {as : Array α} :
@@ -895,6 +811,57 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
   · simp
   · simp only [getElem_map, getElem_pop, size_map]
 
+/-! ### mapIdx -/
+
+-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
+theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
+    (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 : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
+    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
+    induction i generalizing j bs with simp [mapIdxM.map]
+    | zero =>
+      have := (Nat.zero_add _).symm.trans h
+      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
+    | succ i ih =>
+      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
+      · intro i i_lt h'
+        rw [get_push]
+        split
+        · apply h₂
+        · simp only [size_push] at h'
+          obtain rfl : i = j := by omega
+          apply (hs ⟨i, by omega⟩ hm).1
+      · exact (hs ⟨j, by omega⟩ hm).2
+  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
+
+theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[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 (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
+  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapIdx _ _
+
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
+    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+    (a.mapIdx f)[i]? =
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
+  split <;> simp_all
+
 /-! ### modify -/
 
 @[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
@@ -908,12 +875,6 @@ theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
   · 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 : α → α) :
-    (as.modify x f).toList = as.toList.modify f x := by
-  apply List.ext_getElem
-  · simp
-  · simp [getElem_modify, List.getElem_modify]
-
 theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
     (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
   simp [getElem_modify h]
@@ -923,11 +884,6 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
     (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
-theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
-    (as.modify i f)[j]? = if i = j then as[j]?.map f else as[j]? := by
-  simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
-  split <;> split <;> rfl
-
 /-! ### filter -/
 
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -989,7 +945,7 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
+theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
 /-! ### append -/
 
@@ -1021,38 +977,18 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
-theorem getElem?_append_left {as bs : Array α} {n : Nat} (hn : n < as.size) :
-    (as ++ bs)[n]? = as[n]? := by
-  have hn' : n < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
-    size_append .. ▸ Nat.le_add_right ..
-  simp_all [getElem?_eq_getElem, getElem_append]
-
-theorem getElem?_append_right {as bs : Array α} {n : Nat} (h : as.size ≤ n) :
-    (as ++ bs)[n]? = bs[n - as.size]? := by
-  cases as
-  cases bs
-  simp at h
-  simp [List.getElem?_append_right, h]
-
-theorem getElem?_append {as bs : Array α} {n : Nat} :
-    (as ++ bs)[n]? = if n < as.size then as[n]? else bs[n - as.size]? := by
-  split <;> rename_i h
-  · 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
+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 α)} :
-    l.flatten.toList = (l.toList.map toList).flatten := by
+@[simp] theorem toList_flatten {l : Array (Array α)} : l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
   simp only [foldl_eq_foldl_toList]
   generalize l.toList = l
@@ -1167,7 +1103,7 @@ theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i
       have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
         rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
       have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, getElem_push_eq]
+        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
       rw [h]; congr; rw [Nat.add_sub_cancel]
     else
       have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
@@ -1194,14 +1130,6 @@ theorem getElem?_extract {as : Array α} {start stop : Nat} :
     · omega
   · rfl
 
-@[simp] theorem toList_extract (as : Array α) (start stop : Nat) :
-    (as.extract start stop).toList = (as.toList.drop start).take (stop - start) := by
-  apply List.ext_getElem
-  · simp only [length_toList, size_extract, List.length_take, List.length_drop]
-    omega
-  · intros n h₁ h₂
-    simp
-
 @[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
   apply ext
   · rw [size_extract, Nat.min_self, Nat.sub_zero]
@@ -1371,7 +1299,7 @@ open Fin
       · 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
+    (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
   split
   · simp_all only [getElem_swap_left]
   · split <;> simp_all
@@ -1381,7 +1309,7 @@ theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.sw
   apply getElem_swap'
 
 @[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
-    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸ i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸ j.2⟩ = a := by
+    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
   apply ext
   · simp only [size_swap]
   · intros
@@ -1422,10 +1350,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by
   simp only [← mapM'_eq_mapM, mapM_eq_foldlM]
@@ -1520,11 +1444,6 @@ theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p
   apply ext'
   simp
 
-@[simp] theorem modify_toArray (f : α → α) (l : List α) :
-    l.toArray.modify i f = (l.modify f i).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
     l.toArray.filter p 0 stop = (l.filter p).toArray := by
   subst h
@@ -1553,11 +1472,6 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[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
-
 end List
 
 /-! ### Deprecations -/

src/Init/Data/Array/MapIdx.lean

@@ -1,92 +0,0 @@
-/-
-Copyright (c) 2022 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Kim Morrison
--/
-prelude
-import Init.Data.Array.Lemmas
-import Init.Data.List.MapIdx
-
-namespace Array
-
-/-! ### mapFinIdx -/
-
--- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
-theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β)
-    (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 : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := by
-  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
-    let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs
-    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
-    induction i generalizing j bs with simp [mapFinIdxM.map]
-    | zero =>
-      have := (Nat.zero_add _).symm.trans h
-      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
-    | succ i ih =>
-      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
-      · intro i i_lt h'
-        rw [getElem_push]
-        split
-        · apply h₂
-        · simp only [size_push] at h'
-          obtain rfl : i = j := by omega
-          apply (hs ⟨i, by omega⟩ hm).1
-      · exact (hs ⟨j, by omega⟩ hm).2
-  simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0
-
-theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
-    ∃ eq : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) :=
-  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
-
-@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapFinIdx f).size = a.size :=
-  (mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
-
-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
-  Array.size_mapFinIdx _ _
-
-@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
-    (h : i < (mapFinIdx a f).size) :
-    (a.mapFinIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
-  (mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
-
-@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
-    (a.mapFinIdx f)[i]? =
-      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
-  simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
-  split <;> simp_all
-
-/-! ### mapIdx -/
-
-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 : (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 (as : Array α) (f : Nat → α → β)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[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 (a : Array α) (f : Nat → α → β) : (a.mapIdx f).size = a.size :=
-  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
-
-@[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 (a : Array α) (f : Nat → α → β) (i : Nat) :
-    (a.mapIdx f)[i]? =
-      a[i]?.map (f i) := by
-  simp [getElem?_def, size_mapIdx, getElem_mapIdx]
-
-end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -316,12 +316,6 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
   simp [Nat.sub_sub_eq_min, Nat.min_eq_right]
   omega
 
-@[simp] theorem sub_add_bmod_cancel {x y : BitVec w} :
-    ((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) =
-      ((x.toNat : Int) - y.toNat).bmod (2 ^ w) := by
-  rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.bmod_add_cancel, Int.add_comm,
-    Int.sub_eq_add_neg]
-
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
@@ -1980,10 +1974,6 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
 @[simp] theorem toNat_sub {n} (x y : BitVec n) :
     (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
 
-@[simp, bv_toNat] theorem toInt_sub {x y : BitVec w} :
-    (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w) := by
-  simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
-
 -- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
 -- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
 -- results in `omega` generating proof terms that are very slow in the kernel.
@@ -2006,8 +1996,6 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 
 @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
 
-@[simp] protected theorem zero_sub (x : BitVec n) : 0#n - x = -x := rfl
-
 @[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
   apply eq_of_toNat_eq
   simp only [toNat_sub]
@@ -2020,8 +2008,18 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 
 theorem toInt_neg {x : BitVec w} :
     (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
-  rw [← BitVec.zero_sub, toInt_sub]
-  simp [BitVec.toInt_ofNat]
+  simp only [toInt_eq_toNat_bmod, toNat_neg, Int.ofNat_emod, Int.emod_bmod_congr]
+  rw [← Int.subNatNat_of_le (by omega), Int.subNatNat_eq_coe, Int.sub_eq_add_neg, Int.add_comm,
+    Int.bmod_add_cancel]
+  by_cases h : x.toNat < ((2 ^ w) + 1) / 2
+  · rw [Int.bmod_pos (x := x.toNat)]
+    all_goals simp only [toNat_mod_cancel']
+    norm_cast
+  · rw [Int.bmod_neg (x := x.toNat)]
+    · simp only [toNat_mod_cancel']
+      rw_mod_cast [Int.neg_sub, Int.sub_eq_add_neg, Int.add_comm, Int.bmod_add_cancel]
+    · norm_cast
+      simp_all
 
 @[simp] theorem toFin_neg (x : BitVec n) :
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=

src/Init/Data/Hashable.lean

@@ -51,9 +51,6 @@ instance : Hashable USize where
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 
-instance : Hashable Char where
-  hash c := c.val.toUInt64
-
 instance : Hashable Int where
   hash
     | Int.ofNat n => UInt64.ofNat (2 * n)

src/Init/Data/Int/DivModLemmas.lean

@@ -1125,17 +1125,6 @@ theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmo
   simp [Int.emod_def, Int.sub_eq_add_neg]
   rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]
 
-@[simp]
-theorem emod_sub_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n - y) n = Int.bmod (x - y) n := by
-  simp only [emod_def, Int.sub_eq_add_neg]
-  rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]
-
-@[simp]
-theorem sub_emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x - y%n) n = Int.bmod (x - y) n := by
-  simp only [emod_def]
-  rw [Int.sub_eq_add_neg, Int.neg_sub, Int.sub_eq_add_neg, ← Int.add_assoc, Int.add_right_comm,
-    Int.bmod_add_mul_cancel, Int.sub_eq_add_neg]
-
 @[simp]
 theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n * y) n = Int.bmod (x * y) n := by
   simp [Int.emod_def, Int.sub_eq_add_neg]
@@ -1151,28 +1140,9 @@ theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n
     rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
     simp
 
-@[simp]
-theorem bmod_sub_bmod_congr : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n := by
-  rw [Int.bmod_def x n]
-  split
-  next p =>
-    simp only [emod_sub_bmod_congr]
-  next p =>
-    rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg, ← Int.sub_eq_add_neg]
-    simp [emod_sub_bmod_congr]
-
 @[simp] theorem add_bmod_bmod : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n := by
   rw [Int.add_comm x, Int.bmod_add_bmod_congr, Int.add_comm y]
 
-@[simp] theorem sub_bmod_bmod : Int.bmod (x - Int.bmod y n) n = Int.bmod (x - y) n := by
-  rw [Int.bmod_def y n]
-  split
-  next p =>
-    simp [sub_emod_bmod_congr]
-  next p =>
-    rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, ← Int.add_assoc, ← Int.sub_eq_add_neg]
-    simp [sub_emod_bmod_congr]
-
 @[simp]
 theorem bmod_mul_bmod : Int.bmod (Int.bmod x n * y) n = Int.bmod (x * y) n := by
   rw [bmod_def x n]

src/Init/Data/List/Basic.lean

@@ -29,7 +29,7 @@ The operations are organized as follow:
 * Lexicographic ordering: `lt`, `le`, and instances.
 * Head and tail operators: `head`, `head?`, `headD?`, `tail`, `tail?`, `tailD`.
 * Basic operations:
-  `map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `flatMap`, `replicate`, and
+  `map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `bind`, `replicate`, and
   `reverse`.
 * Additional functions defined in terms of these: `leftpad`, `rightPad`, and `reduceOption`.
 * Operations using indexes: `mapIdx`.
@@ -38,7 +38,7 @@ The operations are organized as follow:
 * Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
   `isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`,
   `rotateLeft` and `rotateRight`.
-* Manipulating elements: `replace`, `insert`, `modify`, `erase`, `eraseP`, `eraseIdx`.
+* Manipulating elements: `replace`, `insert`, `erase`, `eraseP`, `eraseIdx`.
 * Finding elements: `find?`, `findSome?`, `findIdx`, `indexOf`, `findIdx?`, `indexOf?`,
  `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
@@ -122,11 +122,6 @@ protected def beq [BEq α] : List α → List α → Bool
   | a::as, b::bs => a == b && List.beq as bs
   | _,     _     => false
 
-@[simp] theorem beq_nil_nil [BEq α] : List.beq ([] : List α) ([] : List α) = true := rfl
-@[simp] theorem beq_cons_nil [BEq α] (a : α) (as : List α) : List.beq (a::as) [] = false := rfl
-@[simp] theorem beq_nil_cons [BEq α] (a : α) (as : List α) : List.beq [] (a::as) = false := rfl
-theorem beq_cons₂ [BEq α] (a b : α) (as bs : List α) : List.beq (a::as) (b::bs) = (a == b && List.beq as bs) := rfl
-
 instance [BEq α] : BEq (List α) := ⟨List.beq⟩
 
 instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
@@ -1119,35 +1114,6 @@ theorem replace_cons [BEq α] {a : α} :
 @[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
   if l.elem a then l else a :: l
 
-/-! ### modify -/
-
-/--
-Apply a function to the nth tail of `l`. Returns the input without
-using `f` if the index is larger than the length of the List.
-```
-modifyTailIdx f 2 [a, b, c] = [a, b] ++ f [c]
-```
--/
-@[simp] def modifyTailIdx (f : List α → List α) : Nat → List α → List α
-  | 0, l => f l
-  | _+1, [] => []
-  | n+1, a :: l => a :: modifyTailIdx f n l
-
-/-- Apply `f` to the head of the list, if it exists. -/
-@[inline] def modifyHead (f : α → α) : List α → List α
-  | [] => []
-  | a :: l => f a :: l
-
-@[simp] theorem modifyHead_nil (f : α → α) : [].modifyHead f = [] := by rw [modifyHead]
-@[simp] theorem modifyHead_cons (a : α) (l : List α) (f : α → α) :
-    (a :: l).modifyHead f = f a :: l := by rw [modifyHead]
-
-/--
-Apply `f` to the nth element of the list, if it exists, replacing that element with the result.
--/
-def modify (f : α → α) : Nat → List α → List α :=
-  modifyTailIdx (modifyHead f)
-
 /-! ### erase -/
 
 /--
@@ -1452,15 +1418,11 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 
 /-- Sum of a list of natural numbers. -/
-@[deprecated List.sum (since := "2024-10-17")]
+-- We intend to subsequently deprecate this in favor of `List.sum`.
 protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
-set_option linter.deprecated false in
-@[simp, deprecated sum_nil (since := "2024-10-17")]
-theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
-set_option linter.deprecated false in
-@[simp, deprecated sum_cons (since := "2024-10-17")]
-theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
+@[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
+@[simp] theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
     Nat.sum (a::l) = a + Nat.sum l := rfl
 
 /-! ### range -/

src/Init/Data/List/BasicAux.lean

@@ -232,8 +232,7 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp_arith
 
-theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
-    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
   match as, bs with
   | [],    []    => rfl
   | [],    _::_ => False.elim <| h₂ (List.lt.nil ..)
@@ -249,8 +248,7 @@ theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
         have : a = b := s.antisymm hab hba
         simp [this, ih]
 
-instance [LT α] [Std.Antisymm (¬ · < · : α → α → Prop)] :
-    Std.Antisymm (· ≤ · : List α → List α → Prop) where
+instance [LT α] [Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm h₁ h₂ := le_antisymm h₁ h₂
 
 end List

src/Init/Data/List/Find.lean

@@ -595,14 +595,15 @@ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length
 
 theorem findIdx_append (p : α → Bool) (l₁ l₂ : List α) :
     (l₁ ++ l₂).findIdx p =
-      if l₁.findIdx p < l₁.length then l₁.findIdx p else l₂.findIdx p + l₁.length := by
+      if ∃ x, x ∈ l₁ ∧ p x = true then l₁.findIdx p else l₂.findIdx p + l₁.length := by
   induction l₁ with
   | nil => simp
   | cons x xs ih =>
     simp only [findIdx_cons, length_cons, cons_append]
     by_cases h : p x
     · simp [h]
-    · simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, add_one_lt_add_one_iff]
+    · simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, mem_cons, exists_eq_or_imp,
+        false_or]
       split <;> simp [Nat.add_assoc]
 
 theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :

src/Init/Data/List/Impl.lean

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

src/Init/Data/List/Lemmas.lean

@@ -1047,6 +1047,9 @@ theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
 
 @[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl
 
+theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
+  | _ :: _, rfl => rfl
+
 theorem getLast?_eq_getLast : ∀ l h, @getLast? α l = some (getLast l h)
   | [], h => nomatch h rfl
   | _ :: _, _ => rfl
@@ -1080,21 +1083,6 @@ theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
 theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
   rw [getLastD_eq_getLast?, getLast?_concat]; rfl
 
-/-! ### getLast! -/
-
-@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
-
-theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
-  | _ :: _, rfl => rfl
-
-theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
-  cases l with
-  | nil => simp
-  | cons _ _ =>
-    apply getLast!_of_getLast?
-    rw [getElem!_pos, getElem_cons_length (h := by simp)]
-    rfl
-
 /-! ## Head and tail -/
 
 /-! ### head -/

src/Init/Data/List/MinMax.lean

@@ -75,7 +75,7 @@ theorem le_min?_iff [Min α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
+theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
     (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
@@ -146,7 +146,7 @@ theorem max?_le_iff [Max α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
 -- and `le_min_iff`.
-theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
+theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
     (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :

src/Init/Data/List/Monadic.lean

@@ -99,14 +99,4 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
     funext b
     split <;> simp_all
 
-/-! ### foldlM and foldrM -/
-
-theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
-    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
-  induction l generalizing g init <;> simp [*]
-
-theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁)
-    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
-  induction l generalizing g init <;> simp [*]
-
 end List

src/Init/Data/List/Nat.lean

@@ -12,5 +12,3 @@ import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Count
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Find
-import Init.Data.List.Nat.BEq
-import Init.Data.List.Nat.Modify

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

@@ -1,47 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Init.Data.Nat.Lemmas
-import Init.Data.List.Basic
-
-namespace List
-
-/-! ### isEqv-/
-
-theorem isEqv_eq_decide (a b : List α) (r) :
-    isEqv a b r = if h : a.length = b.length then
-      decide (∀ (i : Nat) (h' : i < a.length), r (a[i]'(h ▸ h')) (b[i]'(h ▸ h'))) else false := by
-  induction a generalizing b with
-  | nil =>
-    cases b <;> simp
-  | cons a as ih =>
-    cases b with
-    | nil => simp
-    | cons b bs =>
-      simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
-      split <;> simp [Nat.forall_lt_succ_left']
-
-/-! ### beq -/
-
-theorem beq_eq_isEqv [BEq α] (a b : List α) : a.beq b = isEqv a b (· == ·) := by
-  induction a generalizing b with
-  | nil =>
-    cases b <;> simp
-  | cons a as ih =>
-    cases b with
-    | nil => simp
-    | cons b bs =>
-      simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
-        Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
-        Bool.decide_eq_true]
-      split <;> simp
-
-theorem beq_eq_decide [BEq α] (a b : List α) :
-    (a == b) = if h : a.length = b.length then
-      decide (∀ (i : Nat) (h' : i < a.length), a[i] == b[i]'(h ▸ h')) else false := by
-  simp [BEq.beq, beq_eq_isEqv, isEqv_eq_decide]
-
-end List

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

@@ -1,295 +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.TakeDrop
-import Init.Data.List.Nat.Erase
-
-namespace List
-
-/-! ### modifyHead -/
-
-@[simp] theorem length_modifyHead {f : α → α} {l : List α} : (l.modifyHead f).length = l.length := by
-  cases l <;> simp [modifyHead]
-
-theorem modifyHead_eq_set [Inhabited α] (f : α → α) (l : List α) :
-    l.modifyHead f = l.set 0 (f (l[0]?.getD default)) := by cases l <;> simp [modifyHead]
-
-@[simp] theorem modifyHead_eq_nil_iff {f : α → α} {l : List α} :
-    l.modifyHead f = [] ↔ l = [] := by cases l <;> simp [modifyHead]
-
-@[simp] theorem modifyHead_modifyHead {l : List α} {f g : α → α} :
-    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
-
-theorem getElem_modifyHead {l : List α} {f : α → α} {n} (h : n < (l.modifyHead f).length) :
-    (l.modifyHead f)[n] = if h' : n = 0 then f (l[0]'(by simp at h; omega)) else l[n]'(by simpa using h) := by
-  cases l with
-  | nil => simp at h
-  | cons hd tl => cases n <;> simp
-
-@[simp] theorem getElem_modifyHead_zero {l : List α} {f : α → α} {h} :
-    (l.modifyHead f)[0] = f (l[0]'(by simpa using h)) := by simp [getElem_modifyHead]
-
-@[simp] theorem getElem_modifyHead_succ {l : List α} {f : α → α} {n} (h : n + 1 < (l.modifyHead f).length) :
-    (l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h) := by simp [getElem_modifyHead]
-
-theorem getElem?_modifyHead {l : List α} {f : α → α} {n} :
-    (l.modifyHead f)[n]? = if n = 0 then l[n]?.map f else l[n]? := by
-  cases l with
-  | nil => simp
-  | cons hd tl => cases n <;> simp
-
-@[simp] theorem getElem?_modifyHead_zero {l : List α} {f : α → α} :
-    (l.modifyHead f)[0]? = l[0]?.map f := by simp [getElem?_modifyHead]
-
-@[simp] theorem getElem?_modifyHead_succ {l : List α} {f : α → α} {n} :
-    (l.modifyHead f)[n + 1]? = l[n + 1]? := by simp [getElem?_modifyHead]
-
-@[simp] theorem head_modifyHead (f : α → α) (l : List α) (h) :
-    (l.modifyHead f).head h = f (l.head (by simpa using h)) := by
-  cases l with
-  | nil => simp at h
-  | cons hd tl => simp
-
-@[simp] theorem head?_modifyHead {l : List α} {f : α → α} :
-    (l.modifyHead f).head? = l.head?.map f := by cases l <;> simp
-
-@[simp] theorem tail_modifyHead {f : α → α} {l : List α} :
-    (l.modifyHead f).tail = l.tail := by cases l <;> simp
-
-@[simp] theorem take_modifyHead {f : α → α} {l : List α} {n} :
-    (l.modifyHead f).take n = (l.take n).modifyHead f := by
-  cases l <;> cases n <;> simp
-
-@[simp] theorem drop_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
-    (l.modifyHead f).drop n = l.drop n := by
-  cases l <;> cases n <;> simp_all
-
-@[simp] theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
-    (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by cases l <;> simp
-
-@[simp] theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
-    (l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f := by cases l <;> cases n <;> simp_all
-
-@[simp] theorem modifyHead_id : modifyHead (id : α → α) = id := by funext l; cases l <;> simp
-
-/-! ### modifyTailIdx -/
-
-@[simp] theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l
-  | 0, _ => rfl
-  | _+1, [] => rfl
-  | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
-
-theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
-  | 0, l => by cases l <;> rfl
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
-
-@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, length (f l) = length l) :
-    ∀ n l, length (modifyTailIdx f n l) = length l
-  | 0, _ => H _
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
-
-theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
-    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
-  induction l₁ <;> simp [*, Nat.succ_add]
-
-theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
-    ∀ n l, modifyTailIdx f n l = take n l ++ f (drop n l)
-  | 0, _ => rfl
-  | _ + 1, [] => H.symm
-  | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
-
-theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h : n ≤ l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ modifyTailIdx f n l = l₁ ++ f l₂ :=
-  have ⟨_, _, eq, hl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n :=
-    ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
-  ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
-
-/-! ### modify -/
-
-@[simp] theorem modify_nil (f : α → α) (n) : [].modify f n = [] := by cases n <;> rfl
-
-@[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
-    (a :: l).modify f 0 = f a :: l := rfl
-
-@[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (n) :
-    (a :: l).modify f (n + 1) = a :: l.modify f n := by rfl
-
-theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
-    l.modifyHead f = l.modify f 0 := by cases l <;> simp
-
-@[simp] theorem modify_eq_nil_iff (f : α → α) (n) (l : List α) :
-    l.modify f n = [] ↔ l = [] := by cases l <;> cases n <;> simp
-
-theorem getElem?_modify (f : α → α) :
-    ∀ n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
-  | n, l, 0 => by cases l <;> cases n <;> simp
-  | n, [], _+1 => by cases n <;> rfl
-  | 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
-  | n+1, a :: l, m+1 => by
-    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
-    refine (getElem?_modify f n l m).trans ?_
-    cases h' : l[m]? <;> by_cases h : n = m <;>
-      simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
-
-@[simp] theorem length_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
-  length_modifyTailIdx _ fun l => by cases l <;> rfl
-
-@[simp] theorem getElem?_modify_eq (f : α → α) (n) (l : List α) :
-    (modify f n l)[n]? = f <$> l[n]? := by
-  simp only [getElem?_modify, if_pos]
-
-@[simp] theorem getElem?_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
-    (modify f m l)[n]? = l[n]? := by
-  simp only [getElem?_modify, if_neg h, id_map']
-
-theorem getElem_modify (f : α → α) (n) (l : List α) (m) (h : m < (modify f n l).length) :
-    (modify f n l)[m] =
-      if n = m then f (l[m]'(by simp at h; omega)) else l[m]'(by simp at h; omega) := by
-  rw [getElem_eq_iff, getElem?_modify]
-  simp at h
-  simp [h]
-
-@[simp] theorem getElem_modify_eq (f : α → α) (n) (l : List α) (h) :
-    (modify f n l)[n] = f (l[n]'(by simpa using h)) := by simp [getElem_modify]
-
-@[simp] theorem getElem_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) (h') :
-    (modify f m l)[n] = l[n]'(by simpa using h') := by simp [getElem_modify, h]
-
-theorem modify_eq_self {f : α → α} {n} {l : List α} (h : l.length ≤ n) :
-    l.modify f n = l := by
-  apply ext_getElem
-  · simp
-  · intro m h₁ h₂
-    simp only [getElem_modify, ite_eq_right_iff]
-    intro h
-    omega
-
-theorem modify_modify_eq (f g : α → α) (n) (l : List α) :
-    (modify f n l).modify g n = modify (g ∘ f) n l := by
-  apply ext_getElem
-  · simp
-  · intro m h₁ h₂
-    simp only [getElem_modify, Function.comp_apply]
-    split <;> simp
-
-theorem modify_modify_ne (f g : α → α) {m n} (l : List α) (h : m ≠ n) :
-    (modify f m l).modify g n = (l.modify g n).modify f m := by
-  apply ext_getElem
-  · simp
-  · intro m' h₁ h₂
-    simp only [getElem_modify, getElem_modify_ne, h₂]
-    split <;> split <;> first | rfl | omega
-
-theorem modify_eq_set [Inhabited α] (f : α → α) (n) (l : List α) :
-    modify f n l = l.set n (f (l[n]?.getD default)) := by
-  apply ext_getElem
-  · simp
-  · intro m h₁ h₂
-    simp [getElem_modify, getElem_set, h₂]
-    split <;> rename_i h
-    · subst h
-      simp only [length_modify] at h₁
-      simp [h₁]
-    · rfl
-
-theorem modify_eq_take_drop (f : α → α) :
-    ∀ n l, modify f n l = take n l ++ modifyHead f (drop n l) :=
-  modifyTailIdx_eq_take_drop _ rfl
-
-theorem modify_eq_take_cons_drop {f : α → α} {n} {l : List α} (h : n < l.length) :
-    modify f n l = take n l ++ f l[n] :: drop (n + 1) l := by
-  rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
-
-theorem exists_of_modify (f : α → α) {n} {l : List α} (h : n < l.length) :
-    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ modify f n l = l₁ ++ f a :: l₂ :=
-  match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
-  | ⟨_, _::_, eq, hl, H⟩ => ⟨_, _, _, eq, hl, H⟩
-  | ⟨_, [], eq, hl, _⟩ => nomatch Nat.ne_of_gt h (eq ▸ append_nil _ ▸ hl)
-
-@[simp] theorem modify_id (n) (l : List α) : l.modify id n = l := by
-  simp [modify]
-
-theorem take_modify (f : α → α) (n m) (l : List α) :
-    (modify f m l).take n = (take n l).modify f m := by
-  induction n generalizing l m with
-  | zero => simp
-  | succ n ih =>
-    cases l with
-    | nil => simp
-    | cons hd tl =>
-      cases m with
-      | zero => simp
-      | succ m => simp [ih]
-
-theorem drop_modify_of_lt (f : α → α) (n m) (l : List α) (h : n < m) :
-    (modify f n l).drop m = l.drop m := by
-  apply ext_getElem
-  · simp
-  · intro m' h₁ h₂
-    simp only [getElem_drop, getElem_modify, ite_eq_right_iff]
-    intro h'
-    omega
-
-theorem drop_modify_of_ge (f : α → α) (n m) (l : List α) (h : n ≥ m) :
-    (modify f n l).drop m = modify f (n - m) (drop m l) := by
-  apply ext_getElem
-  · simp
-  · intro m' h₁ h₂
-    simp [getElem_drop, getElem_modify, ite_eq_right_iff]
-    split <;> split <;> first | rfl | omega
-
-theorem eraseIdx_modify_of_eq (f : α → α) (n) (l : List α) :
-    (modify f n l).eraseIdx n = l.eraseIdx n := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro m h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    split <;> split <;> first | rfl | omega
-
-theorem eraseIdx_modify_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
-    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f (i - 1) := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : i - 1 = k
-    repeat' split
-    all_goals (first | rfl | omega)
-
-theorem eraseIdx_modify_of_gt (f : α → α) (i j) (l : List α) (h : j > i) :
-    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f i := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : i = k
-    repeat' split
-    all_goals (first | rfl | omega)
-
-theorem modify_eraseIdx_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
-    (l.eraseIdx i).modify f j = (l.modify f j).eraseIdx i := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : j = k + 1
-    repeat' split
-    all_goals (first | rfl | omega)
-
-theorem modify_eraseIdx_of_ge (f : α → α) (i j) (l : List α) (h : j ≥ i) :
-    (l.eraseIdx i).modify f j = (l.modify f (j + 1)).eraseIdx i := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : j + 1 = k + 1
-    repeat' split
-    all_goals (first | rfl | omega)
-
-end List

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

@@ -187,9 +187,6 @@ theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.dro
   · apply length_take_le
   · apply Nat.le_add_right
 
-theorem take_one {l : List α} : l.take 1 = l.head?.toList := by
-  induction l <;> simp
-
 theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
     (l.take n).dropLast = l.take (n - 1) := by
   simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
@@ -285,14 +282,14 @@ theorem mem_drop_iff_getElem {l : List α} {a : α} :
   · rintro ⟨i, hm, rfl⟩
     refine ⟨i, by simp; omega, by rw [getElem_drop]⟩
 
-@[simp] theorem head?_drop (l : List α) (n : Nat) :
+theorem head?_drop (l : List α) (n : Nat) :
     (l.drop n).head? = l[n]? := by
   rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
 
-@[simp] theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
+theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
     (l.drop n).head h = l[n]'(by simp_all) := by
   have w : n < l.length := length_lt_of_drop_ne_nil h
-  simp [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some]
+  simpa [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some] using head?_drop l n
 
 theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n then none else l.getLast? := by
   rw [getLast?_eq_getElem?, getElem?_drop]
@@ -303,7 +300,7 @@ theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n th
     congr
     omega
 
-@[simp] theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
+theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
     (l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
   simp only [ne_eq, drop_eq_nil_iff] at h
   apply Option.some_inj.1
@@ -452,26 +449,6 @@ theorem reverse_drop {l : List α} {n : Nat} :
     rw [w, take_zero, drop_of_length_le, reverse_nil]
     omega
 
-theorem take_add_one {l : List α} {n : Nat} :
-    l.take (n + 1) = l.take n ++ l[n]?.toList := by
-  simp [take_add, take_one]
-
-theorem drop_eq_getElem?_toList_append {l : List α} {n : Nat} :
-    l.drop n = l[n]?.toList ++ l.drop (n + 1) := by
-  induction l generalizing n with
-  | nil => simp
-  | cons hd tl ih =>
-    cases n
-    · simp
-    · simp only [drop_succ_cons, getElem?_cons_succ]
-      rw [ih]
-
-theorem drop_sub_one {l : List α} {n : Nat} (h : 0 < n) :
-    l.drop (n - 1) = l[n - 1]?.toList ++ l.drop n := by
-  rw [drop_eq_getElem?_toList_append]
-  congr
-  omega
-
 /-! ### findIdx -/
 
 theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs.take (xs.findIdx p)) :

src/Init/Data/Nat/Basic.lean

@@ -490,10 +490,10 @@ protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
             (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge)
 protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
 
-instance : Std.Antisymm ( . ≤ . : Nat → Nat → Prop) where
+instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
 
-instance : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
+instance : Antisymm (¬ . < . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=

src/Init/Data/Nat/Lemmas.lean

@@ -32,77 +32,6 @@ namespace Nat
 @[simp] theorem exists_add_one_eq : (∃ n, n + 1 = a) ↔ 0 < a :=
   ⟨fun ⟨n, h⟩ => by omega, fun h => ⟨a - 1, by omega⟩⟩
 
-/-- Dependent variant of `forall_lt_succ_right`. -/
-theorem forall_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∀ m (h : m < n + 1), p m h) ↔ (∀ m (h : m < n), p m (by omega)) ∧ p n (by omega) := by
-  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
-  constructor
-  · intro w
-    constructor
-    · intro m h
-      exact w _ (.inl h)
-    · exact w _ (.inr rfl)
-  · rintro w m (h|rfl)
-    · exact w.1 _ h
-    · exact w.2
-
-/-- See `forall_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
-theorem forall_lt_succ_right {p : Nat → Prop} :
-    (∀ m, m < n + 1 → p m) ↔ (∀ m, m < n → p m) ∧ p n := by
-  simpa using forall_lt_succ_right' (p := fun m _ => p m)
-
-/-- Dependent variant of `forall_lt_succ_left`. -/
-theorem forall_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∀ m (h : m < n + 1), p m h) ↔ p 0 (by omega) ∧ (∀ m (h : m < n), p (m + 1) (by omega)) := by
-  constructor
-  · intro w
-    constructor
-    · exact w 0 (by omega)
-    · intro m h
-      exact w (m + 1) (by omega)
-  · rintro ⟨h₀, h₁⟩ m h
-    cases m with
-    | zero => exact h₀
-    | succ m => exact h₁ m (by omega)
-
-/-- See `forall_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
-theorem forall_lt_succ_left {p : Nat → Prop} :
-    (∀ m, m < n + 1 → p m) ↔ p 0 ∧ (∀ m, m < n → p (m + 1)) := by
-  simpa using forall_lt_succ_left' (p := fun m _ => p m)
-
-/-- Dependent variant of `exists_lt_succ_right`. -/
-theorem exists_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m (by omega)) ∨ p n (by omega) := by
-  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
-  constructor
-  · rintro ⟨m, (h|rfl), w⟩
-    · exact .inl ⟨m, h, w⟩
-    · exact .inr w
-  · rintro (⟨m, h, w⟩ | w)
-    · exact ⟨m, by omega, w⟩
-    · exact ⟨n, by omega, w⟩
-
-/-- See `exists_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
-theorem exists_lt_succ_right {p : Nat → Prop} :
-    (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n := by
-  simpa using exists_lt_succ_right' (p := fun m _ => p m)
-
-/-- Dependent variant of `exists_lt_succ_left`. -/
-theorem exists_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
-    (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 (by omega) ∨ (∃ m, ∃ (h : m < n), p (m + 1) (by omega)) := by
-  constructor
-  · rintro ⟨_|m, h, w⟩
-    · exact .inl w
-    · exact .inr ⟨m, by omega, w⟩
-  · rintro (w|⟨m, h, w⟩)
-    · exact ⟨0, by omega, w⟩
-    · exact ⟨m + 1, by omega, w⟩
-
-/-- See `exists_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
-theorem exists_lt_succ_left {p : Nat → Prop} :
-    (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1)) := by
-  simpa using exists_lt_succ_left' (p := fun m _ => p m)
-
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by

src/Init/Data/OfScientific.lean

@@ -10,10 +10,8 @@ import Init.Data.Nat.Log2
 
 /-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
    Examples:
-   - `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
-   - `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`
-
-   Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
+   - `OfScientific.ofScientific 123 true 2`    represents `1.23`
+   - `OfScientific.ofScientific 121 false 100` represents `121e100`
 -/
 class OfScientific (α : Type u) where
   ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α

src/Init/Data/Option/Attach.lean

@@ -44,7 +44,7 @@ theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
   simp
 
 theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
-    o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w ▸ h) := by
+    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
   subst w
   simp
 
@@ -128,12 +128,12 @@ theorem attach_map {o : Option α} (f : α → β) :
   cases o <;> simp
 
 theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
-    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
+    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
 theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
-    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun _ h => h) := by
+    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
   cases o <;> simp
 
 theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}

src/Init/Data/Option/Basic.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
+import Init.Core
 import Init.Control.Basic
+import Init.Coe
 
 namespace Option
 

src/Init/Data/Repr.lean

@@ -5,6 +5,10 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Format.Basic
+import Init.Data.Int.Basic
+import Init.Data.Nat.Div
+import Init.Data.UInt.BasicAux
+import Init.Control.Id
 open Sum Subtype Nat
 
 open Std

src/Init/Data/String/Basic.lean

@@ -6,6 +6,7 @@ Author: Leonardo de Moura, Mario Carneiro
 prelude
 import Init.Data.List.Basic
 import Init.Data.Char.Basic
+import Init.Data.Option.Basic
 
 universe u
 
@@ -1147,23 +1148,23 @@ namespace String
 /--
 If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
 -/
-def dropPrefix? (s : String) (pre : String) : Option Substring :=
-  s.toSubstring.dropPrefix? pre.toSubstring
+def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
+  s.toSubstring.dropPrefix? pre
 
 /--
 If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
 -/
-def dropSuffix? (s : String) (suff : String) : Option Substring :=
-  s.toSubstring.dropSuffix? suff.toSubstring
+def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
+  s.toSubstring.dropSuffix? suff
 
 /-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
 or otherwise return `s`. -/
-def stripPrefix (s : String) (pre : String) : String :=
+def stripPrefix (s : String) (pre : Substring) : String :=
   s.dropPrefix? pre |>.map Substring.toString |>.getD s
 
 /-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
 or otherwise return `s`. -/
-def stripSuffix (s : String) (suff : String) : String :=
+def stripSuffix (s : String) (suff : Substring) : String :=
   s.dropSuffix? suff |>.map Substring.toString |>.getD s
 
 end String

src/Init/Data/Sum.lean

@@ -4,5 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury G. Kudryashov
 -/
 prelude
-import Init.Data.Sum.Basic
-import Init.Data.Sum.Lemmas
+import Init.Core
+
+namespace Sum
+
+deriving instance DecidableEq for Sum
+deriving instance BEq for Sum
+
+/-- Check if a sum is `inl` and if so, retrieve its contents. -/
+def getLeft? : α ⊕ β → Option α
+  | inl a => some a
+  | inr _ => none
+
+/-- Check if a sum is `inr` and if so, retrieve its contents. -/
+def getRight? : α ⊕ β → Option β
+  | inr b => some b
+  | inl _ => none
+
+end Sum

src/Init/Data/Sum/Basic.lean

@@ -1,178 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Yury G. Kudryashov
--/
-prelude
-import Init.PropLemmas
-
-/-!
-# Disjoint union of types
-
-This file defines basic operations on the the sum type `α ⊕ β`.
-
-`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
-
-## Main declarations
-
-* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
-* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
-* `Sum.getLeft`: Retrieves the left content of a `x : α ⊕ β` that is known to come from the left.
-* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` that is known to come from the right.
-* `Sum.getLeft?`: Retrieves the left content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the right.
-* `Sum.getRight?`: Retrieves the right content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the left.
-* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
-* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
-* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
-* `Sum.LiftRel`: The disjoint union of two relations.
-* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
-
-## Further material
-
-See `Batteries.Data.Sum.Lemmas` for theorems about these definitions.
-
-## Notes
-
-The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
-To this effect, we have `PSum`, which takes value in `Sort _` and carries a more complicated
-universe signature in consequence. The `Prop` version is `Or`.
--/
-
-namespace Sum
-
-deriving instance DecidableEq for Sum
-deriving instance BEq for Sum
-
-section get
-
-/-- Check if a sum is `inl`. -/
-def isLeft : α ⊕ β → Bool
-  | inl _ => true
-  | inr _ => false
-
-/-- Check if a sum is `inr`. -/
-def isRight : α ⊕ β → Bool
-  | inl _ => false
-  | inr _ => true
-
-/-- Retrieve the contents from a sum known to be `inl`.-/
-def getLeft : (ab : α ⊕ β) → ab.isLeft → α
-  | inl a, _ => a
-
-/-- Retrieve the contents from a sum known to be `inr`.-/
-def getRight : (ab : α ⊕ β) → ab.isRight → β
-  | inr b, _ => b
-
-/-- Check if a sum is `inl` and if so, retrieve its contents. -/
-def getLeft? : α ⊕ β → Option α
-  | inl a => some a
-  | inr _ => none
-
-/-- Check if a sum is `inr` and if so, retrieve its contents. -/
-def getRight? : α ⊕ β → Option β
-  | inr b => some b
-  | inl _ => none
-
-@[simp] theorem isLeft_inl : (inl x : α ⊕ β).isLeft = true := rfl
-@[simp] theorem isLeft_inr : (inr x : α ⊕ β).isLeft = false := rfl
-@[simp] theorem isRight_inl : (inl x : α ⊕ β).isRight = false := rfl
-@[simp] theorem isRight_inr : (inr x : α ⊕ β).isRight = true := rfl
-
-@[simp] theorem getLeft_inl (h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x := rfl
-@[simp] theorem getRight_inr (h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x := rfl
-
-@[simp] theorem getLeft?_inl : (inl x : α ⊕ β).getLeft? = some x := rfl
-@[simp] theorem getLeft?_inr : (inr x : α ⊕ β).getLeft? = none := rfl
-@[simp] theorem getRight?_inl : (inl x : α ⊕ β).getRight? = none := rfl
-@[simp] theorem getRight?_inr : (inr x : α ⊕ β).getRight? = some x := rfl
-
-end get
-
-/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
-protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
-  fun x => Sum.casesOn x f g
-
-@[simp] theorem elim_inl (f : α → γ) (g : β → γ) (x : α) :
-    Sum.elim f g (inl x) = f x := rfl
-
-@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
-    Sum.elim f g (inr x) = g x := rfl
-
-/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
-protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
-  Sum.elim (inl ∘ f) (inr ∘ g)
-
-@[simp] theorem map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl
-
-@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
-
-/-- Swap the factors of a sum type -/
-def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl
-
-@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl
-
-@[simp] theorem swap_inr : swap (inr x : α ⊕ β) = inl x := rfl
-
-section LiftRel
-
-/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
-`α ⊕ β` and `γ ⊕ δ`. -/
-inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
-  /-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
-  | protected inl {a c} : r a c → LiftRel r s (inl a) (inl c)
-  /-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
-  | protected inr {b d} : s b d → LiftRel r s (inr b) (inr d)
-
-@[simp] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
-  ⟨fun h => by cases h; assumption, LiftRel.inl⟩
-
-@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
-
-@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
-
-@[simp] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
-  ⟨fun h => by cases h; assumption, LiftRel.inr⟩
-
-instance {r : α → γ → Prop} {s : β → δ → Prop}
-    [∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
-    ∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)
-  | inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
-  | inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
-  | inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr
-
-end LiftRel
-
-section Lex
-
-/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
-respective order on `α` or `β`. -/
-inductive Lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
-  /-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
-  | protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
-  /-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
-  | protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
-  /-- `inl a` and `inr b` are always related via `Lex r s`. -/
-  | sep (a b) : Lex r s (inl a) (inr b)
-
-attribute [simp] Lex.sep
-
-@[simp] theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inl⟩
-
-@[simp] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inr⟩
-
-@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
-
-instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
-  | inl _, inl _ => decidable_of_iff' _ lex_inl_inl
-  | inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
-  | inr _, inl _ => Decidable.isFalse lex_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ lex_inr_inr
-
-end Lex
-
-end Sum

src/Init/Data/Sum/Lemmas.lean

@@ -1,251 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Yury G. Kudryashov
--/
-prelude
-import Init.Data.Sum.Basic
-import Init.Ext
-
-/-!
-# Disjoint union of types
-
-Theorems about the definitions introduced in `Init.Data.Sum.Basic`.
--/
-
-open Function
-
-namespace Sum
-
-@[simp] protected theorem «forall» {p : α ⊕ β → Prop} :
-    (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
-  ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
-
-@[simp] protected theorem «exists» {p : α ⊕ β → Prop} :
-    (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
-  ⟨ fun
-    | ⟨inl a, h⟩ => Or.inl ⟨a, h⟩
-    | ⟨inr b, h⟩ => Or.inr ⟨b, h⟩,
-    fun
-    | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩
-    | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
-
-theorem forall_sum {γ : α ⊕ β → Sort _} (p : (∀ ab, γ ab) → Prop) :
-    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by
-  refine ⟨fun h fa fb => h _, fun h fab => ?_⟩
-  have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
-    apply funext
-    rintro (_ | _) <;> rfl
-  rw [h1]; exact h _ _
-
-section get
-
-@[simp] theorem inl_getLeft : ∀ (x : α ⊕ β) (h : x.isLeft), inl (x.getLeft h) = x
-  | inl _, _ => rfl
-@[simp] theorem inr_getRight : ∀ (x : α ⊕ β) (h : x.isRight), inr (x.getRight h) = x
-  | inr _, _ => rfl
-
-@[simp] theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight := by
-  cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft := by
-  cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
-
-theorem eq_left_getLeft_of_isLeft : ∀ {x : α ⊕ β} (h : x.isLeft), x = inl (x.getLeft h)
-  | inl _, _ => rfl
-
-@[simp] theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a ↔ x = inl a := by
-  cases x <;> simp at h ⊢
-
-theorem eq_right_getRight_of_isRight : ∀ {x : α ⊕ β} (h : x.isRight), x = inr (x.getRight h)
-  | inr _, _ => rfl
-
-@[simp] theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b ↔ x = inr b := by
-  cases x <;> simp at h ⊢
-
-@[simp] theorem getLeft?_eq_some_iff : x.getLeft? = some a ↔ x = inl a := by
-  cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_some_iff : x.getRight? = some b ↔ x = inr b := by
-  cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]
-
-@[simp] theorem bnot_isLeft (x : α ⊕ β) : !x.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isLeft_eq_false {x : α ⊕ β} : x.isLeft = false ↔ x.isRight := by cases x <;> simp
-
-theorem not_isLeft {x : α ⊕ β} : ¬x.isLeft ↔ x.isRight := by simp
-
-@[simp] theorem bnot_isRight (x : α ⊕ β) : !x.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem isRight_eq_false {x : α ⊕ β} : x.isRight = false ↔ x.isLeft := by cases x <;> simp
-
-theorem not_isRight {x : α ⊕ β} : ¬x.isRight ↔ x.isLeft := by simp
-
-theorem isLeft_iff : x.isLeft ↔ ∃ y, x = Sum.inl y := by cases x <;> simp
-
-theorem isRight_iff : x.isRight ↔ ∃ y, x = Sum.inr y := by cases x <;> simp
-
-end get
-
-theorem inl.inj_iff : (inl a : α ⊕ β) = inl b ↔ a = b := ⟨inl.inj, congrArg _⟩
-
-theorem inr.inj_iff : (inr a : α ⊕ β) = inr b ↔ a = b := ⟨inr.inj, congrArg _⟩
-
-theorem inl_ne_inr : inl a ≠ inr b := nofun
-
-theorem inr_ne_inl : inr b ≠ inl a := nofun
-
-/-! ### `Sum.elim` -/
-
-@[simp] theorem elim_comp_inl (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inl = f :=
-  rfl
-
-@[simp] theorem elim_comp_inr (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inr = g :=
-  rfl
-
-@[simp] theorem elim_inl_inr : @Sum.elim α β _ inl inr = id :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
-    f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h) :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-@[simp] theorem elim_comp_inl_inr (f : α ⊕ β → γ) :
-    Sum.elim (f ∘ inl) (f ∘ inr) = f :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
-    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
-  simp [funext_iff]
-
-/-! ### `Sum.map` -/
-
-@[simp] theorem map_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    ∀ x : Sum α β, (x.map f g).map f' g' = x.map (f' ∘ f) (g' ∘ g)
-  | inl _ => rfl
-  | inr _ => rfl
-
-@[simp] theorem map_comp_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g) :=
-  funext <| map_map f' g' f g
-
-@[simp] theorem map_id_id : Sum.map (@id α) (@id β) = id :=
-  funext fun x => Sum.recOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} :
-    Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x := by
-  cases x <;> rfl
-
-theorem elim_comp_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} :
-    Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) :=
-  funext fun _ => elim_map
-
-@[simp] theorem isLeft_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isLeft (x.map f g) = isLeft x := by
-  cases x <;> rfl
-
-@[simp] theorem isRight_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isRight (x.map f g) = isRight x := by
-  cases x <;> rfl
-
-@[simp] theorem getLeft?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getLeft? = x.getLeft?.map f := by
-  cases x <;> rfl
-
-@[simp] theorem getRight?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
-
-/-! ### `Sum.swap` -/
-
-@[simp] theorem swap_swap (x : α ⊕ β) : swap (swap x) = x := by cases x <;> rfl
-
-@[simp] theorem swap_swap_eq : swap ∘ swap = @id (α ⊕ β) := funext <| swap_swap
-
-@[simp] theorem isLeft_swap (x : α ⊕ β) : x.swap.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isRight_swap (x : α ⊕ β) : x.swap.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem getLeft?_swap (x : α ⊕ β) : x.swap.getLeft? = x.getRight? := by cases x <;> rfl
-
-@[simp] theorem getRight?_swap (x : α ⊕ β) : x.swap.getRight? = x.getLeft? := by cases x <;> rfl
-
-section LiftRel
-
-theorem LiftRel.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b)
-  (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y := by
-  cases h
-  · exact LiftRel.inl (hr _ _ ‹_›)
-  · exact LiftRel.inr (hs _ _ ‹_›)
-
-theorem LiftRel.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) :
-    LiftRel r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem LiftRel.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) :
-    LiftRel r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-protected theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap := by
-  cases h
-  · exact LiftRel.inr ‹_›
-  · exact LiftRel.inl ‹_›
-
-@[simp] theorem liftRel_swap_iff : LiftRel s r x.swap y.swap ↔ LiftRel r s x y :=
-  ⟨fun h => by rw [← swap_swap x, ← swap_swap y]; exact h.swap, LiftRel.swap⟩
-
-end LiftRel
-
-section Lex
-
-protected theorem LiftRel.lex {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b := by
-  cases h
-  · exact Lex.inl ‹_›
-  · exact Lex.inr ‹_›
-
-theorem liftRel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex
-
-theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) :
-    Lex r₂ s₂ x y := by
-  cases h
-  · exact Lex.inl (hr _ _ ‹_›)
-  · exact Lex.inr (hs _ _ ‹_›)
-  · exact Lex.sep _ _
-
-theorem Lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem Lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a) := by
-  induction aca with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inl h' => exact IH _ h'
-
-theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
-    Acc (Lex r s) (inr b) := by
-  induction acb with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inr h' => exact IH _ h'
-    | sep => exact aca _
-
-theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=
-  have aca : ∀ a, Acc (Lex r s) (inl a) := fun a => lex_acc_inl (ha.apply a)
-  ⟨fun x => Sum.recOn x aca fun b => lex_acc_inr aca (hb.apply b)⟩
-
-end Lex
-
-theorem elim_const_const (c : γ) :
-    Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c := by
-  apply funext
-  rintro (_ | _) <;> rfl
-
-@[simp] theorem elim_lam_const_lam_const (c : γ) :
-    Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c :=
-  Sum.elim_const_const c

src/Init/Data/ToString/Basic.lean

@@ -4,9 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
+import Init.Data.String.Basic
+import Init.Data.UInt.BasicAux
+import Init.Data.Nat.Div
 import Init.Data.Repr
-import Init.Data.Option.Basic
-
+import Init.Data.Int.Basic
+import Init.Data.Format.Basic
+import Init.Control.Id
+import Init.Control.Option
 open Sum Subtype Nat
 
 open Std

src/Init/GetElem.lean

@@ -144,26 +144,22 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v
     LawfulGetElem coll idx elem valid where
 
 theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
-  have : Decidable (dom c i) := .isTrue h
+    (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
   rw [getElem?_def]
   exact dif_pos h
 
 theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
-  have : Decidable (dom c i) := .isFalse h
+    (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
   rw [getElem?_def]
   exact dif_neg h
 
 theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
+    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
-  have : Decidable (dom c i) := .isTrue h
   simp [getElem!_def, getElem?_def, h]
 
 theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
-  have : Decidable (dom c i) := .isFalse h
+    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
   simp [getElem!_def, getElem?_def, h]
 
 namespace Fin

src/Init/MetaTypes.lean

@@ -224,7 +224,11 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  This option does not have any effect (yet).
+  When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated
+  with an `rfl`-theorem.
+  Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
+  If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
+  will **not** create a proof term which is an application of the annotated theorem.
   -/
   implicitDefEqProofs : Bool := true
   deriving Inhabited, BEq

src/Init/NotationExtra.lean

@@ -10,7 +10,6 @@ import Init.Data.ToString.Basic
 import Init.Data.Array.Subarray
 import Init.Conv
 import Init.Meta
-import Init.While
 
 namespace Lean
 
@@ -169,9 +168,9 @@ end Lean
   | _                => throw ()
 
 @[app_unexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
-  | `($(_) $_)    => `(sorry)
-  | `($(_) $_ $_) => `(sorry)
-  | _             => throw ()
+  | `($(_) _)   => `(sorry)
+  | `($(_) _ _) => `(sorry)
+  | _           => throw ()
 
 @[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)
@@ -345,6 +344,42 @@ syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " t
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
 
+/-! # `repeat` and `while` notation -/
+
+inductive Loop where
+  | mk
+
+@[inline]
+partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop (b : β) : m β := do
+    match ← f () b with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop b
+  loop init
+
+instance : ForIn m Loop Unit where
+  forIn := Loop.forIn
+
+syntax "repeat " doSeq : doElem
+
+macro_rules
+  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
+
+syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
+
+syntax "while " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
+
+syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
+
+macro_rules
+  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
+
 macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
   `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
 

src/Init/PropLemmas.lean

@@ -135,10 +135,6 @@ Both reduce to `b = false ∧ c = false` via `not_or`.
 
 theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
 
-/-! ## not equal -/
-
-theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
-  mt <| congrArg _
 
 /-! ## Ite -/
 
@@ -388,17 +384,6 @@ theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' :
 
 end quantifiers
 
-/-! ## membership -/
-
-section Mem
-variable [Membership α β] {s t : β} {a b : α}
-
-theorem ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt fun e => e ▸ h
-
-theorem ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt fun e => e ▸ h
-
-end Mem
-
 /-! ## Nonempty -/
 
 @[simp] theorem nonempty_prop {p : Prop} : Nonempty p ↔ p :=

src/Init/System/FilePath.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.System.Platform
+import Init.Data.String.Basic
+import Init.Data.Repr
 import Init.Data.ToString.Basic
 
 namespace System

src/Init/System/IO.lean

@@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone
 -/
 prelude
+import Init.Control.Reader
+import Init.Data.String
+import Init.Data.ByteArray
 import Init.System.IOError
 import Init.System.FilePath
 import Init.System.ST
+import Init.Data.ToString.Macro
 import Init.Data.Ord
 
 open System

src/Init/System/IOError.lean

@@ -5,7 +5,10 @@ Authors: Simon Hudon
 -/
 
 prelude
+import Init.Core
+import Init.Data.UInt.Basic
 import Init.Data.ToString.Basic
+import Init.Data.String.Basic
 
 /--
 Imitate the structure of IOErrorType in Haskell:

src/Init/Tactics.lean

@@ -268,9 +268,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
   -- Limit ref variability for incrementality; see Note [Incremental Macros]
-  withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
+  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic
@@ -495,7 +495,7 @@ macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
     `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
-/-- `rwa` is short-hand for `rw; assumption`. -/
+/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
 macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
   `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))
 

src/Init/While.lean

@@ -1,51 +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
--/
-prelude
-import Init.Core
-
-/-!
-# Notation for `while` and `repeat` loops.
--/
-
-namespace Lean
-
-/-! # `repeat` and `while` notation -/
-
-inductive Loop where
-  | mk
-
-@[inline]
-partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop (b : β) : m β := do
-    match ← f () b with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop b
-  loop init
-
-instance : ForIn m Loop Unit where
-  forIn := Loop.forIn
-
-syntax "repeat " doSeq : doElem
-
-macro_rules
-  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
-
-syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
-
-syntax "while " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
-
-syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
-
-macro_rules
-  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
-
-end Lean

src/Lean.lean

@@ -29,6 +29,7 @@ import Lean.Server
 import Lean.ScopedEnvExtension
 import Lean.DocString
 import Lean.DeclarationRange
+import Lean.LazyInitExtension
 import Lean.LoadDynlib
 import Lean.Widget
 import Lean.Log

src/Lean/Compiler/LCNF/PullLetDecls.lean

@@ -46,7 +46,7 @@ partial def withCheckpoint (x : PullM Code) : PullM Code := do
     else
       return c
   let (c, keep) := go toPullSizeSaved (← read).included |>.run #[]
-  modify fun s => { s with toPull := s.toPull.take toPullSizeSaved ++ keep }
+  modify fun s => { s with toPull := s.toPull.shrink toPullSizeSaved ++ keep }
   return c
 
 def attachToPull (c : Code) : PullM Code := do

src/Lean/Declaration.lean

@@ -369,13 +369,8 @@ def RecursorVal.getFirstIndexIdx (v : RecursorVal) : Nat :=
 def RecursorVal.getFirstMinorIdx (v : RecursorVal) : Nat :=
   v.numParams + v.numMotives
 
-/-- The inductive type of the major argument of the recursor. -/
-def RecursorVal.getMajorInduct (v : RecursorVal) : Name :=
-  go v.getMajorIdx v.type
-where
-  go
-  | 0, e => e.bindingDomain!.getAppFn.constName!
-  | n+1, e => go n e.bindingBody!
+def RecursorVal.getInduct (v : RecursorVal) : Name :=
+  v.name.getPrefix
 
 inductive QuotKind where
   | type  -- `Quot`
@@ -472,10 +467,6 @@ def isInductive : ConstantInfo → Bool
   | inductInfo _ => true
   | _            => false
 
-def isTheorem : ConstantInfo → Bool
-  | thmInfo _ => true
-  | _         => false
-
 def inductiveVal! : ConstantInfo → InductiveVal
   | .inductInfo val => val
   | _ => panic! "Expected a `ConstantInfo.inductInfo`."

src/Lean/Elab/BuiltinCommand.lean

@@ -12,18 +12,16 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
-import Init.System.Platform
 
 namespace Lean.Elab.Command
 
 @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
-  match stx[1] with
-  | Syntax.atom _ val =>
-    let doc := val.extract 0 (val.endPos - ⟨2⟩)
-    let some range ← Elab.getDeclarationRange? stx
-      | return  -- must be from partial syntax, ignore
-    modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
-  | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+   match stx[1] with
+   | Syntax.atom _ val =>
+     let doc := val.extract 0 (val.endPos - ⟨2⟩)
+     let range ← Elab.getDeclarationRange stx
+     modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
+   | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
 
 private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with
@@ -343,7 +341,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`
-      addDeclarationRangesFromSyntax declName stx id
+      addAuxDeclarationRanges declName stx id
     addDocString declName (← getDocStringText doc)
   | _ => throwUnsupportedSyntax
 
@@ -405,16 +403,6 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
       includedVars := sc.includedVars.filter (!omittedVars.contains ·) }
   | _ => throwUnsupportedSyntax
 
-@[builtin_command_elab version] def elabVersion : CommandElab := fun _ => do
-  let mut target := System.Platform.target
-  if target.isEmpty then target := "unknown"
-  -- Only one should be set, but good to know if multiple are set in error.
-  let platforms :=
-    (if System.Platform.isWindows then [" Windows"] else [])
-    ++ (if System.Platform.isOSX then [" macOS"] else [])
-    ++ (if System.Platform.isEmscripten then [" Emscripten"] else [])
-  logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
-
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
   logWarning "using 'exit' to interrupt Lean"
 

src/Lean/Elab/BuiltinNotation.lean

@@ -135,21 +135,13 @@ open Meta
   | _                                                => Macro.throwUnsupported
 
 @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices%$tk $x:ident      : $type from $val; $body)   => `(have%$tk $x : $type := $body; $val)
-  | `(suffices%$tk _%$x          : $type from $val; $body)   => `(have%$tk _%$x : $type := $body; $val)
-  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)   => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
-  | `(suffices%$tk $x:ident      : $type $b:byTactic'; $body) =>
-    -- Pass on `SourceInfo` of `b` to `have`. This is necessary to display the goal state in the
-    -- trailing whitespace of `by` and sound since `byTactic` and `byTactic'` are identical.
-    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
-    `(have%$tk $x : $type := $body; $b:byTactic)
-  | `(suffices%$tk _%$x          : $type $b:byTactic'; $body) =>
-    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
-    `(have%$tk _%$x : $type := $body; $b:byTactic)
-  | `(suffices%$tk $hy:hygieneInfo $type $b:byTactic'; $body) =>
-    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
-    `(have%$tk $hy:hygieneInfo : $type := $body; $b:byTactic)
-  | _ => Macro.throwUnsupported
+  | `(suffices%$tk $x:ident      : $type from $val; $body)            => `(have%$tk $x : $type := $body; $val)
+  | `(suffices%$tk _%$x          : $type from $val; $body)            => `(have%$tk _%$x : $type := $body; $val)
+  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)            => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
+  | `(suffices%$tk $x:ident      : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
+  | `(suffices%$tk _%$x          : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
+  | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
+  | _                                                                 => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do

src/Lean/Elab/Command.lean

@@ -711,54 +711,21 @@ def addUnivLevel (idStx : Syntax) : CommandElabM Unit := withRef idStx do
   else
     modifyScope fun scope => { scope with levelNames := id :: scope.levelNames }
 
+def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM ExpandDeclIdResult := do
+  let currNamespace ← getCurrNamespace
+  let currLevelNames ← getLevelNames
+  let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
+  for id in (← (← getScope).varDecls.flatMapM getBracketedBinderIds) do
+    if id == r.shortName then
+      throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
+  return r
+
 end Elab.Command
 
 open Elab Command MonadRecDepth
 
-private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) : CoreM α := do
-  let s : Core.State ← get
-  let ctx : Core.Context ← read
-  let (a, commandState) ←
-    cmd.run {
-      fileName := ctx.fileName
-      fileMap := ctx.fileMap
-      currRecDepth := ctx.currRecDepth
-      currMacroScope := ctx.currMacroScope
-      ref := ctx.ref
-      tacticCache? := none
-      snap? := none
-      cancelTk? := ctx.cancelTk?
-      suppressElabErrors := ctx.suppressElabErrors
-    } |>.run {
-      env := s.env
-      nextMacroScope := s.nextMacroScope
-      maxRecDepth := ctx.maxRecDepth
-      ngen := s.ngen
-      scopes := [{ header := "", opts := ctx.options }]
-      infoState.enabled := s.infoState.enabled
-    }
-  modify fun coreState => { coreState with
-    env := commandState.env
-    nextMacroScope := commandState.nextMacroScope
-    ngen := commandState.ngen
-    traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
-  }
-  if throwOnError then
-    if let some err := commandState.messages.toArray.find? (·.severity matches .error) then
-      throwError err.data
-  modify fun coreState => { coreState with
-    infoState.trees := coreState.infoState.trees.append commandState.infoState.trees
-    messages := coreState.messages ++ commandState.messages
-  }
-  return a
-
 /--
-Lifts an action in `CommandElabM` into `CoreM`, updating the environment,
-messages, info trees, traces, the name generator, and macro scopes.
-The action is run in a context with an empty message log, empty trace state, and empty info trees.
-
-If `throwOnError` is true, then if the command produces an error message, it is converted into an exception.
-In this case, info trees and messages are not carried over.
+Lifts an action in `CommandElabM` into `CoreM`, updating the traces and the environment.
 
 Commands that modify the processing of subsequent commands,
 such as `open` and `namespace` commands,
@@ -771,9 +738,27 @@ to reset the instance cache.
 While the `modifyEnv` function for `MetaM` clears its caches entirely,
 `liftCommandElabM` has no way to reset these caches.
 -/
-def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : CoreM α := do
-  -- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`.
-  MonadExcept.ofExcept (← liftCommandElabMCore (observing cmd) throwOnError)
+def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
+  let (a, commandState) ←
+    cmd.run {
+      fileName := ← getFileName
+      fileMap := ← getFileMap
+      ref := ← getRef
+      tacticCache? := none
+      snap? := none
+      cancelTk? := (← read).cancelTk?
+    } |>.run {
+      env := ← getEnv
+      maxRecDepth := ← getMaxRecDepth
+      scopes := [{ header := "", opts := ← getOptions }]
+    }
+  modify fun coreState => { coreState with
+    traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
+    env := commandState.env
+  }
+  if let some err := commandState.messages.toArray.find? (·.severity matches .error) then
+    throwError err.data
+  pure a
 
 /--
 Given a command elaborator `cmd`, returns a new command elaborator that

src/Lean/Elab/DeclModifiers.lean

@@ -57,8 +57,6 @@ inductive RecKind where
 
 /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
-  /-- Input syntax, used for adjusting declaration range (unless missing) -/
-  stx             : TSyntax ``Parser.Command.declModifiers := ⟨.missing⟩
   docString?      : Option String := none
   visibility      : Visibility := Visibility.regular
   isNoncomputable : Bool := false
@@ -123,16 +121,16 @@ section Methods
 variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
 
 /-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
-def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
-  let docCommentStx := stx.raw[0]
-  let attrsStx      := stx.raw[1]
-  let visibilityStx := stx.raw[2]
-  let noncompStx    := stx.raw[3]
-  let unsafeStx     := stx.raw[4]
+def elabModifiers (stx : Syntax) : m Modifiers := do
+  let docCommentStx := stx[0]
+  let attrsStx      := stx[1]
+  let visibilityStx := stx[2]
+  let noncompStx    := stx[3]
+  let unsafeStx     := stx[4]
   let recKind       :=
-    if stx.raw[5].isNone then
+    if stx[5].isNone then
       RecKind.default
-    else if stx.raw[5][0].getKind == ``Parser.Command.partial then
+    else if stx[5][0].getKind == ``Parser.Command.partial then
       RecKind.partial
     else
       RecKind.nonrec
@@ -150,7 +148,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
     | none       => pure #[]
     | some attrs => elabDeclAttrs attrs
   return {
-    stx, docString?, visibility, recKind, attrs,
+    docString?, visibility, recKind, attrs,
     isUnsafe        := !unsafeStx.isNone
     isNoncomputable := !noncompStx.isNone
   }

src/Lean/Elab/Declaration.lean

@@ -102,16 +102,14 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   -- leading_parser "axiom " >> declId >> declSig
   let declId             := stx[1]
   let (binders, typeStx) := expandDeclSig stx[2]
-  runTermElabM fun vars => do
-    let scopeLevelNames ← Term.getLevelNames
-    let ⟨shortName, declName, allUserLevelNames⟩ ← Term.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
-    addDeclarationRangesForBuiltin declName modifiers.stx stx
-    Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do
+  let scopeLevelNames ← getLevelNames
+  let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
+  addDeclarationRanges declName stx
+  runTermElabM fun vars =>
     Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
       let type ← Term.elabType typeStx
       Term.synthesizeSyntheticMVarsNoPostponing
-      let xs ← Term.addAutoBoundImplicits xs
       let type ← instantiateMVars type
       let type ← mkForallFVars xs type
       let type ← mkForallFVars vars type (usedOnly := true)
@@ -137,6 +135,63 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
           compileDecl decl
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
+/-
+leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
+leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
+-/
+private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
+  checkValidInductiveModifier modifiers
+  let (binders, type?) := expandOptDeclSig decl[2]
+  let declId           := decl[1]
+  let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
+  addDeclarationRanges declName decl
+  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
+    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
+    let mut ctorModifiers ← elabModifiers ctor[2]
+    if let some leadingDocComment := ctor[0].getOptional? then
+      if ctorModifiers.docString?.isSome then
+        logErrorAt leadingDocComment "duplicate doc string"
+      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
+    if ctorModifiers.isPrivate && modifiers.isPrivate then
+      throwError "invalid 'private' constructor in a 'private' inductive datatype"
+    if ctorModifiers.isProtected && modifiers.isPrivate then
+      throwError "invalid 'protected' constructor in a 'private' inductive datatype"
+    checkValidCtorModifier ctorModifiers
+    let ctorName := ctor.getIdAt 3
+    let ctorName := declName ++ ctorName
+    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName
+    let (binders, type?) := expandOptDeclSig ctor[4]
+    addDocString' ctorName ctorModifiers.docString?
+    addAuxDeclarationRanges ctorName ctor ctor[3]
+    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
+    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
+  let classes ← liftCoreM <| getOptDerivingClasses decl[6]
+  if decl[3][0].isToken ":=" then
+    -- https://github.com/leanprover/lean4/issues/5236
+    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
+      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
+  return {
+    ref             := decl
+    shortDeclName   := name
+    derivingClasses := classes
+    declId, modifiers, declName, levelNames
+    binders, type?, ctors
+    computedFields
+  }
+
+private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
+  inductiveSyntaxToView modifiers decl
+
+def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let v ← inductiveSyntaxToView modifiers stx
+  elabInductiveViews #[v]
+
+def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let modifiers := modifiers.addAttr { name := `class }
+  let v ← classInductiveSyntaxToView modifiers stx
+  elabInductiveViews #[v]
+
 /--
 Macro that expands a declaration with a complex name into an explicit `namespace` block.
 Implementing this step as a macro means that reuse checking is handled by `elabCommand`.
@@ -159,22 +214,34 @@ def elabDeclaration : CommandElab := fun stx => do
     -- only case implementing incrementality currently
     elabMutualDef #[stx]
   else withoutCommandIncrementality true do
-    let modifiers : TSyntax ``Parser.Command.declModifiers := ⟨stx[0]⟩
     if declKind == ``Lean.Parser.Command.«axiom» then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabAxiom modifiers decl
     else if declKind == ``Lean.Parser.Command.«inductive» then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.classInductive then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabClassInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.«structure» then
-      let modifiers ← elabModifiers modifiers
+      let modifiers ← elabModifiers stx[0]
       elabStructure modifiers decl
     else
       throwError "unexpected declaration"
 
+/-- Return true if all elements of the mutual-block are inductive declarations. -/
+private def isMutualInductive (stx : Syntax) : Bool :=
+  stx[1].getArgs.all fun elem =>
+    let decl     := elem[1]
+    let declKind := decl.getKind
+    declKind == `Lean.Parser.Command.inductive
+
+private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
+  let views ← elems.mapM fun stx => do
+     let modifiers ← elabModifiers stx[0]
+     inductiveSyntaxToView modifiers stx[1]
+  elabInductiveViews views
+
 /-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/
 private def isMutualDef (stx : Syntax) : Bool :=
   stx[1].getArgs.all fun elem =>
@@ -332,7 +399,7 @@ def elabMutual : CommandElab := fun stx => do
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
-      addDeclarationRangesForBuiltin fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
+      addDeclarationRanges fullId defStx
       elabCommand (← `(
         $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))

src/Lean/Elab/DeclarationRange.lean

@@ -11,14 +11,12 @@ import Lean.Data.Lsp.Utf16
 
 namespace Lean.Elab
 
-def getDeclarationRange? [Monad m] [MonadFileMap m] (stx : Syntax) : m (Option DeclarationRange) := do
-  let some range := stx.getRange?
-    | return none
+def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do
   let fileMap ← getFileMap
-  --let range := fileMap.utf8RangeToLspRange
-  let pos    := fileMap.toPosition range.start
-  let endPos := fileMap.toPosition range.stop
-  return some {
+  let pos    := stx.getPos?.getD 0
+  let endPos := stx.getTailPos?.getD pos |> fileMap.toPosition
+  let pos    := pos |> fileMap.toPosition
+  return {
     pos          := pos
     charUtf16    := fileMap.leanPosToLspPos pos |>.character
     endPos       := endPos
@@ -49,31 +47,25 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
     else
       stx[0]
 
-/--
-Derives and adds declaration ranges from given syntax trees. If `rangeStx` does not have a range,
-nothing is added. If `selectionRangeStx` does not have a range, it is defaulted to that of
-`rangeStx`.
--/
-def addDeclarationRangesFromSyntax [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
-    (rangeStx : Syntax) (selectionRangeStx : Syntax := .missing) : m Unit := do
-  -- may fail on partial syntax, ignore in that case
-  let some range ← getDeclarationRange? rangeStx | return
-  let selectionRange ← (·.getD range) <$> getDeclarationRange? selectionRangeStx
-  Lean.addDeclarationRanges declName { range, selectionRange }
 
 /--
-Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and
-`cmdStx` the remaining part of the syntax tree for `declName`.
-
-This method is for the builtin declarations only. User-defined commands should use
-`Lean.Elab.addDeclarationRangesFromSyntax` or `Lean.addDeclarationRanges` to store this information
-for their commands.
--/
-def addDeclarationRangesForBuiltin [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
-    (modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do
-  if declStx.getKind == ``Parser.Command.«example» then
+  Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object describing `declName`.
+  This method is for the builtin declarations only.
+  User-defined commands should use `Lean.addDeclarationRanges` to store this information for their commands. -/
+def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) : m Unit := do
+  if stx.getKind == ``Parser.Command.«example» then
     return ()
-  let stx := mkNullNode #[modsStx, declStx]
-  addDeclarationRangesFromSyntax declName stx (getDeclarationSelectionRef declStx)
+  else
+    Lean.addDeclarationRanges declName {
+      range          := (← getDeclarationRange stx)
+      selectionRange := (← getDeclarationRange (getDeclarationSelectionRef stx))
+    }
+
+/-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/
+def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do
+  Lean.addDeclarationRanges declName {
+    range          := (← getDeclarationRange stx)
+    selectionRange := (← getDeclarationRange header)
+  }
 
 end Lean.Elab

src/Lean/Elab/Frontend.lean

@@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
 where
   go initialSnap t commands :=
     let snap := t.get
-    let commands := commands.push snap.data
+    let commands := commands.push snap.data.stx
     if let some next := snap.nextCmdSnap? then
       go initialSnap next.task commands
     else
@@ -111,15 +111,13 @@ where
       let messages := toSnapshotTree initialSnap
         |>.getAll.map (·.diagnostics.msgLog)
         |>.foldl (· ++ ·) {}
-      -- In contrast to messages, we should collect info trees only from the top-level command
-      -- snapshots as they subsume any info trees reported incrementally by their children.
-      let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+      let trees := toSnapshotTree initialSnap
+        |>.getAll.map (·.infoTree?) |>.filterMap id |>.toPArray'
       return {
         commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
         parserState := snap.data.parserState
         cmdPos := snap.data.parserState.pos
-        commands := commands.map (·.stx)
-        inputCtx, initialSnap
+        inputCtx, initialSnap, commands
       }
 
 def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
@@ -145,7 +143,7 @@ def runFrontend
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
-  let opts := Language.Lean.internal.cmdlineSnapshots.setIfNotSet opts true
+  let opts := Language.Lean.internal.cmdlineSnapshots.set opts true
   let ctx := { inputCtx with }
   let processor := Language.Lean.process
   let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx

src/Lean/Elab/Inductive.lean

@@ -18,7 +18,6 @@ import Lean.Elab.ComputedFields
 import Lean.Elab.DefView
 import Lean.Elab.DeclUtil
 import Lean.Elab.Deriving.Basic
-import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab.Command
 open Meta
@@ -80,56 +79,10 @@ structure ElabHeaderResult where
   view       : InductiveView
   lctx       : LocalContext
   localInsts : LocalInstances
-  levelNames : List Name
   params     : Array Expr
   type       : Expr
   deriving Inhabited
 
-/-
-leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
-leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
--/
-private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : TermElabM InductiveView := do
-  checkValidInductiveModifier modifiers
-  let (binders, type?) := expandOptDeclSig decl[2]
-  let declId           := decl[1]
-  let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
-  addDeclarationRangesForBuiltin declName modifiers.stx decl
-  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
-    if let some leadingDocComment := ctor[0].getOptional? then
-      if ctorModifiers.docString?.isSome then
-        logErrorAt leadingDocComment "duplicate doc string"
-      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
-    if ctorModifiers.isPrivate && modifiers.isPrivate then
-      throwError "invalid 'private' constructor in a 'private' inductive datatype"
-    if ctorModifiers.isProtected && modifiers.isPrivate then
-      throwError "invalid 'protected' constructor in a 'private' inductive datatype"
-    checkValidCtorModifier ctorModifiers
-    let ctorName := ctor.getIdAt 3
-    let ctorName := declName ++ ctorName
-    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName
-    let (binders, type?) := expandOptDeclSig ctor[4]
-    addDocString' ctorName ctorModifiers.docString?
-    addDeclarationRangesFromSyntax ctorName ctor ctor[3]
-    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
-  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
-    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← getOptDerivingClasses decl[6]
-  if decl[3][0].isToken ":=" then
-    -- https://github.com/leanprover/lean4/issues/5236
-    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
-      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
-  return {
-    ref             := decl
-    shortDeclName   := name
-    derivingClasses := classes
-    declId, modifiers, declName, levelNames
-    binders, type?, ctors
-    computedFields
-  }
-
 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
@@ -141,8 +94,7 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
           let type := mkSort u
           Term.synthesizeSyntheticMVarsNoPostponing
           Term.addAutoBoundImplicits' params type fun params type => do
-            let levelNames ← Term.getLevelNames
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
         | some typeStx =>
           let (type, _) ← Term.withAutoBoundImplicit do
             let type ← Term.elabType typeStx
@@ -153,8 +105,7 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
             return (← mkForallFVars indices type, indices.size)
           Term.addAutoBoundImplicits' params type fun params type => do
             trace[Elab.inductive] "header params: {params}, type: {type}"
-            let levelNames ← Term.getLevelNames
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
       elabHeaderAux views (i+1) acc
     else
       return acc
@@ -172,20 +123,13 @@ private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
     unless r.view.modifiers.isUnsafe == isUnsafe do
       throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
-private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
+private def checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
   if views.size > 1 then
     let levelNames := views[0]!.levelNames
     for view in views do
       unless view.levelNames == levelNames do
         throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
-private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
-  if rs.size > 1 then
-    let levelNames := rs[0]!.levelNames
-    for r in rs do
-      unless r.levelNames == levelNames do
-        throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
-
 private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
   withLCtx r.lctx r.localInsts do
     mkForallFVars r.params r.type
@@ -847,15 +791,12 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind
 private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
   let view0 := views[0]!
   let scopeLevelNames ← Term.getLevelNames
-  InductiveView.checkLevelNames views
+  checkLevelNames views
   let allUserLevelNames := view0.levelNames
   let isUnsafe          := view0.modifiers.isUnsafe
   withRef view0.ref <| Term.withLevelNames allUserLevelNames do
     let rs ← elabHeader views
     Term.synthesizeSyntheticMVarsNoPostponing
-    ElabHeaderResult.checkLevelNames rs
-    let allUserLevelNames := rs[0]!.levelNames
-    trace[Elab.inductive] "level names: {allUserLevelNames}"
     withInductiveLocalDecls rs fun params indFVars => do
       trace[Elab.inductive] "indFVars: {indFVars}"
       let mut indTypesArray := #[]
@@ -947,55 +888,19 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM
   liftTermElabM do Term.withDeclName indViews[0]!.declName do
     ComputedFields.setComputedFields computedFields
 
-def elabInductiveViews (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do
+def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
   let view0 := views[0]!
   let ref := view0.ref
-  Term.withDeclName view0.declName do withRef ref do
+  runTermElabM fun vars => Term.withDeclName view0.declName do withRef ref do
     mkInductiveDecl vars views
     mkSizeOfInstances view0.declName
     Lean.Meta.IndPredBelow.mkBelow view0.declName
     for view in views do
       mkInjectiveTheorems view.declName
-
-def elabInductiveViewsPostprocessing (views : Array InductiveView) : CommandElabM Unit := do
-  let view0 := views[0]!
-  let ref := view0.ref
   applyComputedFields views -- NOTE: any generated code before this line is invalid
   applyDerivingHandlers views
   runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
     for view in views do
       Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
 
-def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit := do
-  let vs ← runTermElabM fun vars => do
-    let vs ← inductives.mapM fun (modifiers, stx) => inductiveSyntaxToView modifiers stx
-    elabInductiveViews vars vs
-    pure vs
-  elabInductiveViewsPostprocessing vs
-
-def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  elabInductives #[(modifiers, stx)]
-
-def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let modifiers := modifiers.addAttr { name := `class }
-  elabInductive modifiers stx
-
-/--
-Returns true if all elements of the `mutual` block (`Lean.Parser.Command.mutual`) are inductive declarations.
--/
-def isMutualInductive (stx : Syntax) : Bool :=
-  stx[1].getArgs.all fun elem =>
-    let decl     := elem[1]
-    let declKind := decl.getKind
-    declKind == `Lean.Parser.Command.inductive
-
-/--
-Elaborates a `mutual` block satisfying `Lean.Elab.Command.isMutualInductive`.
--/
-def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
-  let inductives ← elems.mapM fun stx => do
-    let modifiers ← elabModifiers ⟨stx[0]⟩
-    pure (modifiers, stx[1])
-  elabInductives inductives
-
 end Lean.Elab.Command

src/Lean/Elab/LetRec.lean

@@ -51,7 +51,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?
-      addDeclarationRangesFromSyntax declName decl declId
+      addAuxDeclarationRanges declName decl declId
       let binders := decl[1].getArgs
       let typeStx := expandOptType declId decl[2]
       let (type, binderIds) ← elabBindersEx binders fun xs => do
@@ -90,7 +90,6 @@ 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 := mkTermInfo `MutualDef.body view.valStx) do
          let value ← elabTermEnsuringType view.valStx type
          mkLambdaFVars xs value
 

src/Lean/Elab/MutualDef.lean

@@ -410,15 +410,11 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- skip auto-bound prefix in `xs`
           addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
         let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
-          -- 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 := 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
-            -- leads to more section variables being included than necessary
-            instantiateMVarsProfiling val
+          -- synthesize mvars here to force the top-level tactic block (if any) to run
+          elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
+        -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
+        -- leads to more section variables being included than necessary
+        let val ← instantiateMVarsProfiling val
         let val ← mkLambdaFVars xs val
         if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do
@@ -997,7 +993,7 @@ where
       for view in views, header in headers do
         -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
         -- that depends only on a part of the ref
-        addDeclarationRangesForBuiltin header.declName view.modifiers.stx view.ref
+        addDeclarationRanges header.declName view.ref
 
 
   processDeriving (headers : Array DefViewElabHeader) := do
@@ -1021,7 +1017,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     let mut reusedAllHeaders := true
     for h : i in [0:ds.size], headerPromise in headerPromises do
       let d := ds[i]
-      let modifiers ← elabModifiers ⟨d[0]⟩
+      let modifiers ← elabModifiers d[0]
       if ds.size > 1 && modifiers.isNonrec then
         throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
       let mut view ← mkDefView modifiers d[1]

src/Lean/Elab/ParseImportsFast.lean

@@ -182,7 +182,7 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
   let s := p input s
   match s.error? with
   | none => many p input s
-  | some _ => { pos, error? := none, imports := s.imports.take size }
+  | some _ => { pos, error? := none, imports := s.imports.shrink size }
 
 @[inline] partial def preludeOpt (k : String) : Parser :=
   keywordCore k (fun _ s => s.pushModule `Init false) (fun _ s => s)

src/Lean/Elab/PreDefinition/Basic.lean

@@ -221,7 +221,7 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit :=
               else
                 none
             | _ => none
-          modifiers := default }
+          modifiers := {} }
 
 private def containsRecFn (recFnNames : Array Name) (e : Expr) : Bool :=
   (e.find? fun e => e.isConst && recFnNames.contains e.constName!).isSome

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -5,24 +5,9 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.AppBuilder
-import Lean.PrettyPrinter
 namespace Lean.Elab
 open Meta
 
-private def withInhabitedInstances (xs : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
-  let rec go (i : Nat) (insts : Array Expr) : MetaM α := do
-    if h : i < xs.size then
-      let x := xs[i]
-      let xTy ← inferType x
-      let u ← getLevel xTy
-      let instTy := mkApp (.const ``Inhabited [u]) xTy
-      let instVal := mkApp2 (.const ``Inhabited.mk [u]) xTy x
-      withLetDecl `inst instTy instVal fun inst =>
-        go (i + 1) (insts.push inst)
-    else
-      k insts
-  go 0 #[]
-
 private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) := do
   try
     if useOfNonempty then
@@ -32,41 +17,36 @@ private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option E
   catch _ =>
     return none
 
-/--
-Find an inhabitant while doing delta unfolding.
--/
-private partial def mkInhabitantForAux? (xs insts : Array Expr) (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) := withIncRecDepth do
-  if let some val ← mkInhabitant? type useOfNonempty then
-    mkLambdaFVars xs (← mkLetFVars (usedLetOnly := true) insts val)
-  else
-    let type ← whnfCore type
-    if type.isForall then
-      forallTelescope type fun xs' type' =>
-        withInhabitedInstances xs' fun insts' =>
-          mkInhabitantForAux? (xs ++ xs') (insts ++ insts') type' useOfNonempty
-    else if let some type' ← unfoldDefinition? type then
-      mkInhabitantForAux? xs insts type' useOfNonempty
-    else
-      return none
+private def findAssumption? (xs : Array Expr) (type : Expr) : MetaM (Option Expr) := do
+  xs.findM? fun x => do isDefEq (← inferType x) type
+
+private def mkFnInhabitant? (xs : Array Expr) (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) :=
+  let rec loop
+    | 0,   type => mkInhabitant? type useOfNonempty
+    | i+1, type => do
+      let x := xs[i]!
+      let type ← mkForallFVars #[x] type;
+      match (← mkInhabitant? type useOfNonempty) with
+      | none     => loop i type
+      | some val => return some (← mkLambdaFVars xs[0:i] val)
+  loop xs.size type
 
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
-def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr :=
-  withInhabitedInstances xs fun insts => do
-    if let some val ← mkInhabitantForAux? xs insts type false <||> mkInhabitantForAux? xs insts type true then
-      return val
-    else
-      throwError "\
-        failed to compile 'partial' definition '{declName}', could not prove that the type\
-        {indentExpr (← mkForallFVars xs type)}\n\
-        is nonempty.\n\
-        \n\
-        This process uses multiple strategies:\n\
-        - It looks for a parameter that matches the return type.\n\
-        - It tries synthesizing '{MessageData.ofConstName ``Inhabited}' and '{MessageData.ofConstName ``Nonempty}' \
-          instances for the return type, while making every parameter into a local '{MessageData.ofConstName ``Inhabited}' instance.\n\
-        - It tries unfolding the return type.\n\
-        \n\
-        If the return type is defined using the 'structure' or 'inductive' command, \
-        you can try adding a 'deriving Nonempty' clause to it."
+def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
+  let go? (useOfNonempty : Bool) : MetaM (Option Expr) := do
+    match (← mkInhabitant? type useOfNonempty) with
+    | some val => mkLambdaFVars xs val
+    | none     =>
+    match (← findAssumption? xs type) with
+    | some x => mkLambdaFVars xs x
+    | none   =>
+    match (← mkFnInhabitant? xs type useOfNonempty) with
+    | some val => return val
+    | none     => return none
+  match (← go? false) with
+  | some val => return val
+  | none     => match (← go? true) with
+    | some val => return val
+    | none     => throwError "failed to compile partial definition '{declName}', failed to show that type is inhabited and non empty"
 
 end Lean.Elab

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -212,21 +212,21 @@ def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
 /--
 Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
 The `value` is the function with (only) the fixed parameters moved into the context,
-The `FType` is the expected type of the argument.
+The `type` is the expected type of the argument.
 The `recArgInfos` is used to transform the body of the function to replace recursive calls with
 uses of the `below` induction hypothesis.
 -/
 def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
     (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
   lambdaTelescope value fun xs value => do
-    let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
-    let FType ← instantiateForall FType indicesMajorArgs
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let FType ← instantiateForall FType indexMajorArgs
     forallBoundedTelescope FType (some 1) fun below _ => do
       -- TODO: `below` user name is `f`, and it will make a global `f` to be pretty printed as `_root_.f` in error messages.
       -- We should add an option to `forallBoundedTelescope` to ensure fresh names are used.
       let below := below[0]!
-      let valueNew ← replaceRecApps recArgInfos positions below value
-      mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
+      let valueNew   ← replaceRecApps recArgInfos positions below value
+      mkLambdaFVars (indexMajorArgs ++ #[below] ++ otherArgs) valueNew
 
 /--
 Given the `motives`, figures out whether to use `.brecOn` or `.binductionOn`, pass
@@ -264,7 +264,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
     (brecOnConst : Nat → Expr) : MetaM (Array Expr) := do
   let numTypeFormers := positions.size
   let recArgInfo := recArgInfos[0]! -- pick an arbitrary one
-  let brecOn := brecOnConst recArgInfo.indIdx
+  let brecOn := brecOnConst 0
   check brecOn
   let brecOnType ← inferType brecOn
   -- Skip the indices and major argument

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -77,7 +77,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       if !indIndices.all Expr.isFVar then
         throwError "its type {indInfo.name} is an inductive family and indices are not variables{indentExpr xType}"
       else if !indIndices.allDiff then
-        throwError "its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+        throwError " its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
       else
         let indexMinPos := getIndexMinPos xs indIndices
         let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -107,9 +107,9 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
     check valueNew
     return #[{ preDef with value := valueNew }]
 
-  -- Groups the (indices of the) definitions by their position in indInfo.all
+  -- Sort the (indices of the) definitions by their position in indInfo.all
   let positions : Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers)
-  trace[Elab.definition.structural] "assignments of type formers of {indInfo.name} to functions: {positions}"
+  trace[Elab.definition.structural] "positions: {positions}"
 
   -- Construct the common `.brecOn` arguments
   let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
@@ -117,7 +117,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
   let brecOnConst ← mkBRecOnConst recArgInfos positions motives
   let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
   trace[Elab.definition.structural] "FTypes: {FTypes}"
-  let FArgs ← (recArgInfos.zip (values.zip FTypes)).mapM fun (r, (v, t)) =>
+  let FArgs ← (recArgInfos.zip  (values.zip FTypes)).mapM fun (r, (v, t)) =>
     mkBRecOnF recArgInfos positions r v t
   trace[Elab.definition.structural] "FArgs: {FArgs}"
   -- Assemble the individual `.brecOn` applications

src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean

@@ -15,7 +15,7 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) :
   return { preDef with
     declName  := mkSmartUnfoldingNameFor preDef.declName
     value     := (← visit preDef.value)
-    modifiers := default
+    modifiers := {}
   }
 where
   /--

src/Lean/Elab/StructInst.lean

@@ -826,22 +826,9 @@ def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option
 /-- Reduce default value. It performs beta reduction and projections of the given structures. -/
 partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
   match e with
+  | .lam ..       => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b)
   | .forallE ..   => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b)
-  | .lam ..
-  | .letE ..      => lambdaLetTelescope e fun xs b => do
-    /- The bodies of let-declarations also need to be reduced.
-       Otherwise, some metavariables may be kept in the terms, leading to errors
-       when trying to generate default values.
-       Fixes `#3146`
-    -/
-    let localInsts ← Meta.getLocalInstances
-    let mut lctx ← getLCtx
-    for e in xs do
-      let some lcdl := lctx.findFVar? e | unreachable!
-      let some value := lcdl.value? | continue
-      let value ← Meta.withLCtx lctx localInsts (reduce structNames value)
-      lctx := lctx.modifyLocalDecl e.fvarId! (·.setValue value)
-    Meta.withLCtx lctx localInsts (mkLetFVars xs (← reduce structNames b))
+  | .letE ..      => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b)
   | .proj _ i b   =>
     match (← Meta.project? b i) with
     | some r => reduce structNames r

src/Lean/Elab/Structure.lean

@@ -94,8 +94,8 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
   let useDefault := do
     let declName := structDeclName ++ defaultCtorName
     let ref := structStx[1].mkSynthetic
-    addDeclarationRangesFromSyntax declName ref
-    pure { ref, modifiers := default, name := defaultCtorName, declName }
+    addAuxDeclarationRanges declName ref ref
+    pure { ref, modifiers := {}, name := defaultCtorName, declName }
   if structStx[5].isNone then
     useDefault
   else
@@ -115,7 +115,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
       let declName := structDeclName ++ name
       let declName ← applyVisibility ctorModifiers.visibility declName
       addDocString' declName ctorModifiers.docString?
-      addDeclarationRangesFromSyntax declName ctor[1]
+      addAuxDeclarationRanges declName ctor[1] ctor[1]
       pure { ref := ctor[1], name, modifiers := ctorModifiers, declName }
 
 def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
@@ -815,7 +815,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
   view.fields.forM fun field => do
     if field.declName == view.ctor.declName then
       throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name"
-    addDeclarationRangesFromSyntax field.declName field.ref
+    addAuxDeclarationRanges field.declName field.ref field.ref
   let type ← Term.elabType view.type
   unless validStructType type do throwErrorAt view.type "expected Type"
   withRef view.ref do
@@ -912,7 +912,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
       let scopeLevelNames ← Term.getLevelNames
       let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
       Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do
-        addDeclarationRangesForBuiltin declName modifiers.stx stx
+        addDeclarationRanges declName stx
         Term.withDeclName declName do
           let ctor ← expandCtor stx modifiers declName
           let fields ← expandFields stx modifiers declName

src/Lean/Elab/Syntax.lean

@@ -146,7 +146,7 @@ where
       let args ← args.mapM fun arg => withNestedParser do process arg
       mkParserSeq args
     else
-      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i == 0 }) do process arg
+      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i.val == 0 }) do process arg
       mkParserSeq args
 
   ensureNoPrec (stx : Syntax) :=

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

@@ -29,7 +29,6 @@ instance : ToExpr BVBinOp where
     | .mul => mkConst ``BVBinOp.mul
     | .udiv => mkConst ``BVBinOp.udiv
     | .umod => mkConst ``BVBinOp.umod
-    | .sdiv => mkConst ``BVBinOp.sdiv
   toTypeExpr := mkConst ``BVBinOp
 
 instance : ToExpr BVUnOp where

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

@@ -65,220 +65,202 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
   | _ => return none
 
 /--
-Construct an uninterpreted `BitVec` atom from `x`.
--/
-def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-  let t ← instantiateMVars (← whnfR (← inferType x))
-  let_expr BitVec widthExpr := t | return none
-  let some width ← getNatValue? widthExpr | return none
-  let atom ← mkAtom x width
-  return some atom
-
-/--
-Reify an `Expr` that's a constant-width `BitVec`.
-Unless this function is called on something that is not a constant-width `BitVec` it is always
-going to return `some`.
+Reify an `Expr` that's a `BitVec`.
 -/
 partial def of (x : Expr) : M (Option ReifiedBVExpr) := do
-  goOrAtom x
-where
-  /--
-  Reify `x`, returns `none` if the reification procedure failed.
-  -/
-  go (x : Expr) : M (Option ReifiedBVExpr) := do
-    match_expr x with
-    | BitVec.ofNat _ _ => goBvLit x
-    | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
-    | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
-    | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
-    | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
-    | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
-    | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
-    | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
-    | BitVec.sdiv _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
-    | Complement.complement _ _ innerExpr =>
-      unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
-    | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeftConst
-          ``BVUnOp.shiftLeftConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
-      else
-        shiftReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftLeft
-          ``BVExpr.shiftLeft
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
-    | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
-      let distance? ← getNatOrBvValue? β distanceExpr
-      if distance?.isSome then
-        shiftConstReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRightConst
-          ``BVUnOp.shiftRightConst
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
-      else
-        shiftReflection
-          β
-          distanceExpr
-          innerExpr
-          .shiftRight
-          ``BVExpr.shiftRight
-          ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
-    | BitVec.sshiftRight _ innerExpr distanceExpr =>
-      let some distance ← getNatValue? distanceExpr | return none
-      shiftConstLikeReflection
-        distance
+  match_expr x with
+  | BitVec.ofNat _ _ => goBvLit x
+  | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
+  | HOr.hOr _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr
+  | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
+  | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
+  | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
+  | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
+  | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
+  | Complement.complement _ _ innerExpr =>
+    unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
+  | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
+    let distance? ← getNatOrBvValue? β distanceExpr
+    if distance?.isSome then
+      shiftConstReflection
+        β
+        distanceExpr
         innerExpr
-        .arithShiftRightConst
-        ``BVUnOp.arithShiftRightConst
-        ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
-    | BitVec.zeroExtend _ newWidthExpr innerExpr =>
-      let some newWidth ← getNatValue? newWidthExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .zeroExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.zeroExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
-    | BitVec.signExtend _ newWidthExpr innerExpr =>
-      let some newWidth ← getNatValue? newWidthExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .signExtend newWidth inner.bvExpr
-      let expr :=
-        mkApp3
-          (mkConst ``BVExpr.signExtend)
-          (toExpr inner.width)
-          newWidthExpr
-          inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
-          newWidthExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨newWidth, bvExpr, proof, expr⟩
-    | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
-      let some lhs ← goOrAtom lhsExpr | return none
-      let some rhs ← goOrAtom rhsExpr | return none
-      let bvExpr := .append lhs.bvExpr rhs.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.append)
-        (toExpr lhs.width)
-        (toExpr rhs.width)
-        lhs.expr rhs.expr
-      let proof := do
-        let lhsEval ← mkEvalExpr lhs.width lhs.expr
-        let lhsProof ← lhs.evalsAtAtoms
-        let rhsProof ← rhs.evalsAtAtoms
-        let rhsEval ← mkEvalExpr rhs.width rhs.expr
-        return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
-          (toExpr lhs.width) (toExpr rhs.width)
-          lhsExpr lhsEval
-          rhsExpr rhsEval
-          lhsProof rhsProof
-      return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
-    | BitVec.replicate _ nExpr innerExpr =>
-      let some inner ← goOrAtom innerExpr | return none
-      let some n ← getNatValue? nExpr | return none
-      let bvExpr := .replicate n inner.bvExpr
-      let expr := mkApp3 (mkConst ``BVExpr.replicate)
+        .shiftLeftConst
+        ``BVUnOp.shiftLeftConst
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
+    else
+      shiftReflection
+        β
+        distanceExpr
+        innerExpr
+        .shiftLeft
+        ``BVExpr.shiftLeft
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
+  | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
+    let distance? ← getNatOrBvValue? β distanceExpr
+    if distance?.isSome then
+      shiftConstReflection
+        β
+        distanceExpr
+        innerExpr
+        .shiftRightConst
+        ``BVUnOp.shiftRightConst
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
+    else
+      shiftReflection
+        β
+        distanceExpr
+        innerExpr
+        .shiftRight
+        ``BVExpr.shiftRight
+        ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
+  | BitVec.sshiftRight _ innerExpr distanceExpr =>
+    let some distance ← getNatValue? distanceExpr | return ← ofAtom x
+    shiftConstLikeReflection
+      distance
+      innerExpr
+      .arithShiftRightConst
+      ``BVUnOp.arithShiftRightConst
+      ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
+  | BitVec.zeroExtend _ newWidthExpr innerExpr =>
+    let some newWidth ← getNatValue? newWidthExpr | return ← ofAtom x
+    let some inner ← ofOrAtom innerExpr | return none
+    let bvExpr := .zeroExtend newWidth inner.bvExpr
+    let expr :=
+      mkApp3
+        (mkConst ``BVExpr.zeroExtend)
         (toExpr inner.width)
-        (toExpr n)
+        newWidthExpr
         inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
-          (toExpr n)
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨inner.width * n, bvExpr, proof, expr⟩
-    | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
-      let some start ← getNatValue? startExpr | return none
-      let some len ← getNatValue? lenExpr | return none
-      let some inner ← goOrAtom innerExpr | return none
-      let bvExpr := .extract start len inner.bvExpr
-      let expr := mkApp4 (mkConst ``BVExpr.extract)
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
+        newWidthExpr
         (toExpr inner.width)
+        innerExpr
+        innerEval
+        innerProof
+    return some ⟨newWidth, bvExpr, proof, expr⟩
+  | BitVec.signExtend _ newWidthExpr innerExpr =>
+    let some newWidth ← getNatValue? newWidthExpr | return ← ofAtom x
+    let some inner ← ofOrAtom innerExpr | return none
+    let bvExpr := .signExtend newWidth inner.bvExpr
+    let expr :=
+      mkApp3
+        (mkConst ``BVExpr.signExtend)
+        (toExpr inner.width)
+        newWidthExpr
+        inner.expr
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
+        newWidthExpr
+        (toExpr inner.width)
+        innerExpr
+        innerEval
+        innerProof
+    return some ⟨newWidth, bvExpr, proof, expr⟩
+  | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
+    let some lhs ← ofOrAtom lhsExpr | return none
+    let some rhs ← ofOrAtom rhsExpr | return none
+    let bvExpr := .append lhs.bvExpr rhs.bvExpr
+    let expr := mkApp4 (mkConst ``BVExpr.append)
+      (toExpr lhs.width)
+      (toExpr rhs.width)
+      lhs.expr rhs.expr
+    let proof := do
+      let lhsEval ← mkEvalExpr lhs.width lhs.expr
+      let lhsProof ← lhs.evalsAtAtoms
+      let rhsProof ← rhs.evalsAtAtoms
+      let rhsEval ← mkEvalExpr rhs.width rhs.expr
+      return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
+        (toExpr lhs.width) (toExpr rhs.width)
+        lhsExpr lhsEval
+        rhsExpr rhsEval
+        lhsProof rhsProof
+    return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
+  | BitVec.replicate _ nExpr innerExpr =>
+    let some inner ← ofOrAtom innerExpr | return none
+    let some n ← getNatValue? nExpr | return ← ofAtom x
+    let bvExpr := .replicate n inner.bvExpr
+    let expr := mkApp3 (mkConst ``BVExpr.replicate)
+      (toExpr inner.width)
+      (toExpr n)
+      inner.expr
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
+        (toExpr n)
+        (toExpr inner.width)
+        innerExpr
+        innerEval
+        innerProof
+    return some ⟨inner.width * n, bvExpr, proof, expr⟩
+  | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
+    let some start ← getNatValue? startExpr | return ← ofAtom x
+    let some len ← getNatValue? lenExpr | return ← ofAtom x
+    let some inner ← ofOrAtom innerExpr | return none
+    let bvExpr := .extract start len inner.bvExpr
+    let expr := mkApp4 (mkConst ``BVExpr.extract)
+      (toExpr inner.width)
+      startExpr
+      lenExpr
+      inner.expr
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
         startExpr
         lenExpr
-        inner.expr
-      let proof := do
-        let innerEval ← mkEvalExpr inner.width inner.expr
-        let innerProof ← inner.evalsAtAtoms
-        return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
-          startExpr
-          lenExpr
-          (toExpr inner.width)
-          innerExpr
-          innerEval
-          innerProof
-      return some ⟨len, bvExpr, proof, expr⟩
-    | BitVec.rotateLeft _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
+        (toExpr inner.width)
         innerExpr
-        .rotateLeft
-        ``BVUnOp.rotateLeft
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
-    | BitVec.rotateRight _ innerExpr distanceExpr =>
-      rotateReflection
-        distanceExpr
-        innerExpr
-        .rotateRight
-        ``BVUnOp.rotateRight
-        ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | _ => return none
+        innerEval
+        innerProof
+    return some ⟨len, bvExpr, proof, expr⟩
+  | BitVec.rotateLeft _ innerExpr distanceExpr =>
+    rotateReflection
+      distanceExpr
+      innerExpr
+      .rotateLeft
+      ``BVUnOp.rotateLeft
+      ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
+  | BitVec.rotateRight _ innerExpr distanceExpr =>
+    rotateReflection
+      distanceExpr
+      innerExpr
+      .rotateRight
+      ``BVUnOp.rotateRight
+      ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
+  | _ => ofAtom x
+where
+  ofAtom (x : Expr) : M (Option ReifiedBVExpr) := do
+    let t ← instantiateMVars (← whnfR (← inferType x))
+    let_expr BitVec widthExpr := t | return none
+    let some width ← getNatValue? widthExpr | return none
+    let atom ← mkAtom x width
+    return some atom
 
-  /--
-  Reify `x` or abstract it as an atom.
-  Unless this function is called on something that is not a fixed-width `BitVec` it is always going
-  to return `some`.
-  -/
-  goOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do
-    let res ← go x
+  ofOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do
+    let res ← of x
     match res with
     | some exp => return some exp
-    | none => bitVecAtom x
+    | none => ofAtom x
 
   shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
+    let some inner ← ofOrAtom innerExpr | return none
     let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
     let expr :=
       mkApp3
@@ -296,22 +278,24 @@ where
   rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
       (rotateOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some distance ← getNatValue? distanceExpr | return none
+    -- Either the shift values are constant or we abstract the entire term as atoms
+    let some distance ← getNatValue? distanceExpr | return ← ofAtom x
     shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
 
   shiftConstReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some distance ← getNatOrBvValue? β distanceExpr | return none
+    -- Either the shift values are constant or we abstract the entire term as atoms
+    let some distance ← getNatOrBvValue? β distanceExpr | return ← ofAtom x
     shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
 
   shiftReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr)
       (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
       (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let_expr BitVec _ ← β | return none
-    let some inner ← goOrAtom innerExpr | return none
-    let some distance ← goOrAtom distanceExpr | return none
+    let_expr BitVec _ ← β | return ← ofAtom x
+    let some inner ← of innerExpr | return none
+    let some distance ← of distanceExpr | return none
     let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr
     let expr :=
       mkApp4
@@ -330,8 +314,8 @@ where
 
   binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
+    let some lhs ← ofOrAtom lhsExpr | return none
+    let some rhs ← ofOrAtom rhsExpr | return none
     if h : rhs.width = lhs.width then
       let bvExpr : BVExpr lhs.width := .bin lhs.bvExpr op (h ▸ rhs.bvExpr)
       let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
@@ -351,7 +335,7 @@ where
 
   unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
       M (Option ReifiedBVExpr) := do
-    let some inner ← goOrAtom innerExpr | return none
+    let some inner ← ofOrAtom innerExpr | return none
     let bvExpr := .un op inner.bvExpr
     let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
     let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
@@ -363,7 +347,7 @@ where
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← bitVecAtom x
+    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← ofAtom x
     let bvExpr : BVExpr width := .const bvVal
     let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr width) (toExpr bvVal)
     let proof := do

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

@@ -44,75 +44,40 @@ def mkTrans (x y z : Expr) (hxy hyz : Expr) : Expr :=
 def mkEvalExpr (expr : Expr) : M Expr := do
   return mkApp2 (mkConst ``BVLogicalExpr.eval) (← M.atomsAssignment) expr
 
-/--
-Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
--/
-def ofPred  (bvPred : ReifiedBVPred) : M (Option ReifiedBVLogical) := do
-  let boolExpr := .literal bvPred.bvPred
-  let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
-  let proof := bvPred.evalsAtAtoms
-  return some ⟨boolExpr, proof, expr⟩
-
-/--
-Construct an uninterrpeted `Bool` atom from `t`.
--/
-def boolAtom (t : Expr) : M (Option ReifiedBVLogical) := do
-  let some pred ← ReifiedBVPred.boolAtom t | return none
-  ofPred pred
-
-/--
-Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
-Unless this function is called on something that is not a `Bool` it is always going to return `some`.
--/
 partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
-  goOrAtom t
+  match_expr t with
+  | Bool.true =>
+    let boolExpr := .const true
+    let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true)
+    let proof := return mkRefl (mkConst ``Bool.true)
+    return some ⟨boolExpr, proof, expr⟩
+  | Bool.false =>
+    let boolExpr := .const false
+    let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
+    let proof := return mkRefl (mkConst ``Bool.false)
+    return some ⟨boolExpr, proof, expr⟩
+  | Bool.not subExpr =>
+    let some sub ← of subExpr | return none
+    let boolExpr := .not sub.bvExpr
+    let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
+    let proof := do
+      let subEvalExpr ← mkEvalExpr sub.expr
+      let subProof ← sub.evalsAtAtoms
+      return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
+    return some ⟨boolExpr, proof, expr⟩
+  | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
+  | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
+  | BEq.beq α _ lhsExpr rhsExpr =>
+    match_expr α with
+    | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
+    | BitVec _ => goPred t
+    | _ => return none
+  | _ => goPred t
 where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVLogical) := do
-    match_expr t with
-    | Bool.true =>
-      let boolExpr := .const true
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true)
-      let proof := pure <| mkRefl (mkConst ``Bool.true)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.false =>
-      let boolExpr := .const false
-      let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
-      let proof := pure <| mkRefl (mkConst ``Bool.false)
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.not subExpr =>
-      let some sub ← goOrAtom subExpr | return none
-      let boolExpr := .not sub.bvExpr
-      let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
-      let proof := do
-        let subEvalExpr ← mkEvalExpr sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
-      return some ⟨boolExpr, proof, expr⟩
-    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
-    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      match_expr α with
-      | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
-      | BitVec _ => goPred t
-      | _ => return none
-    | _ => goPred t
-
-  /--
-  Reify `t` or abstract it as an atom.
-  Unless this function is called on something that is not a `Bool` it is always going to return `some`.
-  -/
-  goOrAtom (t : Expr) : M (Option ReifiedBVLogical) := do
-    match ← go t with
-    | some boolExpr => return some boolExpr
-    | none => boolAtom t
-
   gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (congrThm : Name) :
       M (Option ReifiedBVLogical) := do
-    let some lhs ← goOrAtom lhsExpr | return none
-    let some rhs ← goOrAtom rhsExpr | return none
+    let some lhs ← of lhsExpr | return none
+    let some rhs ← of rhsExpr | return none
     let boolExpr := .gate  gate lhs.bvExpr rhs.bvExpr
     let expr :=
       mkApp4
@@ -134,8 +99,11 @@ where
     return some ⟨boolExpr, proof, expr⟩
 
   goPred (t : Expr) : M (Option ReifiedBVLogical) := do
-    let some pred ← ReifiedBVPred.of t | return none
-    ofPred pred
+    let some bvPred ← ReifiedBVPred.of t | return none
+    let boolExpr := .literal bvPred.bvPred
+    let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
+    let proof := bvPred.evalsAtAtoms
+    return some ⟨boolExpr, proof, expr⟩
 
 end ReifiedBVLogical
 

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

@@ -37,68 +37,54 @@ structure ReifiedBVPred where
 namespace ReifiedBVPred
 
 /--
-Construct an uninterpreted `Bool` atom from `t`.
+Reify an `Expr` that is a proof of a predicate about `BitVec`.
 -/
-def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
-  /-
-  Idea: we have t : Bool here, let's construct:
-    BitVec.ofBool t : BitVec 1
-  as an atom. Then construct the BVPred corresponding to
-    BitVec.getLsb (BitVec.ofBool t) 0 : Bool
-  We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
-  -/
-  let ty ← inferType t
-  let_expr Bool := ty | return none
-  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
-  let bvExpr : BVPred := .getLsbD atom.bvExpr 0
-  let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
-  let proof := do
-    let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
-    let atomProof ← atom.evalsAtAtoms
-    return mkApp3
-      (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
-      t
-      atomEval
-      atomProof
-  return some ⟨bvExpr, proof, expr⟩
-
-/--
-Reify an `Expr` that is a predicate about `BitVec`.
-Unless this function is called on something that is not a `Bool` it is always going to return `some`.
--/
-partial def of (t : Expr) : M (Option ReifiedBVPred) := do
-  match ← go t with
-  | some pred => return some pred
-  | none => boolAtom t
+def of (t : Expr) : M (Option ReifiedBVPred) := do
+  match_expr t with
+  | BEq.beq α _ lhsExpr rhsExpr =>
+    let_expr BitVec _ := α | return none
+    binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
+  | BitVec.ult _ lhsExpr rhsExpr =>
+    binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
+  | BitVec.getLsbD _ subExpr idxExpr =>
+    let some sub ← ReifiedBVExpr.of subExpr | return none
+    let some idx ← getNatValue? idxExpr | return none
+    let bvExpr : BVPred := .getLsbD sub.bvExpr idx
+    let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
+    let proof := do
+      let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
+      let subProof ← sub.evalsAtAtoms
+      return mkApp5
+        (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
+        idxExpr
+        (toExpr sub.width)
+        subExpr
+        subEval
+        subProof
+    return some ⟨bvExpr, proof, expr⟩
+  | _ =>
+    /-
+    Idea: we have t : Bool here, let's construct:
+      BitVec.ofBool t : BitVec 1
+    as an atom. Then construct the BVPred corresponding to
+      BitVec.getLsb (BitVec.ofBool t) 0 : Bool
+    We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
+    -/
+    let ty ← inferType t
+    let_expr Bool := ty | return none
+    let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
+    let bvExpr : BVPred := .getLsbD atom.bvExpr 0
+    let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
+    let proof := do
+      let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
+      let atomProof ← atom.evalsAtAtoms
+      return mkApp3
+        (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
+        t
+        atomEval
+        atomProof
+    return some ⟨bvExpr, proof, expr⟩
 where
-  /--
-  Reify `t`, returns `none` if the reification procedure failed.
-  -/
-  go (t : Expr) : M (Option ReifiedBVPred) := do
-    match_expr t with
-    | BEq.beq α _ lhsExpr rhsExpr =>
-      let_expr BitVec _ := α | return none
-      binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
-    | BitVec.ult _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
-    | BitVec.getLsbD _ subExpr idxExpr =>
-      let some sub ← ReifiedBVExpr.of subExpr | return none
-      let some idx ← getNatValue? idxExpr | return none
-      let bvExpr : BVPred := .getLsbD sub.bvExpr idx
-      let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
-      let proof := do
-        let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
-        let subProof ← sub.evalsAtAtoms
-        return mkApp5
-          (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
-          idxExpr
-          (toExpr sub.width)
-          subExpr
-          subEval
-          subProof
-      return some ⟨bvExpr, proof, expr⟩
-    | _ => return none
-
   binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (congrThm : Name) :
       M (Option ReifiedBVPred) := do
     let some lhs ← ReifiedBVExpr.of lhsExpr | return none

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -520,7 +520,7 @@ where
 
 @[builtin_tactic «case», builtin_incremental]
 def evalCase : Tactic
-  | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
+  | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
     -- disable incrementality if body is run multiple times
     Term.withoutTacticIncrementality (tag.size > 1) do
       for tag in tag, hs in hs do
@@ -528,20 +528,20 @@ def evalCase : Tactic
         let g ← renameInaccessibles g hs
         setGoals [g]
         g.setTag Name.anonymous
-        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <|
+        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext stx <|
           Term.withNarrowedArgTacticReuse (argIdx := 3) (evalTactic ·) stx
         setGoals gs
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic «case'»] def evalCase' : Tactic
-  | `(tactic| case'%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
+  | `(tactic| case' $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
     let mut acc := #[]
     for tag in tag, hs in hs do
       let (g, gs) ← getCaseGoals tag
       let g ← renameInaccessibles g hs
       let mvarTag ← g.getTag
       setGoals [g]
-      withCaseRef arr tac <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <| evalTactic tac
+      withCaseRef arr tac (evalTactic tac)
       let gs' ← getUnsolvedGoals
       if let [g'] := gs' then
         g'.setTag mvarTag

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

@@ -119,7 +119,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         let ids ← ids.mapIdxM fun i id =>
           match id.getNat with
           | 0 => throwErrorAt id "positive integer expected"
-          | n+1 => pure (n, i)
+          | n+1 => pure (n, i.1)
         let ids := ids.qsort (·.1 < ·.1)
         unless @Array.allDiff _ ⟨(·.1 == ·.1)⟩ ids do
           throwError "occurrence list is not distinct"

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

@@ -12,16 +12,13 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
   for declNameId in stx[1].getArgs do
-    withRef declNameId do
-      let e ← elabTermForApply declNameId (mayPostpone := false)
-      match e with
-      | .const declName _ =>
-        applySimpResult (← unfold (← getLhs) declName)
-      | .fvar declFVarId =>
-        unless ← declFVarId.isLetVar do
-          throwError "conv tactic 'unfold' failed, local variable '{Expr.fvar declFVarId}' has no definition"
-        let lhs ← instantiateMVars (← getLhs)
-        changeLhs (← Meta.zetaDeltaFVars lhs #[declFVarId])
-      | _ => throwError "conv tactic 'unfold' failed, expression {e} is not a global or local constant"
+    let e ← elabTermForApply declNameId (mayPostpone := false)
+    match e with
+    | .const declName _ =>
+      applySimpResult (← unfold (← getLhs) declName)
+    | .fvar declFVarId =>
+      let lhs ← instantiateMVars (← getLhs)
+      changeLhs (← Meta.zetaDeltaFVars lhs #[declFVarId])
+    | _ => throwErrorAt declNameId m!"'unfold' conv tactic failed, expression {e} is not a global or local constant"
 
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Ext.lean

@@ -123,7 +123,9 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
           levelParams := info.levelParams
         }
         modifyEnv fun env => addProtected env extName
-        addDeclarationRangesFromSyntax extName (← getRef)
+        Lean.addDeclarationRanges extName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
     catch e =>
       throwError m!"\
         Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
@@ -161,7 +163,9 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
         -- Only declarations in a namespace can be protected:
         unless extIffName.isAtomic do
           modifyEnv fun env => addProtected env extIffName
-        addDeclarationRangesFromSyntax extName (← getRef)
+        Lean.addDeclarationRanges extIffName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
     catch e =>
       throwError m!"\
         Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\

src/Lean/Elab/Tactic/Induction.lean

@@ -27,10 +27,8 @@ open Meta
   syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq)
   ```
 -/
-private def getAltLhses (alt : Syntax) : Syntax :=
-  alt[0]
 private def getFirstAltLhs (alt : Syntax) : Syntax :=
-  (getAltLhses alt)[0]
+  alt[0][0]
 /-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS` -/
 private def getAltName (alt : Syntax) : Name :=
   let lhs := getFirstAltLhs alt
@@ -72,9 +70,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic
       let goals ← getGoals
       try
         setGoals [mvarId]
-        closeUsingOrAdmit <|
-          withTacticInfoContext (mkNullNode #[getAltLhses alt, getAltDArrow alt]) <|
-            (addInfo *> evalTactic rhs)
+        closeUsingOrAdmit (withTacticInfoContext alt (addInfo *> evalTactic rhs))
       finally
         setGoals goals
 

src/Lean/Elab/Tactic/Unfold.lean

@@ -29,15 +29,13 @@ def zetaDeltaTarget (declFVarId : FVarId) : TacticM Unit := do
   for declNameId in stx[1].getArgs do
     go declNameId loc
 where
-  go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext <| withRef declNameId do
+  go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext do
     let e ← elabTermForApply declNameId (mayPostpone := false)
     match e with
     | .const declName _ =>
       withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
     | .fvar declFVarId =>
-      unless ← declFVarId.isLetVar do
-        throwError "tactic 'unfold' failed, local variable '{Expr.fvar declFVarId}' has no definition"
       withLocation loc (zetaDeltaLocalDecl declFVarId) (zetaDeltaTarget declFVarId) (throwTacticEx `unfold · m!"did not unfold '{e}'")
-    | _ => throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"
+    | _ => withRef declNameId <| throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"
 
 end Lean.Elab.Tactic

src/Lean/Elab/Term.lean

@@ -914,9 +914,7 @@ private def applyAttributesCore
   Remark: if the declaration has syntax errors, `declName` may be `.anonymous` see issue #4309
   In this case, we skip attribute application.
   -/
-  if declName == .anonymous then
-    return
-  withDeclName declName do
+  unless declName == .anonymous do
     for attr in attrs do
       withRef attr.stx do withLogging do
       let env ← getEnv

src/Lean/Language/Basic.lean

@@ -243,16 +243,11 @@ instance : ToSnapshotTree SnapshotLeaf where
 structure DynamicSnapshot where
   /-- Concrete snapshot value as `Dynamic`. -/
   val  : Dynamic
-  /--
-  Snapshot tree retrieved from `val` before erasure. We do thunk even the first level as accessing
-  it too early can create some unnecessary tasks from `toSnapshotTree` that are otherwise avoided by
-  `(sync := true)` when accessing only after elaboration has finished. Early access can even lead to
-  deadlocks when later forcing these unnecessary tasks on a starved thread pool.
-  -/
-  tree : Thunk SnapshotTree
+  /-- Snapshot tree retrieved from `val` before erasure. -/
+  tree : SnapshotTree
 
 instance : ToSnapshotTree DynamicSnapshot where
-  toSnapshotTree s := s.tree.get
+  toSnapshotTree s := s.tree
 
 /-- Creates a `DynamicSnapshot` from a typed snapshot value. -/
 def DynamicSnapshot.ofTyped [TypeName α] [ToSnapshotTree α] (val : α) : DynamicSnapshot where

src/Lean/Language/Lean.lean

@@ -300,9 +300,7 @@ General notes:
 * We must make sure to trigger `oldCancelTk?` as soon as discarding `old?`.
 * Control flow up to finding the last still-valid snapshot (which should be quick) is synchronous so
   as not to report this "fast forwarding" to the user as well as to make sure the next run sees all
-  fast-forwarded snapshots without having to wait on tasks. It also ensures this part cannot be
-  delayed by threadpool starvation. We track whether we are still on the fast-forwarding path using
-  the `sync` parameter on `parseCmd` and spawn an elaboration task when we leave it.
+  fast-forwarded snapshots without having to wait on tasks.
 -/
 partial def process
     (setupImports : Syntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
@@ -332,7 +330,7 @@ where
                 -- elaboration reuse
                 oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
                   let prom ← IO.Promise.new
-                  parseCmd oldCmd newParserState oldProcSuccess.cmdState prom (sync := true) ctx
+                  let _ ← IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState prom ctx)
                   return .pure {
                     diagnostics := oldProcessed.diagnostics
                     result? := some {
@@ -448,7 +446,7 @@ where
       let parserState := Runtime.markPersistent parserState
       let cmdState := Runtime.markPersistent cmdState
       let ctx := Runtime.markPersistent ctx
-      parseCmd none parserState cmdState prom (sync := true) ctx
+      let _ ← IO.asTask (parseCmd none parserState cmdState prom ctx)
       return {
         diagnostics
         infoTree? := cmdState.infoState.trees[0]!
@@ -459,10 +457,24 @@ where
       }
 
   parseCmd (old? : Option CommandParsedSnapshot) (parserState : Parser.ModuleParserState)
-      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) (sync : Bool) :
+      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) :
       LeanProcessingM Unit := do
     let ctx ← read
 
+    -- check for cancellation, most likely during elaboration of previous command, before starting
+    -- processing of next command
+    if (← ctx.newCancelTk.isSet) then
+      -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
+      -- (as no-one should look at this result in that case) but anything containing `Environment`
+      -- is not `Inhabited`
+      prom.resolve <| .mk (nextCmdSnap? := none) {
+        diagnostics := .empty, stx := .missing, parserState
+        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+        finishedSnap := .pure { diagnostics := .empty, cmdState }
+        tacticCache := (← IO.mkRef {})
+      }
+      return
+
     let unchanged old newParserState : BaseIO Unit :=
       -- when syntax is unchanged, reuse command processing task as is
       -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
@@ -470,11 +482,11 @@ where
       -- from `old`
       if let some oldNext := old.nextCmdSnap? then do
         let newProm ← IO.Promise.new
-        let _ ← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
+        let _ ← old.data.finishedSnap.bindIO fun oldFinished =>
           -- also wait on old command parse snapshot as parsing is cheap and may allow for
           -- elaboration reuse
           oldNext.bindIO (sync := true) fun oldNext => do
-            parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx
+            parseCmd oldNext newParserState oldFinished.cmdState newProm ctx
             return .pure ()
         prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result })
       else prom.resolve old  -- terminal command, we're done!
@@ -509,61 +521,44 @@ where
       if let some tk := ctx.oldCancelTk? then
         tk.set
 
-    -- check for cancellation, most likely during elaboration of previous command, before starting
-    -- processing of next command
-    if (← ctx.newCancelTk.isSet) then
-      -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
-      -- (as no-one should look at this result in that case) but anything containing `Environment`
-      -- is not `Inhabited`
-      prom.resolve <| .mk (nextCmdSnap? := none) {
-        diagnostics := .empty, stx := .missing, parserState
-        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
-        finishedSnap := .pure { diagnostics := .empty, cmdState }
-        tacticCache := (← IO.mkRef {})
-      }
-      return
+    -- definitely resolved in `doElab` task
+    let elabPromise ← IO.Promise.new
+    let finishedPromise ← IO.Promise.new
+    -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
+    -- retract the progress bar to a previous position in case the command support incremental
+    -- reporting but has significant work after resolving its last incremental promise, such as
+    -- final type checking; if it does not support incrementality, `elabSnap` constructed in
+    -- `parseCmd` and containing the entire range of the command will determine the reported
+    -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
+    -- irrelevant in this case.
+    let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
+    let finishedSnap := { range? := endRange?, task := finishedPromise.result }
+    let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
 
-    -- Start new task when leaving fast-forwarding path; see "General notes" above
-    let _ ← (if sync then BaseIO.asTask else (.pure <$> ·)) do
-      -- definitely resolved in `doElab` task
-      let elabPromise ← IO.Promise.new
-      let finishedPromise ← IO.Promise.new
-      -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
-      -- retract the progress bar to a previous position in case the command support incremental
-      -- reporting but has significant work after resolving its last incremental promise, such as
-      -- final type checking; if it does not support incrementality, `elabSnap` constructed in
-      -- `parseCmd` and containing the entire range of the command will determine the reported
-      -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
-      -- irrelevant in this case.
-      let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
-      let finishedSnap := { range? := endRange?, task := finishedPromise.result }
-      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
-
-      let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
-      let next? ← if Parser.isTerminalCommand stx then pure none
-        -- for now, wait on "command finished" snapshot before parsing next command
-        else some <$> IO.Promise.new
-      let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
-      let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
-        diagnostics
-        stx := .missing
-        parserState := {}
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
-        tacticCache
-      } else {
-        diagnostics, stx, parserState, tacticCache
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
-      }
-      prom.resolve <| .mk (nextCmdSnap? := next?.map
-        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
-      let cmdState ← doElab stx cmdState beginPos
-        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
-        finishedPromise tacticCache ctx
-      if let some next := next? then
-        -- We're definitely off the fast-forwarding path now
-        parseCmd none parserState cmdState next (sync := false) ctx
+    let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
+    let next? ← if Parser.isTerminalCommand stx then pure none
+      -- for now, wait on "command finished" snapshot before parsing next command
+      else some <$> IO.Promise.new
+    let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
+    let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
+      diagnostics
+      stx := .missing
+      parserState := {}
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap
+      tacticCache
+    } else {
+      diagnostics, stx, parserState, tacticCache
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap
+    }
+    prom.resolve <| .mk (nextCmdSnap? := next?.map
+      ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
+    let cmdState ← doElab stx cmdState beginPos
+      { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
+      finishedPromise tacticCache ctx
+    if let some next := next? then
+      parseCmd none parserState cmdState next ctx
 
   doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
       (snap : SnapshotBundle DynamicSnapshot) (finishedPromise : IO.Promise CommandFinishedSnapshot)
@@ -630,7 +625,7 @@ def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.Modul
     (old? : Option (Parser.InputContext × CommandParsedSnapshot) := none) :
     BaseIO (Task CommandParsedSnapshot) := do
   let prom ← IO.Promise.new
-  process.parseCmd (old?.map (·.2)) parserState commandState prom (sync := true)
+  process.parseCmd (old?.map (·.2)) parserState commandState prom
     |>.run (old?.map (·.1))
     |>.run { inputCtx with }
   return prom.result

src/Lean/LazyInitExtension.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.MonadEnv
+
+namespace Lean
+
+structure LazyInitExtension (m : Type → Type) (α : Type) where
+  ext : EnvExtension (Option α)
+  fn  : m α
+
+instance [Monad m] [Inhabited α] : Inhabited (LazyInitExtension m α) where
+  default := {
+    ext := default
+    fn  := pure default
+  }
+
+/--
+  Register an environment extension for storing the result of `fn`.
+  We initialize the extension with `none`, and `fn` is executed the
+  first time `LazyInit.get` is executed.
+
+  This kind of extension is useful for avoiding work duplication in
+  scenarios where a thunk cannot be used because the computation depends
+  on state from the `m` monad. For example, we may want to "cache" a collection
+  of theorems as a `SimpLemmas` object.  -/
+def registerLazyInitExtension (fn : m α) : IO (LazyInitExtension m α) := do
+  let ext ← registerEnvExtension (pure none)
+  return { ext, fn }
+
+def LazyInitExtension.get [MonadEnv m] [Monad m] (init : LazyInitExtension m α) : m α := do
+  match init.ext.getState (← getEnv) with
+  | some a => return a
+  | none   =>
+    let a ← init.fn
+    modifyEnv fun env => init.ext.setState env (some a)
+    return a
+
+end Lean

src/Lean/Linter/ConstructorAsVariable.lean

@@ -37,7 +37,7 @@ def constructorNameAsVariable : Linter where
     let warnings : IO.Ref (Std.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
 
     for tree in infoTrees do
-      tree.visitM' (postNode := fun ci info _ => do
+      tree.visitM' (preNode := fun ci info _ => do
         match info with
         | .ofTermInfo ti =>
           match ti.expr with

src/Lean/Linter/UnusedVariables.lean

@@ -10,55 +10,41 @@ set_option linter.missingDocs true -- keep it documented
 
 /-! # Unused variable Linter
 
-This file implements the unused variable linter, which runs automatically on all
-commands and reports any local variables that are never referred to, using
-information from the info tree.
+This file implements the unused variable linter, which runs automatically on all commands
+and reports any local variables that are never referred to, using information from the info tree.
 
-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`: 
+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".
+For example, we would like this to be considered a use of `x`:
 ```
 def foo (x : Nat) : Nat := by assumption
 ```
 
-The final proof term is `fun x => x` so clearly `x` was used, but we can't make
-use of this because the final proof term is after we have abstracted over the
-original `fvar` for `x`. Instead, we make sure to store the proof term before
-abstraction but after instantiation of mvars in the info tree and retrieve it in
-the linter. Using the instantiated term is very important as redoing that step
-in the linter can be prohibitively expensive. The downside of special-casing the
-definition body in this way is that while it works for parameters, it does not
-work for local variables in the body, so we ignore them by default if any tactic
-infos are present (`linter.unusedVariables.analyzeTactics`).
+The final proof term is `fun x => x` so clearly `x` was used, but we can't make use of this because
+the final proof term is after we have abstracted over the original `fvar` for `x`. If we look
+further into the tactic state we can see the `fvar` show up in the instantiation to the original
+goal metavariable `?m : Nat := x`, but it is not always the case that we can follow metavariable
+instantiations to determine what happened after the fact, because tactics might skip the goal
+metavariable and instantiate some other metavariable created prior to it instead.
 
-If we do turn on this option and look further into the tactic state, we can see
-the `fvar` show up in the instantiation to the original goal metavariable
-`?m : Nat := x`, but it is not always the case that we can follow metavariable
-instantiations to determine what happened after the fact, because tactics might
-skip the goal metavariable and instantiate some other metavariable created prior
-to it instead.  Instead, we use a (much more expensive) overapproximation, which
-is just to look through the entire metavariable context looking for occurrences
-of `x`. We use caching to ensure that this is still linear in the size of the
-info tree, even though there are many metavariable contexts in all the
-intermediate stages of elaboration; these are highly similar and make use of
-`PersistentHashMap` so there is a lot of subterm sharing we can take advantage
-of.
+Instead, we use a (much more expensive) overapproximation, which is just to look through the entire
+metavariable context looking for occurrences of `x`. We use caching to ensure that this is still
+linear in the size of the info tree, even though there are many metavariable contexts in all the
+intermediate stages of elaboration; these are highly similar and make use of `PersistentHashMap`
+so there is a lot of subterm sharing we can take advantage of.
 
 ## The `@[unused_variables_ignore_fn]` attribute
 
-Some occurrences of variables are deliberately unused, or at least we don't want
-to lint on unused variables in these positions. For example:
+Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused
+variables in these positions. For example:
 
 ```
 def foo (x : Nat) : (y : Nat) → Nat := fun _ => x
                   -- ^ don't lint this unused variable because it is public API
 ```
 
-They are generally a syntactic criterion, so we allow adding custom
-`IgnoreFunction`s so that external syntax can also opt in to lint suppression,
-like so:
+They are generally a syntactic criterion, so we allow adding custom `IgnoreFunction`s so that
+external syntax can also opt in to lint suppression, like so:
 
 ```
 macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)
@@ -91,17 +77,6 @@ register_builtin_option linter.unusedVariables.patternVars : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter to mark unused pattern variables"
 }
-/-- Enables linting variables defined in tactic blocks, may be expensive for complex proofs -/
-register_builtin_option linter.unusedVariables.analyzeTactics : Bool := {
-  defValue := false
-  descr := "enable analysis of local variables in presence of tactic proofs\
-          \n\
-          \nBy default, the linter will limit itself to linting a declaration's parameters \
-            whenever tactic proofs are present as these can be expensive to analyze. Enabling this \
-            option extends linting to local variables both inside and outside tactic proofs, \
-            though it can also lead to some false negatives as intermediate tactic states may \
-            reference some variables without the declaration ultimately depending on them."
-}
 
 /-- Gets the status of `linter.unusedVariables` -/
 def getLinterUnusedVariables (o : Options) : Bool :=
@@ -381,82 +356,55 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
-    StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
+def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+    StateRefT References IO Unit := do
+  for tree in infoTrees do
+    tree.visitM' (preNode := fun ci info _ => do
+      match info with
+      | .ofTermInfo ti =>
+        match ti.expr with
+        | .const .. =>
+          if ti.isBinder then
+            let some range := info.range? | return
+            let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
+            modify fun s => { s with constDecls := s.constDecls.insert range }
+        | .fvar id .. =>
+          let some range := info.range? | return
+          let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
+          if ti.isBinder then
+            -- This is a local variable declaration.
+            let some ldecl := ti.lctx.find? id | return
+            -- Skip declarations which are outside the command syntax range, like `variable`s
+            -- (it would be confusing to lint these), or those which are macro-generated
+            if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
+            let opts := ci.options
+            -- we have to check for the option again here because it can be set locally
+            if !getLinterUnusedVariables opts then return
+            let stx := skipDeclIdIfPresent info.stx
+            if let .str _ s := stx.getId then
+              -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
+              -- This is the suggested way to silence the warning
+              if s.startsWith "_" then return
+            -- Record this either as a new `fvarDefs`, or an alias of an existing one
+            modify fun s =>
+              if let some ref := s.fvarDefs[range]? then
+                { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
+              else
+                { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+          else
+            -- Found a direct use, keep track of it
+            modify fun s => { s with fvarUses := s.fvarUses.insert id }
+        | _ => pure ()
+      | .ofTacticInfo ti =>
+        -- Keep track of the `MetavarContext` after a tactic for later
+        modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
+      | .ofFVarAliasInfo i =>
+        -- 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 ())
 where
-  go infoTrees ctx? := do
-    for tree in infoTrees do
-      tree.visitM' (ctx? := ctx?) (preNode := fun ci info children => do
-        -- set if `analyzeTactics` is unset, tactic infos are present, and we're inside the body
-        let ignored ← read
-        match info with
-        | .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 .. =>
-            if ti.isBinder then
-              let some range := info.range? | return true
-              let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
-              modify fun s => { s with constDecls := s.constDecls.insert range }
-          | .fvar id .. =>
-            let some range := info.range? | return true
-            let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
-            if ti.isBinder then
-              -- This is a local variable declaration.
-              if ignored then return true
-              let some ldecl := ti.lctx.find? id | return true
-              -- Skip declarations which are outside the command syntax range, like `variable`s
-              -- (it would be confusing to lint these), or those which are macro-generated
-              if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
-              let opts := ci.options
-              -- we have to check for the option again here because it can be set locally
-              if !getLinterUnusedVariables opts then return true
-              let stx := skipDeclIdIfPresent info.stx
-              if let .str _ s := stx.getId then
-                -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
-                -- This is the suggested way to silence the warning
-                if s.startsWith "_" then return true
-              -- Record this either as a new `fvarDefs`, or an alias of an existing one
-              modify fun s =>
-                if let some ref := s.fvarDefs[range]? then
-                  { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
-                else
-                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
-            else
-              -- 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 }
-          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 :=
@@ -545,7 +493,7 @@ def unusedVariables : Linter where
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
         -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
-        fvarUsesRef.modify fun fvarUses => fvarUses.toArray.map getCanonVar |> .insertMany {}
+        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now

src/Lean/Meta/AppBuilder.lean

@@ -28,7 +28,6 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
 /--
 `mkLetFun x v e` creates the encoding for the `let_fun x := v; e` expression.
 The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
-NB: `x` must not be a let-bound free variable.
 -/
 def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
   let f ← mkLambdaFVars #[x] e

src/Lean/Meta/IndPredBelow.lean

@@ -54,7 +54,7 @@ def mkContext (declName : Name) : MetaM Context := do
   let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
   let motiveTypes ← typeInfos.mapM motiveType
   let motives ← motiveTypes.mapIdxM fun j motive =>
-    return (← motiveName motiveTypes j, motive)
+    return (← motiveName motiveTypes j.val, motive)
   let headers ← typeInfos.mapM $ mkHeader motives indVal.numParams
   return {
     motives := motives
@@ -214,7 +214,7 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor :=
 
 def mkInductiveType
     (ctx : Context)
-    (i : Nat)
+    (i : Fin ctx.typeInfos.size)
     (indVal : InductiveVal) : MetaM InductiveType := do
   return {
     name := ctx.belowNames[i]!
@@ -340,11 +340,11 @@ where
   mkIH
       (params : Array Expr)
       (motives : Array Expr)
-      (idx : Nat)
+      (idx : Fin ctx.motives.size)
       (motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do
     let name :=
       if ctx.motives.size > 1
-      then mkFreshUserName <| .mkSimple s!"ih_{idx + 1}"
+      then mkFreshUserName <| .mkSimple s!"ih_{idx.val.succ}"
       else mkFreshUserName <| .mkSimple "ih"
     let ih ← instantiateForall motive.2 params
     let mkDomain (_ : Array Expr) : MetaM Expr :=
@@ -353,7 +353,7 @@ where
         let args := params ++ motives ++ ys
         let premise :=
           mkAppN
-            (mkConst ctx.belowNames[idx]! levels) args
+            (mkConst ctx.belowNames[idx.val]! levels) args
         let conclusion :=
           mkAppN motives[idx]! ys
         mkForallFVars ys (←mkArrow premise conclusion)

src/Lean/Meta/InferType.lean

@@ -441,8 +441,6 @@ This can be used to infer the expected type of the alternatives when constructin
 -/
 def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do
   forallBoundedTelescope type n fun xs _ => do
-    unless xs.size = n do
-      throwError "type {type} does not have {n} parameters"
     let types ← xs.mapM (inferType ·)
     for t in types do
       if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then

src/Lean/Meta/LitValues.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Basic
-import Init.Control.Option
 
 namespace Lean.Meta
 

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -70,7 +70,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
       let subst  := subgoal.subst
       let mvarId := subgoal.mvarId
       let hEqSz  := (subst.get hEq).fvarId!
-      if h : i < sizes.size then
+      if h : i.val < sizes.size then
          let n := sizes.get ⟨i, h⟩
          let mvarId ← mvarId.clear subgoal.newHs[0]!
          let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId!

src/Lean/Meta/Match/Match.lean

@@ -545,7 +545,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
   let subgoals ← caseValues p.mvarId x.fvarId! values (substNewEqs := true)
   subgoals.mapIdxM fun i subgoal => do
     trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
-    if h : i < values.size then
+    if h : i.val < values.size then
       let value := values.get ⟨i, h⟩
       -- (x = value) branch
       let subst := subgoal.subst
@@ -599,7 +599,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
   let sizes := collectArraySizes p
   let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
   subgoals.mapIdxM fun i subgoal => do
-    if i < sizes.size then
+    if i.val < sizes.size then
       let size     := sizes.get! i
       let subst    := subgoal.subst
       let elems    := subgoal.elems.toList

src/Lean/Meta/Offset.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Control.Option
 import Lean.Data.LBool
 import Lean.Meta.InferType
 import Lean.Meta.NatInstTesters

src/Lean/Meta/Tactic/FunInd.lean

@@ -262,8 +262,8 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
     if let some (n, t, v, b) := e.letFun? then
       let t' ← foldAndCollect oldIH newIH isRecCall t
       let v' ← foldAndCollect oldIH newIH isRecCall v
-      return ← withLocalDeclD n t' fun x => do
-        M.localMapM (mkLetFun x v' ·) do
+      return ← withLetDecl n t' v' fun x => do
+        M.localMapM (mkLetFVars (usedLetOnly := true) #[x] ·) do
           let b' ← foldAndCollect oldIH newIH isRecCall (b.instantiate1 x)
           mkLetFun x v' b'
 
@@ -598,11 +598,6 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
           buildInductionBody toClear expAltType oldIH newIH isRecCall alt)
       return matcherApp'.toExpr
 
-  -- we look through mdata
-  if e.isMData then
-    let b ← buildInductionBody toClear goal oldIH newIH isRecCall e.mdataExpr!
-    return e.updateMData! b
-
   if let .letE n t v b _ := e then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
@@ -613,7 +608,7 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
   if let some (n, t, v, b) := e.letFun? then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
-    return ← withLocalDeclD n t' fun x => M2.branch do
+    return ← withLocalDecl n .default t' fun x => M2.branch do
       let b' ← buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFun x v' b'
 
@@ -648,7 +643,7 @@ def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : M
       pure mvar
   trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}"
   let decls := mvars.mapIdx fun i mvar =>
-    (.mkSimple s!"case{i+1}", (fun _ => mvar.getType))
+    (.mkSimple s!"case{i.val+1}", (fun _ => mvar.getType))
   Meta.withLocalDeclsD decls fun xs => do
       for mvar in mvars, x in xs do
         mvar.assign x
@@ -976,7 +971,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
             mkForallFVars ys (.sort levelZero)
         let motiveArities ← infos.mapM fun info => do
           lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
-        let motiveDecls ← motiveTypes.mapIdxM fun i motiveType => do
+        let motiveDecls ← motiveTypes.mapIdxM fun ⟨i,_⟩ motiveType => do
           let n := if infos.size = 1 then .mkSimple "motive"
                                      else .mkSimple s!"motive_{i+1}"
           pure (n, fun _ => pure motiveType)

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -36,8 +36,8 @@ abbrev Assignment.get? (a : Assignment) (x : Var) : Option Rat :=
 abbrev Assignment.push (a : Assignment) (v : Rat) : Assignment :=
   { a with val := a.val.push v }
 
-abbrev Assignment.take (a : Assignment) (newSize : Nat) : Assignment :=
-  { a with val := a.val.take newSize }
+abbrev Assignment.shrink (a : Assignment) (newSize : Nat) : Assignment :=
+  { a with val := a.val.shrink newSize }
 
 structure Poly where
   val : Array (Int × Var)
@@ -242,7 +242,7 @@ def resolve (s : State) (cl : Cnstr) (cu : Cnstr) : Sum Result State :=
     let maxVarIdx := c.lhs.getMaxVar.id
     match s with -- Hack: we avoid { s with ... } to make sure we get a destructive update
     | { lowers, uppers, int, assignment, } =>
-      let assignment := assignment.take maxVarIdx
+      let assignment := assignment.shrink maxVarIdx
       if c.lhs.getMaxVarCoeff < 0 then
         let lowers := lowers.modify maxVarIdx (·.push c)
         Sum.inr { lowers, uppers, int, assignment }

src/Lean/Meta/Tactic/SplitIf.lean

@@ -4,26 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.LazyInitExtension
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 namespace SplitIf
 
+builtin_initialize ext : LazyInitExtension MetaM Simp.Context ←
+  registerLazyInitExtension do
+    let mut s : SimpTheorems := {}
+    s ← s.addConst ``if_pos
+    s ← s.addConst ``if_neg
+    s ← s.addConst ``dif_pos
+    s ← s.addConst ``dif_neg
+    return {
+      simpTheorems  := #[s]
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := { Simp.neutralConfig with dsimp := false }
+    }
+
 /--
   Default `Simp.Context` for `simpIf` methods. It contains all congruence theorems, but
   just the rewriting rules for reducing `if` expressions. -/
-def getSimpContext : MetaM Simp.Context := do
-  let mut s : SimpTheorems := {}
-  s ← s.addConst ``if_pos
-  s ← s.addConst ``if_neg
-  s ← s.addConst ``dif_pos
-  s ← s.addConst ``dif_neg
-  return {
-    simpTheorems  := #[s]
-    congrTheorems := (← getSimpCongrTheorems)
-    config        := { Simp.neutralConfig with dsimp := false }
-  }
+def getSimpContext : MetaM Simp.Context :=
+  ext.get
 
 /--
   Default `discharge?` function for `simpIf` methods.