fix test

.github/ISSUE_TEMPLATE/bug_report.md

@@ -39,7 +39,7 @@ Please put an X between the brackets as you perform the following steps:
 
 ### Versions
 
-[Output of `#version` or `#eval Lean.versionString`]
+[Output of `#eval Lean.versionString`]
 [OS version, if not using live.lean-lang.org.]
 
 ### Additional Information

.github/workflows/ci.yml

@@ -217,7 +217,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "msys2 {0}",
-                "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
+                "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
                 // for reasons unknown, interactivetests are flaky on Windows
                 "CTEST_OPTIONS": "--repeat until-pass:2",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -227,7 +227,7 @@ jobs:
               {
                 "name": "Linux aarch64",
                 "os": "nscloud-ubuntu-22.04-arm64-4x8",
-                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
+                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",

RELEASES.md

@@ -8,21 +8,6 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.15.0
-----------
-
-Development in progress.
-
-v4.14.0
-----------
-
-Release candidate, release notes will be copied from the branch `releases/v4.14.0` once completed.
-
-v4.13.0
-----------
-
-Release candidate, release notes will be copied from the branch `releases/v4.13.0` once completed.
-
 v4.12.0
 ----------
 

doc/monads/applicatives.lean

@@ -138,8 +138,8 @@ definition:
 
 -/
 instance : Applicative List where
-  pure := List.singleton
-  seq f x := List.flatMap f fun y => Functor.map y (x ())
+  pure := List.pure
+  seq f x := List.bind f fun y => Functor.map y (x ())
 /-!
 
 Notice you can now sequence a _list_ of functions and a _list_ of items.

doc/monads/laws.lean

@@ -128,8 +128,8 @@ Applying the identity function through an applicative structure should not chang
 values or structure.  For example:
 -/
 instance : Applicative List where
-  pure := List.singleton
-  seq f x := List.flatMap f fun y => Functor.map y (x ())
+  pure := List.pure
+  seq f x := List.bind f fun y => Functor.map y (x ())
 
 #eval pure id <*> [1, 2, 3]  -- [1, 2, 3]
 /-!
@@ -235,8 +235,8 @@ structure or its values.
 Left identity is `x >>= pure = x` and is demonstrated by the following examples on a monadic `List`:
 -/
 instance : Monad List  where
-  pure := List.singleton
-  bind := List.flatMap
+  pure := List.pure
+  bind := List.bind
 
 def a := ["apple", "orange"]
 

doc/monads/monads.lean

@@ -192,8 +192,8 @@ implementation of `pure` and `bind`.
 
 -/
 instance : Monad List  where
-  pure := List.singleton
-  bind := List.flatMap
+  pure := List.pure
+  bind := List.bind
 /-!
 
 Like you saw with the applicative `seq` operator, the `bind` operator applies the given function

flake.nix

@@ -38,11 +38,7 @@
           # more convenient `ctest` output
           CTEST_OUTPUT_ON_FAILURE = 1;
         } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-          GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
-            pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
-              # would need additional linking setup on Linux aarch64, we don't use it anywhere else either
-              hardeningDisable = [ "stackprotector" ];
-            });
+          GMP = pkgsDist.gmp.override { withStatic = true; };
           LIBUV = pkgsDist.libuv.overrideAttrs (attrs: {
             configureFlags = ["--enable-static"];
             hardeningDisable = [ "stackprotector" ];

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 15)
+set(LEAN_VERSION_MINOR 12)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -155,10 +155,6 @@ endif ()
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
 string(APPEND LEANC_EXTRA_FLAGS " -fstack-clash-protection")
 
-# This makes signed integer overflow guaranteed to match 2's complement.
-string(APPEND CMAKE_CXX_FLAGS " -fwrapv")
-string(APPEND LEANC_EXTRA_FLAGS " -fwrapv")
-
 if(NOT MULTI_THREAD)
   message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
   set(AUTO_THREAD_FINALIZATION OFF)

src/Init.lean

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

src/Init/Control/Basic.lean

@@ -11,13 +11,8 @@ universe u v w
 /--
 A `ForIn'` instance, which handles `for h : x in c do`,
 can also handle `for x in x do` by ignoring `h`, and so provides a `ForIn` instance.
-
-Note that this instance will cause a potentially non-defeq duplication if both `ForIn` and `ForIn'`
-instances are provided for the same type.
 -/
--- We set the priority to 500 so it is below the default,
--- but still above the low priority instance from `Stream`.
-instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
+instance (priority := low) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
   forIn x b f := forIn' x b fun a _ => f a
 
 @[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
@@ -35,15 +30,6 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [h]
   rfl
 
-/-- Extract the value from a `ForInStep`, ignoring whether it is `done` or `yield`. -/
-def ForInStep.value (x : ForInStep α) : α :=
-  match x with
-  | ForInStep.done b => b
-  | ForInStep.yield b => b
-
-@[simp] theorem ForInStep.value_done (b : β) : (ForInStep.done b).value = b := rfl
-@[simp] theorem ForInStep.value_yield (b : β) : (ForInStep.yield b).value = b := rfl
-
 @[reducible]
 def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β :=
   fun a f => f <$> a

src/Init/Conv.lean

@@ -7,7 +7,6 @@ Notation for operators defined at Prelude.lean
 -/
 prelude
 import Init.Tactics
-import Init.Meta
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -47,20 +46,12 @@ scoped syntax (name := withAnnotateState)
 /-- `skip` does nothing. -/
 syntax (name := skip) "skip" : conv
 
-/--
-Traverses into the left subterm of a binary operator.
-
-In general, for an `n`-ary operator, it traverses into the second to last argument.
-It is a synonym for `arg -2`.
--/
+/-- Traverses into the left subterm of a binary operator.
+(In general, for an `n`-ary operator, it traverses into the second to last argument.) -/
 syntax (name := lhs) "lhs" : conv
 
-/--
-Traverses into the right subterm of a binary operator.
-
-In general, for an `n`-ary operator, it traverses into the last argument.
-It is a synonym for `arg -1`.
--/
+/-- Traverses into the right subterm of a binary operator.
+(In general, for an `n`-ary operator, it traverses into the last argument.) -/
 syntax (name := rhs) "rhs" : conv
 
 /-- Traverses into the function of a (unary) function application.
@@ -83,17 +74,13 @@ subgoals for all the function arguments. For example, if the target is `f x y` t
 `congr` produces two subgoals, one for `x` and one for `y`. -/
 syntax (name := congr) "congr" : conv
 
-syntax argArg := "@"? "-"? num
-
 /--
 * `arg i` traverses into the `i`'th argument of the target. For example if the
   target is `f a b c d` then `arg 1` traverses to `a` and `arg 3` traverses to `c`.
-  The index may be negative; `arg -1` traverses into the last argument,
-  `arg -2` into the second-to-last argument, and so on.
 * `arg @i` is the same as `arg i` but it counts all arguments instead of just the
   explicit arguments.
 * `arg 0` traverses into the function. If the target is `f a b c d`, `arg 0` traverses into `f`. -/
-syntax (name := arg) "arg " argArg : conv
+syntax (name := arg) "arg " "@"? num : conv
 
 /-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)
 to target `e`, introducing name `x` in the process. -/
@@ -143,11 +130,11 @@ For example, if we are searching for `f _` in `f (f a) = f b`:
 syntax (name := pattern) "pattern " (occs)? term : conv
 
 /-- `rw [thm]` rewrites the target using `thm`. See the `rw` tactic for more information. -/
-syntax (name := rewrite) "rewrite" optConfig rwRuleSeq : conv
+syntax (name := rewrite) "rewrite" (config)? rwRuleSeq : conv
 
 /-- `simp [thm]` performs simplification using `thm` and marked `@[simp]` lemmas.
 See the `simp` tactic for more information. -/
-syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
+syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
 
 /--
@@ -164,7 +151,7 @@ example (a : Nat): (0 + 0) = a - a := by
     rw [← Nat.sub_self a]
 ```
 -/
-syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
+syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
 
 /-- `simp_match` simplifies match expressions. For example,
@@ -260,12 +247,12 @@ macro (name := failIfSuccess) tk:"fail_if_success " s:convSeq : conv =>
 
 /-- `rw [rules]` applies the given list of rewrite rules to the target.
 See the `rw` tactic for more information. -/
-macro "rw" c:optConfig s:rwRuleSeq : conv => `(conv| rewrite $c:optConfig $s)
+macro "rw" c:(config)? s:rwRuleSeq : conv => `(conv| rewrite $[$c]? $s)
 
-/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
+/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
 This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
 which only unfolds `@[reducible]` definitions). -/
-macro "erw" c:optConfig s:rwRuleSeq : conv => `(conv| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq)
+macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s)
 
 /-- `args` traverses into all arguments. Synonym for `congr`. -/
 macro "args" : conv => `(conv| congr)
@@ -276,7 +263,7 @@ macro "right" : conv => `(conv| rhs)
 /-- `intro` traverses into binders. Synonym for `ext`. -/
 macro "intro" xs:(ppSpace colGt ident)* : conv => `(conv| ext $xs*)
 
-syntax enterArg := ident <|> argArg
+syntax enterArg := ident <|> ("@"? num)
 
 /-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
 It is a shorthand for other conv tactics as follows:
@@ -285,7 +272,12 @@ It is a shorthand for other conv tactics as follows:
 * `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.
 For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]`
 will traverse to the subterm `b`. -/
-syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv
+syntax "enter" " [" withoutPosition(enterArg,+) "]" : conv
+macro_rules
+  | `(conv| enter [$i:num]) => `(conv| arg $i)
+  | `(conv| enter [@$i]) => `(conv| arg @$i)
+  | `(conv| enter [$id:ident]) => `(conv| ext $id)
+  | `(conv| enter [$arg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
 
 /-- The `apply thm` conv tactic is the same as `apply thm` the tactic.
 There are no restrictions on `thm`, but strange results may occur if `thm`

src/Init/Data.lean

@@ -19,7 +19,6 @@ import Init.Data.ByteArray
 import Init.Data.FloatArray
 import Init.Data.Fin
 import Init.Data.UInt
-import Init.Data.SInt
 import Init.Data.Float
 import Init.Data.Option
 import Init.Data.Ord

src/Init/Data/Array.lean

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

src/Init/Data/Array/Basic.lean

@@ -12,7 +12,6 @@ import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
 import Init.Data.List.ToArray
-import Init.Data.Array.Set
 universe u v w
 
 /-! ### Array literal syntax -/
@@ -26,12 +25,11 @@ variable {α : Type u}
 
 namespace Array
 
-@[deprecated toList (since := "2024-10-13")] abbrev data := @toList
+@[deprecated size (since := "2024-10-13")] abbrev data := @toList
 
 /-! ### Preliminary theorems -/
 
-@[simp] theorem size_set (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    (set a i v h).size = a.size :=
+@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
   List.length_set ..
 
 @[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@@ -143,7 +141,7 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
    `fset` may be slightly slower than `uset`. -/
 @[extern "lean_array_uset"]
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
-  a.set i.toNat v h
+  a.set ⟨i.toNat, h⟩ v
 
 @[extern "lean_array_pop"]
 def pop (a : Array α) : Array α where
@@ -169,10 +167,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let v₁ := a.get i
   let v₂ := a.get j
   let a'  := a.set i v₂
-  a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
+  a'.set (size_set a i v₂ ▸ j) v₁
 
 @[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set j (a.get i) (Nat.lt_of_lt_of_eq j.isLt (size_set a i (a.get j) _).symm)).size = a.size
+  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
   rw [size_set, size_set]
 
 /--
@@ -237,11 +235,9 @@ def range (n : Nat) : Array Nat :=
 def singleton (v : α) : Array α :=
   mkArray 1 v
 
-def back! [Inhabited α] (a : Array α) : α :=
+def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 
-@[deprecated back! (since := "2024-10-31")] abbrev back := @back!
-
 def get? (a : Array α) (i : Nat) : Option α :=
   if h : i < a.size then some a[i] else none
 
@@ -280,7 +276,7 @@ unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) :
     -- of the element type, and that it is valid to store `box(0)` in any array.
     let a'               := a.set idx (unsafeCast ())
     let v ← f v
-    pure <| a'.set idx v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
+    pure <| a'.set (size_set a .. ▸ idx) v
   else
     pure a
 
@@ -306,6 +302,37 @@ def modifyOp (self : Array α) (idx : Nat) (f : α → α) : Array α :=
   We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
 
   This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/
+@[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
+  let sz := as.usize
+  let rec @[specialize] loop (i : USize) (b : β) : m β := do
+    if i < sz then
+      let a := as.uget i lcProof
+      match (← f a b) with
+      | ForInStep.done  b => pure b
+      | ForInStep.yield b => loop (i+1) b
+    else
+      pure b
+  loop 0 b
+
+/-- Reference implementation for `forIn` -/
+@[implemented_by Array.forInUnsafe]
+protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
+  let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
+    match i, h with
+    | 0,   _ => pure b
+    | i+1, h =>
+      have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
+      have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
+      have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
+      match (← f as[as.size - 1 - i] b) with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop i (Nat.le_of_lt h') b
+  loop as.size (Nat.le_refl _) b
+
+instance : ForIn m (Array α) α where
+  forIn := Array.forIn
+
+/-- See comment at `forInUnsafe` -/
 @[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
   let sz := as.usize
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -336,9 +363,7 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
 instance : ForIn' m (Array α) α inferInstance where
   forIn' := Array.forIn'
 
--- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
-
-/-- See comment at `forIn'Unsafe` -/
+/-- See comment at `forInUnsafe` -/
 @[inline]
 unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β :=
   let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do
@@ -373,7 +398,7 @@ def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     fold as.size (Nat.le_refl _)
 
-/-- See comment at `forIn'Unsafe` -/
+/-- See comment at `forInUnsafe` -/
 @[inline]
 unsafe def foldrMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start := as.size) (stop := 0) : m β :=
   let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do
@@ -412,7 +437,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   else
     pure init
 
-/-- See comment at `forIn'Unsafe` -/
+/-- See comment at `forInUnsafe` -/
 @[inline]
 unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   let sz := as.usize
@@ -667,7 +692,7 @@ instance : HAppend (Array α) (List α) (Array α) := ⟨Array.appendList⟩
 def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
   as.foldlM (init := empty) fun bs a => do return bs ++ (← f a)
 
-@[deprecated flatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
+@[deprecated concatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
 
 @[inline]
 def flatMap (f : α → Array β) (as : Array α) : Array β :=

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

@@ -69,8 +69,8 @@ namespace Array
   if as.isEmpty then do let v ← add (); pure <| as.push v
   else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertAt! 0 v
   else if !lt (as.get! 0) k then as.modifyM 0 <| merge
-  else if lt as.back! k then do let v ← add (); pure <| as.push v
-  else if !lt k as.back! then as.modifyM (as.size - 1) <| merge
+  else if lt as.back k then do let v ← add (); pure <| as.push v
+  else if !lt k as.back then as.modifyM (as.size - 1) <| merge
   else binInsertAux lt merge add as k 0 (as.size - 1)
 
 @[inline] def binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α :=

src/Init/Data/Array/Bootstrap.lean

@@ -23,7 +23,7 @@ theorem foldlM_eq_foldlM_toList.aux [Monad m]
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
-    rw (occs := .pos [2]) [← List.get_drop_eq_drop _ _ ‹_›]
+    rw (config := {occs := .pos [2]}) [← List.get_drop_eq_drop _ _ ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 

src/Init/Data/Array/DecidableEq.lean

@@ -13,9 +13,9 @@ import Init.ByCases
 namespace Array
 
 theorem rel_of_isEqvAux
-    {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
+    (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
     (heqv : Array.isEqvAux a b hsz r i hi)
-    {j : Nat} (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))) := by
+    (j : Nat) (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))) := by
   induction i with
   | zero => contradiction
   | succ i ih =>
@@ -28,7 +28,7 @@ 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)
+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]
@@ -36,18 +36,18 @@ theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size
     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 α} :
+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]
   split <;> rename_i h
-  · exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩
+  · 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, fun ⟨h, w⟩ => by
+  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
     simp only [isEqv, ← h, ↓reduceDIte]
-    exact isEqvAux_of_rel h (by simp [h]) w⟩
+    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 =
@@ -67,7 +67,7 @@ theorem isEqv_eq_decide (a b : Array α) (r) :
   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 h
+  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)
 
 theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :

src/Init/Data/Array/Lemmas.lean

@@ -10,10 +10,7 @@ import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
-import Init.Data.List.Monadic
-import Init.Data.List.OfFn
 import Init.Data.Array.Mem
-import Init.Data.Array.DecidableEq
 import Init.TacticsExtra
 
 /-!
@@ -72,9 +69,6 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
     rfl
   · simp [getElem?_eq_none_iff.2 (by simpa using h)]
 
-theorem singleton_inj : #[a] = #[b] ↔ a = b := by
-  simp
-
 end Array
 
 namespace List
@@ -107,8 +101,27 @@ We prefer to pull `List.toArray` outwards.
 
 @[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 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
 
 @[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
     (h : i ≤ l.length) (b : β) :
@@ -118,7 +131,7 @@ We prefer to pull `List.toArray` outwards.
   | zero =>
     simp [Array.forIn'.loop]
   | succ i ih =>
-    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
+    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih, forIn_eq_forIn]
     have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
       simp only [Nat.sub_add_eq]
       rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
@@ -132,11 +145,7 @@ We prefer to pull `List.toArray` outwards.
     forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
   change Array.forIn' _ _ _ = List.forIn' _ _ _
   rw [Array.forIn', forIn'_loop_toArray]
-  simp
-
-@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn l.toArray b f = forIn l b f := by
-  simpa using forIn'_toArray l b fun a m b => f a b
+  simp [List.forIn_eq_forIn]
 
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
@@ -206,32 +215,21 @@ 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]
 
-/--
-Variant of `foldrM_push` with `h : start = arr.size + 1`
-rather than `(arr.push a).size` as the argument.
--/
-@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α)
-    {start} (h : start = arr.size + 1) :
-    (arr.push a).foldrM f init start = f a init >>= arr.foldrM f := by
-  simp [← foldrM_push, h]
+/-- Variant of `foldrM_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
+@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
+  simp [← foldrM_push]
 
 theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
 
-/--
-Variant of `foldr_push` with the `h : start = arr.size + 1`
-rather than `(arr.push a).size` as the argument.
--/
-@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) {start}
-    (h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) :=
-  foldrM_push' _ _ _ _ h
+/-- Variant of `foldr_push` with the `start := arr.size + 1` rather than `(arr.push a).size`. -/
+@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
+    (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
 
 /-- A more efficient version of `arr.toList.reverse`. -/
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@@ -337,26 +335,25 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 
 /-! # set -/
 
-@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
-      (eq : i = j) (p : j < (a.set i v).size) :
+@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
+      (eq : i.val = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
   simp [set, getElem_eq_getElem_toList, ←eq]
 
-@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
-    (pj : j < (a.set i v).size) (h : i ≠ j) :
-    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
+@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
+    (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
-theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
+theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
-  by_cases p : i = j <;> simp [p]
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v ▸ h) := by
+  by_cases p : i.1 = j <;> simp [p]
 
-@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
-    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
 
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
-    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
+    (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
 /-! # setD -/
@@ -373,7 +370,7 @@ theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat
 @[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
     (setD a i v)[i]'h = v := by
   simp at h
-  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
+  simp only [setD, h, dite_true, getElem_set, ite_true]
 
 @[simp]
 theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
@@ -506,14 +503,13 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
   cases as
   simp [List.getElem?_eq_some_iff]
 
-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] 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] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
   simp [back?, getElem?_eq_getElem?_toList]
 
-@[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
-  simp [back!_eq_back?]
+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) :
     (a.push x)[i]? = some a[i] := by
@@ -548,43 +544,43 @@ theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some
 
 @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
 
-@[simp] theorem toList_set (a : Array α) (i v h) : (a.set i v).toList = a.toList.set i v := rfl
+@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
-theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    (a.set i v h)[i]'(by simp [h]) = v := by
+theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1] = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
 
-theorem get?_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    (a.set i v)[i]? = v := by simp [getElem?_pos, h]
+theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
 
-@[simp] theorem get?_set_ne (a : Array α) (i : Nat) (h' : i < a.size) {j : Nat} (v : α)
-    (h : i ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
+    (h : i.1 ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
 
-theorem get?_set (a : Array α) (i : Nat) (h : i < a.size) (j : Nat) (v : α) :
-    (a.set i v)[j]? = if i = j then some v else a[j]? := by
-  if h : i = j then subst j; simp [*] else simp [*]
+theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
+    (a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
+  if h : i.1 = j then subst j; simp [*] else simp [*]
 
-theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) :
+theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
     (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
-  if h : i = j then subst j; simp [*] else simp [*]
+  if h : i.1 = j then subst j; simp [*] else simp [*]
 
-@[simp] theorem get_set_ne (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size)
-    (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
+@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
+    (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
     (setD a i v)[i] = v := by
   simp at h
-  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
+  simp only [setD, h, dite_true, get_set, ite_true]
 
-theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
-    (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
+theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
+    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
 
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Fin a.size) :
-    a.swap i j = (a.set i (a.get j)).set j (a.get i) := by
+    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
   simp [swap, fin_cast_val]
 
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
@@ -602,7 +598,7 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
 
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    a.swapAt! i v = (a[i], a.set i v) := by simp [swapAt!, h]
+    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
 
 @[simp] theorem size_swapAt! (a : Array α) (i : Nat) (v : α) :
     (a.swapAt! i v).2.size = a.size := by
@@ -626,8 +622,8 @@ theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] :=
   · simp [h]
   · intros; contradiction
 
-theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
-    as = as.pop.push as.back! := by
+theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
+    as = as.pop.push as.back := by
   apply ext
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
   · intros i h h'
@@ -636,12 +632,12 @@ theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as
     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 [getElem_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 :=
   let _ : Inhabited α := ⟨as[0]⟩
-  ⟨as.pop, as.back!, eq_push_pop_back!_of_size_ne_zero h⟩
+  ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
 
 theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
 
@@ -714,43 +710,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 ▸ ‹_›)]
 
-/-! ### BEq -/
-
-@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α := by
-  constructor
-  · intro h
-    constructor
-    intro a
-    suffices (#[a] == #[a]) = true by
-      simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
-    simp
-  · intro h
-    constructor
-    apply Array.isEqv_self_beq
-
-@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α := by
-  constructor
-  · intro h
-    constructor
-    · intro a b h
-      apply singleton_inj.1
-      apply eq_of_beq
-      simp only [instBEq, isEqv, isEqvAux]
-      simpa
-    · intro a
-      suffices (#[a] == #[a]) = true by
-        simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
-      simp
-  · intro h
-    constructor
-    · intro a b h
-      obtain ⟨hs, hi⟩ := rel_of_isEqv h
-      ext i h₁ h₂
-      · exact hs
-      · simpa using hi _ h₁
-    · intro a
-      apply Array.isEqv_self_beq
-
 /-! ### take -/
 
 @[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
@@ -910,7 +869,7 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
   obtain ⟨m, eq, w⟩ := t
   · refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩
     intro i h
-    simp only [eq] at w
+    simp [eq] at w
     specialize w ⟨i, h⟩ h
     simpa [map_eq_foldl] using w
   · exact ⟨h0, rfl, nofun⟩
@@ -967,7 +926,7 @@ theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
     (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
   simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
   split
-  · simp only [Id.bind_eq, get_set _ _ _ _ (by simpa using h)]; split <;> simp [*]
+  · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
   · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
 @[simp] theorem toList_modify (as : Array α) (f : α → α) :
@@ -1083,38 +1042,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
@@ -1407,15 +1346,30 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
 
 open Fin
 
-@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.1] = a[i] := by
-  simp [swap_def, getElem_set]
+@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
+  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
 
-@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.1] = a[j] := by
-  simp +contextual [swap_def, getElem_set]
+@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
+  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
+    simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
+  else by
+    apply Eq.trans
+    · apply Array.get_set_ne
+      · simp only [size_set, Fin.isLt]
+      · assumption
+    · simp [get_set_ne]
 
 @[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
     (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
-  simp [swap_def, getElem_set, hi.symm, hj.symm]
+  apply Eq.trans
+  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
+    apply Array.get_set_ne
+    · simp only [this]
+      apply Ne.symm
+      · assumption
+  · apply Array.get_set_ne
+    · apply Ne.symm
+      · assumption
 
 theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
     (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
@@ -1602,21 +1556,8 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
-  ext <;> simp
-
 end List
 
-namespace Array
-
-@[simp] theorem mapM_id {l : Array α} {f : α → Id β} : l.mapM f = l.map f := by
-  induction l; simp_all
-
-@[simp] theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f := by
-  apply List.ext_getElem <;> simp
-
-end Array
-
 /-! ### Deprecations -/
 
 namespace List
@@ -1630,8 +1571,6 @@ theorem toArray_concat {as : List α} {x : α} :
   apply ext'
   simp
 
-@[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
-
 end List
 
 namespace Array
@@ -1772,9 +1711,4 @@ abbrev get_swap := @getElem_swap
 @[deprecated getElem_swap' (since := "2024-09-30")]
 abbrev get_swap' := @getElem_swap'
 
-@[deprecated back!_eq_back? (since := "2024-10-31")] abbrev back_eq_back? := @back!_eq_back?
-@[deprecated back!_push (since := "2024-10-31")] abbrev back_push := @back!_push
-@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
-abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
-
 end Array

src/Init/Data/Array/MapIdx.lean

@@ -60,10 +60,6 @@ theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
-@[simp] theorem toList_mapFinIdx (a : Array α) (f : Fin a.size → α → β) :
-    (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a => f ⟨i, by simp⟩ a) := by
-  apply List.ext_getElem <;> simp
-
 /-! ### mapIdx -/
 
 theorem mapIdx_induction (as : Array α) (f : Nat → α → β)
@@ -93,20 +89,4 @@ theorem mapIdx_spec (as : Array α) (f : Nat → α → β)
       a[i]?.map (f i) := by
   simp [getElem?_def, size_mapIdx, getElem_mapIdx]
 
-@[simp] theorem toList_mapIdx (a : Array α) (f : Nat → α → β) :
-    (a.mapIdx f).toList = a.toList.mapIdx (fun i a => f i a) := by
-  apply List.ext_getElem <;> simp
-
 end Array
-
-namespace List
-
-@[simp] theorem mapFinIdx_toArray (l : List α) (f : Fin l.length → α → β) :
-    l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
-  ext <;> simp
-
-@[simp] theorem mapIdx_toArray (l : List α) (f : Nat → α → β) :
-    l.toArray.mapIdx f = (l.mapIdx f).toArray := by
-  ext <;> simp
-
-end List

src/Init/Data/Array/Set.lean

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

src/Init/Data/BitVec/Basic.lean

@@ -634,16 +634,6 @@ def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
 
 end bitwise
 
-/-- Compute a hash of a bitvector, combining 64-bit words using `mixHash`. -/
-def hash (bv : BitVec n) : UInt64 :=
-  if n ≤ 64 then
-    bv.toFin.val.toUInt64
-  else
-    mixHash (bv.toFin.val.toUInt64) (hash ((bv >>> 64).setWidth (n - 64)))
-
-instance : Hashable (BitVec n) where
-  hash := hash
-
 section normalization_eqs
 /-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
 @[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl

src/Init/Data/BitVec/Bitblast.lean

@@ -174,30 +174,6 @@ theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
     exact mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ ..
   cases x.toNat.testBit i <;> cases y.toNat.testBit i <;> (simp; omega)
 
-theorem carry_succ_one (i : Nat) (x : BitVec w) (h : 0 < w) :
-    carry (i+1) x (1#w) false = decide (∀ j ≤ i, x.getLsbD j = true) := by
-  induction i with
-  | zero => simp [carry_succ, h]
-  | succ i ih =>
-    rw [carry_succ, ih]
-    simp only [getLsbD_one, add_one_ne_zero, decide_False, Bool.and_false, atLeastTwo_false_mid]
-    cases hx : x.getLsbD (i+1)
-    case false =>
-      have : ∃ j ≤ i + 1, x.getLsbD j = false :=
-        ⟨i+1, by omega, hx⟩
-      simpa
-    case true =>
-      suffices
-          (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
-          ↔ (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true) by
-        simpa
-      constructor
-      · intro h j hj
-        rcases Nat.le_or_eq_of_le_succ hj with (hj' | rfl)
-        · apply h; assumption
-        · exact hx
-      · intro h j hj; apply h; omega
-
 /--
 If `x &&& y = 0`, then the carry bit `(x + y + 0)` is always `false` for any index `i`.
 Intuitively, this is because a carry is only produced when at least two of `x`, `y`, and the
@@ -376,117 +352,6 @@ theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c
     simp [← sub_toAdd, BitVec.sub_add_cancel]
   · simp [bit_not_testBit x _]
 
-/--
-Remember that negating a bitvector is equal to incrementing the complement
-by one, i.e., `-x = ~~~x + 1`. See also `neg_eq_not_add`.
-
-This computation has two crucial properties:
-- The least significant bit of `-x` is the same as the least significant bit of `x`, and
-- The `i+1`-th least significant bit of `-x` is the complement of the `i+1`-th bit of `x`, unless
-  all of the preceding bits are `false`, in which case the bit is equal to the `i+1`-th bit of `x`
--/
-theorem getLsbD_neg {i : Nat} {x : BitVec w} :
-    getLsbD (-x) i =
-      (getLsbD x i ^^ decide (i < w) && decide (∃ j < i, getLsbD x j = true)) := by
-  rw [neg_eq_not_add]
-  by_cases hi : i < w
-  · rw [getLsbD_add hi]
-    have : 0 < w := by omega
-    simp only [getLsbD_not, hi, decide_True, Bool.true_and, getLsbD_one, this, not_bne,
-      _root_.true_and, not_eq_eq_eq_not]
-    cases i with
-    | zero =>
-      have carry_zero : carry 0 ?x ?y false = false := by
-        simp [carry]; omega
-      simp [hi, carry_zero]
-    | succ =>
-      rw [carry_succ_one _ _ (by omega), ← Bool.xor_not, ← decide_not]
-      simp only [add_one_ne_zero, decide_False, getLsbD_not, and_eq_true, decide_eq_true_eq,
-        not_eq_eq_eq_not, Bool.not_true, false_bne, not_exists, _root_.not_and, not_eq_true,
-        bne_left_inj, decide_eq_decide]
-      constructor
-      · rintro h j hj; exact And.right <| h j (by omega)
-      · rintro h j hj; exact ⟨by omega, h j (by omega)⟩
-  · have h_ge : w ≤ i := by omega
-    simp [getLsbD_ge _ _ h_ge, h_ge, hi]
-
-theorem getMsbD_neg {i : Nat} {x : BitVec w} :
-    getMsbD (-x) i =
-      (getMsbD x i ^^ decide (∃ j < w, i < j ∧ getMsbD x j = true)) := by
-  simp only [getMsbD, getLsbD_neg, Bool.decide_and, Bool.and_eq_true, decide_eq_true_eq]
-  by_cases hi : i < w
-  case neg =>
-    simp [hi]; omega
-  case pos =>
-    have h₁ : w - 1 - i < w := by omega
-    simp only [hi, decide_True, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide]
-    constructor
-    · rintro ⟨j, hj, h⟩
-      refine ⟨w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h⟩
-      congr; omega
-    · rintro ⟨j, hj₁, hj₂, -, h⟩
-      exact ⟨w - 1 - j, by omega, h⟩
-
-theorem msb_neg {w : Nat} {x : BitVec w} :
-    (-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb) := by
-  simp only [BitVec.msb, getMsbD_neg]
-  by_cases hmin : x = intMin _
-  case pos =>
-    have : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False := by
-      simp; omega
-    simp [hmin, getMsbD_intMin, this]
-  case neg =>
-    by_cases hzero : x = 0#w
-    case pos => simp [hzero]
-    case neg =>
-      have w_pos : 0 < w := by
-        cases w
-        · rw [@of_length_zero x] at hzero
-          contradiction
-        · omega
-      suffices ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
-        by simp [show x != 0#w by simpa, show x != intMin w by simpa, this]
-      false_or_by_contra
-      rename_i getMsbD_x
-      simp only [not_exists, _root_.not_and, not_eq_true] at getMsbD_x
-      /- `getMsbD` says that all bits except the msb are `false` -/
-      cases hmsb : x.msb
-      case true =>
-        apply hmin
-        apply eq_of_getMsbD_eq
-        rintro ⟨i, hi⟩
-        simp only [getMsbD_intMin, w_pos, decide_True, Bool.true_and]
-        cases i
-        case zero => exact hmsb
-        case succ => exact getMsbD_x _ hi (by omega)
-      case false =>
-        apply hzero
-        apply eq_of_getMsbD_eq
-        rintro ⟨i, hi⟩
-        simp only [getMsbD_zero]
-        cases i
-        case zero => exact hmsb
-        case succ => exact getMsbD_x _ hi (by omega)
-
-/-! ### abs -/
-
-theorem msb_abs {w : Nat} {x : BitVec w} :
-    x.abs.msb = (decide (x = intMin w) && decide (0 < w)) := by
-  simp only [BitVec.abs, getMsbD_neg, ne_eq, decide_not, Bool.not_bne]
-  by_cases h₀ : 0 < w
-  · by_cases h₁ : x = intMin w
-    · simp [h₁, msb_intMin]
-    · simp only [neg_eq, h₁, decide_False]
-      by_cases h₂ : x.msb
-      · simp [h₂, msb_neg]
-        and_intros
-        · by_cases h₃ : x = 0#w
-          · simp [h₃] at h₂
-          · simp [h₃]
-        · simp [h₁]
-      · simp [h₂]
-  · simp [BitVec.msb, show w = 0 by omega]
-
 /-! ### Inequalities (le / lt) -/
 
 theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true := by

src/Init/Data/BitVec/Lemmas.lean

@@ -1062,7 +1062,7 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
 
 @[simp]
-theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
+theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
   apply eq_of_toNat_eq
   simp
 
@@ -1232,11 +1232,7 @@ theorem ushiftRight_or_distrib (x y : BitVec w)  (n : Nat) :
   simp
 
 @[simp]
-theorem ushiftRight_zero (x : BitVec w) : x >>> 0 = x := by
-  simp [bv_toNat]
-
-@[simp]
-theorem zero_ushiftRight {n : Nat} : 0#w >>> n = 0#w := by
+theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by
   simp [bv_toNat]
 
 /--
@@ -1391,10 +1387,6 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
   ext i
   simp [getLsbD_sshiftRight]
 
-@[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
-  ext i
-  simp [getLsbD_sshiftRight]
-
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
@@ -1792,7 +1784,7 @@ theorem setWidth_succ (x : BitVec w) :
     · simp_all
     · omega
 
-@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]
+@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
 theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
   simp
 
@@ -1917,31 +1909,6 @@ theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
   ext
   simp [getLsbD_concat]
 
-@[simp]
-theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} :
-    (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b := by
-  simp only [getMsbD_eq_getLsbD, Nat.add_sub_cancel, getLsbD_concat]
-  by_cases h₀ : i = w
-  · simp [h₀]
-  · by_cases h₁ : i < w
-    · simp [h₀, h₁, show ¬ w - i = 0 by omega, show i < w + 1 by omega, Nat.sub_sub, Nat.add_comm]
-    · simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_False, Bool.false_and,
-        Bool.and_eq_false_imp, decide_eq_true_eq]
-      intro
-      omega
-
-@[simp]
-theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
-    (x.concat b).msb = if 0 < w then x.msb else b := by
-  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_True, Nat.add_one_sub_one,
-    Nat.sub_zero, Bool.true_and]
-  by_cases h₀ : 0 < w
-  · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_True,
-      Bool.true_and, ite_eq_right_iff]
-    intro
-    omega
-  · simp [h₀, show w = 0 by omega]
-
 /-! ### add -/
 
 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
@@ -2146,6 +2113,17 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
         show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
       omega
 
+/-! ### abs -/
+
+@[simp, bv_toNat]
+theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
+  simp only [BitVec.abs, neg_eq]
+  by_cases h : x.msb = true
+  · simp only [h, ↓reduceIte, toNat_neg]
+    have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
+    rw [Nat.mod_eq_of_lt (by omega)]
+  · simp [h]
+
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -2173,23 +2151,18 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
   right_id := BitVec.mul_one
 
 @[simp]
-theorem mul_zero {x : BitVec w} : x * 0#w = 0#w := by
+theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
   apply eq_of_toNat_eq
   simp [toNat_mul]
 
-@[simp]
-theorem zero_mul {x : BitVec w} : 0#w * x = 0#w := by
-  apply eq_of_toNat_eq
-  simp [toNat_mul]
-
-theorem mul_add {x y z : BitVec w} :
+theorem BitVec.mul_add {x y z : BitVec w} :
     x * (y + z) = x * y + x * z := by
   apply eq_of_toNat_eq
   simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
-theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add]
+theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [BitVec.mul_add]
 theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
 
 theorem mul_two {x : BitVec w} : x * 2#w = x + x := by
@@ -2370,11 +2343,6 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
     rcases hy with rfl | rfl <;>
       rfl
 
-/-! ### smtUDiv -/
-
-theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
-  simp [smtUDiv]
-
 /-! ### sdiv -/
 
 /-- Equation theorem for `sdiv` in terms of `udiv`. -/
@@ -2431,28 +2399,6 @@ theorem sdiv_self {x : BitVec w} :
       rcases x.msb with msb | msb <;> simp
     · rcases x.msb with msb | msb <;> simp [h]
 
-/-! ### smtSDiv -/
-
-theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
-  match x.msb, y.msb with
-  | false, false => smtUDiv x y
-  | false, true  => -(smtUDiv x (-y))
-  | true,  false => -(smtUDiv (-x) y)
-  | true,  true  => smtUDiv (-x) (-y) := by
-  rw [BitVec.smtSDiv]
-  rcases x.msb <;> rcases y.msb <;> simp
-
-/-! ### srem -/
-
-theorem srem_eq (x y : BitVec w) : srem x y =
-  match x.msb, y.msb with
-  | false, false => x % y
-  | false, true  => x % (-y)
-  | true,  false => - ((-x) % y)
-  | true,  true  => -((-x) % (-y)) := by
-  rw [BitVec.srem]
-  rcases x.msb <;> rcases y.msb <;> simp
-
 /-! ### smod -/
 
 /-- Equation theorem for `smod` in terms of `umod`. -/
@@ -2726,21 +2672,6 @@ theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (j = i
   simp [eq_comm]
   omega
 
-@[simp]
-theorem getMsbD_twoPow {i j w: Nat} :
-    (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1)) := by
-  simp only [getMsbD_eq_getLsbD, getLsbD_twoPow]
-  by_cases h₀ : i < w <;> by_cases h₁ : j < w <;>
-  simp [h₀, h₁] <;> omega
-
-@[simp]
-theorem msb_twoPow {i w: Nat} :
-    (twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by
-  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow,
-    Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]
-  intros
-  omega
-
 theorem and_twoPow (x : BitVec w) (i : Nat) :
     x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
   ext j
@@ -2886,14 +2817,6 @@ theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) :=
   simp only [intMin, getLsbD_twoPow, boolToPropSimps]
   omega
 
-theorem getMsbD_intMin {w i : Nat} :
-    (intMin w).getMsbD i = (decide (0 < w) && decide (i = 0)) := by
-  simp only [getMsbD, getLsbD_intMin]
-  match w, i with
-  | 0,   _    => simp
-  | w+1, 0    => simp
-  | w+1, i+1  => simp; omega
-
 /--
 The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
 -/
@@ -2916,21 +2839,6 @@ theorem toInt_intMin {w : Nat} :
     rw [Nat.mul_comm]
     simp [w_pos]
 
-theorem toInt_intMin_le (x : BitVec w) :
-    (intMin w).toInt ≤ x.toInt := by
-  cases w
-  case zero => simp [@of_length_zero x]
-  case succ w =>
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
-    have : 0 < 2 ^ w := Nat.two_pow_pos w
-    rw [Int.emod_eq_of_lt (by omega) (by omega)]
-    rw [BitVec.toInt_eq_toNat_bmod]
-    rw [show (2 ^ w : Nat) = ((2 ^ (w + 1) : Nat) : Int) / 2 by omega]
-    apply Int.le_bmod (by omega)
-
-theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by
-  simp only [BitVec.sle, toInt_intMin_le x, decide_True]
-
 @[simp]
 theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   by_cases h : 0 < w
@@ -2938,10 +2846,6 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   · simp only [Nat.not_lt, Nat.le_zero_eq] at h
     simp [bv_toNat, h]
 
-@[simp]
-theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by
-  simp [BitVec.abs, bv_toNat]
-
 theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
     (-x).toInt = -(x.toInt) := by
   simp only [ne_eq, toNat_eq, toNat_intMin] at rs
@@ -2958,10 +2862,6 @@ theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
   have := @Nat.two_pow_pred_mul_two w (by omega)
   split <;> split <;> omega
 
-theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by
-  simp only [msb_eq_decide, toNat_intMin, decide_eq_decide]
-  by_cases h : 0 < w <;> simp_all
-
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
@@ -3054,38 +2954,6 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
     BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
   omega
 
-/-! ### neg -/
-
-theorem msb_eq_toInt {x : BitVec w}:
-    x.msb = decide (x.toInt < 0) := by
-  by_cases h : x.msb <;>
-  · simp [h, toInt_eq_msb_cond]
-    omega
-
-theorem msb_eq_toNat {x : BitVec w}:
-    x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by
-  simp only [msb_eq_decide, ge_iff_le]
-
-/-! ### abs -/
-
-theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
-
-@[simp, bv_toNat]
-theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
-  simp only [BitVec.abs, neg_eq]
-  by_cases h : x.msb = true
-  · simp only [h, ↓reduceIte, toNat_neg]
-    have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
-    rw [Nat.mod_eq_of_lt (by omega)]
-  · simp [h]
-
-theorem getLsbD_abs {i : Nat} {x : BitVec w} :
-   getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by
-  by_cases h : x.msb <;> simp [BitVec.abs, h]
-
-theorem getMsbD_abs {i : Nat} {x : BitVec w} :
-    getMsbD (x.abs) i = if x.msb then getMsbD (-x) i else getMsbD x i := by
-  by_cases h : x.msb <;> simp [BitVec.abs, h]
 
 /-! ### Decidable quantifiers -/
 
@@ -3294,10 +3162,4 @@ abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLs
 @[deprecated msb_sshiftRight (since := "2024-10-03")]
 abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight
 
-@[deprecated shiftLeft_zero (since := "2024-10-27")]
-abbrev shiftLeft_zero_eq := @shiftLeft_zero
-
-@[deprecated ushiftRight_zero (since := "2024-10-27")]
-abbrev ushiftRight_zero_eq := @ushiftRight_zero
-
 end BitVec

src/Init/Data/ByteArray/Basic.lean

@@ -65,7 +65,7 @@ def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
 
 @[extern "lean_byte_array_fset"]
 def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
-  | ⟨bs⟩, i, b => ⟨bs.set i.1 b i.2⟩
+  | ⟨bs⟩, i, b => ⟨bs.set i b⟩
 
 @[extern "lean_byte_array_uset"]
 def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray

src/Init/Data/Fin/Fold.lean

@@ -5,8 +5,6 @@ Authors: François G. Dorais
 -/
 prelude
 import Init.Data.Nat.Linear
-import Init.Control.Lawful.Basic
-import Init.Data.Fin.Lemmas
 
 namespace Fin
 
@@ -25,195 +23,4 @@ namespace Fin
   | ⟨0, _⟩, x => x
   | ⟨i+1, h⟩, x => loop ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x)
 
-/--
-Folds a monadic function over `Fin n` from left to right:
-```
-Fin.foldlM n f x₀ = do
-  let x₁ ← f x₀ 0
-  let x₂ ← f x₁ 1
-  ...
-  let xₙ ← f xₙ₋₁ (n-1)
-  pure xₙ
-```
--/
-@[inline] def foldlM [Monad m] (n) (f : α → Fin n → m α) (init : α) : m α := loop init 0 where
-  /--
-  Inner loop for `Fin.foldlM`.
-  ```
-  Fin.foldlM.loop n f xᵢ i = do
-    let xᵢ₊₁ ← f xᵢ i
-    ...
-    let xₙ ← f xₙ₋₁ (n-1)
-    pure xₙ
-  ```
-  -/
-  loop (x : α) (i : Nat) : m α := do
-    if h : i < n then f x ⟨i, h⟩ >>= (loop · (i+1)) else pure x
-  termination_by n - i
-  decreasing_by decreasing_trivial_pre_omega
-
-/--
-Folds a monadic function over `Fin n` from right to left:
-```
-Fin.foldrM n f xₙ = do
-  let xₙ₋₁ ← f (n-1) xₙ
-  let xₙ₋₂ ← f (n-2) xₙ₋₁
-  ...
-  let x₀ ← f 0 x₁
-  pure x₀
-```
--/
-@[inline] def foldrM [Monad m] (n) (f : Fin n → α → m α) (init : α) : m α :=
-  loop ⟨n, Nat.le_refl n⟩ init where
-  /--
-  Inner loop for `Fin.foldrM`.
-  ```
-  Fin.foldrM.loop n f i xᵢ = do
-    let xᵢ₋₁ ← f (i-1) xᵢ
-    ...
-    let x₁ ← f 1 x₂
-    let x₀ ← f 0 x₁
-    pure x₀
-  ```
-  -/
-  loop : {i // i ≤ n} → α → m α
-  | ⟨0, _⟩, x => pure x
-  | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩
-
-/-! ### foldlM -/
-
-theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
-    foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by
-  rw [foldlM.loop, dif_pos h]
-
-theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x := by
-  rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)]
-
-theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) :
-    foldlM.loop (n+1) f x i = f x ⟨i, h⟩ >>= (foldlM.loop n (fun x j => f x j.succ) . i) := by
-  if h' : i < n then
-    rw [foldlM_loop_lt _ _ h]
-    congr; funext
-    rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl
-  else
-    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
-    rw [foldlM_loop_lt]
-    congr; funext
-    rw [foldlM_loop_eq, foldlM_loop_eq]
-termination_by n - i
-
-@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x :=
-  foldlM_loop_eq ..
-
-theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) :
-    foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
-
-/-! ### foldrM -/
-
-theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) :
-    foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by
-  rw [foldrM.loop]
-
-theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) :
-    foldrM.loop n f ⟨i+1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, Nat.le_of_lt h⟩ := by
-  rw [foldrM.loop]
-
-theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) :
-    foldrM.loop (n+1) f ⟨i+1, h⟩ x =
-      foldrM.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x >>= f 0 := by
-  induction i generalizing x with
-  | zero =>
-    rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
-    conv => rhs; rw [←bind_pure (f 0 x)]
-    congr; funext; exact foldrM_loop_zero ..
-  | succ i ih =>
-    rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
-    congr; funext; exact ih ..
-
-@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x :=
-  foldrM_loop_zero ..
-
-theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
-    foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
-
-/-! ### foldl -/
-
-theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) :
-    foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by
-  rw [foldl.loop, dif_pos h]
-
-theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by
-  rw [foldl.loop, dif_neg (Nat.lt_irrefl _)]
-
-theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : i < n+1) :
-    foldl.loop (n+1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i := by
-  if h' : i < n then
-    rw [foldl_loop_lt _ _ h]
-    rw [foldl_loop_lt _ _ h', foldl_loop]; rfl
-  else
-    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
-    rw [foldl_loop_lt]
-    rw [foldl_loop_eq, foldl_loop_eq]
-
-@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x :=
-  foldl_loop_eq ..
-
-theorem foldl_succ (f : α → Fin (n+1) → α) (x) :
-    foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) :=
-  foldl_loop ..
-
-theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
-    foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by
-  rw [foldl_succ]
-  induction n generalizing x with
-  | zero => simp [foldl_succ, Fin.last]
-  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
-
-theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
-    foldl n f x = foldlM (m:=Id) n f x := by
-  induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
-
-/-! ### foldr -/
-
-theorem foldr_loop_zero (f : Fin n → α → α) (x) :
-    foldr.loop n f ⟨0, Nat.zero_le _⟩ x = x := by
-  rw [foldr.loop]
-
-theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) :
-    foldr.loop n f ⟨i+1, h⟩ x = foldr.loop n f ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x) := by
-  rw [foldr.loop]
-
-theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) :
-    foldr.loop (n+1) f ⟨i+1, h⟩ x =
-      f 0 (foldr.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x) := by
-  induction i generalizing x <;> simp [foldr_loop_zero, foldr_loop_succ, *]
-
-@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x :=
-  foldr_loop_zero ..
-
-theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
-    foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
-
-theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
-    foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
-  induction n generalizing x with
-  | zero => simp [foldr_succ, Fin.last]
-  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
-
-theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
-    foldr n f x = foldrM (m:=Id) n f x := by
-  induction n <;> simp [foldr_succ, foldrM_succ, *]
-
-theorem foldl_rev (f : Fin n → α → α) (x) :
-    foldl n (fun x i => f i.rev x) x = foldr n f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ]
-
-theorem foldr_rev (f : α → Fin n → α) (x) :
-     foldr n (fun i x => f x i.rev) x = foldl n f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]
-
 end Fin

src/Init/Data/FloatArray/Basic.lean

@@ -71,7 +71,7 @@ def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → F
 
 @[extern "lean_float_array_fset"]
 def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
-  | ⟨ds⟩, i, d => ⟨ds.set i.1 d i.2⟩
+  | ⟨ds⟩, i, d => ⟨ds.set i d⟩
 
 @[extern "lean_float_array_set"]
 def set! : FloatArray → (@& Nat) → Float → FloatArray

src/Init/Data/Hashable.lean

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

src/Init/Data/Int/DivModLemmas.lean

@@ -1267,7 +1267,7 @@ theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
     _ = ((m + 1 - 2) + 2)/2 := by simp
     _ = (m - 1) / 2 + 1     := by
       rw [add_ediv_of_dvd_right]
-      · simp +decide only [Int.ediv_self]
+      · simp (config := {decide := true}) only [Int.ediv_self]
         congr 2
         rw [Int.add_sub_assoc, ← Int.sub_neg]
         congr
@@ -1285,7 +1285,7 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
     simp only [bmod, ofNat_eq_coe, natAbs_ofNat, natCast_add, ofNat_one,
       emod_self_add_one (ofNat_nonneg x)]
     match x with
-    | 0 => rw [if_pos] <;> simp +decide
+    | 0 => rw [if_pos] <;> simp (config := {decide := true})
     | (x+1) =>
       rw [if_neg]
       · simp [← Int.sub_sub]

src/Init/Data/Int/Order.lean

@@ -1007,9 +1007,9 @@ theorem sign_eq_neg_one_iff_neg {a : Int} : sign a = -1 ↔ a < 0 :=
   match x with
   | 0 => rfl
   | .ofNat (_ + 1) =>
-    simp +decide only [sign, true_iff]
+    simp (config := { decide := true }) only [sign, true_iff]
     exact Int.le_add_one (ofNat_nonneg _)
-  | .negSucc _ => simp +decide [sign]
+  | .negSucc _ => simp (config := { decide := true }) [sign]
 
 theorem mul_sign : ∀ i : Int, i * sign i = natAbs i
   | succ _ => Int.mul_one _

src/Init/Data/List.lean

@@ -25,4 +25,3 @@ import Init.Data.List.Perm
 import Init.Data.List.Sort
 import Init.Data.List.ToArray
 import Init.Data.List.MapIdx
-import Init.Data.List.OfFn

src/Init/Data/List/Basic.lean

@@ -45,7 +45,7 @@ The operations are organized as follow:
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
 * Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
 * Minima and maxima: `min?` and `max?`.
-* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `splitBy`,
+* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
   `removeAll`
   (currently these functions are mostly only used in meta code,
   and do not have API suitable for verification).
@@ -1639,23 +1639,23 @@ where
     | true  => loop as (a::rs)
     | false => (rs.reverse, a::as)
 
-/-! ### splitBy -/
+/-! ### groupBy -/
 
 /--
-`O(|l|)`. `splitBy R l` splits `l` into chains of elements
+`O(|l|)`. `groupBy R l` splits `l` into chains of elements
 such that adjacent elements are related by `R`.
 
-* `splitBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
-* `splitBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
+* `groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
+* `groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
 -/
-@[specialize] def splitBy (R : α → α → Bool) : List α → List (List α)
+@[specialize] def groupBy (R : α → α → Bool) : List α → List (List α)
   | []    => []
   | a::as => loop as a [] []
 where
   /--
-  The arguments of `splitBy.loop l ag g gs` represent the following:
+  The arguments of `groupBy.loop l ag g gs` represent the following:
 
-  - `l : List α` are the elements which we still need to split.
+  - `l : List α` are the elements which we still need to group.
   - `ag : α` is the previous element for which a comparison was performed.
   - `g : List α` is the group currently being assembled, in **reverse order**.
   - `gs : List (List α)` is all of the groups that have been completed, in **reverse order**.
@@ -1666,8 +1666,6 @@ where
     | false => loop as a [] ((ag::g).reverse::gs)
   | [], ag, g, gs => ((ag::g).reverse::gs).reverse
 
-@[deprecated splitBy (since := "2024-10-30"), inherit_doc splitBy] abbrev groupBy := @splitBy
-
 /-! ### removeAll -/
 
 /-- `O(|xs|)`. Computes the "set difference" of lists,

src/Init/Data/List/Control.lean

@@ -215,6 +215,27 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
     | some b => pure (some b)
     | none   => findSomeM? f as
 
+@[inline] protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop
+    | [], b    => pure b
+    | a::as, b => do
+      match (← f a b) with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop as b
+  loop as init
+
+instance : ForIn m (List α) α where
+  forIn := List.forIn
+
+@[simp] theorem forIn_eq_forIn [Monad m] : @List.forIn α β m _ = forIn := rfl
+
+@[simp] theorem forIn_nil [Monad m] (f : α → β → m (ForInStep β)) (b : β) : forIn [] b f = pure b :=
+  rfl
+
+@[simp] theorem forIn_cons [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β)
+    : forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f :=
+  rfl
+
 @[inline] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
     | [], b, _    => pure b
@@ -233,15 +254,16 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
 instance : ForIn' m (List α) α inferInstance where
   forIn' := List.forIn'
 
--- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
-
 @[simp] theorem forIn'_eq_forIn' [Monad m] : @List.forIn' α β m _ = forIn' := rfl
 
-@[simp] theorem forIn'_nil [Monad m] (f : (a : α) → a ∈ [] → β → m (ForInStep β)) (b : β) : forIn' [] b f = pure b :=
-  rfl
-
-@[simp] theorem forIn_nil [Monad m] (f : α → β → m (ForInStep β)) (b : β) : forIn [] b f = pure b :=
-  rfl
+@[simp] theorem forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : forIn' as init (fun a _ b => f a b) = forIn as init f := by
+  simp [forIn', forIn, List.forIn, List.forIn']
+  have : ∀ cs h, List.forIn'.loop cs (fun a _ b => f a b) as init h = List.forIn.loop f as init := by
+    intro cs h
+    induction as generalizing cs init with
+    | nil => intros; rfl
+    | cons a as ih => intros; simp [List.forIn.loop, List.forIn'.loop, ih]
+  apply this
 
 instance : ForM m (List α) α where
   forM := List.forM

src/Init/Data/List/Count.lean

@@ -153,7 +153,7 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
   simp only [length_filterMap_eq_countP]
   congr
   ext a
-  simp +contextual [Option.getD_eq_iff, Option.isSome_eq_isSome]
+  simp (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
 
 @[simp] theorem countP_flatten (l : List (List α)) :
     countP p l.flatten = (l.map (countP p)).sum := by
@@ -315,7 +315,7 @@ theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = len
 theorem count_le_count_map [DecidableEq β] (l : List α) (f : α → β) (x : α) :
     count x l ≤ count (f x) (map f l) := by
   rw [count, count, countP_map]
-  apply countP_mono_left; simp +contextual
+  apply countP_mono_left; simp (config := { contextual := true })
 
 theorem count_filterMap {α} [BEq β] (b : β) (f : α → Option β) (l : List α) :
     count b (filterMap f l) = countP (fun a => f a == some b) l := by

src/Init/Data/List/Find.lean

@@ -179,7 +179,7 @@ theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β}
     List.findSome? f l₁ = some b → List.findSome? f l₂ = some b := by
   rw [IsPrefix] at h
   obtain ⟨t, rfl⟩ := h
-  simp +contextual [findSome?_append]
+  simp (config := {contextual := true}) [findSome?_append]
 
 theorem IsPrefix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
     List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
@@ -436,7 +436,7 @@ theorem IsPrefix.find?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁
     List.find? p l₁ = some b → List.find? p l₂ = some b := by
   rw [IsPrefix] at h
   obtain ⟨t, rfl⟩ := h
-  simp +contextual [find?_append]
+  simp (config := {contextual := true}) [find?_append]
 
 theorem IsPrefix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
     List.find? p l₂ = none → List.find? p l₁ = none :=
@@ -562,7 +562,7 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
     | inr e =>
       have ipm := Nat.succ_pred_eq_of_pos e
       have ilt := Nat.le_trans ho (findIdx_le_length p)
-      simp +singlePass only [← ipm, getElem_cons_succ]
+      simp (config := { singlePass := true }) only [← ipm, getElem_cons_succ]
       rw [← ipm, Nat.succ_lt_succ_iff] at h
       simpa using ih h
 

src/Init/Data/List/Impl.lean

@@ -23,7 +23,7 @@ namespace List
 The following operations are already tail-recursive, and do not need `@[csimp]` replacements:
 `get`, `foldl`, `beq`, `isEqv`, `reverse`, `elem` (and hence `contains`), `drop`, `dropWhile`,
 `partition`, `isPrefixOf`, `isPrefixOf?`, `find?`, `findSome?`, `lookup`, `any` (and hence `or`),
-`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `splitBy`.
+`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `groupBy`.
 
 The following operations are still missing `@[csimp]` replacements:
 `concat`, `zipWithAll`.

src/Init/Data/List/Lemmas.lean

@@ -3328,7 +3328,7 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
 
 @[simp] theorem all_replicate {n : Nat} {a : α} :
     (replicate n a).all f = if n = 0 then true else f a := by
-  cases n <;> simp +contextual [replicate_succ]
+  cases n <;> simp (config := {contextual := true}) [replicate_succ]
 
 @[simp] theorem any_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.insert a).any f = (f a || l.any f) := by

src/Init/Data/List/MapIdx.lean

@@ -7,9 +7,6 @@ Authors: Kim Morrison, Mario Carneiro
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Range
-import Init.Data.List.OfFn
-import Init.Data.Fin.Lemmas
-import Init.Data.Option.Attach
 
 namespace List
 
@@ -17,21 +14,8 @@ namespace List
 
 /-! ### mapIdx -/
 
-
 /--
-Given a list `as = [a₀, a₁, ...]` function `f : Fin as.length → α → β`, returns the list
-`[f 0 a₀, f 1 a₁, ...]`.
--/
-@[inline] def mapFinIdx (as : List α) (f : Fin as.length → α → β) : List β := go as #[] (by simp) where
-  /-- Auxiliary for `mapFinIdx`:
-  `mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀, f 1 a₁, ...]` -/
-  @[specialize] go : (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → List β
-  | [], acc, h => acc.toList
-  | a :: as, acc, h =>
-    go as (acc.push (f ⟨acc.size, by simp at h; omega⟩ a)) (by simp at h ⊢; omega)
-
-/--
-Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁, ...]`, returns the list
+Given a function `f : Nat → α → β` and `as : list α`, `as = [a₀, a₁, ...]`, returns the list
 `[f 0 a₀, f 1 a₁, ...]`.
 -/
 @[inline] def mapIdx (f : Nat → α → β) (as : List α) : List β := go as #[] where
@@ -41,177 +25,34 @@ Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁,
   | [], acc => acc.toList
   | a :: as, acc => go as (acc.push (f acc.size a))
 
-/-! ### mapFinIdx -/
-
-@[simp]
-theorem mapFinIdx_nil {f : Fin 0 → α → β} : mapFinIdx [] f = [] :=
-  rfl
-
-@[simp] theorem length_mapFinIdx_go :
-    (mapFinIdx.go as f bs acc h).length = as.length := by
-  induction bs generalizing acc with
-  | nil => simpa using h
-  | cons _ _ ih => simp [mapFinIdx.go, ih]
-
-@[simp] theorem length_mapFinIdx {as : List α} {f : Fin as.length → α → β} :
-    (as.mapFinIdx f).length = as.length := by
-  simp [mapFinIdx, length_mapFinIdx_go]
-
-theorem getElem_mapFinIdx_go {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} {w} :
-    (mapFinIdx.go as f bs acc h)[i] =
-      if w' : i < acc.size then acc[i] else f ⟨i, by simp at w; omega⟩ (bs[i - acc.size]'(by simp at w; omega)) := by
-  induction bs generalizing acc with
-  | nil =>
-    simp only [length_mapFinIdx_go, length_nil, Nat.zero_add] at w h
-    simp only [mapFinIdx.go, Array.getElem_toList]
-    rw [dif_pos]
-  | cons _ _ ih =>
-    simp [mapFinIdx.go]
-    rw [ih]
-    simp
-    split <;> rename_i h₁ <;> split <;> rename_i h₂
-    · rw [Array.getElem_push_lt]
-    · have h₃ : i = acc.size := by omega
-      subst h₃
-      simp
-    · omega
-    · have h₃ : i - acc.size = (i - (acc.size + 1)) + 1 := by omega
-      simp [h₃]
-
-@[simp] theorem getElem_mapFinIdx {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} :
-    (as.mapFinIdx f)[i] = f ⟨i, by simp at h; omega⟩ (as[i]'(by simp at h; omega)) := by
-  simp [mapFinIdx, getElem_mapFinIdx_go]
-
-theorem mapFinIdx_eq_ofFn {as : List α} {f : Fin as.length → α → β} :
-    as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] := by
-  apply ext_getElem <;> simp
-
-@[simp] theorem getElem?_mapFinIdx {l : List α} {f : Fin l.length → α → β} {i : Nat} :
-    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some] at m; exact m.1⟩ x := by
-  simp only [getElem?_eq, length_mapFinIdx, getElem_mapFinIdx]
-  split <;> simp
-
-@[simp]
-theorem mapFinIdx_cons {l : List α} {a : α} {f : Fin (l.length + 1) → α → β} :
-    mapFinIdx (a :: l) f = f 0 a :: mapFinIdx l (fun i => f i.succ) := by
-  apply ext_getElem
-  · simp
-  · rintro (_|i) h₁ h₂ <;> simp
-
-theorem mapFinIdx_append {K L : List α} {f : Fin (K ++ L).length → α → β} :
-    (K ++ L).mapFinIdx f =
-      K.mapFinIdx (fun i => f (i.castLE (by simp))) ++ L.mapFinIdx (fun i => f ((i.natAdd K.length).cast (by simp))) := by
-  apply ext_getElem
-  · simp
-  · intro i h₁ h₂
-    rw [getElem_append]
-    simp only [getElem_mapFinIdx, length_mapFinIdx]
-    split <;> rename_i h
-    · rw [getElem_append_left]
-      congr
-    · simp only [Nat.not_lt] at h
-      rw [getElem_append_right h]
-      congr
-      simp
-      omega
-
-@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : Fin (l ++ [e]).length → α → β}:
-    (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i => f (i.castLE (by simp))) ++ [f ⟨l.length, by simp⟩ e] := by
-  simp [mapFinIdx_append]
-  congr
-
-theorem mapFinIdx_singleton {a : α} {f : Fin 1 → α → β} :
-    [a].mapFinIdx f = [f ⟨0, by simp⟩ a] := by
-  simp
-
-theorem mapFinIdx_eq_enum_map {l : List α} {f : Fin l.length → α → β} :
-    l.mapFinIdx f = l.enum.attach.map
-      fun ⟨⟨i, x⟩, m⟩ => f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some] at m; exact m.1⟩ x := by
-  apply ext_getElem <;> simp
-
-@[simp]
-theorem mapFinIdx_eq_nil_iff {l : List α} {f : Fin l.length → α → β} :
-    l.mapFinIdx f = [] ↔ l = [] := by
-  rw [mapFinIdx_eq_enum_map, map_eq_nil_iff, attach_eq_nil_iff, enum_eq_nil_iff]
-
-theorem mapFinIdx_ne_nil_iff {l : List α} {f : Fin l.length → α → β} :
-    l.mapFinIdx f ≠ [] ↔ l ≠ [] := by
-  simp
-
-theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β}
-    (h : b ∈ l.mapFinIdx f) : ∃ (i : Fin l.length), f i l[i] = b := by
-  rw [mapFinIdx_eq_enum_map] at h
-  replace h := exists_of_mem_map h
-  simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_enum_iff_getElem?] at h
-  obtain ⟨i, b, h, rfl⟩ := h
-  rw [getElem?_eq_some_iff] at h
-  obtain ⟨h', rfl⟩ := h
-  exact ⟨⟨i, h'⟩, rfl⟩
-
-@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β} :
-    b ∈ l.mapFinIdx f ↔ ∃ (i : Fin l.length), f i l[i] = b := by
-  constructor
-  · intro h
-    exact exists_of_mem_mapFinIdx h
-  · rintro ⟨i, h, rfl⟩
-    rw [mem_iff_getElem]
-    exact ⟨i, by simp⟩
-
-theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : Fin l.length → α → β} :
-    l.mapFinIdx f = b :: l₂ ↔
-      ∃ (a : α) (l₁ : List α) (h : l = a :: l₁),
-        f ⟨0, by simp [h]⟩ a = b ∧ l₁.mapFinIdx (fun i => f (i.succ.cast (by simp [h]))) = l₂ := by
-  cases l with
-  | nil => simp
-  | cons x l' =>
-    simp only [mapFinIdx_cons, cons.injEq, length_cons, Fin.zero_eta, Fin.cast_succ_eq,
-      exists_and_left]
-    constructor
-    · rintro ⟨rfl, rfl⟩
-      refine ⟨x, rfl, l', by simp⟩
-    · rintro ⟨a, ⟨rfl, h⟩, ⟨_, ⟨rfl, rfl⟩, h⟩⟩
-      exact ⟨rfl, h⟩
-
-theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : Fin l.length → α → β} :
-    l.mapFinIdx f = b :: l₂ ↔
-      l.head?.pbind (fun x m => (f ⟨0, by cases l <;> simp_all⟩ x)) = some b ∧
-        l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i => f (i.succ.cast (by cases l <;> simp_all))) = some l₂ := by
-  cases l <;> simp
-
-theorem mapFinIdx_eq_iff {l : List α} {f : Fin l.length → α → β} :
-    l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f ⟨i, h⟩ l[i] := by
-  constructor
-  · rintro rfl
-    simp
-  · rintro ⟨h, w⟩
-    apply ext_getElem <;> simp_all
-
-theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : Fin l.length → α → β} :
-    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Fin l.length), f i l[i] = g i l[i] := by
-  rw [eq_comm, mapFinIdx_eq_iff]
-  simp [Fin.forall_iff]
-
-@[simp] theorem mapFinIdx_mapFinIdx {l : List α} {f : Fin l.length → α → β} {g : Fin _ → β → γ} :
-    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i => g (i.cast (by simp)) ∘ f i) := by
-  simp [mapFinIdx_eq_iff]
-
-theorem mapFinIdx_eq_replicate_iff {l : List α} {f : Fin l.length → α → β} {b : β} :
-    l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Fin l.length), f i l[i] = b := by
-  simp [eq_replicate_iff, length_mapFinIdx, mem_mapFinIdx, forall_exists_index, true_and]
-
-@[simp] theorem mapFinIdx_reverse {l : List α} {f : Fin l.reverse.length → α → β} :
-    l.reverse.mapFinIdx f = (l.mapFinIdx (fun i => f ⟨l.length - 1 - i, by simp; omega⟩)).reverse := by
-  simp [mapFinIdx_eq_iff]
-  intro i h
-  congr
-  omega
-
-/-! ### mapIdx -/
-
 @[simp]
 theorem mapIdx_nil {f : Nat → α → β} : mapIdx f [] = [] :=
   rfl
 
+theorem mapIdx_go_append  {l₁ l₂ : List α} {arr : Array β} :
+    mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (List.toArray (mapIdx.go f l₁ arr)) := by
+  generalize h : (l₁ ++ l₂).length = len
+  induction len generalizing l₁ arr with
+  | zero =>
+    have l₁_nil : l₁ = [] := by
+      cases l₁
+      · rfl
+      · contradiction
+    have l₂_nil : l₂ = [] := by
+      cases l₂
+      · rfl
+      · rw [List.length_append] at h; contradiction
+    rw [l₁_nil, l₂_nil]; simp only [mapIdx.go, List.toArray_toList]
+  | succ len ih =>
+    cases l₁ with
+    | nil =>
+      simp only [mapIdx.go, nil_append, List.toArray_toList]
+    | cons head tail =>
+      simp only [mapIdx.go, List.append_eq]
+      rw [ih]
+      · simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
+        simp only [length_append, h]
+
 theorem mapIdx_go_length {arr : Array β} :
     length (mapIdx.go f l arr) = length l + arr.size := by
   induction l generalizing arr with
@@ -219,6 +60,16 @@ theorem mapIdx_go_length {arr : Array β} :
   | cons _ _ ih =>
     simp only [mapIdx.go, ih, Array.size_push, Nat.add_succ, length_cons, Nat.add_comm]
 
+@[simp] theorem mapIdx_concat {l : List α} {e : α} :
+    mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] := by
+  unfold mapIdx
+  rw [mapIdx_go_append]
+  simp only [mapIdx.go, Array.size_toArray, mapIdx_go_length, length_nil, Nat.add_zero,
+    Array.push_toList]
+
+@[simp] theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a] := by
+  simpa using mapIdx_concat (l := [])
+
 theorem length_mapIdx_go : ∀ {l : List α} {arr : Array β},
     (mapIdx.go f l arr).length = l.length + arr.size
   | [], _ => by simp [mapIdx.go]
@@ -261,15 +112,6 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
   rw [← getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)]
   simp
 
-@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : Fin l.length → α → β} {g : Nat → α → β}
-    (h : ∀ (i : Fin l.length), f i l[i] = g i l[i]) :
-    l.mapFinIdx f = l.mapIdx g := by
-  simp_all [mapFinIdx_eq_iff]
-
-theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} :
-    l.mapIdx f = l.mapFinIdx (fun i => f i) := by
-  simp [mapFinIdx_eq_mapIdx]
-
 theorem mapIdx_eq_enum_map {l : List α} :
     l.mapIdx f = l.enum.map (Function.uncurry f) := by
   ext1 i
@@ -288,16 +130,9 @@ theorem mapIdx_append {K L : List α} :
   | nil => rfl
   | cons _ _ ih => simp [ih (f := fun i => f (i + 1)), Nat.add_assoc]
 
-@[simp] theorem mapIdx_concat {l : List α} {e : α} :
-    mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] := by
-  simp [mapIdx_append]
-
-theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a] := by
-  simp
-
 @[simp]
 theorem mapIdx_eq_nil_iff {l : List α} : List.mapIdx f l = [] ↔ l = [] := by
-  rw [List.mapIdx_eq_enum_map, List.map_eq_nil_iff, List.enum_eq_nil_iff]
+  rw [List.mapIdx_eq_enum_map, List.map_eq_nil_iff, List.enum_eq_nil]
 
 theorem mapIdx_ne_nil_iff {l : List α} :
     List.mapIdx f l ≠ [] ↔ l ≠ [] := by
@@ -305,8 +140,13 @@ theorem mapIdx_ne_nil_iff {l : List α} :
 
 theorem exists_of_mem_mapIdx {b : β} {l : List α}
     (h : b ∈ mapIdx f l) : ∃ (i : Nat) (h : i < l.length), f i l[i] = b := by
-  rw [mapIdx_eq_mapFinIdx] at h
-  simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h
+  rw [mapIdx_eq_enum_map] at h
+  replace h := exists_of_mem_map h
+  simp only [Prod.exists, mk_mem_enum_iff_getElem?, Function.uncurry_apply_pair] at h
+  obtain ⟨i, b, h, rfl⟩ := h
+  rw [getElem?_eq_some_iff] at h
+  obtain ⟨h, rfl⟩ := h
+  exact ⟨i, h, rfl⟩
 
 @[simp] theorem mem_mapIdx {b : β} {l : List α} :
     b ∈ mapIdx f l ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] = b := by

src/Init/Data/List/Monadic.lean

@@ -5,7 +5,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.TakeDrop
-import Init.Data.List.Attach
 
 /-!
 # Lemmas about `List.mapM` and `List.forM`.
@@ -49,9 +48,6 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
 @[simp] theorem mapM_cons [Monad m] [LawfulMonad m] (f : α → m β) :
     (a :: l).mapM f = (return (← f a) :: (← l.mapM f)) := by simp [← mapM'_eq_mapM, mapM']
 
-@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f := by
-  induction l <;> simp_all
-
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} :
     (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
 
@@ -76,16 +72,6 @@ theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β)
       reverse_cons, reverse_nil, nil_append, singleton_append]
     simp [bind_pure_comp]
 
-/-! ### 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 [*]
-
 /-! ### forM -/
 
 -- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
@@ -103,6 +89,9 @@ theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂
 
 /-! ### forIn' -/
 
+@[simp] theorem forIn'_nil [Monad m] (f : (a : α) → a ∈ [] → β → m (ForInStep β)) (b : β) : forIn' [] b f = pure b :=
+  rfl
+
 theorem forIn'_loop_congr [Monad m] {as bs : List α}
     {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
     {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
@@ -133,11 +122,6 @@ theorem forIn'_loop_congr [Monad m] {as bs : List α}
     intros
     rfl
 
-@[simp] theorem forIn_cons [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) :
-    forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f := by
-  have := forIn'_cons (a := a) (as := as) (fun a' _ b => f a' b) b
-  simpa only [forIn'_eq_forIn]
-
 @[congr] theorem forIn'_congr [Monad m] {as bs : List α} (w : as = bs)
     {b b' : β} (hb : b = b')
     {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
@@ -165,65 +149,6 @@ theorem forIn'_loop_congr [Monad m] {as bs : List α}
           intro a m b
           exact h a (mem_cons_of_mem _ m) b
 
-/--
-We can express a for loop over a list as a fold,
-in which whenever we reach `.done b` we keep that value through the rest of the fold.
--/
-theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
-    (l : List α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
-    forIn' l init f = ForInStep.value <$>
-      l.attach.foldlM (fun b a => match b with
-        | .yield b => f a.1 a.2 b
-        | .done b => pure (.done b)) (ForInStep.yield init) := by
-  induction l generalizing init with
-  | nil => simp
-  | cons a as ih =>
-    simp only [forIn'_cons, attach_cons, foldlM_cons, _root_.map_bind]
-    congr 1
-    funext x
-    match x with
-    | .done b =>
-      clear ih
-      dsimp
-      induction as with
-      | nil => simp
-      | cons a as ih =>
-        simp only [attach_cons, map_cons, map_map, Function.comp_def, foldlM_cons, pure_bind]
-        specialize ih (fun a m b => f a (by
-          simp only [mem_cons] at m
-          rcases m with rfl|m
-          · apply mem_cons_self
-          · exact mem_cons_of_mem _ (mem_cons_of_mem _ m)) b)
-        simp [ih, List.foldlM_map]
-    | .yield b =>
-      simp [ih, List.foldlM_map]
-
-/--
-We can express a for loop over a list as a fold,
-in which whenever we reach `.done b` we keep that value through the rest of the fold.
--/
-theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
-    (f : α → β → m (ForInStep β)) (init : β) (l : List α) :
-    forIn l init f = ForInStep.value <$>
-      l.foldlM (fun b a => match b with
-        | .yield b => f a b
-        | .done b => pure (.done b)) (ForInStep.yield init) := by
-  induction l generalizing init with
-  | nil => simp
-  | cons a as ih =>
-    simp only [foldlM_cons, bind_pure_comp, forIn_cons, _root_.map_bind]
-    congr 1
-    funext x
-    match x with
-    | .done b =>
-      clear ih
-      dsimp
-      induction as with
-      | nil => simp
-      | cons a as ih => simp [ih]
-    | .yield b =>
-      simp [ih]
-
 /-! ### allM -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
@@ -236,4 +161,14 @@ 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/Range.lean

@@ -169,7 +169,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
 theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp
 
 theorem pairwise_lt_range (n : Nat) : Pairwise (· < ·) (range n) := by
-  simp +decide only [range_eq_range', pairwise_lt_range']
+  simp (config := {decide := true}) only [range_eq_range', pairwise_lt_range']
 
 theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) :=
   Pairwise.imp Nat.le_of_lt (pairwise_lt_range _)
@@ -177,10 +177,10 @@ theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) :=
 theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by
   apply List.ext_getElem
   · simp
-  · simp +contextual [getElem_take, Nat.lt_min]
+  · simp (config := { contextual := true }) [getElem_take, Nat.lt_min]
 
 theorem nodup_range (n : Nat) : Nodup (range n) := by
-  simp +decide only [range_eq_range', nodup_range']
+  simp (config := {decide := true}) only [range_eq_range', nodup_range']
 
 @[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by
@@ -430,10 +430,7 @@ theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
 /-! ### enum -/
 
 @[simp]
-theorem enum_eq_nil_iff {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
-
-@[deprecated enum_eq_nil_iff (since := "2024-11-04")]
-theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enum_eq_nil_iff
+theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
 
 @[simp] theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rfl
 

src/Init/Data/List/OfFn.lean

@@ -1,55 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Kim Morrison
--/
-prelude
-import Init.Data.List.Basic
-import Init.Data.Fin.Fold
-
-/-!
-# Theorems about `List.ofFn`
--/
-
-namespace List
-
-/--
-`ofFn f` with `f : fin n → α` returns the list whose ith element is `f i`
-```
-ofFn f = [f 0, f 1, ... , f (n - 1)]
-```
--/
-def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []
-
-@[simp]
-theorem length_ofFn (f : Fin n → α) : (ofFn f).length = n := by
-  simp only [ofFn]
-  induction n with
-  | zero => simp
-  | succ n ih => simp [Fin.foldr_succ, ih]
-
-@[simp]
-protected theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length) :
-    (ofFn f)[i] = f ⟨i, by simp_all⟩ := by
-  simp only [ofFn]
-  induction n generalizing i with
-  | zero => simp at h
-  | succ n ih =>
-    match i with
-    | 0 => simp [Fin.foldr_succ]
-    | i+1 =>
-      simp only [Fin.foldr_succ]
-      apply ih
-      simp_all
-
-@[simp]
-protected theorem getElem?_ofFn (f : Fin n → α) (i) : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
-  if h : i < (ofFn f).length
-  then by
-    rw [getElem?_eq_getElem h, List.getElem_ofFn]
-    · simp only [length_ofFn] at h; simp [h]
-  else by
-    rw [dif_neg] <;>
-    simpa using h
-
-end List

src/Init/Data/List/Pairwise.lean

@@ -76,11 +76,11 @@ theorem pairwise_of_forall {l : List α} (H : ∀ x y, R x y) : Pairwise R l :=
 
 theorem Pairwise.and_mem {l : List α} :
     Pairwise R l ↔ Pairwise (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l :=
-  Pairwise.iff_of_mem <| by simp +contextual
+  Pairwise.iff_of_mem <| by simp (config := { contextual := true })
 
 theorem Pairwise.imp_mem {l : List α} :
     Pairwise R l ↔ Pairwise (fun x y => x ∈ l → y ∈ l → R x y) l :=
-  Pairwise.iff_of_mem <| by simp +contextual
+  Pairwise.iff_of_mem <| by simp (config := { contextual := true })
 
 theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pairwise R l)
     (h₃ : l.Pairwise (flip R)) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y := by

src/Init/Data/List/Sublist.lean

@@ -116,7 +116,7 @@ fun s => Subset.trans s <| subset_append_right _ _
 theorem replicate_subset {n : Nat} {a : α} {l : List α} : replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l := by
   induction n with
   | zero => simp
-  | succ n ih => simp +contextual [replicate_succ, ih, cons_subset]
+  | succ n ih => simp (config := {contextual := true}) [replicate_succ, ih, cons_subset]
 
 theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆ replicate n a ↔ ∀ x ∈ l, x = a := by
   induction l with
@@ -835,7 +835,7 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
       simpa using ⟨0, by simp⟩
     | cons b l₂ =>
       simp only [cons_append, cons_prefix_cons, ih]
-      rw (occs := .pos [2]) [← Nat.and_forall_add_one]
+      rw (config := {occs := .pos [2]}) [← Nat.and_forall_add_one]
       simp [Nat.succ_lt_succ_iff, eq_comm]
 
 theorem isPrefix_iff_getElem {l₁ l₂ : List α} :

src/Init/Data/Nat/Dvd.lean

@@ -92,7 +92,7 @@ protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
   rw [Nat.mul_comm, Nat.mul_div_cancel' H]
 
 @[simp] theorem mod_mod_of_dvd (a : Nat) (h : c ∣ b) : a % b % c = a % c := by
-  rw (occs := .pos [2]) [← mod_add_div a b]
+  rw (config := {occs := .pos [2]}) [← mod_add_div a b]
   have ⟨x, h⟩ := h
   subst h
   rw [Nat.mul_assoc, add_mul_mod_self_left]

src/Init/Data/Nat/Lemmas.lean

@@ -651,8 +651,8 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
   | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
 
 theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
-  rw (occs := .pos [1]) [← mod_add_div a n]
-  rw (occs := .pos [1]) [← mod_add_div b n]
+  rw (config := {occs := .pos [1]}) [← mod_add_div a n]
+  rw (config := {occs := .pos [1]}) [← mod_add_div b n]
   rw [Nat.add_mul, Nat.mul_add, Nat.mul_add,
     Nat.mul_assoc, Nat.mul_assoc, ← Nat.mul_add n, add_mul_mod_self_left,
     Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]
@@ -873,10 +873,6 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
 theorem log2_lt (h : n ≠ 0) : n.log2 < k ↔ n < 2 ^ k := by
   rw [← Nat.not_le, ← Nat.not_le, le_log2 h]
 
-@[simp]
-theorem log2_two_pow : (2 ^ n).log2 = n := by
-  apply Nat.eq_of_le_of_lt_succ <;> simp [le_log2, log2_lt, NeZero.ne, Nat.pow_lt_pow_iff_right]
-
 theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_refl _)
 
 theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=

src/Init/Data/Option/Instances.lean

@@ -86,6 +86,4 @@ instance : ForIn' m (Option α) α inferInstance where
       match ← f a rfl init with
       | .done r | .yield r => return r
 
--- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
-
 end Option

src/Init/Data/Range.lean

@@ -20,6 +20,21 @@ instance : Membership Nat Range where
 namespace Range
 universe u v
 
+@[inline] protected def forIn {β : Type u} {m : Type u → Type v} [Monad m] (range : Range) (init : β) (f : Nat → β → m (ForInStep β)) : m β :=
+  -- pass `stop` and `step` separately so the `range` object can be eliminated through inlining
+  let rec @[specialize] loop (fuel i stop step : Nat) (b : β) : m β := do
+    if i ≥ stop then
+      return b
+    else match fuel with
+     | 0   => pure b
+     | fuel+1 => match (← f i b) with
+        | ForInStep.done b  => pure b
+        | ForInStep.yield b => loop fuel (i + step) stop step b
+  loop range.stop range.start range.stop range.step init
+
+instance : ForIn m Range Nat where
+  forIn := Range.forIn
+
 @[inline] protected def forIn' {β : Type u} {m : Type u → Type v} [Monad m] (range : Range) (init : β) (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop (start stop step : Nat) (f : (i : Nat) → start ≤ i ∧ i < stop → β → m (ForInStep β)) (fuel i : Nat) (hl : start ≤ i) (b : β) : m β := do
     if hu : i < stop then
@@ -35,8 +50,6 @@ universe u v
 instance : ForIn' m Range Nat inferInstance where
   forIn' := Range.forIn'
 
--- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
-
 @[inline] protected def forM {m : Type u → Type v} [Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit :=
   let rec @[specialize] loop (fuel i stop step : Nat) : m PUnit := do
     if i ≥ stop then

src/Init/Data/SInt.lean

@@ -1,11 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Init.Data.SInt.Basic
-
-/-!
-This module contains the definitions and basic theory about signed fixed width integer types.
--/

src/Init/Data/SInt/Basic.lean

@@ -1,116 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Init.Data.UInt.Basic
-
-/-!
-This module contains the definition of signed fixed width integer types as well as basic arithmetic
-and bitwise operations on top of it.
--/
-
-
-/--
-The type of signed 8-bit integers. This type has special support in the
-compiler to make it actually 8 bits rather than wrapping a `Nat`.
--/
-structure Int8 where
-  /--
-  Obtain the `UInt8` that is 2's complement equivalent to the `Int8`.
-  -/
-  toUInt8 : UInt8
-
-/-- The size of type `Int8`, that is, `2^8 = 256`. -/
-abbrev Int8.size : Nat := 256
-
-/--
-Obtain the `BitVec` that contains the 2's complement representation of the `Int8`.
--/
-@[inline] def Int8.toBitVec (x : Int8) : BitVec 8 := x.toUInt8.toBitVec
-
-@[extern "lean_int8_of_int"]
-def Int8.ofInt (i : @& Int) : Int8 := ⟨⟨BitVec.ofInt 8 i⟩⟩
-@[extern "lean_int8_of_int"]
-def Int8.ofNat (n : @& Nat) : Int8 := ⟨⟨BitVec.ofNat 8 n⟩⟩
-abbrev Int.toInt8 := Int8.ofInt
-abbrev Nat.toInt8 := Int8.ofNat
-@[extern "lean_int8_to_int"]
-def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
-@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
-@[extern "lean_int8_neg"]
-def Int8.neg (i : Int8) : Int8 := ⟨⟨-i.toBitVec⟩⟩
-
-instance : ToString Int8 where
-  toString i := toString i.toInt
-
-instance : OfNat Int8 n := ⟨Int8.ofNat n⟩
-instance : Neg Int8 where
-  neg := Int8.neg
-
-@[extern "lean_int8_add"]
-def Int8.add (a b : Int8) : Int8 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
-@[extern "lean_int8_sub"]
-def Int8.sub (a b : Int8) : Int8 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
-@[extern "lean_int8_mul"]
-def Int8.mul (a b : Int8) : Int8 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
-@[extern "lean_int8_div"]
-def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
-@[extern "lean_int8_mod"]
-def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.smod a.toBitVec b.toBitVec⟩⟩
-@[extern "lean_int8_land"]
-def Int8.land (a b : Int8) : Int8 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
-@[extern "lean_int8_lor"]
-def Int8.lor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
-@[extern "lean_int8_xor"]
-def Int8.xor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
-@[extern "lean_int8_shift_left"]
-def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (mod b 8).toBitVec⟩⟩
-@[extern "lean_int8_shift_right"]
-def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (mod b 8).toBitVec⟩⟩
-@[extern "lean_int8_complement"]
-def Int8.complement (a : Int8) : Int8 := ⟨⟨~~~a.toBitVec⟩⟩
-
-@[extern "lean_int8_dec_eq"]
-def Int8.decEq (a b : Int8) : Decidable (a = b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ =>
-    if h : n = m then
-      isTrue <| h ▸ rfl
-    else
-      isFalse (fun h' => Int8.noConfusion h' (fun h' => absurd h' h))
-
-def Int8.lt (a b : Int8) : Prop := a.toBitVec.slt b.toBitVec
-def Int8.le (a b : Int8) : Prop := a.toBitVec.sle b.toBitVec
-
-instance : Inhabited Int8 where
-  default := 0
-
-instance : Add Int8         := ⟨Int8.add⟩
-instance : Sub Int8         := ⟨Int8.sub⟩
-instance : Mul Int8         := ⟨Int8.mul⟩
-instance : Mod Int8         := ⟨Int8.mod⟩
-instance : Div Int8         := ⟨Int8.div⟩
-instance : LT Int8          := ⟨Int8.lt⟩
-instance : LE Int8          := ⟨Int8.le⟩
-instance : Complement Int8  := ⟨Int8.complement⟩
-instance : AndOp Int8       := ⟨Int8.land⟩
-instance : OrOp Int8        := ⟨Int8.lor⟩
-instance : Xor Int8         := ⟨Int8.xor⟩
-instance : ShiftLeft Int8   := ⟨Int8.shiftLeft⟩
-instance : ShiftRight Int8  := ⟨Int8.shiftRight⟩
-instance : DecidableEq Int8 := Int8.decEq
-
-@[extern "lean_int8_dec_lt"]
-def Int8.decLt (a b : Int8) : Decidable (a < b) :=
-  inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
-
-@[extern "lean_int8_dec_le"]
-def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
-  inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
-
-instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
-instance (a b : Int8) : Decidable (a ≤ b) := Int8.decLe a b
-instance : Max Int8 := maxOfLe
-instance : Min Int8 := minOfLe

src/Init/Data/Sum/Lemmas.lean

@@ -17,11 +17,11 @@ open Function
 
 namespace Sum
 
-protected theorem «forall» {p : α ⊕ β → Prop} :
+@[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₂⟩
 
-protected theorem «exists» {p : α ⊕ β → Prop} :
+@[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⟩
@@ -116,7 +116,7 @@ theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
 
 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.forall]
+  simp [funext_iff]
 
 /-! ### `Sum.map` -/
 

src/Init/Data/UInt/Basic.lean

@@ -19,8 +19,8 @@ def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint8_mod"]
 def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[deprecated UInt8.mod (since := "2024-09-23")]
-def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.val n⟩
+@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
+def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint8_land"]
 def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint8_lor"]
@@ -79,8 +79,8 @@ def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint16_mod"]
 def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[deprecated UInt16.mod (since := "2024-09-23")]
-def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.val n⟩
+@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
+def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint16_land"]
 def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint16_lor"]
@@ -141,8 +141,8 @@ def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint32_mod"]
 def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[deprecated UInt32.mod (since := "2024-09-23")]
-def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.val n⟩
+@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
+def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint32_land"]
 def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint32_lor"]
@@ -184,8 +184,8 @@ def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint64_mod"]
 def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[deprecated UInt64.mod (since := "2024-09-23")]
-def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.val n⟩
+@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
+def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint64_land"]
 def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint64_lor"]
@@ -243,8 +243,8 @@ def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
 def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
 @[extern "lean_usize_mod"]
 def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
-@[deprecated USize.mod (since := "2024-09-23")]
-def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.val n⟩
+@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
+def USize.modn (a : USize) (n : @& Nat) : USize := ⟨Fin.modn a.val n⟩
 @[extern "lean_usize_land"]
 def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_usize_lor"]

src/Init/Meta.lean

@@ -7,7 +7,6 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
-import Init.Syntax
 import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
@@ -443,7 +442,7 @@ def unsetTrailing (stx : Syntax) : Syntax :=
   if h : i < a.size then
     let v := a[i]
     match f v with
-    | some v => some <| a.set i v h
+    | some v => some <| a.set ⟨i, h⟩ v
     | none   => updateFirst a f (i+1)
   else
     none
@@ -630,9 +629,6 @@ def mkStrLit (val : String) (info := SourceInfo.none) : StrLit :=
 def mkNumLit (val : String) (info := SourceInfo.none) : NumLit :=
   mkLit numLitKind val info
 
-def mkNatLit (val : Nat) (info := SourceInfo.none) : NumLit :=
-  mkLit numLitKind (toString val) info
-
 def mkScientificLit (val : String) (info := SourceInfo.none) : TSyntax scientificLitKind :=
   mkLit scientificLitKind val info
 
@@ -1413,87 +1409,64 @@ namespace Parser
 
 namespace Tactic
 
-/--
-Extracts the items from a tactic configuration,
-either a `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, or these wrapped in null nodes.
--/
-partial def getConfigItems (c : Syntax) : TSyntaxArray ``configItem :=
-  if c.isOfKind nullKind then
-    c.getArgs.flatMap getConfigItems
-  else
-    match c with
-    | `(optConfig| $items:configItem*) => items
-    | `(config| (config := $_)) => #[⟨c⟩] -- handled by mkConfigItemViews
-    | _ => #[]
-
-def mkOptConfig (items : TSyntaxArray ``configItem) : TSyntax ``optConfig :=
-  ⟨Syntax.node1 .none ``optConfig (mkNullNode items)⟩
-
-/--
-Appends two tactic configurations.
-The configurations can be `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`,
-or these wrapped in null nodes (for example because the syntax is `(config)?`).
--/
-def appendConfig (cfg cfg' : Syntax) : TSyntax ``optConfig :=
-  mkOptConfig <| getConfigItems cfg ++ getConfigItems cfg'
-
-/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
+/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
 This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
 which only unfolds `@[reducible]` definitions). -/
-macro "erw" c:optConfig s:rwRuleSeq loc:(location)? : tactic => do
-  `(tactic| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq $(loc)?)
+macro "erw" s:rwRuleSeq loc:(location)? : tactic =>
+  `(tactic| rw (config := { transparency := .default }) $s $(loc)?)
 
 syntax simpAllKind := atomic(" (" &"all") " := " &"true" ")"
 syntax dsimpKind   := atomic(" (" &"dsimp") " := " &"true" ")"
 
 macro (name := declareSimpLikeTactic) doc?:(docComment)?
     "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?)
-    ppSpace tacName:ident ppSpace tacToken:str ppSpace cfg:optConfig : command => do
+    ppSpace tacName:ident ppSpace tacToken:str ppSpace updateCfg:term : command => do
   let (kind, tkn, stx) ←
     if opt.raw.isNone then
-      pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
     else if opt.raw[0].getKind == ``simpAllKind then
-      pure (← `(``simpAll), ← `("simp_all"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
+      pure (← `(``simpAll), ← `("simp_all"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
     else
-      pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
   `($stx:command
     @[macro $tacName] def expandSimp : Macro := fun s => do
-      let cfg ← `(optConfig| $cfg)
+      let c ← match s[1][0] with
+        | `(config| (config := $$c)) => `(config| (config := $updateCfg $$c))
+        | _ => `(config| (config := $updateCfg {}))
       let s := s.setKind $kind
       let s := s.setArg 0 (mkAtomFrom s[0] $tkn (canonical := true))
-      let s := s.setArg 1 (appendConfig s[1] cfg)
-      let s := s.mkSynthetic
-      return s)
+      let r := s.setArg 1 (mkNullNode #[c])
+      return r)
 
 /-- `simp!` is shorthand for `simp` with `autoUnfold := true`.
 This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
-declare_simp_like_tactic simpAutoUnfold "simp! " (autoUnfold := true)
+declare_simp_like_tactic simpAutoUnfold "simp! " fun (c : Lean.Meta.Simp.Config) => { c with autoUnfold := true }
 
 /-- `simp_arith` is shorthand for `simp` with `arith := true` and `decide := true`.
 This enables the use of normalization by linear arithmetic. -/
-declare_simp_like_tactic simpArith "simp_arith " (arith := true) (decide := true)
+declare_simp_like_tactic simpArith "simp_arith " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, decide := true }
 
 /-- `simp_arith!` is shorthand for `simp_arith` with `autoUnfold := true`.
 This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
-declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " (arith := true) (autoUnfold := true) (decide := true)
+declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, autoUnfold := true, decide := true }
 
 /-- `simp_all!` is shorthand for `simp_all` with `autoUnfold := true`.
 This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
-declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " (autoUnfold := true)
+declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with autoUnfold := true }
 
 /-- `simp_all_arith` combines the effects of `simp_all` and `simp_arith`. -/
-declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " (arith := true) (decide := true)
+declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, decide := true }
 
 /-- `simp_all_arith!` combines the effects of `simp_all`, `simp_arith` and `simp!`. -/
-declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " (arith := true) (autoUnfold := true) (decide := true)
+declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, autoUnfold := true, decide := true }
 
 /-- `dsimp!` is shorthand for `dsimp` with `autoUnfold := true`.
 This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
-declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " (autoUnfold := true)
+declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean.Meta.DSimp.Config) => { c with autoUnfold := true }
 
 end Tactic
 

src/Init/Notation.lean

@@ -341,19 +341,16 @@ macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
 notation:50 a:50 " ∉ " b:50 => ¬ (a ∈ b)
 
 @[inherit_doc] infixr:67 " :: " => List.cons
-@[inherit_doc] infixr:100 " <$> " => Functor.map
-@[inherit_doc] infixl:55  " >>= " => Bind.bind
-@[inherit_doc HOrElse.hOrElse]   syntax:20 term:21 " <|> " term:20 : term
+@[inherit_doc HOrElse.hOrElse] syntax:20 term:21 " <|> " term:20 : term
 @[inherit_doc HAndThen.hAndThen] syntax:60 term:61 " >> " term:60 : term
-@[inherit_doc Seq.seq]           syntax:60 term:60 " <*> " term:61 : term
-@[inherit_doc SeqLeft.seqLeft]   syntax:60 term:60 " <* " term:61 : term
-@[inherit_doc SeqRight.seqRight] syntax:60 term:60 " *> " term:61 : term
+@[inherit_doc] infixl:55  " >>= " => Bind.bind
+@[inherit_doc] notation:60 a:60 " <*> " b:61 => Seq.seq a fun _ : Unit => b
+@[inherit_doc] notation:60 a:60 " <* " b:61 => SeqLeft.seqLeft a fun _ : Unit => b
+@[inherit_doc] notation:60 a:60 " *> " b:61 => SeqRight.seqRight a fun _ : Unit => b
+@[inherit_doc] infixr:100 " <$> " => Functor.map
 
 macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
 macro_rules | `($x >> $y)  => `(binop_lazy% HAndThen.hAndThen $x $y)
-macro_rules | `($x <*> $y) => `(Seq.seq $x fun _ : Unit => $y)
-macro_rules | `($x <* $y)  => `(SeqLeft.seqLeft $x fun _ : Unit => $y)
-macro_rules | `($x *> $y)  => `(SeqRight.seqRight $x fun _ : Unit => $y)
 
 namespace Lean
 

src/Init/Prelude.lean

@@ -2688,6 +2688,35 @@ def Array.mkArray7 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : α) : Arr
 def Array.mkArray8 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : α) : Array α :=
   ((((((((mkEmpty 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈
 
+/--
+Set an element in an array without bounds checks, using a `Fin` index.
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
+@[extern "lean_array_fset"]
+def Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α where
+  toList := a.toList.set i.val v
+
+/--
+Set an element in an array, or do nothing if the index is out of bounds.
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
+@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=
+  dite (LT.lt i a.size) (fun h => a.set ⟨i, h⟩ v) (fun _ => a)
+
+/--
+Set an element in an array, or panic if the index is out of bounds.
+
+This will perform the update destructively provided that `a` has a reference
+count of 1 when called.
+-/
+@[extern "lean_array_set"]
+def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
+  Array.setD a i v
+
 /-- Slower `Array.append` used in quotations. -/
 protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) : Array α :=
   let rec loop (i : Nat) (j : Nat) (as : Array α) : Array α :=
@@ -3608,13 +3637,6 @@ def appendCore : Name → Name → Name
 
 end Name
 
-/-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option. -/
-def defaultMaxRecDepth := 512
-
-/-- The message to display on stack overflow. -/
-def maxRecDepthErrorMessage : String :=
-  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
-
 /-! # Syntax -/
 
 /-- Source information of tokens. -/
@@ -3947,6 +3969,24 @@ def getId : Syntax → Name
   | ident _ _ val _ => val
   | _               => Name.anonymous
 
+/--
+Updates the argument list without changing the node kind.
+Does nothing for non-`node` nodes.
+-/
+def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
+  match stx with
+  | node info k _ => node info k args
+  | stx           => stx
+
+/--
+Updates the `i`'th argument of the syntax.
+Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
+-/
+def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
+  match stx with
+  | node info k args => node info k (args.setD i arg)
+  | stx              => stx
+
 /-- Retrieve the left-most node or leaf's info in the Syntax tree. -/
 partial def getHeadInfo? : Syntax → Option SourceInfo
   | atom info _   => some info
@@ -4383,6 +4423,13 @@ main module and current macro scope.
   bind getCurrMacroScope fun scp =>
   pure (Lean.addMacroScope mainModule n scp)
 
+/-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option. -/
+def defaultMaxRecDepth := 512
+
+/-- The message to display on stack overflow. -/
+def maxRecDepthErrorMessage : String :=
+  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
+
 namespace Syntax
 
 /-- Is this syntax a null `node`? -/

src/Init/PropLemmas.lean

@@ -643,11 +643,11 @@ theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop)
     (@ite _ p h q (decide p)) = (decide p && q) := by
   split <;> simp_all
 
-@[deprecated ite_then_decide_self (since := "2024-08-29")]
+@[deprecated ite_then_decide_self]
 theorem ite_true_decide_same (p : Prop) [Decidable p] (b : Bool) :
   (if p then decide p else b) = (decide p || b) := ite_then_decide_self p b
 
-@[deprecated ite_false_decide_same (since := "2024-08-29")]
+@[deprecated ite_false_decide_same]
 theorem ite_false_decide_same (p : Prop) [Decidable p] (b : Bool) :
   (if p then b else decide p) = (decide p && b) := ite_else_decide_self p b
 

src/Init/SimpLemmas.lean

@@ -54,13 +54,6 @@ theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂
     : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) := by
   subst h₁; simp [← h₂]
 
-theorem forall_prop_congr_dom {p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ → Prop) :
-    (∀ a : p₁, q a) = (∀ a : p₂, q (h.substr a)) :=
-  h ▸ rfl
-
-theorem pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a :=
-  (funext h : β = β') ▸ rfl
-
 theorem let_congr {α : Sort u} {β : Sort v} {a a' : α} {b b' : α → β}
     (h₁ : a = a') (h₂ : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a'; b' x) :=
   h₁ ▸ (funext h₂ : b = b') ▸ rfl

src/Init/Syntax.lean

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

src/Init/Tactics.lean

@@ -417,27 +417,7 @@ It synthesizes a value of any target type by typeclass inference.
 -/
 macro "infer_instance" : tactic => `(tactic| exact inferInstance)
 
-/--
-`+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
--/
-syntax posConfigItem := "+" noWs ident
-/--
-`-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
--/
-syntax negConfigItem := "-" noWs ident
-/--
-`(opt := val)` sets the `opt` configuration option to `val`.
-
-As a special case, `(config := ...)` sets the entire configuration.
--/
-syntax valConfigItem := atomic(" (" notFollowedBy(&"discharger" <|> &"disch") (ident <|> &"config")) " := " withoutPosition(term) ")"
-/-- A configuration item for a tactic configuration. -/
-syntax configItem := posConfigItem <|> negConfigItem <|> valConfigItem
-
-/-- Configuration options for tactics. -/
-syntax optConfig := (colGt configItem)*
-
-/-- Optional configuration option for tactics. (Deprecated. Replace `(config)?` with `optConfig`.) -/
+/-- Optional configuration option for tactics -/
 syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
 
 /-- The `*` location refers to all hypotheses and the goal. -/
@@ -494,25 +474,25 @@ This provides a convenient way to unfold `e`.
   list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
   can also be used, to signify the target of the goal.
 
-Using `rw (occs := .pos L) [e]`,
+Using `rw (config := {occs := .pos L}) [e]`,
 where `L : List Nat`, you can control which "occurrences" are rewritten.
 (This option applies to each rule, so usually this will only be used with a single rule.)
 Occurrences count from `1`.
 At each allowed occurrence, arguments of the rewrite rule `e` may be instantiated,
 restricting which later rewrites can be found.
 (Disallowed occurrences do not result in instantiation.)
-`(occs := .neg L)` allows skipping specified occurrences.
+`{occs := .neg L}` allows skipping specified occurrences.
 -/
-syntax (name := rewriteSeq) "rewrite" optConfig rwRuleSeq (location)? : tactic
+syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
 
 /--
 `rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 -/
-macro (name := rwSeq) "rw " c:optConfig s:rwRuleSeq l:(location)? : tactic =>
+macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
   match s with
   | `(rwRuleSeq| [$rs,*]%$rbrak) =>
     -- We show the `rfl` state on `]`
-    `(tactic| (rewrite $c [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
+    `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
 /-- `rwa` is short-hand for `rw; assumption`. -/
@@ -581,14 +561,14 @@ non-dependent hypotheses. It has many variants:
 - `simp [*] at *` simplifies target and all (propositional) hypotheses using the
   other hypotheses.
 -/
-syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
+syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 /--
 `simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target
 are simplified multiple times until no simplification is applicable.
 Only non-dependent propositional hypotheses are considered.
 -/
-syntax (name := simpAll) "simp_all" optConfig (discharger)? (&" only")?
+syntax (name := simpAll) "simp_all" (config)? (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic
 
 /--
@@ -596,7 +576,7 @@ The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but o
 applies theorems that hold by reflexivity. Thus, the result is guaranteed to be
 definitionally equal to the input.
 -/
-syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
+syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 
 /--
@@ -618,7 +598,7 @@ def dsimpArg := simpErase.binary `orelse simpLemma
 syntax dsimpArgs := " [" dsimpArg,* "]"
 
 /-- The common arguments of `simp?` and `simp?!`. -/
-syntax simpTraceArgsRest := optConfig (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
+syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
 
 /--
 `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
@@ -637,7 +617,7 @@ syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic
 macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest)
 
 /-- The common arguments of `simp_all?` and `simp_all?!`. -/
-syntax simpAllTraceArgsRest := optConfig (discharger)? (&" only")? (dsimpArgs)?
+syntax simpAllTraceArgsRest := (config)? (discharger)? (&" only")? (dsimpArgs)?
 
 @[inherit_doc simpTrace]
 syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
@@ -646,7 +626,7 @@ syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
 macro tk:"simp_all?!" rest:simpAllTraceArgsRest : tactic => `(tactic| simp_all?%$tk ! $rest)
 
 /-- The common arguments of `dsimp?` and `dsimp?!`. -/
-syntax dsimpTraceArgsRest := optConfig (&" only")? (dsimpArgs)? (ppSpace location)?
+syntax dsimpTraceArgsRest := (config)? (&" only")? (dsimpArgs)? (ppSpace location)?
 
 @[inherit_doc simpTrace]
 syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
@@ -655,7 +635,7 @@ syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
 macro tk:"dsimp?!" rest:dsimpTraceArgsRest : tactic => `(tactic| dsimp?%$tk ! $rest)
 
 /-- The arguments to the `simpa` family tactics. -/
-syntax simpaArgsRest := optConfig (discharger)? &" only "? (simpArgs)? (" using " term)?
+syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (" using " term)?
 
 /--
 This is a "finishing" tactic modification of `simp`. It has two forms.
@@ -1168,7 +1148,8 @@ a natural subtraction appearing in a hypothesis, and try again.
 
 The options
 ```
-omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
+omega (config :=
+  { splitDisjunctions := true, splitNatSub := true, splitNatAbs := true, splitMinMax := true })
 ```
 can be used to:
 * `splitDisjunctions`: split any disjunctions found in the context,
@@ -1178,7 +1159,7 @@ can be used to:
 * `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
 Currently, all of these are on by default.
 -/
-syntax (name := omega) "omega" optConfig : tactic
+syntax (name := omega) "omega" (config)? : tactic
 
 /--
 `bv_omega` is `omega` with an additional preprocessor that turns statements about `BitVec` into statements about `Nat`.
@@ -1291,7 +1272,7 @@ example (a b : Nat)
 
 See also `norm_cast`.
 -/
-syntax (name := pushCast) "push_cast" optConfig (discharger)? (&" only")?
+syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
 /--
@@ -1367,7 +1348,7 @@ See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for th
 Both `apply_assumption` and `apply_rules` are implemented via these hooks.
 -/
 syntax (name := solveByElim)
-  "solve_by_elim" "*"? optConfig (&" only")? (args)? (using_)? : tactic
+  "solve_by_elim" "*"? (config)? (&" only")? (args)? (using_)? : tactic
 
 /--
 `apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
@@ -1390,7 +1371,7 @@ You can pass a further configuration via the syntax `apply_rules (config := {...
 The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
 -/
 syntax (name := applyAssumption)
-  "apply_assumption" optConfig (&" only")? (args)? (using_)? : tactic
+  "apply_assumption" (config)? (&" only")? (args)? (using_)? : tactic
 
 /--
 `apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
@@ -1415,7 +1396,7 @@ You can bound the iteration depth using the syntax `apply_rules (config := {maxD
 Unlike `solve_by_elim`, `apply_rules` does not perform backtracking, and greedily applies
 a lemma from the list until it gets stuck.
 -/
-syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
+syntax (name := applyRules) "apply_rules" (config)? (&" only")? (args)? (using_)? : tactic
 end SolveByElim
 
 /--
@@ -1509,11 +1490,6 @@ have been simplified by using the modifier `↓`. Here is an example
 @[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=
 ```
 
-You can instruct the simplifier to rewrite the lemma from right-to-left:
-```lean
-attribute @[simp ←] and_assoc
-```
-
 When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
 The equational theorems of function are applied at very low priority (100 and below).
 If there are several with the same priority, it is uses the "most recent one". Example:
@@ -1525,7 +1501,7 @@ If there are several with the same priority, it is uses the "most recent one". E
   cases d <;> rfl
 ```
 -/
-syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
 
 /--
 Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
@@ -1614,7 +1590,7 @@ where `i < arr.size` is in the context) and `simp_arith` and `omega`
 syntax "get_elem_tactic_trivial" : tactic
 
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; done)
+macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
 
 /--

src/Init/TacticsExtra.lean

@@ -70,11 +70,11 @@ macro_rules
 /--
 Rewrites with the given rules, normalizing casts prior to each step.
 -/
-syntax "rw_mod_cast" optConfig rwRuleSeq (location)? : tactic
+syntax "rw_mod_cast" (config)? rwRuleSeq (location)? : tactic
 macro_rules
-  | `(tactic| rw_mod_cast $cfg:optConfig [$rules,*] $[$loc]?) => do
+  | `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
     let tacs ← rules.getElems.mapM fun rule =>
-      `(tactic| (norm_cast at *; rw $cfg [$rule] $[$loc]?))
+      `(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
     `(tactic| ($[$tacs]*))
 
 /--

src/Init/WFTactics.lean

@@ -16,14 +16,15 @@ user, and this tactic should no longer be necessary. Calls to `simp_wf` can be r
 by plain calls to `simp`.
 -/
 macro "simp_wf" : tactic =>
-  `(tactic| try simp +unfoldPartialApp +zetaDelta [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
+  `(tactic| try simp (config := { unfoldPartialApp := true, zetaDelta := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
 /--
 This tactic is used internally by lean before presenting the proof obligations from a well-founded
 definition to the user via `decreasing_by`. It is not necessary to use this tactic manually.
 -/
 macro "clean_wf" : tactic =>
-  `(tactic| simp +unfoldPartialApp +zetaDelta -failIfUnchanged
+  `(tactic| simp
+     (config := { unfoldPartialApp := true, zetaDelta := true, failIfUnchanged := false })
      only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel,
            WellFoundedRelation.rel, sizeOf_nat, reduceCtorEq])
 
@@ -36,7 +37,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
 -/
 syntax "decreasing_trivial" : tactic
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp +arith -failIfUnchanged) <;> done)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
 

src/Lean/Class.lean

@@ -87,7 +87,7 @@ def hasOutParams (env : Environment) (declName : Name) : Bool :=
   incorrect. This transformation would be counterintuitive to users since
   we would implicitly treat these regular parameters as `outParam`s.
 -/
-private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except MessageData (Array Nat) :=
+private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except String (Array Nat) :=
   match type with
   | .forallE _ d b bi =>
     let addOutParam (_ : Unit) :=
@@ -102,7 +102,7 @@ private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (ou
         /- See issue #1852 for a motivation for `bi.isInstImplicit` -/
         addOutParam ()
       else
-        Except.error m!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`"
+        Except.error s!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`"
     else
       checkOutParam (i+1) outParamFVarIds outParams b
   | _ => return outParams
@@ -149,13 +149,13 @@ and it must be the name of constant in `env`.
 `declName` must be a inductive datatype or axiom.
 Recall that all structures are inductive datatypes.
 -/
-def addClass (env : Environment) (clsName : Name) : Except MessageData Environment := do
+def addClass (env : Environment) (clsName : Name) : Except String Environment := do
   if isClass env clsName then
-    throw m!"class has already been declared '{.ofConstName clsName true}'"
+    throw s!"class has already been declared '{clsName}'"
   let some decl := env.find? clsName
-    | throw m!"unknown declaration '{clsName}'"
+    | throw s!"unknown declaration '{clsName}'"
   unless decl matches .inductInfo .. | .axiomInfo .. do
-    throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant"
+    throw s!"invalid 'class', declaration '{clsName}' must be inductive datatype, structure, or constant"
   let outParams ← checkOutParam 0 #[] #[] decl.type
   return classExtension.addEntry env { name := clsName, outParams }
 

src/Lean/Compiler/IR/ElimDeadVars.lean

@@ -13,7 +13,7 @@ partial def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
   let rec reshape (bs : Array FnBody) (b : FnBody) (used : IndexSet) :=
     if bs.isEmpty then b
     else
-      let curr := bs.back!
+      let curr := bs.back
       let bs   := bs.pop
       let keep (_ : Unit) :=
         let used := curr.collectFreeIndices used

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1075,7 +1075,7 @@ def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmct
 def ensureHasDefault' (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
   else
-    let last := alts.back!
+    let last := alts.back
     let alts := alts.pop
     alts.push (Alt.default last.body)
 

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -56,7 +56,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
   let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
   if bs.size < 2 then done ()
   else
-    let b := bs.back!
+    let b := bs.back
     match b with
     | .vdecl _ _ (.sproj _ _ _) _ => keepInstr b
     | .vdecl _ _ (.uproj _ _) _   => keepInstr b

src/Lean/Compiler/IR/PushProj.lean

@@ -13,7 +13,7 @@ namespace Lean.IR
 partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array IndexSet) (ctx : Array FnBody) (ctxF : IndexSet) : Array FnBody × Array Alt :=
   if bs.isEmpty then (ctx.reverse, alts)
   else
-    let b    := bs.back!
+    let b    := bs.back
     let bs   := bs.pop
     let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts)
     let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF)

src/Lean/Compiler/IR/SimpCase.lean

@@ -13,8 +13,8 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
   else if alts.size < 2 then alts
   else
-    let last := alts.back!
-    let alts := alts.pop
+    let last := alts.back;
+    let alts := alts.pop;
     alts.push (Alt.default last.body)
 
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do

src/Lean/Compiler/LCNF/InferType.lean

@@ -168,12 +168,13 @@ mutual
       /- TODO: after we erase universe variables, we can just extract a better type using just `structName` and `idx`. -/
       return erasedExpr
     else
-      matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal =>
-        let structTypeArgs := structType.getAppArgs
-        if structVal.numParams + structVal.numIndices != structTypeArgs.size then
+      matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal =>
+        let n := structVal.numParams
+        let structParams := structType.getAppArgs
+        if n != structParams.size then
           failed ()
         else do
-          let mut ctorType ← inferAppType (mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[:structVal.numParams])
+          let mut ctorType ← inferAppType (mkAppN (mkConst ctorVal.name structLvls) structParams)
           for _ in [:idx] do
             match ctorType with
             | .forallE _ _ body _ =>

src/Lean/Data/HashMap.lean

@@ -271,11 +271,11 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
 
-attribute [deprecated Std.HashMap (since := "2024-08-08")] HashMap
-attribute [deprecated Std.HashMap.Raw (since := "2024-08-08")] HashMapImp
-attribute [deprecated Std.HashMap.Raw.empty (since := "2024-08-08")] mkHashMapImp
-attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] mkHashMap
-attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] HashMap.empty
-attribute [deprecated Std.HashMap.ofList (since := "2024-08-08")] HashMap.ofList
+attribute [deprecated Std.HashMap] HashMap
+attribute [deprecated Std.HashMap.Raw] HashMapImp
+attribute [deprecated Std.HashMap.Raw.empty] mkHashMapImp
+attribute [deprecated Std.HashMap.empty] mkHashMap
+attribute [deprecated Std.HashMap.empty] HashMap.empty
+attribute [deprecated Std.HashMap.ofList] HashMap.ofList
 
 end Lean.HashMap

src/Lean/Data/HashSet.lean

@@ -219,8 +219,8 @@ def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :
   t.fold (init := s) fun s a => s.insert a
   -- We don't use `insertMany` here because it gives weird universes.
 
-attribute [deprecated Std.HashSet (since := "2024-08-08")] HashSet
-attribute [deprecated Std.HashSet.Raw (since := "2024-08-08")] HashSetImp
-attribute [deprecated Std.HashSet.Raw.empty (since := "2024-08-08")] mkHashSetImp
-attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] mkHashSet
-attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] HashSet.empty
+attribute [deprecated Std.HashSet] HashSet
+attribute [deprecated Std.HashSet.Raw] HashSetImp
+attribute [deprecated Std.HashSet.Raw.empty] mkHashSetImp
+attribute [deprecated Std.HashSet.empty] mkHashSet
+attribute [deprecated Std.HashSet.empty] HashSet.empty

src/Lean/Data/KVMap.lean

@@ -177,7 +177,7 @@ def updateSyntax (m : KVMap) (k : Name) (f : Syntax → Syntax) : KVMap :=
 
 @[inline] protected def forIn.{w, w'} {δ : Type w} {m : Type w → Type w'} [Monad m]
   (kv : KVMap) (init : δ) (f : Name × DataValue → δ → m (ForInStep δ)) : m δ :=
-  forIn kv.entries init f
+  kv.entries.forIn init f
 
 instance : ForIn m KVMap (Name × DataValue) where
   forIn := KVMap.forIn

src/Lean/Data/Lsp/Utf16.lean

@@ -70,7 +70,7 @@ private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
   else if text.positions.isEmpty then
     0
   else
-    text.positions.back!
+    text.positions.back
 
 /-- Computes an UTF-8 offset into `text.source`
 from an LSP-style 0-indexed (ln, col) position. -/

src/Lean/Data/PersistentArray.lean

@@ -159,7 +159,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
           let cs' := cs'.pop
           if cs'.isEmpty then (some l, emptyArray) else (some l, cs')
         else
-          (some l, cs'.set idx (node newLast) (by simp only [cs', Array.size_set]; omega))
+          (some l, cs'.set (Array.size_set cs idx _ ▸ idx) (node newLast))
     else
       (none, emptyArray)
   | leaf vs   => (some vs, emptyArray)

src/Lean/Data/Position.lean

@@ -66,12 +66,12 @@ partial def ofString (s : String) : FileMap :=
       let i := s.next i
       if c == '\n' then loop i (line+1) (ps.push i)
       else loop i line ps
-  loop 0 1 #[0]
+  loop 0 1 (#[0])
 
 partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
   match fmap with
   | { source := str, positions := ps } =>
-    if ps.size >= 2 && pos <= ps.back! then
+    if ps.size >= 2 && pos <= ps.back then
       let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
         if i == pos || str.atEnd i then c
         else toColumn (str.next i) (c+1)
@@ -84,14 +84,14 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
           if pos == posM then { line := fmap.getLine m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
-      loop 0 (ps.size - 1)
+      loop 0 (ps.size -1)
     else if ps.isEmpty then
       ⟨0, 0⟩
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
       -- which would violate `toPositionAux`'s invariant.
       -- Can also happen with EOF errors, which are not strictly inside the file.
-      ⟨fmap.getLastLine, (pos - ps.back!).byteIdx⟩
+      ⟨fmap.getLastLine, (pos - ps.back).byteIdx⟩
 
 /-- Convert a `Lean.Position` to a `String.Pos`. -/
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
@@ -101,7 +101,7 @@ def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
     else if text.positions.isEmpty then
       0
     else
-      text.positions.back!
+      text.positions.back
   String.Iterator.nextn ⟨text.source, colPos⟩ pos.column |>.pos
 
 /--

src/Lean/Data/RBMap.lean

@@ -298,14 +298,9 @@ instance : ForIn m (RBMap α β cmp) (α × β) where
   | ⟨leaf, _⟩ => true
   | _         => false
 
-/-- Returns a `List` of the key/value pairs in order. -/
 @[specialize] def toList : RBMap α β cmp → List (α × β)
   | ⟨t, _⟩ => t.revFold (fun ps k v => (k, v)::ps) []
 
-/-- Returns an `Array` of the key/value pairs in order. -/
-@[specialize] def toArray : RBMap α β cmp → Array (α × β)
-  | ⟨t, _⟩ => t.fold (fun ps k v => ps.push (k, v)) #[]
-
 /-- Returns the kv pair `(a,b)` such that `a ≤ k` for all keys in the RBMap. -/
 @[inline] protected def min : RBMap α β cmp → Option (α × β)
   | ⟨t, _⟩ =>

src/Lean/Data/Xml/Parser.lean

@@ -463,7 +463,7 @@ mutual
     let mut res := #[]
     for x in xs do
       if res.size > 0 then
-        match res.back!, x with
+        match res.back, x with
         | Content.Character x, Content.Character y => res := res.set! (res.size - 1) (Content.Character $ x ++ y)
         | _, x => res := res.push x
       else res := res.push x

src/Lean/Elab/App.lean

@@ -595,22 +595,6 @@ mutual
       elabAndAddNewArg argName arg
       main
     | _ =>
-      if (← read).ellipsis && (← readThe Term.Context).inPattern then
-        /-
-        In patterns, ellipsis should always be an implicit argument, even if it is an optparam or autoparam.
-        This prevents examples such as the one in #4555 from failing:
-        ```lean
-        match e with
-        | .internal .. => sorry
-        | .error .. => sorry
-        ```
-        The `internal` has an optparam (`| internal (id : InternalExceptionId) (extra : KVMap := {})`).
-
-        We may consider having ellipsis suppress optparams and autoparams in general.
-        We avoid doing so for now since it's possible to opt-out of them (for example with `.internal (extra := _) ..`)
-        but it's not possible to opt-in.
-        -/
-        return ← addImplicitArg argName
       let argType ← getArgExpectedType
       match (← read).explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
       | false, some defVal, _  => addNewArg argName defVal; main
@@ -1151,29 +1135,24 @@ private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermE
   throwError "{msg}{indentExpr e}\nhas type{indentExpr eType}"
 
 /--
-`findMethod? S fName` tries the following for each namespace `S'` in the resolution order for `S`:
-- If `env` contains `S' ++ fName`, returns `(S', S' ++ fName)`
-- Otherwise if `env` contains private name `prv` for `S' ++ fName`, returns `(S', prv)`
+`findMethod? env S fName`.
+- If `env` contains `S ++ fName`, return `(S, S++fName)`
+- Otherwise if `env` contains private name `prv` for `S ++ fName`, return `(S, prv)`, o
+- Otherwise for each parent structure `S'` of  `S`, we try `findMethod? env S' fname`
 -/
-private partial def findMethod? (structName fieldName : Name) : MetaM (Option (Name × Name)) := do
-  let env ← getEnv
-  let find? structName' : MetaM (Option (Name × Name)) := do
-    let fullName := structName' ++ fieldName
-    if env.contains fullName then
-      return some (structName', fullName)
+private partial def findMethod? (env : Environment) (structName fieldName : Name) : Option (Name × Name) :=
+  let fullName := structName ++ fieldName
+  match env.find? fullName with
+  | some _ => some (structName, fullName)
+  | none   =>
     let fullNamePrv := mkPrivateName env fullName
-    if env.contains fullNamePrv then
-      return some (structName', fullNamePrv)
-    return none
-  -- Optimization: the first element of the resolution order is `structName`,
-  -- so we can skip computing the resolution order in the common case
-  -- of the name resolving in the `structName` namespace.
-  find? structName <||> do
-    let resolutionOrder ← if isStructure env structName then getStructureResolutionOrder structName else pure #[structName]
-    for h : i in [1:resolutionOrder.size] do
-      if let some res ← find? resolutionOrder[i] then
-        return res
-    return none
+    match env.find? fullNamePrv with
+    | some _ => some (structName, fullNamePrv)
+    | none   =>
+      if isStructure env structName then
+        (getParentStructures env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
+      else
+        none
 
 /--
   Return `some (structName', fullName)` if `structName ++ fieldName` is an alias for `fullName`, and
@@ -1209,23 +1188,23 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     if idx == 0 then
       throwError "invalid projection, index must be greater than 0"
     let env ← getEnv
-    let failK _ := throwLValError e eType "invalid projection, structure expected"
-    matchConstStructure eType.getAppFn failK fun _ _ ctorVal => do
-      let numFields := ctorVal.numFields
-      if idx - 1 < numFields then
-        if isStructure env structName then
-          let fieldNames := getStructureFields env structName
-          return LValResolution.projFn structName structName fieldNames[idx - 1]!
-        else
-          /- `structName` was declared using `inductive` command.
-            So, we don't projection functions for it. Thus, we use `Expr.proj` -/
-          return LValResolution.projIdx structName (idx - 1)
+    unless isStructureLike env structName do
+      throwLValError e eType "invalid projection, structure expected"
+    let numFields := getStructureLikeNumFields env structName
+    if idx - 1 < numFields then
+      if isStructure env structName then
+        let fieldNames := getStructureFields env structName
+        return LValResolution.projFn structName structName fieldNames[idx - 1]!
       else
-        throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
+        /- `structName` was declared using `inductive` command.
+           So, we don't projection functions for it. Thus, we use `Expr.proj` -/
+        return LValResolution.projIdx structName (idx - 1)
+    else
+      throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
   | some structName, LVal.fieldName _ fieldName _ _ =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do
-      if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
+      if let some (baseStructName, fullName) := findMethod? env structName (.mkSimple fieldName) then
         return LValResolution.const baseStructName structName fullName
       else if let some (structName', fullName) := findMethodAlias? env structName (.mkSimple fieldName) then
         return LValResolution.const structName' structName' fullName
@@ -1411,17 +1390,19 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       loop f lvals
     | LValResolution.projFn baseStructName structName fieldName =>
       let f ← mkBaseProjections baseStructName structName f
-      let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
-      if isPrivateNameFromImportedModule (← getEnv) info.projFn then
-        throwError "field '{fieldName}' from structure '{structName}' is private"
-      let projFn ← mkConst info.projFn
-      let projFn ← addProjTermInfo lval.getRef projFn
-      if lvals.isEmpty then
-        let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
-        elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
+      if let some info := getFieldInfo? (← getEnv) baseStructName fieldName then
+        if isPrivateNameFromImportedModule (← getEnv) info.projFn then
+          throwError "field '{fieldName}' from structure '{structName}' is private"
+        let projFn ← mkConst info.projFn
+        let projFn ← addProjTermInfo lval.getRef projFn
+        if lvals.isEmpty then
+          let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
+          elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
+        else
+          let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
+          loop f lvals
       else
-        let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
-        loop f lvals
+        unreachable!
     | LValResolution.const baseStructName structName constName =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
       let projFn ← mkConst constName

src/Lean/Elab/Arg.lean

@@ -39,7 +39,7 @@ partial def expandArgs (args : Array Syntax) : MetaM (Array NamedArg × Array Ar
   let (args, ellipsis) :=
     if args.isEmpty then
       (args, false)
-    else if args.back!.isOfKind ``Lean.Parser.Term.ellipsis then
+    else if args.back.isOfKind ``Lean.Parser.Term.ellipsis then
       (args.pop, true)
     else
       (args, false)

src/Lean/Elab/BuiltinCommand.lean

@@ -424,87 +424,4 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
 @[builtin_command_elab Parser.Command.eoi] def elabEoi : CommandElab := fun _ =>
   return
 
-@[builtin_command_elab Parser.Command.where] def elabWhere : CommandElab := fun _ => do
-  let scope ← getScope
-  let mut msg : Array MessageData := #[]
-  -- Noncomputable
-  if scope.isNoncomputable then
-    msg := msg.push <| ← `(command| noncomputable section)
-  -- Namespace
-  if !scope.currNamespace.isAnonymous then
-    msg := msg.push <| ← `(command| namespace $(mkIdent scope.currNamespace))
-  -- Open namespaces
-  if let some openMsg ← describeOpenDecls scope.openDecls.reverse then
-    msg := msg.push openMsg
-  -- Universe levels
-  if !scope.levelNames.isEmpty then
-    let levels := scope.levelNames.reverse.map mkIdent
-    msg := msg.push <| ← `(command| universe $levels.toArray*)
-  -- Variables
-  if !scope.varDecls.isEmpty then
-    let varDecls : Array (TSyntax `Lean.Parser.Term.bracketedBinder) := scope.varDecls.map (⟨·.raw.unsetTrailing⟩)
-    msg := msg.push <| ← `(command| variable $varDecls*)
-  -- Included variables
-  if !scope.includedVars.isEmpty then
-    msg := msg.push <| ← `(command| include $(scope.includedVars.toArray.map (mkIdent ·.eraseMacroScopes))*)
-  -- Options
-  if let some optionsMsg ← describeOptions scope.opts then
-    msg := msg.push optionsMsg
-  if msg.isEmpty then
-    logInfo m!"-- In root namespace with initial scope"
-  else
-    logInfo <| MessageData.joinSep msg.toList "\n\n"
-where
-  /--
-  'Delaborate' open declarations.
-  Current limitations:
-  - does not check whether or not successive namespaces need `_root_`
-  - does not combine commands with `renaming` clauses into a single command
-  -/
-  describeOpenDecls (ds : List OpenDecl) : CommandElabM (Option MessageData) := do
-    let mut lines : Array MessageData := #[]
-    let mut simple : Array Name := #[]
-    let flush (lines : Array MessageData) (simple : Array Name) : CommandElabM (Array MessageData × Array Name) := do
-      if simple.isEmpty then
-        return (lines, simple)
-      else
-        return (lines.push <| ← `(command| open $(simple.map mkIdent)*), #[])
-    for d in ds do
-      match d with
-      | .explicit id decl =>
-        (lines, simple) ← flush lines simple
-        let ns := decl.getPrefix
-        let «from» := Name.mkSimple decl.getString!
-        lines := lines.push <| ← `(command| open $(mkIdent ns) renaming $(mkIdent «from») → $(mkIdent id))
-      | .simple ns ex =>
-        if ex == [] then
-          simple := simple.push ns
-        else
-          (lines, simple) ← flush lines simple
-          lines := lines.push <| ← `(command| open $(mkIdent ns) hiding $[$(ex.toArray.map mkIdent)]*)
-    (lines, _) ← flush lines simple
-    return if lines.isEmpty then none else MessageData.joinSep lines.toList "\n"
-
-  describeOptions (opts : Options) : CommandElabM (Option MessageData) := do
-    let mut lines : Array MessageData := #[]
-    let decls ← getOptionDecls
-    for (name, val) in opts do
-      let (isSet, isUnknown) :=
-        match decls.find? name with
-        | some decl => (decl.defValue != val, false)
-        | none      => (true, true)
-      if isSet then
-        let cmd : TSyntax `command ←
-          match val with
-          | .ofBool true  => `(set_option $(mkIdent name) true)
-          | .ofBool false => `(set_option $(mkIdent name) false)
-          | .ofString str => `(set_option $(mkIdent name) $(Syntax.mkStrLit str))
-          | .ofNat n      => `(set_option $(mkIdent name) $(Syntax.mkNatLit n))
-          | _             => `(set_option $(mkIdent name) 0 /- unrepresentable value -/)
-        if isUnknown then
-          lines := lines.push m!"-- {cmd} -- unknown option"
-        else
-          lines := lines.push cmd
-    return if lines.isEmpty then none else MessageData.joinSep lines.toList "\n"
-
 end Lean.Elab.Command

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -136,8 +136,8 @@ private def mkFormat (e : Expr) : MetaM Expr := do
     if eval.derive.repr.get (← getOptions) then
       if let .const name _ := (← whnf (← inferType e)).getAppFn then
         try
-          trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{.ofConstName name}'"
-          liftCommandElabM do applyDerivingHandlers ``Repr #[name]
+          trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{MessageData.ofConstName name}'"
+          liftCommandElabM do applyDerivingHandlers ``Repr #[name] none
           resetSynthInstanceCache
           return ← mkRepr e
         catch ex =>
@@ -201,9 +201,9 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
           discard <| withLocalDeclD `x ty fun x => mkT x
         catch _ =>
           throw ex
-        throwError m!"unable to synthesize '{.ofConstName ``MonadEval}' instance \
+        throwError m!"unable to synthesize '{MessageData.ofConstName ``MonadEval}' instance \
           to adapt{indentExpr (← inferType e)}\n\
-          to '{.ofConstName ``IO}' or '{.ofConstName ``CommandElabM}'."
+          to '{MessageData.ofConstName ``IO}' or '{MessageData.ofConstName ``CommandElabM}'."
       addAndCompileExprForEval declName r (allowSorry := bang)
       -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
       let r ← toMessageData <$> evalConst t declName

src/Lean/Elab/BuiltinNotation.lean

@@ -226,7 +226,7 @@ partial def mkPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back!
+  loop (elems.size - 1) elems.back
 
 /-- Return syntax `PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkPPairs (elems : Array Term) : MacroM Term :=
@@ -238,7 +238,7 @@ partial def mkPPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back!
+  loop (elems.size - 1) elems.back
 
 /-- Return syntax `MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
 partial def mkMPairs (elems : Array Term) : MacroM Term :=
@@ -250,7 +250,7 @@ partial def mkMPairs (elems : Array Term) : MacroM Term :=
       loop i acc
     else
       pure acc
-  loop (elems.size - 1) elems.back!
+  loop (elems.size - 1) elems.back
 
 
 open Parser in

src/Lean/Elab/Calc.lean

@@ -10,11 +10,10 @@ namespace Lean.Elab.Term
 open Meta
 
 /--
-Decompose `e` into `(r, a, b)`.
+  Decompose `e` into `(r, a, b)`.
 
-Remark: it assumes the last two arguments are explicit.
--/
-def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
+  Remark: it assumes the last two arguments are explicit. -/
+def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
   if e.getAppNumArgs < 2 then
     return none
   else
@@ -69,102 +68,56 @@ where
     | .node i k as => return .node i k (← as.mapM go)
     | _ => set false; return t
 
-/-- View of a `calcStep`. -/
-structure CalcStepView where
-  ref : Syntax
-  /-- A relation term like `a ≤ b` -/
-  term : Term
-  /-- A proof of `term` -/
-  proof : Term
-  deriving Inhabited
-
-def mkCalcFirstStepView (step0 : TSyntax ``calcFirstStep) : TermElabM CalcStepView :=
+def getCalcFirstStep (step0 : TSyntax ``calcFirstStep) : TermElabM (TSyntax ``calcStep) :=
   withRef step0 do
   match step0  with
-  | `(calcFirstStep| $term:term)      => return { ref := step0, term := ← `($term = _), proof := ← ``(rfl)}
-  | `(calcFirstStep| $term := $proof) => return { ref := step0, term, proof}
+  | `(calcFirstStep| $term:term) =>
+    `(calcStep| $term = _ := rfl)
+  | `(calcFirstStep| $term := $proof) =>
+    `(calcStep| $term := $proof)
   | _ => throwUnsupportedSyntax
 
-def mkCalcStepViews (steps : TSyntax ``calcSteps) : TermElabM (Array CalcStepView) :=
+def getCalcSteps (steps : TSyntax ``calcSteps) : TermElabM (Array (TSyntax ``calcStep)) :=
   match steps with
   | `(calcSteps|
         $step0:calcFirstStep
         $rest*) => do
-    let mut steps := #[← mkCalcFirstStepView step0]
-    for step in rest do
-      let `(calcStep| $term := $proof) := step | throwUnsupportedSyntax
-      steps := steps.push { ref := step, term, proof }
-    return steps
-  | _ => throwUnsupportedSyntax
+    let step0 ← getCalcFirstStep step0
+    pure (#[step0] ++ rest)
+  | _ => unreachable!
 
-def elabCalcSteps (steps : Array CalcStepView) : TermElabM (Expr × Expr) := do
+def elabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
   let mut result? := none
   let mut prevRhs? := none
-  for step in steps do
+  for step in ← getCalcSteps steps do
+    let `(calcStep| $pred := $proofTerm) := step | unreachable!
     let type ← elabType <| ← do
       if let some prevRhs := prevRhs? then
-        annotateFirstHoleWithType step.term (← inferType prevRhs)
+        annotateFirstHoleWithType pred (← inferType prevRhs)
       else
-        pure step.term
+        pure pred
     let some (_, lhs, rhs) ← getCalcRelation? type |
-      throwErrorAt step.term "invalid 'calc' step, relation expected{indentExpr type}"
+      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr type}"
     if let some prevRhs := prevRhs? then
       unless (← isDefEqGuarded lhs prevRhs) do
-        throwErrorAt step.term "\
-          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
-          but previous right-hand side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}"
-    let proof ← withFreshMacroScope do elabTermEnsuringType step.proof type
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}" -- "
+    let proof ← withFreshMacroScope do elabTermEnsuringType proofTerm type
     result? := some <| ← do
       if let some (result, resultType) := result? then
         synthesizeSyntheticMVarsUsingDefault
-        withRef step.term do mkCalcTrans result resultType proof type
+        withRef pred do mkCalcTrans result resultType proof type
       else
         pure (proof, type)
     prevRhs? := rhs
-  synthesizeSyntheticMVarsUsingDefault
-  return result?.get!
-
-def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) : MetaM α := do
-  let resultType := (← instantiateMVars (← inferType result)).headBeta
-  let some (r, lhs, rhs) ← getCalcRelation? resultType | unreachable!
-  if let some (er, elhs, erhs) ← getCalcRelation? expectedType then
-    if ← isDefEqGuarded r er then
-      let mut failed := false
-      unless ← isDefEqGuarded lhs elhs do
-        logErrorAt steps[0]!.term m!"\
-          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
-          but is expected to be{indentD m!"{elhs} : {← inferType elhs}"}"
-        failed := true
-      unless ← isDefEqGuarded rhs erhs do
-        logErrorAt steps.back!.term m!"\
-          invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {← inferType rhs}"}\n\
-          but is expected to be{indentD m!"{erhs} : {← inferType erhs}"}"
-        failed := true
-      if failed then
-        throwAbortTerm
-  throwTypeMismatchError "'calc' expression" expectedType resultType result
-
-/-!
-Warning! It is *very* tempting to try to improve `calc` so that it makes use of the expected type
-to unify with the LHS and RHS.
-Two people have already re-implemented `elabCalcSteps` trying to do so and then reverted the changes,
-not being aware of examples like https://github.com/leanprover/lean4/issues/2073
-
-The problem is that the expected type might need to be unfolded to get an accurate LHS and RHS.
-(Consider `≤` vs `≥`. Users expect to be able to use `calc` to prove `≥` using chained `≤`!)
-Furthermore, the types of the LHS and RHS do not need to be the same (consider `x ∈ S` as a relation),
-so we also cannot use the expected LHS and RHS as type hints.
--/
+  return result?.get!.1
 
 /-- Elaborator for the `calc` term mode variant. -/
 @[builtin_term_elab Lean.calc]
-def elabCalc : TermElab
-  | `(calc%$tk $steps:calcSteps), expectedType? => withRef tk do
-    let steps ← mkCalcStepViews steps
-    let (result, _) ← elabCalcSteps steps
-    ensureHasTypeWithErrorMsgs expectedType? result
-      (mkImmedErrorMsg := fun _ => throwCalcFailure steps)
-      (mkErrorMsg := fun _ => throwCalcFailure steps)
-  | _, _ => throwUnsupportedSyntax
+def elabCalc : TermElab := fun stx expectedType? => do
+  let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
+  let result ← elabCalcSteps steps
+  synthesizeSyntheticMVarsUsingDefault
+  let result ← ensureHasType expectedType? result
+  return result
 
 end Lean.Elab.Term

src/Lean/Elab/DeclModifiers.lean

@@ -25,19 +25,19 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
   if env.contains declName then
     addInfo declName
     match privateToUserName? declName with
-    | none          => throwError "'{.ofConstName declName true}' has already been declared"
-    | some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared"
+    | none          => throwError "'{declName}' has already been declared"
+    | some declName => throwError "private declaration '{declName}' has already been declared"
   if isReservedName env declName then
     throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
-    throwError "a private declaration '{.ofConstName declName true}' has already been declared"
+    throwError "a private declaration '{declName}' has already been declared"
   match privateToUserName? declName with
   | none => pure ()
   | some declName =>
     if env.contains declName then
       addInfo declName
-      throwError "a non-private declaration '{.ofConstName declName true}' has already been declared"
+      throwError "a non-private declaration '{declName}' has already been declared"
 
 /-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/
 inductive Visibility where

src/Lean/Elab/Deriving/Basic.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Wojciech Nawrocki
 -/
 prelude
 import Lean.Elab.Command
-import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab
 open Command
@@ -56,17 +55,13 @@ def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool :=
       safety      := info.safety
     }
     addInstance instName AttributeKind.global (eval_prio default)
-    addDeclarationRangesFromSyntax instName (← getRef)
     return true
   catch _ =>
     return false
 
 end Term
 
-def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
-
-/-- Deprecated - `DerivingHandler` no longer assumes arguments -/
-@[deprecated DerivingHandler (since := "2024-09-09")]
+def DerivingHandler := (typeNames : Array Name) → (args? : Option (TSyntax ``Parser.Term.structInst)) → CommandElabM Bool
 def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
 
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) ← IO.mkRef {}
@@ -76,21 +71,25 @@ as well as the syntax of a `with` argument, if present.
 
 For example, `deriving instance Foo with fooArgs for Bar, Baz` invokes
 ``fooHandler #[`Bar, `Baz] `(fooArgs)``. -/
-def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
+def registerDerivingHandlerWithArgs (className : Name) (handler : DerivingHandler) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
   derivingHandlersRef.modify fun m => match m.find? className with
     | some handlers => m.insert className (handler :: handlers)
     | none => m.insert className [handler]
 
+/-- Like `registerBuiltinDerivingHandlerWithArgs` but ignoring any `with` argument. -/
+def registerDerivingHandler (className : Name) (handler : DerivingHandlerNoArgs) : IO Unit := do
+  registerDerivingHandlerWithArgs className fun typeNames _ => handler typeNames
+
 def defaultHandler (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
   throwError "default handlers have not been implemented yet, class: '{className}' types: {typeNames}"
 
-def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
+def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Unit := do
   match (← derivingHandlersRef.get).find? className with
   | some handlers =>
     for handler in handlers do
-      if (← handler typeNames) then
+      if (← handler typeNames args?) then
         return ()
     defaultHandler className typeNames
   | none => defaultHandler className typeNames
@@ -100,16 +99,16 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
     Term.processDefDeriving className declName
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
-  | `(deriving instance $[$classes],* for $[$declNames],*) => do
+  | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
      let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
-     for cls in classes do
+     for cls in classes, args? in argss? do
        try
          let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
          withRef cls do
-           if declNames.size == 1 then
+           if declNames.size == 1 && args?.isNone then
              if (← tryApplyDefHandler className declNames[0]!) then
                return ()
-           applyDerivingHandlers className declNames
+           applyDerivingHandlers className declNames args?
        catch ex =>
          logException ex
   | _ => throwUnsupportedSyntax
@@ -117,19 +116,20 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
 structure DerivingClassView where
   ref : Syntax
   className : Name
+  args? : Option (TSyntax ``Parser.Term.structInst)
 
 def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
   match optDeriving with
-  | `(Parser.Command.optDeriving| deriving $[$classes],*) =>
+  | `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
     let mut ret := #[]
-    for cls in classes do
+    for cls in classes, args? in argss? do
       let className ← realizeGlobalConstNoOverloadWithInfo cls
-      ret := ret.push { ref := cls, className := className }
+      ret := ret.push { ref := cls, className := className, args? }
     return ret
   | _ => return #[]
 
 def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit :=
-  withRef view.ref do applyDerivingHandlers view.className declNames
+  withRef view.ref do applyDerivingHandlers view.className declNames view.args?
 
 builtin_initialize
   registerTraceClass `Elab.Deriving

src/Lean/Elab/Deriving/TypeName.lean

@@ -14,7 +14,7 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool
   for declName in declNames do
     let cinfo ← getConstInfo declName
     unless cinfo.levelParams.isEmpty do
-      throwError m!"{.ofConstName declName} has universe level parameters"
+      throwError m!"{mkConst declName} has universe level parameters"
     elabCommand <| ← withFreshMacroScope `(
       unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
       @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName)

src/Lean/Elab/Do.lean

@@ -801,7 +801,7 @@ private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
   else if elems.size == 1 then
     return elems[0]!
   else
-    elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
+    elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back) fun elem tuple =>
       ``(MProd.mk $elem $tuple)
 
 /-- Return `some action` if `doElem` is a `doExpr <action>`-/

src/Lean/Elab/Inductive.lean

@@ -740,7 +740,10 @@ private def getArity (indType : InductiveType) : MetaM Nat :=
   forallTelescopeReducing indType.type fun xs _ => return xs.size
 
 private def resetMaskAt (mask : Array Bool) (i : Nat) : Array Bool :=
-  mask.setD i false
+  if h : i < mask.size then
+    mask.set ⟨i, h⟩ false
+  else
+    mask
 
 /--
   Compute a bit-mask that for `indType`. The size of the resulting array `result` is the arity of `indType`.

src/Lean/Elab/Level.lean

@@ -60,11 +60,11 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
     elabLevel (stx.getArg 1)
   else if kind == ``Lean.Parser.Level.max then
     let args := stx.getArg 1 |>.getArgs
-    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl =>
       return mkLevelMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.imax then
     let args := stx.getArg 1 |>.getArgs
-    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back) fun stx lvl =>
       return mkLevelIMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.hole then
     mkFreshLevelMVar

src/Lean/Elab/PreDefinition/Basic.lean

@@ -125,7 +125,7 @@ private def reportTheoremDiag (d : TheoremVal) : TermElabM Unit := do
     if proofSize > diagnostics.threshold.proofSize.get (← getOptions) then
       let sizeMsg := MessageData.trace { cls := `size } m!"{proofSize}" #[]
       let constOccs ← d.value.numApps (threshold := diagnostics.threshold.get (← getOptions))
-      let constOccsMsg ← constOccs.mapM fun (declName, numOccs) => return MessageData.trace { cls := `occs } m!"{.ofConstName declName} ↦ {numOccs}" #[]
+      let constOccsMsg ← constOccs.mapM fun (declName, numOccs) => return MessageData.trace { cls := `occs } m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {numOccs}" #[]
       -- let info
       logInfo <| MessageData.trace { cls := `theorem } m!"{d.name}" (#[sizeMsg] ++ constOccsMsg)
 

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -62,8 +62,8 @@ def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Ex
         \n\
         This process uses multiple strategies:\n\
         - It looks for a parameter that matches the return type.\n\
-        - It tries synthesizing '{.ofConstName ``Inhabited}' and '{.ofConstName ``Nonempty}' \
-          instances for the return type, while making every parameter into a local '{.ofConstName ``Inhabited}' instance.\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, \

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

@@ -114,9 +114,8 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
   The dictionary is built using the `PProd` (`And` for inductive predicates).
   We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`.  -/
 private partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr := do
-  withTraceNode `Elab.definition.structural (return m!"{exceptEmoji ·} searching IH for {recArg} in {←inferType below}") do
-    withBelowDict below numIndParams positions fun Cs belowDict =>
-      toBelowAux Cs[fnIndex]! belowDict recArg below
+  withBelowDict below numIndParams positions fun Cs belowDict =>
+    toBelowAux Cs[fnIndex]! belowDict recArg below
 
 private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
     (below : Expr) (e : Expr) : M Expr :=

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

@@ -105,6 +105,6 @@ def IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr) :=
   auxMotives.mapM fun motive =>
     forallTelescopeReducing motive fun xs _ => do
       assert! xs.size > 0
-      mkForallFVars xs.pop (← inferType xs.back!)
+      mkForallFVars xs.pop (← inferType xs.back)
 
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -118,7 +118,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
         Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars
       -- drop trailing underscores
       let mut vars := vars
-      while ! vars.isEmpty && vars.back!.raw.isOfKind ``hole do vars := vars.pop
+      while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
       if termArg.structural then
         if vars.isEmpty then
           `(terminationBy|termination_by structural $stxBody)

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -4,15 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Data.Array
-import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.Basic
-import Lean.Elab.Tactic.Basic
-import Lean.Meta.ArgsPacker
-import Lean.Meta.ForEachExpr
-import Lean.Meta.Match.MatcherApp.Transform
-import Lean.Meta.Tactic.Cleanup
 import Lean.Util.HasConstCache
+import Lean.Meta.Match.Match
+import Lean.Meta.Tactic.Simp.Main
+import Lean.Meta.Tactic.Cleanup
+import Lean.Meta.ArgsPacker
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.RecAppSyntax
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Elab.PreDefinition.WF.Basic
+import Lean.Data.Array
 
 namespace Lean.Elab.WF
 open Meta

src/Lean/Elab/Print.lean

@@ -11,7 +11,7 @@ import Lean.Elab.Command
 namespace Lean.Elab.Command
 
 private def throwUnknownId (id : Name) : CommandElabM Unit :=
-  throwError "unknown identifier '{.ofConstName id}'"
+  throwError "unknown identifier '{mkConst id}'"
 
 private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
   match levelParams with

src/Lean/Elab/Quotation.lean

@@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
                 | $[some $ids:ident],* => $(quote inner)
                 | $[_%$ids],*          => Array.empty)
             | _ =>
-              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
+              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back
               `(Array.map (fun $(← mkTuple ids) => $(inner[0]!)) $arr)
           let arr ← if k == `sepBy then
             `(mkSepArray $arr $(getSepStxFromSplice arg))

src/Lean/Elab/StructInst.lean

@@ -434,7 +434,7 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
     | { lhs := .fieldName ref fieldName :: _,    .. } =>
       addCompletionInfo <| CompletionInfo.fieldId ref fieldName (← getLCtx) s.structName
       match findField? env s.structName fieldName with
-      | none => throwErrorAt ref "'{fieldName}' is not a field of structure '{.ofConstName s.structName}'"
+      | none => throwErrorAt ref "'{fieldName}' is not a field of structure '{MessageData.ofConstName s.structName}'"
       | some baseStructName =>
         if baseStructName == s.structName then pure field
         else match getPathToBaseStructure? env baseStructName s.structName with
@@ -826,12 +826,22 @@ 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
-  | .forallE ..   =>
-    forallTelescope e fun xs b => withReduceLCtx xs do
-      mkForallFVars xs (← reduce structNames b)
-  | .lam .. | .letE .. =>
-    lambdaLetTelescope e fun xs b => withReduceLCtx xs do
-      mkLambdaFVars (usedLetOnly := true) 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))
   | .proj _ i b   =>
     match (← Meta.project? b i) with
     | some r => reduce structNames r
@@ -861,24 +871,6 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
     | some val => if val.isMVar then pure val else reduce structNames val
     | none     => return e
   | e => return e
-where
-  /--
-  Reduce the types and values of the local variables `xs` in the local context.
-  -/
-  withReduceLCtx {α} (xs : Array Expr) (k : MetaM α) (i : Nat := 0) : MetaM α := do
-    if h : i < xs.size then
-      let fvarId := xs[i].fvarId!
-      let decl ← fvarId.getDecl
-      let type ← reduce structNames decl.type
-      let mut lctx ← getLCtx
-      if let some value := decl.value? then
-        let value ← reduce structNames value
-        lctx := lctx.modifyLocalDecl fvarId (· |>.setType type |>.setValue value)
-      else
-        lctx := lctx.modifyLocalDecl fvarId (· |>.setType type)
-      withLCtx lctx (← getLocalInstances) (withReduceLCtx xs k (i + 1))
-    else
-      k
 
 partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
   let rec loop (i : Nat) (dist : Nat) := do
@@ -894,7 +886,6 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
         | none     => setMCtx mctx; loop (i+1) (dist+1)
         | some val =>
           let val ← reduce allStructNames val
-          trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
           match val.find? fun e => (defaultMissing? e).isSome with
           | some _ => setMCtx mctx; loop (i+1) (dist+1)
           | none   =>

src/Lean/Elab/Structure.lean

@@ -20,16 +20,6 @@ import Lean.Elab.Binders
 
 namespace Lean.Elab.Command
 
-register_builtin_option structureDiamondWarning : Bool := {
-  defValue := false
-  descr    := "if true, enable warnings when a structure has diamond inheritance"
-}
-
-register_builtin_option structure.strictResolutionOrder : Bool := {
-  defValue := false
-  descr := "if true, require a strict resolution order for structures"
-}
-
 open Meta
 open TSyntax.Compat
 
@@ -44,83 +34,53 @@ structure StructCtorView where
   modifiers : Modifiers
   name      : Name
   declName  : Name
-  deriving Inhabited
 
 structure StructFieldView where
   ref        : Syntax
   modifiers  : Modifiers
   binderInfo : BinderInfo
   declName   : Name
-  /-- Ref for the field name -/
-  nameId     : Syntax
-  /-- The name of the field. (Without macro scopes.) -/
-  name       : Name
-  /-- Same as `name` but includes macro scopes. Used for field elaboration. -/
-  rawName    : Name
+  name       : Name -- The field name as it is going to be registered in the kernel. It does not include macroscopes.
+  rawName    : Name -- Same as `name` but including macroscopes.
   binders    : Syntax
   type?      : Option Syntax
   value?     : Option Syntax
 
 structure StructView where
-  ref             : Syntax
-  declId          : Syntax
-  modifiers       : Modifiers
-  isClass         : Bool -- struct-only
-  shortDeclName   : Name
-  declName        : Name
-  levelNames      : List Name
-  binders         : Syntax
-  type            : Syntax -- modified (inductive has type?)
-  parents         : Array Syntax -- struct-only
-  ctor            : StructCtorView -- struct-only
-  fields          : Array StructFieldView -- struct-only
-  derivingClasses : Array DerivingClassView
-  deriving Inhabited
-
-structure StructParentInfo where
-  ref        : Syntax
-  fvar?      : Option Expr
-  structName : Name
-  subobject  : Bool
-  type       : Expr
-  deriving Inhabited
+  ref               : Syntax
+  modifiers         : Modifiers
+  scopeLevelNames   : List Name  -- All `universe` declarations in the current scope
+  allUserLevelNames : List Name  -- `scopeLevelNames` ++ explicit universe parameters provided in the `structure` command
+  isClass           : Bool
+  declName          : Name
+  scopeVars         : Array Expr -- All `variable` declaration in the current scope
+  params            : Array Expr -- Explicit parameters provided in the `structure` command
+  parents           : Array Syntax
+  type              : Syntax
+  ctor              : StructCtorView
+  fields            : Array StructFieldView
 
 inductive StructFieldKind where
-  | newField | copiedField | fromParent
-  /-- The field is an embedded parent. -/
-  | subobject (structName : Name)
+  | newField | copiedField | fromParent | subobject
   deriving Inhabited, DecidableEq, Repr
 
 structure StructFieldInfo where
-  ref      : Syntax
   name     : Name
-  /-- Name of projection function.
-  Remark: for `fromParent` fields, `declName` is only relevant in the generation of auxiliary "default value" functions. -/
-  declName : Name
+  declName : Name -- Remark: for `fromParent` fields, `declName` is only relevant in the generation of auxiliary "default value" functions.
   fvar     : Expr
   kind     : StructFieldKind
   value?   : Option Expr := none
   deriving Inhabited, Repr
 
-structure ElabStructHeaderResult where
-  view             : StructView
-  lctx             : LocalContext
-  localInsts       : LocalInstances
-  levelNames       : List Name
-  params           : Array Expr
-  type             : Expr
-  parents          : Array StructParentInfo
-  /-- Field infos from parents. -/
-  parentFieldInfos : Array StructFieldInfo
-  deriving Inhabited
-
 def StructFieldInfo.isFromParent (info : StructFieldInfo) : Bool :=
   match info.kind with
   | StructFieldKind.fromParent => true
   | _                          => false
 
 def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool :=
-  info.kind matches StructFieldKind.subobject ..
+  match info.kind with
+  | StructFieldKind.subobject => true
+  | _                         => false
 
 private def defaultCtorName := `mk
 
@@ -201,15 +161,14 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
       throwError "invalid 'private' field in a 'private' structure"
     if fieldModifiers.isProtected && structModifiers.isPrivate then
       throwError "invalid 'protected' field in a 'private' structure"
-    let (binders, type?, value?) ←
+    let (binders, type?) ←
       if binfo == BinderInfo.default then
         let (binders, type?) := expandOptDeclSig fieldBinder[3]
         let optBinderTacticDefault := fieldBinder[4]
         if optBinderTacticDefault.isNone then
-          pure (binders, type?, none)
+          pure (binders, type?)
         else if optBinderTacticDefault[0].getKind != ``Parser.Term.binderTactic then
-          -- binderDefault := leading_parser " := " >> termParser
-          pure (binders, type?, some optBinderTacticDefault[0][1])
+          pure (binders, type?)
         else
           let binderTactic := optBinderTacticDefault[0]
           match type? with
@@ -221,10 +180,22 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
             -- It is safe to reset the binders to a "null" node since there is no value to be elaborated
             let type ← `(forall $(binders.getArgs):bracketedBinder*, $type)
             let type ← `(autoParam $type $(mkIdentFrom tac name))
-            pure (mkNullNode, some type.raw, none)
+            pure (mkNullNode, some type.raw)
       else
         let (binders, type) := expandDeclSig fieldBinder[3]
-        pure (binders, some type, none)
+        pure (binders, some type)
+    let value? ← if binfo != BinderInfo.default then
+      pure none
+    else
+      let optBinderTacticDefault := fieldBinder[4]
+      -- trace[Elab.struct] ">>> {optBinderTacticDefault}"
+      if optBinderTacticDefault.isNone then
+        pure none
+      else if optBinderTacticDefault[0].getKind == ``Parser.Term.binderTactic then
+        pure none
+      else
+        -- binderDefault := leading_parser " := " >> termParser
+        pure (some optBinderTacticDefault[0][1])
     let idents := fieldBinder[2].getArgs
     idents.foldlM (init := views) fun (views : Array StructFieldView) ident => withRef ident do
       let rawName := ident.getId
@@ -240,59 +211,16 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
         binderInfo := binfo
         declName
         name
-        nameId     := ident
         rawName
         binders
         type?
         value?
       }
 
-/-
-leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >>
-  optional (("where" <|> ":=") >> optional structCtor >> structFields) >> optDeriving
-
-where
-def «extends» := leading_parser " extends " >> sepBy1 termParser ", "
-def typeSpec := leading_parser " : " >> termParser
-def optType : Parser := optional typeSpec
-
-def structFields         := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
-def structCtor           := leading_parser try (declModifiers >> ident >> " :: ")
--/
-def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM StructView := do
-  checkValidInductiveModifier modifiers
-  let isClass   := stx[0].getKind == ``Parser.Command.classTk
-  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
-  let declId    := stx[1]
-  let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
-  addDeclarationRangesForBuiltin declName modifiers.stx stx
-  let binders   := stx[2]
-  let exts      := stx[3]
-  let parents   := if exts.isNone then #[] else exts[0][1].getSepArgs
-  let optType   := stx[4]
-  let derivingClasses ← getOptDerivingClasses stx[6]
-  let type      ← if optType.isNone then `(Sort _) else pure optType[0][1]
-  let ctor ← expandCtor stx modifiers declName
-  let fields ← expandFields stx modifiers declName
-  fields.forM fun field => do
-    if field.declName == ctor.declName then
-      throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name"
-    addDeclarationRangesFromSyntax field.declName field.ref
-  return {
-    ref := stx
-    declId
-    modifiers
-    isClass
-    shortDeclName := name
-    declName
-    levelNames
-    binders
-    type
-    parents
-    ctor
-    fields
-    derivingClasses
-  }
+private def validStructType (type : Expr) : Bool :=
+  match type with
+  | Expr.sort .. => true
+  | _            => false
 
 private def findFieldInfo? (infos : Array StructFieldInfo) (fieldName : Name) : Option StructFieldInfo :=
   infos.find? fun info => info.name == fieldName
@@ -300,12 +228,17 @@ private def findFieldInfo? (infos : Array StructFieldInfo) (fieldName : Name) :
 private def containsFieldName (infos : Array StructFieldInfo) (fieldName : Name) : Bool :=
   (findFieldInfo? infos fieldName).isSome
 
-private def replaceFieldInfo (infos : Array StructFieldInfo) (info : StructFieldInfo) : Array StructFieldInfo :=
-  infos.map fun info' =>
-    if info'.name == info.name then
-      info
+private def updateFieldInfoVal (infos : Array StructFieldInfo) (fieldName : Name) (value : Expr) : Array StructFieldInfo :=
+  infos.map fun info =>
+    if info.name == fieldName then
+      { info with value? := value  }
     else
-      info'
+      info
+
+register_builtin_option structureDiamondWarning : Bool := {
+  defValue := false
+  descr    := "enable/disable warning messages for structure diamonds"
+}
 
 /-- Return `some fieldName` if field `fieldName` of the parent structure `parentStructName` is already in `infos` -/
 private def findExistingField? (infos : Array StructFieldInfo) (parentStructName : Name) : CoreM (Option Name) := do
@@ -323,14 +256,14 @@ where
     if h : i < subfieldNames.size then
       let subfieldName := subfieldNames.get ⟨i, h⟩
       if containsFieldName infos subfieldName then
-        throwError "field '{subfieldName}' from '{.ofConstName parentStructName}' has already been declared"
+        throwError "field '{subfieldName}' from '{parentStructName}' has already been declared"
       let val  ← mkProjection parentFVar subfieldName
       let type ← inferType val
-      withLetDecl subfieldName type val fun subfieldFVar => do
+      withLetDecl subfieldName type val fun subfieldFVar =>
         /- The following `declName` is only used for creating the `_default` auxiliary declaration name when
            its default value is overwritten in the structure. If the default value is not overwritten, then its value is irrelevant. -/
         let declName := structDeclName ++ subfieldName
-        let infos := infos.push { ref := (← getRef), name := subfieldName, declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent }
+        let infos := infos.push { name := subfieldName, declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent }
         go (i+1) infos
     else
       k infos
@@ -433,7 +366,7 @@ private partial def copyDefaultValue? (fieldMap : FieldMap) (expandedStructNames
     go? (← instantiateValueLevelParams cinfo us)
 where
   failed : TermElabM (Option Expr) := do
-    logWarning m!"ignoring default value for field '{fieldName}' defined at '{.ofConstName structName}'"
+    logWarning s!"ignoring default value for field '{fieldName}' defined at '{structName}'"
     return none
 
   go? (e : Expr) : TermElabM (Option Expr) := do
@@ -469,7 +402,7 @@ where
         | some existingFieldInfo =>
           let existingFieldType ← inferType existingFieldInfo.fvar
           unless (← isDefEq fieldType existingFieldType) do
-            throwError "parent field type mismatch, field '{fieldName}' from parent '{.ofConstName parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
+            throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
           /- Remark: if structure has a default value for this field, it will be set at the `processOveriddenDefaultValues` below. -/
           copy (i+1) infos (fieldMap.insert fieldName existingFieldInfo.fvar) expandedStructNames
         | none =>
@@ -481,11 +414,10 @@ where
               let fieldDeclName := structDeclName ++ fieldName
               let fieldDeclName ← applyVisibility (← toVisibility fieldInfo) fieldDeclName
               addDocString' fieldDeclName (← findDocString? (← getEnv) fieldInfo.projFn)
-              let infos := infos.push { ref := (← getRef)
-                                        name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?,
+              let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?,
                                         kind := StructFieldKind.copiedField }
               copy (i+1) infos fieldMap expandedStructNames
-          if let some parentParentStructName := fieldInfo.subobject? then
+          if fieldInfo.subobject?.isSome then
             let fieldParentStructName ← getStructureName fieldType
             if (← findExistingField? infos fieldParentStructName).isSome then
               -- See comment at `copyDefaultValue?`
@@ -496,10 +428,8 @@ where
             else
               let subfieldNames := getStructureFieldsFlattened (← getEnv) fieldParentStructName
               let fieldName := fieldInfo.fieldName
-              withLocalDecl fieldName fieldInfo.binderInfo fieldType fun parentFVar => do
-                let infos := infos.push { ref := (← getRef)
-                                          name := fieldName, declName := structDeclName ++ fieldName, fvar := parentFVar,
-                                          kind := StructFieldKind.subobject parentParentStructName }
+              withLocalDecl fieldName fieldInfo.binderInfo fieldType fun parentFVar =>
+                let infos := infos.push { name := fieldName, declName := structDeclName ++ fieldName, fvar := parentFVar, kind := StructFieldKind.subobject }
                 processSubfields structDeclName parentFVar fieldParentStructName subfieldNames infos fun infos =>
                   copy (i+1) infos (fieldMap.insert fieldName parentFVar) expandedStructNames
           else
@@ -536,24 +466,20 @@ private partial def mkToParentName (parentStructName : Name) (p : Name → Bool)
       if p curr then curr else go (i+1)
     go 1
 
-private partial def elabParents (view : StructView)
-    (k : Array StructFieldInfo → Array StructParentInfo → TermElabM α) : TermElabM α := do
+private partial def withParents (view : StructView) (k : Array StructFieldInfo → Array Expr → TermElabM α) : TermElabM α := do
   go 0 #[] #[]
 where
-  go (i : Nat) (infos : Array StructFieldInfo) (parents : Array StructParentInfo) : TermElabM α := do
+  go (i : Nat) (infos : Array StructFieldInfo) (copiedParents : Array Expr) : TermElabM α := do
     if h : i < view.parents.size then
-      let parent := view.parents[i]
-      withRef parent do
-      let type ← Term.elabType parent
-      let parentType ← whnf type
+      let parentStx := view.parents.get ⟨i, h⟩
+      withRef parentStx do
+      let parentType ← Term.withSynthesize <| Term.elabType parentStx
+      let parentType ← whnf parentType
       let parentStructName ← getStructureName parentType
-      if parents.any (fun info => info.structName == parentStructName) then
-        logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}'"
       if let some existingFieldName ← findExistingField? infos parentStructName then
         if structureDiamondWarning.get (← getOptions) then
-          logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared"
-        let parents := parents.push { ref := parent, fvar? := none, subobject := false, structName := parentStructName, type := parentType }
-        copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos parents
+          logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
+        copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos (copiedParents.push parentType)
         -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`
       else
         let env ← getEnv
@@ -561,13 +487,10 @@ where
         let toParentName := mkToParentName parentStructName fun n => !containsFieldName infos n && !subfieldNames.contains n
         let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
         withLocalDecl toParentName binfo parentType fun parentFVar =>
-          let infos := infos.push { ref := parent,
-                                    name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar,
-                                    kind := StructFieldKind.subobject parentStructName }
-          let parents := parents.push { ref := parent, fvar? := parentFVar, subobject := true, structName := parentStructName, type := parentType }
-          processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos parents
+          let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject }
+          processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos copiedParents
     else
-      k infos parents
+      k infos copiedParents
 
 private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) :=
   Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <| Term.elabBinders view.binders.getArgs fun params => do
@@ -602,7 +525,7 @@ private partial def withFields (views : Array StructFieldView) (infos : Array St
 where
   go (i : Nat) (defaultValsOverridden : NameSet) (infos : Array StructFieldInfo) : TermElabM α := do
     if h : i < views.size then
-      let view := views[i]
+      let view := views.get ⟨i, h⟩
       withRef view.ref do
       match findFieldInfo? infos view.name with
       | none      =>
@@ -611,15 +534,13 @@ where
         | none,      none => throwError "invalid field, type expected"
         | some type, _    =>
           withLocalDecl view.rawName view.binderInfo type fun fieldFVar =>
-            let infos := infos.push { ref := view.nameId
-                                      name := view.name, declName := view.declName, fvar := fieldFVar, value? := value?,
+            let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, value? := value?,
                                       kind := StructFieldKind.newField }
             go (i+1) defaultValsOverridden infos
         | none, some value =>
           let type ← inferType value
           withLocalDecl view.rawName view.binderInfo type fun fieldFVar =>
-            let infos := infos.push { ref := view.nameId
-                                      name := view.name, declName := view.declName, fvar := fieldFVar, value? := value,
+            let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, value? := value,
                                       kind := StructFieldKind.newField }
             go (i+1) defaultValsOverridden infos
       | some info =>
@@ -639,11 +560,11 @@ where
               let fvarType ← inferType info.fvar
               let value ← Term.elabTermEnsuringType valStx fvarType
               pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref }
-              let infos := replaceFieldInfo infos { info with ref := view.nameId, value? := value }
+              let infos := updateFieldInfoVal infos info.name value
               go (i+1) defaultValsOverridden infos
         match info.kind with
         | StructFieldKind.newField    => throwError "field '{view.name}' has already been declared"
-        | StructFieldKind.subobject n => throwError "unexpected reference to subobject field '{n}'" -- improve error message
+        | StructFieldKind.subobject   => throwError "unexpected subobject field reference" -- improve error message
         | StructFieldKind.copiedField => updateDefaultValue
         | StructFieldKind.fromParent  => updateDefaultValue
     else
@@ -733,13 +654,13 @@ private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type :
   let r ← getResultUniverse type
   let rOffset : Nat   := r.getOffset
   let r       : Level := r.getLevelOffset
-  unless r.isMVar do
-    throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly: {r}"
-  let us ← collectUniversesFromFields r rOffset fieldInfos
-  trace[Elab.structure] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
-  let rNew := mkResultUniverse us rOffset (isPropCandidate fieldInfos)
-  assignLevelMVar r.mvarId! rNew
-  instantiateMVars type
+  match r with
+  | Level.mvar mvarId =>
+    let us ← collectUniversesFromFields r rOffset fieldInfos
+    let rNew := mkResultUniverse us rOffset (isPropCandidate fieldInfos)
+    assignLevelMVar mvarId rNew
+    instantiateMVars type
+  | _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"
 
 private def collectLevelParamsInFVar (s : CollectLevelParams.State) (fvar : Expr) : TermElabM CollectLevelParams.State := do
   let type ← inferType fvar
@@ -783,13 +704,9 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
 @[extern "lean_mk_projections"]
 private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except KernelException Environment
 
-private def addProjections (r : ElabStructHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
-  if r.type.isProp then
-    if let some fieldInfo ← fieldInfos.findM? (not <$> Meta.isProof ·.fvar) then
-      throwErrorAt fieldInfo.ref m!"failed to generate projections for 'Prop' structure, field '{format fieldInfo.name}' is not a proof"
-  let projNames := fieldInfos |>.filter (!·.isFromParent) |>.map (·.declName)
+private def addProjections (structName : Name) (projs : List Name) (isClass : Bool) : TermElabM Unit := do
   let env ← getEnv
-  let env ← ofExceptKernelException (mkProjections env r.view.declName projNames.toList r.view.isClass)
+  let env ← ofExceptKernelException (mkProjections env structName projs isClass)
   setEnv env
 
 private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do
@@ -797,46 +714,46 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
       if info.kind == StructFieldKind.fromParent then
         return none
       else
+        let env ← getEnv
         return some {
           fieldName  := info.name
           projFn     := info.declName
           binderInfo := (← getFVarLocalDecl info.fvar).binderInfo
           autoParam? := (← inferType info.fvar).getAutoParamTactic?
-          subobject? := if let .subobject parentName := info.kind then parentName else none
+          subobject? :=
+            if info.kind == StructFieldKind.subobject then
+              match env.find? info.declName with
+              | some info =>
+                match info.type.getForallBody.getAppFn with
+                | Expr.const parentName .. => some parentName
+                | _ => panic! "ill-formed structure"
+              | _ => panic! "ill-formed environment"
+            else
+              none
         }
   modifyEnv fun env => Lean.registerStructure env { structName, fields }
 
 private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
   let env ← getEnv
-  let hasEq   := env.contains ``Eq
-  let hasHEq  := env.contains ``HEq
-  let hasUnit := env.contains ``PUnit
-  let hasProd := env.contains ``Prod
+  let hasUnit := env.contains `PUnit
+  let hasEq   := env.contains `Eq
+  let hasHEq  := env.contains `HEq
   mkRecOn declName
   if hasUnit then mkCasesOn declName
   if hasUnit && hasEq && hasHEq then mkNoConfusion declName
-  let ival ← getConstInfoInduct declName
-  if ival.isRec then
-    if hasUnit && hasProd then mkBelow declName
-    if hasUnit && hasProd then mkIBelow declName
-    if hasUnit && hasProd then mkBRecOn declName
-    if hasUnit && hasProd then mkBInductionOn declName
 
-private def addDefaults (lctx : LocalContext) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
-  withLCtx lctx (← getLocalInstances) do
-    fieldInfos.forM fun fieldInfo => do
-      if let some value := fieldInfo.value? then
-        let declName := mkDefaultFnOfProjFn fieldInfo.declName
-        let type ← inferType fieldInfo.fvar
-        let value ← instantiateMVars value
-        if value.hasExprMVar then
-          discard <| Term.logUnassignedUsingErrorInfos (← getMVars value)
-          throwErrorAt fieldInfo.ref "invalid default value for field '{format fieldInfo.name}', it contains metavariables{indentExpr value}"
-        /- The identity function is used as "marker". -/
-        let value ← mkId value
-        -- No need to compile the definition, since it is only used during elaboration.
-        discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
-        setReducibleAttribute declName
+private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name × Expr × Expr)) : TermElabM Unit := do
+  let localInsts ← getLocalInstances
+  withLCtx lctx localInsts do
+    defaultAuxDecls.forM fun (declName, type, value) => do
+      let value ← instantiateMVars value
+      if value.hasExprMVar then
+        throwError "invalid default value for field, it contains metavariables{indentExpr value}"
+      /- The identity function is used as "marker". -/
+      let value ← mkId value
+      -- No need to compile the definition, since it is only used during elaboration.
+      discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
+      setReducibleAttribute declName
 
 /--
 Given `type` of the form `forall ... (source : A), B`, return `forall ... [source : A], B`.
@@ -850,14 +767,12 @@ private def setSourceInstImplicit (type : Expr) : Expr :=
       type.updateForall! .instImplicit d b
   | _ => unreachable!
 
-/--
-Creates a projection function to a non-subobject parent.
--/
-private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentStructName : Name) (parentType : Expr) : MetaM StructureParentInfo := do
+private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentType : Expr) : MetaM Unit := do
   let env ← getEnv
   let structName := view.declName
   let sourceFieldNames := getStructureFieldsFlattened env structName
   let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
+  let Expr.const parentStructName _ ← pure parentType.getAppFn | unreachable!
   let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
   withLocalDeclD `self structType fun source => do
     let mut declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType))
@@ -895,182 +810,139 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
       addInstance declName AttributeKind.global (eval_prio default)
     else
       setReducibleAttribute declName
-    return { structName := parentStructName, subobject := false, projFn := declName }
 
-private def elabStructHeader (view : StructView) : TermElabM ElabStructHeaderResult :=
-  Term.withAutoBoundImplicitForbiddenPred (fun n => view.shortDeclName == n) do
-  Term.withAutoBoundImplicit do
-  Term.elabBinders view.binders.getArgs fun params => do
-  elabParents view fun parentFieldInfos parents => do
-    let type ← Term.elabType view.type
+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
+  let type ← Term.elabType view.type
+  unless validStructType type do throwErrorAt view.type "expected Type"
+  withRef view.ref do
+  withParents view fun fieldInfos copiedParents => do
+  withFields view.fields fieldInfos fun fieldInfos => do
     Term.synthesizeSyntheticMVarsNoPostponing
-    let u ← mkFreshLevelMVar
-    unless ← isDefEq type (mkSort u) do
-      throwErrorAt view.type "invalid structure type, expecting 'Type _' or 'Prop'"
-    let type ← instantiateMVars (← whnf type)
-    Term.addAutoBoundImplicits' params type fun params type => do
-      let levelNames ← Term.getLevelNames
-      trace[Elab.structure] "header params: {params}, type: {type}, levelNames: {levelNames}"
-      return { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view, parents, parentFieldInfos }
-
-private def mkTypeFor (r : ElabStructHeaderResult) : TermElabM Expr := do
-  withLCtx r.lctx r.localInsts do
-    mkForallFVars r.params r.type
-
-/--
-Create a local declaration for the structure and execute `x params indFVar`, where `params` are the structure's type parameters and
-`indFVar` is the new local declaration.
--/
-private partial def withStructureLocalDecl (r : ElabStructHeaderResult) (x : Array Expr → Expr → TermElabM α) : TermElabM α := do
-  let declName := r.view.declName
-  let shortDeclName := r.view.shortDeclName
-  let type ← mkTypeFor r
-  let params := r.params
-  withLCtx r.lctx r.localInsts <| withRef r.view.ref do
-    Term.withAuxDecl shortDeclName type declName fun indFVar =>
-      x params indFVar
-
-/--
-Remark: `numVars <= numParams`.
-`numVars` is the number of context `variables` used in the declaration,
-and `numParams - numVars` is the number of parameters provided as binders in the declaration.
--/
-private def mkInductiveType (view : StructView) (indFVar : Expr) (levelNames : List Name)
-    (numVars : Nat) (numParams : Nat) (type : Expr) (ctor : Constructor) : TermElabM InductiveType := do
-  let levelParams := levelNames.map mkLevelParam
-  let const := mkConst view.declName levelParams
-  let ctorType ← forallBoundedTelescope ctor.type numParams fun params type => do
-    let type := type.replace fun e =>
-      if e == indFVar then
-        mkAppN const (params.extract 0 numVars)
-      else
-        none
-    instantiateMVars (← mkForallFVars params type)
-  return { name := view.declName, type := ← instantiateMVars type, ctors := [{ ctor with type := ← instantiateMVars ctorType }] }
-
-/--
-Precomputes the structure's resolution order.
-Option `structure.strictResolutionOrder` controls whether to create a warning if the C3 algorithm failed.
--/
-private def checkResolutionOrder (structName : Name) : TermElabM Unit := do
-  let resolutionOrderResult ← computeStructureResolutionOrder structName (relaxed := !structure.strictResolutionOrder.get (← getOptions))
-  trace[Elab.structure.resolutionOrder] "computed resolution order: {resolutionOrderResult.resolutionOrder}"
-  unless resolutionOrderResult.conflicts.isEmpty do
-    let mut defects : List MessageData := []
-    for conflict in resolutionOrderResult.conflicts do
-      let parentKind direct := if direct then "parent" else "indirect parent"
-      let conflicts := conflict.conflicts.map fun (isDirect, name) =>
-        m!"{parentKind isDirect} '{MessageData.ofConstName name}'"
-      defects := m!"- {parentKind conflict.isDirectParent} '{MessageData.ofConstName conflict.badParent}' \
-        must come after {MessageData.andList conflicts.toList}" :: defects
-    logWarning m!"failed to compute strict resolution order:\n{MessageData.joinSep defects.reverse "\n"}"
-
-def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
-  let scopeLevelNames ← Term.getLevelNames
-  let isUnsafe := view.modifiers.isUnsafe
-  withRef view.ref <| Term.withLevelNames view.levelNames do
-    let r ← elabStructHeader view
-    Term.synthesizeSyntheticMVarsNoPostponing
-    withLCtx r.lctx r.localInsts do
-    withStructureLocalDecl r fun params indFVar => do
-    trace[Elab.structure] "indFVar: {indFVar}"
-    Term.addLocalVarInfo view.declId indFVar
-    withFields view.fields r.parentFieldInfos fun fieldInfos =>
-    withRef view.ref do
-      Term.synthesizeSyntheticMVarsNoPostponing
-      let type ← instantiateMVars r.type
-      let u ← getResultUniverse type
-      let univToInfer? ← shouldInferResultUniverse u
-      withUsed vars params fieldInfos fun scopeVars => do
-        let fieldInfos ← levelMVarToParam scopeVars params fieldInfos univToInfer?
-        let type ← withRef view.ref do
-          if univToInfer?.isSome then
-            updateResultingUniverse fieldInfos type
-          else
-            checkResultingUniverse (← getResultUniverse type)
-            pure type
-        trace[Elab.structure] "type: {type}"
-        let usedLevelNames ← collectLevelParamsInStructure type scopeVars params fieldInfos
-        match sortDeclLevelParams scopeLevelNames r.levelNames usedLevelNames with
-        | Except.error msg      => throwErrorAt view.declId msg
-        | Except.ok levelParams =>
-          let params := scopeVars ++ params
-          let ctor ← mkCtor view levelParams params fieldInfos
-          let type ← mkForallFVars params type
-          let type ← instantiateMVars type
-          let indType ← mkInductiveType view indFVar levelParams scopeVars.size params.size type ctor
-          let decl    := Declaration.inductDecl levelParams params.size [indType] isUnsafe
-          Term.ensureNoUnassignedMVars decl
-          addDecl decl
-          -- rename indFVar so that it does not shadow the actual declaration:
-          let lctx := (← getLCtx).modifyLocalDecl indFVar.fvarId! fun decl => decl.setUserName .anonymous
-          withLCtx lctx (← getLocalInstances) do
-          addProjections r fieldInfos
-          registerStructure view.declName fieldInfos
-          mkAuxConstructions view.declName
-          let instParents ← fieldInfos.filterM fun info => do
-            let decl ← Term.getFVarLocalDecl! info.fvar
-            pure (info.isSubobject && decl.binderInfo.isInstImplicit)
-          withSaveInfoContext do  -- save new env
-            Term.addLocalVarInfo view.ref[1] (← mkConstWithLevelParams view.declName)
-            if let some _ := view.ctor.ref.getPos? (canonicalOnly := true) then
-              Term.addTermInfo' view.ctor.ref (← mkConstWithLevelParams view.ctor.declName) (isBinder := true)
-            for field in view.fields do
-              -- may not exist if overriding inherited field
-              if (← getEnv).contains field.declName then
-                Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
-          withRef view.declId do
-            Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
-          let projInstances := instParents.toList.map fun info => info.declName
-          projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default)
-          let parentInfos ← r.parents.mapM fun parent => do
-            if parent.subobject then
-              let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable!
-              pure { structName := parent.structName, subobject := true, projFn := info.declName }
+    let u ← getResultUniverse type
+    let univToInfer? ← shouldInferResultUniverse u
+    withUsed view.scopeVars view.params fieldInfos fun scopeVars => do
+      let fieldInfos ← levelMVarToParam scopeVars view.params fieldInfos univToInfer?
+      let type ← withRef view.ref do
+        if univToInfer?.isSome then
+          updateResultingUniverse fieldInfos type
+        else
+          checkResultingUniverse (← getResultUniverse type)
+          pure type
+      trace[Elab.structure] "type: {type}"
+      let usedLevelNames ← collectLevelParamsInStructure type scopeVars view.params fieldInfos
+      match sortDeclLevelParams view.scopeLevelNames view.allUserLevelNames usedLevelNames with
+      | Except.error msg      => withRef view.ref <| throwError msg
+      | Except.ok levelParams =>
+        let params := scopeVars ++ view.params
+        let ctor ← mkCtor view levelParams params fieldInfos
+        let type ← mkForallFVars params type
+        let type ← instantiateMVars type
+        let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType }
+        let decl    := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe
+        Term.ensureNoUnassignedMVars decl
+        addDecl decl
+        let projNames := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) => info.declName
+        addProjections view.declName projNames view.isClass
+        registerStructure view.declName fieldInfos
+        mkAuxConstructions view.declName
+        let instParents ← fieldInfos.filterM fun info => do
+          let decl ← Term.getFVarLocalDecl! info.fvar
+          pure (info.isSubobject && decl.binderInfo.isInstImplicit)
+        withSaveInfoContext do  -- save new env
+          Term.addLocalVarInfo view.ref[1] (← mkConstWithLevelParams view.declName)
+          if let some _ := view.ctor.ref.getPos? (canonicalOnly := true) then
+            Term.addTermInfo' view.ctor.ref (← mkConstWithLevelParams view.ctor.declName) (isBinder := true)
+          for field in view.fields do
+            -- may not exist if overriding inherited field
+            if (← getEnv).contains field.declName then
+              Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
+        Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
+        let projInstances := instParents.toList.map fun info => info.declName
+        projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default)
+        copiedParents.forM fun parent => mkCoercionToCopiedParent levelParams params view parent
+        let lctx ← getLCtx
+        let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome
+        let defaultAuxDecls ← fieldsWithDefault.mapM fun info => do
+          let type ← inferType info.fvar
+          pure (mkDefaultFnOfProjFn info.declName, type, info.value?.get!)
+        /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations
+           The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
+        let lctx :=
+          params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) =>
+            if p.isFVar then
+              lctx.setBinderInfo p.fvarId! BinderInfo.implicit
             else
-              mkCoercionToCopiedParent levelParams params view parent.structName parent.type
-          setStructureParents view.declName parentInfos
-          checkResolutionOrder view.declName
+              lctx
+        let lctx :=
+          fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) =>
+            if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating "default value" auxiliary functions
+            else lctx.setBinderInfo info.fvar.fvarId! BinderInfo.default
+        addDefaults lctx defaultAuxDecls
 
-          let lctx ← getLCtx
-          /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations
-            The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
-          let lctx :=
-            params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) =>
-              if p.isFVar then
-                lctx.setBinderInfo p.fvarId! BinderInfo.implicit
-              else
-                lctx
-          let lctx :=
-            fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) =>
-              if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating "default value" auxiliary functions
-              else lctx.setBinderInfo info.fvar.fvarId! BinderInfo.default
-          addDefaults lctx fieldInfos
+/-
+leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >>
+  optional (("where" <|> ":=") >> optional structCtor >> structFields) >> optDeriving
 
+where
+def «extends» := leading_parser " extends " >> sepBy1 termParser ", "
+def typeSpec := leading_parser " : " >> termParser
+def optType : Parser := optional typeSpec
 
-def elabStructureView (vars : Array Expr) (view : StructView) : TermElabM Unit := do
-  Term.withDeclName view.declName <| withRef view.ref do
-    mkStructureDecl vars view
-    unless view.isClass do
-      Lean.Meta.IndPredBelow.mkBelow view.declName
-      mkSizeOfInstances view.declName
-      mkInjectiveTheorems view.declName
-
-def elabStructureViewPostprocessing (view : StructView) : CommandElabM Unit := do
-  view.derivingClasses.forM fun classView => classView.applyHandlers #[view.declName]
-  runTermElabM fun _ => Term.withDeclName view.declName <| withRef view.declId do
-    Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
+def structFields         := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
+def structCtor           := leading_parser try (declModifiers >> ident >> " :: ")
 
+-/
 def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let view ← runTermElabM fun vars => do
-    let view ← structureSyntaxToView modifiers stx
-    trace[Elab.structure] "view.levelNames: {view.levelNames}"
-    elabStructureView vars view
-    pure view
-  elabStructureViewPostprocessing view
+  checkValidInductiveModifier modifiers
+  let isClass   := stx[0].getKind == ``Parser.Command.classTk
+  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
+  let declId    := stx[1]
+  let params    := stx[2].getArgs
+  let exts      := stx[3]
+  let parents   := if exts.isNone then #[] else exts[0][1].getSepArgs
+  let optType   := stx[4]
+  let derivingClassViews ← liftCoreM <| getOptDerivingClasses stx[6]
+  let type ← if optType.isNone then `(Sort _) else pure optType[0][1]
+  let declName ←
+    runTermElabM fun scopeVars => do
+      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
+        Term.withDeclName declName do
+          let ctor ← expandCtor stx modifiers declName
+          let fields ← expandFields stx modifiers declName
+          Term.withLevelNames allUserLevelNames <| Term.withAutoBoundImplicit <|
+            Term.elabBinders params fun params => do
+              Term.synthesizeSyntheticMVarsNoPostponing
+              let params ← Term.addAutoBoundImplicits params
+              let allUserLevelNames ← Term.getLevelNames
+              elabStructureView {
+                ref := stx
+                modifiers
+                scopeLevelNames
+                allUserLevelNames
+                declName
+                isClass
+                scopeVars
+                params
+                parents
+                type
+                ctor
+                fields
+              }
+              unless isClass do
+                mkSizeOfInstances declName
+                mkInjectiveTheorems declName
+              return declName
+  derivingClassViews.forM fun view => view.applyHandlers #[declName]
+  runTermElabM fun _ => Term.withDeclName declName do
+    Term.applyAttributesAt declName modifiers.attrs .afterCompilation
 
-builtin_initialize
-  registerTraceClass `Elab.structure
-  registerTraceClass `Elab.structure.resolutionOrder
+builtin_initialize registerTraceClass `Elab.structure
 
 end Lean.Elab.Command

src/Lean/Elab/SyntheticMVars.lean

@@ -219,13 +219,10 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
           let mvarDecl ← getMVarDecl mvarId
           unless (← MonadLog.hasErrors) do
             throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}{extraErrorMsg}"
-    | .coe header expectedType e f? mkErrorMsg? =>
+    | .coe header expectedType e f? =>
       mvarId.withContext do
-        if let some mkErrorMsg := mkErrorMsg? then
-          throwError (← mkErrorMsg mvarId expectedType e)
-        else
-          throwTypeMismatchError header expectedType (← inferType e) e f?
-            m!"failed to create type class instance for{indentExpr (← getMVarDecl mvarId).type}"
+        throwTypeMismatchError header expectedType (← inferType e) e f?
+          m!"failed to create type class instance for{indentExpr (← getMVarDecl mvarId).type}"
     | _ => unreachable! -- TODO handle other cases.
 
 /--
@@ -389,7 +386,7 @@ mutual
     withRef mvarSyntheticDecl.stx do
     match mvarSyntheticDecl.kind with
     | .typeClass extraErrorMsg? => synthesizePendingInstMVar mvarId extraErrorMsg?
-    | .coe _header? expectedType e _f? _ => mvarId.withContext do
+    | .coe _header? expectedType e _f? => mvarId.withContext do
       if (← withDefault do isDefEq (← inferType e) expectedType) then
         -- Types may be defeq now due to mvar assignments, type class
         -- defaulting, etc.

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

@@ -225,8 +225,8 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let mut sats := #[]
   let mut unusedHypotheses := {}
   for hyp in hyps do
-    if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then
-      sats := (sats ++ lemmas).push reflected
+    if let some reflected ← SatAtBVLogical.of (mkFVar hyp) then
+      sats := sats.push reflected
     else
       unusedHypotheses := unusedHypotheses.insert hyp
   if h : sats.size = 0 then

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

@@ -29,6 +29,7 @@ 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
@@ -79,7 +80,6 @@ instance : ToExpr Gate where
     | .and => mkConst ``Gate.and
     | .xor => mkConst ``Gate.xor
     | .beq => mkConst ``Gate.beq
-    | .imp => mkConst ``Gate.imp
   toTypeExpr := mkConst ``Gate
 
 instance : ToExpr BVPred where
@@ -102,7 +102,6 @@ where
   | .const b => mkApp2 (mkConst ``BoolExpr.const) (toTypeExpr α) (toExpr b)
   | .not x => mkApp2 (mkConst ``BoolExpr.not) (toTypeExpr α) (go x)
   | .gate g x y => mkApp4 (mkConst ``BoolExpr.gate) (toTypeExpr α) (toExpr g) (go x) (go y)
-  | .ite d l r => mkApp4 (mkConst ``BoolExpr.ite) (toTypeExpr α) (go d) (go l) (go r)
 
 
 open Lean.Meta
@@ -126,76 +125,6 @@ The reflection monad, used to track `BitVec` variables that we see as we travers
 -/
 abbrev M := StateRefT State MetaM
 
-/--
-A reified version of an `Expr` representing a `BVExpr`.
--/
-structure ReifiedBVExpr where
-  width : Nat
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVExpr width
-  /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`.
-  -/
-  expr : Expr
-
-/--
-A reified version of an `Expr` representing a `BVPred`.
--/
-structure ReifiedBVPred where
-  /--
-  The reified expression.
-  -/
-  bvPred : BVPred
-  /--
-  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvPred`
-  -/
-  expr : Expr
-
-/--
-A reified version of an `Expr` representing a `BVLogicalExpr`.
--/
-structure ReifiedBVLogical where
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVLogicalExpr
-  /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`.
-  -/
-  evalsAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`
-  -/
-  expr : Expr
-
-/--
-A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true.
--/
-structure SatAtBVLogical where
-  /--
-  The reified expression.
-  -/
-  bvExpr : BVLogicalExpr
-  /--
-  A proof that `bvExpr.eval atomsAssignment = true`.
-  -/
-  satAtAtoms : M Expr
-  /--
-  A cache for `toExpr bvExpr`
-  -/
-  expr : Expr
-
-
 namespace M
 
 /--
@@ -243,34 +172,5 @@ where
 
 end M
 
-/--
-The state of the lemma reflection monad.
--/
-structure LemmaState where
-  /--
-  The list of top level lemmas that got created on the fly during reflection.
-  -/
-  lemmas : Array SatAtBVLogical := #[]
-
-/--
-The lemma reflection monad. It extends the usual reflection monad `M` by adding the ability to
-add additional top level lemmas on the fly.
--/
-abbrev LemmaM := StateRefT LemmaState M
-
-namespace LemmaM
-
-def run (m : LemmaM α) (state : LemmaState := {}) : M (α × Array SatAtBVLogical) := do
-  let (res, state) ← StateRefT'.run m state
-  return (res, state.lemmas)
-
-/--
-Add another top level lemma.
--/
-def addLemma (lemma : SatAtBVLogical) : LemmaM Unit := do
-  modify fun s => { s with lemmas := s.lemmas.push lemma }
-
-end LemmaM
-
 end Frontend
 end Lean.Elab.Tactic.BVDecide