whitespace

In patterns, ellipsis should always fill in each remaining argument as
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` constructor 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 individually (for example with `.internal (extra := _) ..`) but
it's not possible to opt-in, and it is plausible that `..` with
optparams is useful in contexts such as the `refine` tactic. With
patterns however, it is hard to imagine a use case that offsets the
inconvenience of optparams being eagerly supplied.

Closes #4555

.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 `#eval Lean.versionString`]
+[Output of `#version` or `#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\" -DUSE_GMP=OFF",
+                "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 // 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": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
+                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",

RELEASES.md

@@ -8,6 +8,21 @@ 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
 ----------
 

flake.nix

@@ -38,7 +38,11 @@
           # more convenient `ctest` output
           CTEST_OUTPUT_ON_FAILURE = 1;
         } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-          GMP = pkgsDist.gmp.override { withStatic = true; };
+          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" ];
+            });
           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 12)
+set(LEAN_VERSION_MINOR 15)
 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'")

src/Init.lean

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

src/Init/Control/Basic.lean

@@ -11,8 +11,13 @@ 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.
 -/
-instance (priority := low) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
+-- 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
   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 : β)
@@ -30,6 +35,15 @@ instance (priority := low) 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,6 +7,7 @@ Notation for operators defined at Prelude.lean
 -/
 prelude
 import Init.Tactics
+import Init.Meta
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -46,12 +47,20 @@ 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.) -/
+/--
+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`.
+-/
 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.) -/
+/--
+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`.
+-/
 syntax (name := rhs) "rhs" : conv
 
 /-- Traverses into the function of a (unary) function application.
@@ -74,13 +83,17 @@ 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 " "@"? num : conv
+syntax (name := arg) "arg " argArg : conv
 
 /-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)
 to target `e`, introducing name `x` in the process. -/
@@ -130,11 +143,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" (config)? rwRuleSeq : conv
+syntax (name := rewrite) "rewrite" optConfig rwRuleSeq : conv
 
 /-- `simp [thm]` performs simplification using `thm` and marked `@[simp]` lemmas.
 See the `simp` tactic for more information. -/
-syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
+syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
 
 /--
@@ -151,7 +164,7 @@ example (a : Nat): (0 + 0) = a - a := by
     rw [← Nat.sub_self a]
 ```
 -/
-syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
+syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
 
 /-- `simp_match` simplifies match expressions. For example,
@@ -247,12 +260,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:(config)? s:rwRuleSeq : conv => `(conv| rewrite $[$c]? $s)
+macro "rw" c:optConfig s:rwRuleSeq : conv => `(conv| rewrite $c:optConfig $s)
 
-/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
+/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
 This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
 which only unfolds `@[reducible]` definitions). -/
-macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s)
+macro "erw" c:optConfig s:rwRuleSeq : conv => `(conv| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq)
 
 /-- `args` traverses into all arguments. Synonym for `congr`. -/
 macro "args" : conv => `(conv| congr)
@@ -263,7 +276,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 <|> ("@"? num)
+syntax enterArg := ident <|> argArg
 
 /-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
 It is a shorthand for other conv tactics as follows:
@@ -272,12 +285,7 @@ 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 "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,*]))
+syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv
 
 /-- 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/Array.lean

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

src/Init/Data/Array/Basic.lean

@@ -12,6 +12,7 @@ import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
 import Init.Data.List.ToArray
+import Init.Data.Array.Set
 universe u v w
 
 /-! ### Array literal syntax -/
@@ -29,7 +30,8 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+@[simp] theorem size_set (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (set a i v h).size = a.size :=
   List.length_set ..
 
 @[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@@ -141,7 +143,7 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
    `fset` may be slightly slower than `uset`. -/
 @[extern "lean_array_uset"]
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
-  a.set ⟨i.toNat, h⟩ v
+  a.set i.toNat v h
 
 @[extern "lean_array_pop"]
 def pop (a : Array α) : Array α where
@@ -167,10 +169,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 (size_set a i v₂ ▸ j) v₁
+  a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
 
 @[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
+  show ((a.set i (a.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
   rw [size_set, size_set]
 
 /--
@@ -235,9 +237,11 @@ 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
 
@@ -276,7 +280,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 (size_set a .. ▸ idx) v
+    pure <| a'.set idx v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
   else
     pure a
 
@@ -302,37 +306,6 @@ 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
@@ -363,7 +336,9 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
 instance : ForIn' m (Array α) α inferInstance where
   forIn' := Array.forIn'
 
-/-- See comment at `forInUnsafe` -/
+-- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
+
+/-- See comment at `forIn'Unsafe` -/
 @[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
@@ -398,7 +373,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 `forInUnsafe` -/
+/-- See comment at `forIn'Unsafe` -/
 @[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
@@ -437,7 +412,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   else
     pure init
 
-/-- See comment at `forInUnsafe` -/
+/-- See comment at `forIn'Unsafe` -/
 @[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

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/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 (config := {occs := .pos [2]}) [← List.get_drop_eq_drop _ _ ‹_›]
+    rw (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, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
+  · exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
 theorem isEqv_iff_rel (a b : Array α) (r) :
     Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
-  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
+  ⟨rel_of_isEqv, fun ⟨h, w⟩ => by
     simp only [isEqv, ← h, ↓reduceDIte]
-    exact isEqvAux_of_rel r a b h a.size (by simp [h]) w⟩
+    exact isEqvAux_of_rel h (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 (fun x y => x = y) a b h
+  have ⟨h, h'⟩ := rel_of_isEqv 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,7 +10,10 @@ 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
 
 /-!
@@ -69,6 +72,9 @@ 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
@@ -101,27 +107,8 @@ 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 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 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 : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
     (h : i ≤ l.length) (b : β) :
@@ -131,7 +118,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, forIn_eq_forIn]
+    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
     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)]
@@ -145,7 +132,11 @@ 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 [List.forIn_eq_forIn]
+  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
 
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
@@ -222,17 +213,25 @@ theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array
     (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 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]
+/--
+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]
 
 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 `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' ..
+/--
+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
 
 /-- A more efficient version of `arr.toList.reverse`. -/
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@@ -338,25 +337,26 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 
 /-! # set -/
 
-@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
-      (eq : i.val = j) (p : j < (a.set i v).size) :
+@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
+      (eq : i = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
   simp [set, getElem_eq_getElem_toList, ←eq]
 
-@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
-    (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
+@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
+    (pj : j < (a.set i v).size) (h : i ≠ j) :
+    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
-theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
+theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v ▸ h) := by
-  by_cases p : i.1 = j <;> simp [p]
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
+  by_cases p : i = j <;> simp [p]
 
-@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
+    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
 
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
+    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
 /-! # setD -/
@@ -373,7 +373,7 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
 @[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
     (setD a i v)[i]'h = v := by
   simp at h
-  simp only [setD, h, dite_true, getElem_set, ite_true]
+  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
 
 @[simp]
 theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
@@ -506,13 +506,14 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
   cases as
   simp [List.getElem?_eq_some_iff]
 
-@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]
+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]
 
-theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
+@[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
+  simp [back!_eq_back?]
 
 theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
@@ -547,43 +548,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) : (a.set i v).toList = a.toList.set i.1 v := rfl
+@[simp] theorem toList_set (a : Array α) (i v h) : (a.set i v).toList = a.toList.set i v := rfl
 
-theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1] = v := by
+theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (a.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
 
-theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
+theorem get?_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    (a.set i v)[i]? = v := by simp [getElem?_pos, h]
 
-@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (h : i.1 ≠ j) : (a.set i v)[j]? = a[j]? := by
+@[simp] theorem get?_set_ne (a : Array α) (i : Nat) (h' : i < a.size) {j : Nat} (v : α)
+    (h : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
 
-theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
-    (a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
+theorem get?_set (a : Array α) (i : Nat) (h : i < a.size) (j : Nat) (v : α) :
+    (a.set i v)[j]? = if i = j then some v else a[j]? := by
+  if h : i = j then subst j; simp [*] else simp [*]
 
-theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
+theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) :
     (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
+  if h : i = j then subst j; simp [*] else simp [*]
 
-@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
-    (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
+@[simp] theorem get_set_ne (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size)
+    (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
     (setD a i v)[i] = v := by
   simp at h
-  simp only [setD, h, dite_true, get_set, ite_true]
+  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
 
-theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
-    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
+theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
+    (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
 
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Fin a.size) :
-    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
+    a.swap i j = (a.set i (a.get j)).set j (a.get i) := by
   simp [swap, fin_cast_val]
 
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
@@ -601,7 +602,7 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
 
 @[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
+    a.swapAt! i v = (a[i], a.set i v) := by simp [swapAt!, h]
 
 @[simp] theorem size_swapAt! (a : Array α) (i : Nat) (v : α) :
     (a.swapAt! i v).2.size = a.size := by
@@ -625,8 +626,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'
@@ -635,12 +636,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
 
@@ -713,6 +714,43 @@ 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
@@ -872,7 +910,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 [eq] at w
+    simp only [eq] at w
     specialize w ⟨i, h⟩ h
     simpa [map_eq_foldl] using w
   · exact ⟨h0, rfl, nofun⟩
@@ -929,7 +967,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 : α → α) :
@@ -1369,30 +1407,15 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
 
 open Fin
 
-@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
-  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
+@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.1] = a[i] := by
+  simp [swap_def, getElem_set]
 
-@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
-  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
-    simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
-  else by
-    apply Eq.trans
-    · apply Array.get_set_ne
-      · simp only [size_set, Fin.isLt]
-      · assumption
-    · simp [get_set_ne]
+@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.1] = a[j] := by
+  simp +contextual [swap_def, getElem_set]
 
 @[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
     (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
-  apply Eq.trans
-  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
-    apply Array.get_set_ne
-    · simp only [this]
-      apply Ne.symm
-      · assumption
-  · apply Array.get_set_ne
-    · apply Ne.symm
-      · assumption
+  simp [swap_def, getElem_set, hi.symm, hj.symm]
 
 theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
     (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
@@ -1579,8 +1602,21 @@ 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
@@ -1594,6 +1630,8 @@ 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
@@ -1734,4 +1772,9 @@ 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,6 +60,10 @@ 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 → α → β)
@@ -89,4 +93,20 @@ 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

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

src/Init/Data/BitVec/Basic.lean

@@ -634,6 +634,16 @@ 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,6 +174,30 @@ 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
@@ -352,6 +376,117 @@ 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

@@ -1792,7 +1792,7 @@ theorem setWidth_succ (x : BitVec w) :
     · simp_all
     · omega
 
-@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
+@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]
 theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
   simp
 
@@ -2146,19 +2146,6 @@ 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 -/
-
-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]
-
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -2899,6 +2886,14 @@ 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`.
 -/
@@ -2921,6 +2916,21 @@ 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
@@ -2928,6 +2938,10 @@ 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
@@ -2944,6 +2958,10 @@ 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. -/
@@ -3036,6 +3054,38 @@ 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 -/
 

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 b⟩
+  | ⟨bs⟩, i, b => ⟨bs.set i.1 b i.2⟩
 
 @[extern "lean_byte_array_uset"]
 def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray

src/Init/Data/Fin/Fold.lean

@@ -5,6 +5,8 @@ Authors: François G. Dorais
 -/
 prelude
 import Init.Data.Nat.Linear
+import Init.Control.Lawful.Basic
+import Init.Data.Fin.Lemmas
 
 namespace Fin
 
@@ -23,4 +25,195 @@ 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 d⟩
+  | ⟨ds⟩, i, d => ⟨ds.set i.1 d i.2⟩
 
 @[extern "lean_float_array_set"]
 def set! : FloatArray → (@& Nat) → Float → FloatArray

src/Init/Data/Hashable.lean

@@ -48,6 +48,9 @@ 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 (config := {decide := true}) only [Int.ediv_self]
+      · simp +decide 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 (config := {decide := true})
+    | 0 => rw [if_pos] <;> simp +decide
     | (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 (config := { decide := true }) only [sign, true_iff]
+    simp +decide only [sign, true_iff]
     exact Int.le_add_one (ofNat_nonneg _)
-  | .negSucc _ => simp (config := { decide := true }) [sign]
+  | .negSucc _ => simp +decide [sign]
 
 theorem mul_sign : ∀ i : Int, i * sign i = natAbs i
   | succ _ => Int.mul_one _

src/Init/Data/List.lean

@@ -25,3 +25,4 @@ 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`, `groupBy`,
+* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `splitBy`,
   `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)
 
-/-! ### groupBy -/
+/-! ### splitBy -/
 
 /--
-`O(|l|)`. `groupBy R l` splits `l` into chains of elements
+`O(|l|)`. `splitBy R l` splits `l` into chains of elements
 such that adjacent elements are related by `R`.
 
-* `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]]`
+* `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]]`
 -/
-@[specialize] def groupBy (R : α → α → Bool) : List α → List (List α)
+@[specialize] def splitBy (R : α → α → Bool) : List α → List (List α)
   | []    => []
   | a::as => loop as a [] []
 where
   /--
-  The arguments of `groupBy.loop l ag g gs` represent the following:
+  The arguments of `splitBy.loop l ag g gs` represent the following:
 
-  - `l : List α` are the elements which we still need to group.
+  - `l : List α` are the elements which we still need to split.
   - `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,6 +1666,8 @@ 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,27 +215,6 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
     | some b => pure (some b)
     | none   => findSomeM? f as
 
-@[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
@@ -254,16 +233,15 @@ instance : ForIn m (List α) α where
 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'_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
+@[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
 
 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 (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
+  simp +contextual [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 (config := { contextual := true })
+  apply countP_mono_left; simp +contextual
 
 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 (config := {contextual := true}) [findSome?_append]
+  simp +contextual [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 (config := {contextual := true}) [find?_append]
+  simp +contextual [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 (config := { singlePass := true }) only [← ipm, getElem_cons_succ]
+      simp +singlePass 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`, `groupBy`.
+`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `splitBy`.
 
 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 (config := {contextual := true}) [replicate_succ]
+  cases n <;> simp +contextual [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,6 +7,9 @@ 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
 
@@ -14,8 +17,21 @@ namespace List
 
 /-! ### mapIdx -/
 
+
 /--
-Given a function `f : Nat → α → β` and `as : list α`, `as = [a₀, a₁, ...]`, returns the list
+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
 `[f 0 a₀, f 1 a₁, ...]`.
 -/
 @[inline] def mapIdx (f : Nat → α → β) (as : List α) : List β := go as #[] where
@@ -25,34 +41,177 @@ 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
@@ -60,16 +219,6 @@ 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]
@@ -112,6 +261,15 @@ 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
@@ -130,9 +288,16 @@ 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]
+  rw [List.mapIdx_eq_enum_map, List.map_eq_nil_iff, List.enum_eq_nil_iff]
 
 theorem mapIdx_ne_nil_iff {l : List α} :
     List.mapIdx f l ≠ [] ↔ l ≠ [] := by
@@ -140,13 +305,8 @@ 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_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⟩
+  rw [mapIdx_eq_mapFinIdx] at h
+  simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h
 
 @[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,6 +5,7 @@ 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`.
@@ -48,6 +49,9 @@ 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 [*]
 
@@ -72,6 +76,16 @@ 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`.
@@ -89,9 +103,6 @@ theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β)
 
 /-! ### 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 β)}
@@ -122,6 +133,11 @@ 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 β)}
@@ -149,6 +165,65 @@ 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 α) :
@@ -161,14 +236,4 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
     funext b
     split <;> simp_all
 
-/-! ### foldlM and foldrM -/
-
-theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
-    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
-  induction l generalizing g init <;> simp [*]
-
-theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁)
-    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
-  induction l generalizing g init <;> simp [*]
-
 end List

src/Init/Data/List/Nat/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 (config := {decide := true}) only [range_eq_range', pairwise_lt_range']
+  simp +decide 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 (config := { contextual := true }) [getElem_take, Nat.lt_min]
+  · simp +contextual [getElem_take, Nat.lt_min]
 
 theorem nodup_range (n : Nat) : Nodup (range n) := by
-  simp (config := {decide := true}) only [range_eq_range', nodup_range']
+  simp +decide 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,7 +430,10 @@ theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
 /-! ### enum -/
 
 @[simp]
-theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
+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
 
 @[simp] theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rfl
 

src/Init/Data/List/OfFn.lean

@@ -0,0 +1,55 @@
+/-
+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 (config := { contextual := true })
+  Pairwise.iff_of_mem <| by simp +contextual
 
 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 (config := { contextual := true })
+  Pairwise.iff_of_mem <| by simp +contextual
 
 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 (config := {contextual := true}) [replicate_succ, ih, cons_subset]
+  | succ n ih => simp +contextual [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 (config := {occs := .pos [2]}) [← Nat.and_forall_add_one]
+      rw (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 (config := {occs := .pos [2]}) [← mod_add_div a b]
+  rw (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 (config := {occs := .pos [1]}) [← mod_add_div a n]
-  rw (config := {occs := .pos [1]}) [← mod_add_div b n]
+  rw (occs := .pos [1]) [← mod_add_div a n]
+  rw (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]

src/Init/Data/Option/Instances.lean

@@ -86,4 +86,6 @@ 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,21 +20,6 @@ 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
@@ -50,6 +35,8 @@ instance : ForIn m Range Nat where
 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/Sum/Lemmas.lean

@@ -17,11 +17,11 @@ open Function
 
 namespace Sum
 
-@[simp] protected theorem «forall» {p : α ⊕ β → Prop} :
+protected theorem «forall» {p : α ⊕ β → Prop} :
     (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
   ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
 
-@[simp] protected theorem «exists» {p : α ⊕ β → Prop} :
+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]
+  simp [funext_iff, Sum.forall]
 
 /-! ### `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⟩
-@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
-def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨Fin.modn a.val n⟩
+@[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⟩
-@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
-def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨Fin.modn a.val n⟩
+@[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⟩
-@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
-def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨Fin.modn a.val n⟩
+@[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⟩
-@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
-def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨Fin.modn a.val n⟩
+@[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⟩
-@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
-def USize.modn (a : USize) (n : @& Nat) : USize := ⟨Fin.modn a.val n⟩
+@[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,6 +7,7 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
+import Init.Syntax
 import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
@@ -442,7 +443,7 @@ def unsetTrailing (stx : Syntax) : Syntax :=
   if h : i < a.size then
     let v := a[i]
     match f v with
-    | some v => some <| a.set ⟨i, h⟩ v
+    | some v => some <| a.set i v h
     | none   => updateFirst a f (i+1)
   else
     none
@@ -629,6 +630,9 @@ 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
 
@@ -1409,64 +1413,87 @@ namespace Parser
 
 namespace Tactic
 
-/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
+/--
+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]`.
 This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
 which only unfolds `@[reducible]` definitions). -/
-macro "erw" s:rwRuleSeq loc:(location)? : tactic =>
-  `(tactic| rw (config := { transparency := .default }) $s $(loc)?)
+macro "erw" c:optConfig s:rwRuleSeq loc:(location)? : tactic => do
+  `(tactic| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq $(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 updateCfg:term : command => do
+    ppSpace tacName:ident ppSpace tacToken:str ppSpace cfg:optConfig : command => do
   let (kind, tkn, stx) ←
     if opt.raw.isNone then
-      pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (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 (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
+      pure (← `(``simpAll), ← `("simp_all"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
     else
-      pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
   `($stx:command
     @[macro $tacName] def expandSimp : Macro := fun s => do
-      let c ← match s[1][0] with
-        | `(config| (config := $$c)) => `(config| (config := $updateCfg $$c))
-        | _ => `(config| (config := $updateCfg {}))
+      let cfg ← `(optConfig| $cfg)
       let s := s.setKind $kind
       let s := s.setArg 0 (mkAtomFrom s[0] $tkn (canonical := true))
-      let r := s.setArg 1 (mkNullNode #[c])
-      return r)
+      let s := s.setArg 1 (appendConfig s[1] cfg)
+      let s := s.mkSynthetic
+      return s)
 
 /-- `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! " fun (c : Lean.Meta.Simp.Config) => { c with autoUnfold := true }
+declare_simp_like_tactic simpAutoUnfold "simp! " (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 " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, decide := true }
+declare_simp_like_tactic simpArith "simp_arith " (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! " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, autoUnfold := true, decide := true }
+declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " (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! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with autoUnfold := true }
+declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " (autoUnfold := true)
 
 /-- `simp_all_arith` combines the effects of `simp_all` and `simp_arith`. -/
-declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, decide := true }
+declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " (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! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, autoUnfold := true, decide := true }
+declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " (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! " fun (c : Lean.Meta.DSimp.Config) => { c with autoUnfold := true }
+declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " (autoUnfold := true)
 
 end Tactic
 

src/Init/Prelude.lean

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

src/Init/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]
+@[deprecated ite_then_decide_self (since := "2024-08-29")]
 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]
+@[deprecated ite_false_decide_same (since := "2024-08-29")]
 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,6 +54,13 @@ 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

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

src/Init/Tactics.lean

@@ -417,7 +417,27 @@ It synthesizes a value of any target type by typeclass inference.
 -/
 macro "infer_instance" : tactic => `(tactic| exact inferInstance)
 
-/-- Optional configuration option for tactics -/
+/--
+`+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`.) -/
 syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
 
 /-- The `*` location refers to all hypotheses and the goal. -/
@@ -474,25 +494,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 (config := {occs := .pos L}) [e]`,
+Using `rw (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" (config)? rwRuleSeq (location)? : tactic
+syntax (name := rewriteSeq) "rewrite" optConfig rwRuleSeq (location)? : tactic
 
 /--
 `rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 -/
-macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
+macro (name := rwSeq) "rw " c:optConfig 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`. -/
@@ -561,14 +581,14 @@ non-dependent hypotheses. It has many variants:
 - `simp [*] at *` simplifies target and all (propositional) hypotheses using the
   other hypotheses.
 -/
-syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
+syntax (name := simp) "simp" optConfig (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" (config)? (discharger)? (&" only")?
+syntax (name := simpAll) "simp_all" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic
 
 /--
@@ -576,7 +596,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" (config)? (discharger)? (&" only")?
+syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 
 /--
@@ -598,7 +618,7 @@ def dsimpArg := simpErase.binary `orelse simpLemma
 syntax dsimpArgs := " [" dsimpArg,* "]"
 
 /-- The common arguments of `simp?` and `simp?!`. -/
-syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
+syntax simpTraceArgsRest := optConfig (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
 
 /--
 `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
@@ -617,7 +637,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 := (config)? (discharger)? (&" only")? (dsimpArgs)?
+syntax simpAllTraceArgsRest := optConfig (discharger)? (&" only")? (dsimpArgs)?
 
 @[inherit_doc simpTrace]
 syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
@@ -626,7 +646,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 := (config)? (&" only")? (dsimpArgs)? (ppSpace location)?
+syntax dsimpTraceArgsRest := optConfig (&" only")? (dsimpArgs)? (ppSpace location)?
 
 @[inherit_doc simpTrace]
 syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
@@ -635,7 +655,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 := (config)? (discharger)? &" only "? (simpArgs)? (" using " term)?
+syntax simpaArgsRest := optConfig (discharger)? &" only "? (simpArgs)? (" using " term)?
 
 /--
 This is a "finishing" tactic modification of `simp`. It has two forms.
@@ -1148,8 +1168,7 @@ a natural subtraction appearing in a hypothesis, and try again.
 
 The options
 ```
-omega (config :=
-  { splitDisjunctions := true, splitNatSub := true, splitNatAbs := true, splitMinMax := true })
+omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
 ```
 can be used to:
 * `splitDisjunctions`: split any disjunctions found in the context,
@@ -1159,7 +1178,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" (config)? : tactic
+syntax (name := omega) "omega" optConfig : tactic
 
 /--
 `bv_omega` is `omega` with an additional preprocessor that turns statements about `BitVec` into statements about `Nat`.
@@ -1272,7 +1291,7 @@ example (a b : Nat)
 
 See also `norm_cast`.
 -/
-syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
+syntax (name := pushCast) "push_cast" optConfig (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
 /--
@@ -1348,7 +1367,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" "*"? (config)? (&" only")? (args)? (using_)? : tactic
+  "solve_by_elim" "*"? optConfig (&" only")? (args)? (using_)? : tactic
 
 /--
 `apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
@@ -1371,7 +1390,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" (config)? (&" only")? (args)? (using_)? : tactic
+  "apply_assumption" optConfig (&" only")? (args)? (using_)? : tactic
 
 /--
 `apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
@@ -1396,7 +1415,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" (config)? (&" only")? (args)? (using_)? : tactic
+syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
 end SolveByElim
 
 /--
@@ -1595,7 +1614,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 (config := { arith := true }); done)
+macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; 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" (config)? rwRuleSeq (location)? : tactic
+syntax "rw_mod_cast" optConfig rwRuleSeq (location)? : tactic
 macro_rules
-  | `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
+  | `(tactic| rw_mod_cast $cfg:optConfig [$rules,*] $[$loc]?) => do
     let tacs ← rules.getElems.mapM fun rule =>
-      `(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
+      `(tactic| (norm_cast at *; rw $cfg [$rule] $[$loc]?))
     `(tactic| ($[$tacs]*))
 
 /--

src/Init/WFTactics.lean

@@ -16,15 +16,14 @@ 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 (config := { unfoldPartialApp := true, zetaDelta := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
+  `(tactic| try simp +unfoldPartialApp +zetaDelta [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
-     (config := { unfoldPartialApp := true, zetaDelta := true, failIfUnchanged := false })
+  `(tactic| simp +unfoldPartialApp +zetaDelta -failIfUnchanged
      only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel,
            WellFoundedRelation.rel, sizeOf_nat, reduceCtorEq])
 
@@ -37,7 +36,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
 -/
 syntax "decreasing_trivial" : tactic
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp +arith -failIfUnchanged) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
 

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

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 δ :=
-  kv.entries.forIn init f
+  forIn kv.entries 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 (Array.size_set cs idx _ ▸ idx) (node newLast))
+          (some l, cs'.set idx (node newLast) (by simp only [cs', Array.size_set]; omega))
     else
       (none, emptyArray)
   | leaf vs   => (some vs, emptyArray)

src/Lean/Data/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,9 +298,14 @@ 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,6 +595,22 @@ 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
@@ -1135,24 +1151,29 @@ private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermE
   throwError "{msg}{indentExpr e}\nhas type{indentExpr eType}"
 
 /--
-`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`
+`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)`
 -/
-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   =>
+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)
     let fullNamePrv := mkPrivateName env fullName
-    match env.find? fullNamePrv with
-    | some _ => some (structName, fullNamePrv)
-    | none   =>
-      if isStructure env structName then
-        (getStructureSubobjects env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
-      else
-        none
+    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
 
 /--
   Return `some (structName', fullName)` if `structName ++ fieldName` is an alias for `fullName`, and
@@ -1188,23 +1209,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
-    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]!
+    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)
       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)
-    else
-      throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
+        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? env structName (.mkSimple fieldName) then
+      if let some (baseStructName, fullName) ← findMethod? 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
@@ -1390,19 +1411,17 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       loop f lvals
     | LValResolution.projFn baseStructName structName fieldName =>
       let f ← mkBaseProjections baseStructName structName f
-      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
+      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
       else
-        unreachable!
+        let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
+        loop f lvals
     | 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,4 +424,87 @@ 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

@@ -137,7 +137,7 @@ private def mkFormat (e : Expr) : MetaM Expr := do
       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] none
+          liftCommandElabM do applyDerivingHandlers ``Repr #[name]
           resetSynthInstanceCache
           return ← mkRepr e
         catch ex =>

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

@@ -136,7 +136,7 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
           but is expected to be{indentD m!"{elhs} : {← inferType elhs}"}"
         failed := true
       unless ← isDefEqGuarded rhs erhs do
-        logErrorAt steps.back.term m!"\
+        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

src/Lean/Elab/Deriving/Basic.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Wojciech Nawrocki
 -/
 prelude
 import Lean.Elab.Command
+import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab
 open Command
@@ -55,13 +56,17 @@ 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) → (args? : Option (TSyntax ``Parser.Term.structInst)) → CommandElabM Bool
+def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
+
+/-- Deprecated - `DerivingHandler` no longer assumes arguments -/
+@[deprecated DerivingHandler (since := "2024-09-09")]
 def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
 
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) ← IO.mkRef {}
@@ -71,25 +76,21 @@ 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 registerDerivingHandlerWithArgs (className : Name) (handler : DerivingHandler) : IO Unit := do
+def registerDerivingHandler (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) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Unit := do
+def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
   match (← derivingHandlersRef.get).find? className with
   | some handlers =>
     for handler in handlers do
-      if (← handler typeNames args?) then
+      if (← handler typeNames) then
         return ()
     defaultHandler className typeNames
   | none => defaultHandler className typeNames
@@ -99,16 +100,16 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
     Term.processDefDeriving className declName
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
-  | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
+  | `(deriving instance $[$classes],* for $[$declNames],*) => do
      let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
-     for cls in classes, args? in argss? do
+     for cls in classes do
        try
          let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
          withRef cls do
-           if declNames.size == 1 && args?.isNone then
+           if declNames.size == 1 then
              if (← tryApplyDefHandler className declNames[0]!) then
                return ()
-           applyDerivingHandlers className declNames args?
+           applyDerivingHandlers className declNames
        catch ex =>
          logException ex
   | _ => throwUnsupportedSyntax
@@ -116,20 +117,19 @@ 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 $[with $argss?]?],*) =>
+  | `(Parser.Command.optDeriving| deriving $[$classes],*) =>
     let mut ret := #[]
-    for cls in classes, args? in argss? do
+    for cls in classes do
       let className ← realizeGlobalConstNoOverloadWithInfo cls
-      ret := ret.push { ref := cls, className := className, args? }
+      ret := ret.push { ref := cls, className := className }
     return ret
   | _ => return #[]
 
 def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit :=
-  withRef view.ref do applyDerivingHandlers view.className declNames view.args?
+  withRef view.ref do applyDerivingHandlers view.className declNames
 
 builtin_initialize
   registerTraceClass `Elab.Deriving

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

src/Lean/Elab/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/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/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/Structure.lean

@@ -22,7 +22,12 @@ namespace Lean.Elab.Command
 
 register_builtin_option structureDiamondWarning : Bool := {
   defValue := false
-  descr    := "enable/disable warning messages for structure diamonds"
+  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
@@ -806,9 +811,16 @@ private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
   let hasEq   := env.contains ``Eq
   let hasHEq  := env.contains ``HEq
   let hasUnit := env.contains ``PUnit
+  let hasProd := env.contains ``Prod
   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
@@ -928,8 +940,6 @@ private def mkInductiveType (view : StructView) (indFVar : Expr) (levelNames : L
   let levelParams := levelNames.map mkLevelParam
   let const := mkConst view.declName levelParams
   let ctorType ← forallBoundedTelescope ctor.type numParams fun params type => do
-    if type.containsFVar indFVar.fvarId! then
-      throwErrorAt view.ref "Recursive structures are not yet supported."
     let type := type.replace fun e =>
       if e == indFVar then
         mkAppN const (params.extract 0 numVars)
@@ -938,6 +948,23 @@ private def mkInductiveType (view : StructView) (indFVar : Expr) (levelNames : L
     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
@@ -1003,6 +1030,8 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
             else
               mkCoercionToCopiedParent levelParams params view parent.structName parent.type
           setStructureParents view.declName parentInfos
+          checkResolutionOrder view.declName
+
           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. -/
@@ -1040,6 +1069,8 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
     pure view
   elabStructureViewPostprocessing view
 
-builtin_initialize registerTraceClass `Elab.structure
+builtin_initialize
+  registerTraceClass `Elab.structure
+  registerTraceClass `Elab.structure.resolutionOrder
 
 end Lean.Elab.Command

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

@@ -112,7 +112,6 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
     | some ⟨w', exp1Val⟩ =>
       if h : w = w' then
         let newLhs := exp3Val + h ▸ exp1Val
-        -- TODO
         let expr ← mkAppM ``HAdd.hAdd #[toExpr newLhs, exp2]
         let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_left'
         return .visit { expr := expr, proof? := some proof }
@@ -178,6 +177,33 @@ def rewriteRulesPass : Pass := fun goal => do
   let some (_, newGoal) := result? | return none
   return newGoal
 
+/--
+Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
+them to substitute occurences of `x` within other hypotheses
+-/
+def embeddedConstraintPass : Pass := fun goal =>
+  goal.withContext do
+    let hyps ← goal.getNondepPropHyps
+    let relevanceFilter acc hyp := do
+      let typ ← hyp.getType
+      let_expr Eq α _ rhs := typ | return acc
+      let_expr Bool := α | return acc
+      let_expr Bool.true := rhs | return acc
+      let localDecl ← hyp.getDecl
+      let proof  := localDecl.toExpr
+      acc.addTheorem (.fvar hyp) proof
+    let relevantHyps : SimpTheoremsArray ← hyps.foldlM (init := #[]) relevanceFilter
+
+    let simpCtx : Simp.Context := {
+      config := { failIfUnchanged := false }
+      simpTheorems := relevantHyps
+      congrTheorems := (← getSimpCongrTheorems)
+    }
+
+    let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps)
+    let some (_, newGoal) := result? | return none
+    return newGoal
+
 /--
 Normalize with respect to Associativity and Commutativity.
 -/
@@ -196,7 +222,7 @@ def acNormalizePass : Pass := fun goal => do
 /--
 The normalization passes used by `bv_normalize` and thus `bv_decide`.
 -/
-def defaultPipeline : List Pass := [rewriteRulesPass]
+def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
 
 def passPipeline : MetaM (List Pass) := do
   let opts ← getOptions
@@ -222,8 +248,8 @@ def evalBVNormalize : Tactic := fun
   | `(tactic| bv_normalize) => do
     let g ← getMainGoal
     match ← bvNormalize g with
-    | some newGoal => setGoals [newGoal]
-    | none => setGoals []
+    | some newGoal => replaceMainGoal [newGoal]
+    | none => replaceMainGoal []
   | _ => throwUnsupportedSyntax
 
 end Frontend.Normalize

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -465,7 +465,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
         let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
         let shadowed := found.contains localDecl.userName
         if inaccessible || shadowed then
-          if let `(binderIdent| $h:ident) := hs.back then
+          if let `(binderIdent| $h:ident) := hs.back! then
             let newName := h.getId
             lctx := lctx.setUserName localDecl.fvarId newName
             info := info.push (localDecl.fvarId, h)

src/Lean/Elab/Tactic/Config.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Kyle Miller
 -/
 prelude
 import Lean.Meta.Eval
@@ -10,25 +10,174 @@ import Lean.Elab.SyntheticMVars
 import Lean.Linter.MissingDocs
 
 namespace Lean.Elab.Tactic
-open Meta
-macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command =>
- `(unsafe def evalUnsafe (e : Expr) : TermElabM $type :=
-    Meta.evalExpr' (safety := .unsafe) $type ``$type e
-   @[implemented_by evalUnsafe] opaque eval (e : Expr) : TermElabM $type
-   $[$doc?:docComment]?
-   def $elabName (optConfig : Syntax) : TermElabM $type := do
-     if optConfig.isNone then
-       return { : $type }
-     else
-       let c ← withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do
-         let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type)
-         Term.synthesizeSyntheticMVarsNoPostponing
-         instantiateMVars c
-       eval c
-  )
+open Meta Parser.Tactic Command
+
+private structure ConfigItemView where
+  ref : Syntax
+  option : Ident
+  value : Term
+  /-- Whether this was using `+`/`-`, to be able to give a better error message on type mismatch. -/
+  (bool : Bool := false)
+
+/-- Interprets the `config` as an array of option/value pairs. -/
+private def mkConfigItemViews (c : TSyntaxArray ``configItem) : Array ConfigItemView :=
+  c.map fun item =>
+    match item with
+    | `(configItem| ($option:ident := $value)) => { ref := item, option, value }
+    | `(configItem| +$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``true }
+    | `(configItem| -$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``false }
+    | `(config| (config%$tk := $value)) => { ref := item, option := mkCIdentFrom tk `config, value := value }
+    | _ => { ref := item, option := ⟨Syntax.missing⟩, value := ⟨Syntax.missing⟩ }
+
+/--
+Expands a field access into full field access like `toB.toA.x`.
+Returns that and the last projection function for `x` itself.
+-/
+private def expandFieldName (structName : Name) (fieldName : Name) : MetaM (Name × Name) := do
+  let env ← getEnv
+  unless isStructure env structName do throwError "'{.ofConstName structName}' is not a structure"
+  let some baseStructName := findField? env structName fieldName
+    | throwError "structure '{.ofConstName structName}' does not have a field named '{fieldName}'"
+  let some path := getPathToBaseStructure? env baseStructName structName
+    | throwError "(internal error) failed to access field '{fieldName}' in parent structure"
+  let field := path.foldl (init := .anonymous) (fun acc s => Name.appendCore acc <| Name.mkSimple s.getString!) ++ fieldName
+  let fieldInfo := (getFieldInfo? env baseStructName fieldName).get!
+  return (field, fieldInfo.projFn)
+
+
+/--
+Given a hierarchical name `field`, returns the fully resolved field access, the base struct name, and the last projection function.
+-/
+private partial def expandField (structName : Name) (field : Name) : MetaM (Name × Name) := do
+  match field with
+  | .num .. | .anonymous => throwError m!"invalid configuration field"
+  | .str .anonymous fieldName => expandFieldName structName (Name.mkSimple fieldName)
+  | .str field' fieldName =>
+    let (field', projFn) ← expandField structName field'
+    let notStructure {α} : MetaM α := throwError "field '{field'}' of structure '{.ofConstName structName}' is not a structure"
+    let .const structName' _ := (← getConstInfo projFn).type.getForallBody | notStructure
+    unless isStructure (← getEnv) structName' do notStructure
+    let (field'', projFn) ← expandFieldName structName' (Name.mkSimple fieldName)
+    return (field' ++ field'', projFn)
+
+/-- Elaborates a tactic configuration. -/
+private def elabConfig (recover : Bool) (structName : Name) (items : Array ConfigItemView) : TermElabM Expr :=
+  withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext do
+    let mkStructInst (source? : Option Term) (fields : TSyntaxArray ``Parser.Term.structInstField) : TermElabM Term :=
+      match source? with
+      | some source => `({$source with $fields* : $(mkCIdent structName)})
+      | none        => `({$fields* : $(mkCIdent structName)})
+    let mut source? : Option Term := none
+    let mut seenFields : NameSet := {}
+    let mut fields : TSyntaxArray ``Parser.Term.structInstField := #[]
+    for item in items do
+      try
+        let option := item.option.getId.eraseMacroScopes
+        if option == `config then
+          unless fields.isEmpty do
+            -- Flush fields. Even though these values will not be used, we still want to elaborate them.
+            source? ← mkStructInst source? fields
+            seenFields := {}
+            fields := #[]
+          let valSrc ← withRef item.value `(($item.value : $(mkCIdent structName)))
+          if let some source := source? then
+            source? ← withRef item.value `({$valSrc, $source with : $(mkCIdent structName)})
+          else
+            source? := valSrc
+        else
+          addCompletionInfo <| CompletionInfo.fieldId item.option option {} structName
+          let (path, projFn) ← withRef item.option <| expandField structName option
+          if item.bool then
+            -- Verify that the type is `Bool`
+            unless (← getConstInfo projFn).type.bindingBody! == .const ``Bool [] do
+              throwErrorAt item.ref m!"option is not boolean-valued, so '({option} := ...)' syntax must be used"
+          let value ←
+            match item.value with
+            | `(by $seq:tacticSeq) =>
+              -- Special case: `(opt := by tacs)` uses the `tacs` syntax itself
+              withRef item.value <| `(Unhygienic.run `(tacticSeq| $seq))
+            | value => pure value
+          if seenFields.contains path then
+            -- Flush fields. There is a duplicate, but we still want to elaborate both.
+            source? ← mkStructInst source? fields
+            seenFields := {}
+            fields := #[]
+          fields := fields.push <| ← `(Parser.Term.structInstField|
+            $(mkCIdentFrom item.option path (canonical := true)):ident := $value)
+          seenFields := seenFields.insert path
+      catch ex =>
+        if recover then
+          logException ex
+        else
+          throw ex
+    let stx : Term ← mkStructInst source? fields
+    let e ← Term.withSynthesize <| Term.elabTermEnsuringType stx (mkConst structName)
+    instantiateMVars e
+
+private def mkConfigElaborator
+    (doc? : Option (TSyntax ``Parser.Command.docComment)) (elabName type monadName : Ident)
+    (adapt recover : Term) : MacroM (TSyntax `command) := do
+  let empty ← withRef type `({ : $type})
+  `(unsafe def evalUnsafe (e : Expr) : TermElabM $type :=
+      Meta.evalExpr' (safety := .unsafe) $type ``$type e
+    @[implemented_by evalUnsafe] opaque eval (e : Expr) : TermElabM $type
+    $[$doc?:docComment]?
+    def $elabName (optConfig : Syntax) : $monadName $type := $adapt do
+      let recover := $recover
+      let go : TermElabM $type := withRef optConfig do
+        let items := mkConfigItemViews (getConfigItems optConfig)
+        if items.isEmpty then
+          return $empty
+        unless (← getEnv).contains ``$type do
+          throwError m!"error evaluating configuration, environment does not yet contain type {``$type}"
+        let c ← elabConfig recover ``$type items
+        if c.hasSyntheticSorry then
+          -- An error is already logged, return the default.
+          return $empty
+        if c.hasSorry then
+          throwError m!"configuration contains 'sorry'"
+        try
+          let res ← eval c
+          return res
+        catch ex =>
+          let msg := m!"error evaluating configuration\n{indentD c}\n\nException: {ex.toMessageData}"
+          if false then
+            logError msg
+            return $empty
+          else
+            throwError msg
+      go)
+
+/-!
+`declare_config_elab elabName TypeName` declares a function `elabName : Syntax → TacticM TypeName`
+that elaborates a tactic configuration.
+The tactic configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`,
+and these can also be wrapped in null nodes (for example, from `(config)?`).
+
+The elaborator responds to the current recovery state.
+
+For defining elaborators for commands, use `declare_command_config_elab`.
+-/
+macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command => do
+  mkConfigElaborator doc? elabName type (mkCIdent ``TacticM) (mkCIdent ``id) (← `((← read).recover))
 
 open Linter.MissingDocs in
 @[builtin_missing_docs_handler Elab.Tactic.configElab]
 def checkConfigElab : SimpleHandler := mkSimpleHandler "config elab"
 
+/-!
+`declare_command_config_elab elabName TypeName` declares a function `elabName : Syntax → CommandElabM TypeName`
+that elaborates a command configuration.
+The configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`,
+and these can also be wrapped in null nodes (for example, from `(config)?`).
+
+The elaborator has error recovery enabled.
+-/
+macro (name := commandConfigElab) doc?:(docComment)? "declare_command_config_elab" elabName:ident type:ident : command => do
+  mkConfigElaborator doc? elabName type (mkCIdent ``CommandElabM) (mkCIdent ``liftTermElabM) (mkCIdent ``true)
+
+open Linter.MissingDocs in
+@[builtin_missing_docs_handler Elab.Tactic.commandConfigElab]
+def checkCommandConfigElab : SimpleHandler := mkSimpleHandler "config elab"
+
 end Lean.Elab.Tactic

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

@@ -11,6 +11,8 @@ import Lean.Elab.Tactic.Conv.Basic
 namespace Lean.Elab.Tactic.Conv
 open Meta
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure ()
+
 private def congrImplies (mvarId : MVarId) : MetaM (List MVarId) := do
   let [mvarId₁, mvarId₂, _, _] ← mvarId.apply (← mkConstWithFreshMVarLevels ``implies_congr) | throwError "'apply implies_congr' unexpected result"
   let mvarId₁ ← markAsConvGoal mvarId₁
@@ -72,6 +74,14 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) (
     mvarIdsNewInsts := mvarIdsNewInsts ++ mvarIdsNewInsts'
   return (proof, mvarIdsNew, mvarIdsNewInsts)
 
+private def resolveRhs (tacticName : String) (rhs rhs' : Expr) : MetaM Unit := do
+  unless (← isDefEqGuarded rhs rhs') do
+    throwError "invalid '{tacticName}' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+
+private def resolveRhsFromProof (tacticName : String) (rhs proof : Expr) : MetaM Unit := do
+  let some (_, _, rhs') := (← whnf (← inferType proof)).eq? | throwError "'{tacticName}' conv tactic failed, equality expected"
+  resolveRhs tacticName rhs rhs'
+
 def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
     MetaM (List (Option MVarId)) := mvarId.withContext do
   let origTag ← mvarId.getTag
@@ -82,9 +92,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
   else if lhs.isApp then
     let (proof, mvarIdsNew, mvarIdsNewInsts) ←
       mkCongrThm origTag lhs.getAppFn lhs.getAppArgs addImplicitArgs nameSubgoals
-    let some (_, _, rhs') := (← whnf (← inferType proof)).eq? | throwError "'congr' conv tactic failed, equality expected"
-    unless (← isDefEqGuarded rhs rhs') do
-      throwError "invalid 'congr' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+    resolveRhsFromProof "congr" rhs proof
     mvarId.assign proof
     return mvarIdsNew.toList ++ mvarIdsNewInsts.toList
   else
@@ -93,42 +101,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
 @[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
   replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
 
--- mvarIds is the list of goals produced by congr. We only want to change the one at position `i`
--- so this closes all other equality goals with `rfl.`. There are non-equality goals produced
--- by `congr` (e.g. dependent instances), these are kept as goals.
-private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
-  TacticM Unit := do
-  if i >= 0 then
-    let i := i.toNat
-    if h : i < mvarIds.length then
-      let mut otherGoals := #[]
-      for mvarId? in mvarIds, j in [:mvarIds.length] do
-        match mvarId? with
-        | none => pure ()
-        | some mvarId =>
-          if i != j then
-            if (← mvarId.getType').isEq then
-              mvarId.refl
-            else
-              -- If its not an equality, it's likely a class constraint, to be left open
-              otherGoals := otherGoals.push mvarId
-      match mvarIds[i] with
-      | none => throwError "cannot select argument"
-      | some mvarId => replaceMainGoal (mvarId :: otherGoals.toList)
-      return ()
-  throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)"
-
-@[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure ()
-
-@[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do
-  let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
-  selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
-
-@[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do
-  let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
-  selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
-
-/-- Implementation of `arg 0` -/
+/-- Implementation of `arg 0`. -/
 def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let (lhs, rhs) ← getLhsRhsCore mvarId
   let lhs := (← instantiateMVars lhs).cleanupAnnotations
@@ -136,24 +109,137 @@ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
     throwError "invalid 'arg 0' conv tactic, application expected{indentExpr lhs}"
   lhs.withApp fun f xs => do
     let (g, mvarNew) ← mkConvGoalFor f
-    mvarId.assign (← xs.foldlM (fun mvar a => Meta.mkCongrFun mvar a) mvarNew)
-    let rhs' := mkAppN g xs
-    unless ← isDefEqGuarded rhs rhs' do
-      throwError "invalid 'arg 0' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+    mvarId.assign (← xs.foldlM (init := mvarNew) Meta.mkCongrFun)
+    resolveRhs "arg 0" rhs (mkAppN g xs)
     return mvarNew.mvarId!
 
-@[builtin_tactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
-  match stx with
-  | `(conv| arg $[@%$tk?]? $i:num) =>
-    let i := i.getNat
-    if i == 0 then
-      replaceMainGoal [← congrFunN (← getMainGoal)]
+private partial def mkCongrArgZeroThm (tacticName : String) (origTag : Name) (f : Expr) (args : Array Expr) :
+    MetaM (Expr × MVarId × Array MVarId) := do
+  let funInfo ← getFunInfoNArgs f args.size
+  let some congrThm ← mkCongrSimpCore? f funInfo (← getCongrSimpKindsForArgZero funInfo) (subsingletonInstImplicitRhs := false)
+    | throwError "'{tacticName}' conv tactic failed to create congruence theorem"
+  unless congrThm.argKinds[0]! matches .eq do
+    throwError "'{tacticName}' conv tactic failed, cannot select argument"
+  let mut eNew := f
+  let mut proof := congrThm.proof
+  let mut mvarIdNew? := none
+  let mut mvarIdsNewInsts := #[]
+  for h : i in [:congrThm.argKinds.size] do
+    let arg := args[i]!
+    let argInfo := funInfo.paramInfo[i]!
+    match congrThm.argKinds[i] with
+    | .fixed | .cast =>
+      eNew := mkApp eNew arg
+      proof := mkApp proof arg
+    | .eq =>
+      let (rhs, mvarNew) ← mkConvGoalFor arg origTag
+      eNew := mkApp eNew rhs
+      proof := mkApp3 proof arg rhs mvarNew
+      if mvarIdNew?.isSome then throwError "'{tacticName}' conv tactic failed, cannot select argument"
+      mvarIdNew? := some mvarNew.mvarId!
+    | .subsingletonInst =>
+      proof := mkApp proof arg
+      let rhs ← mkFreshExprMVar (← whnf (← inferType proof)).bindingDomain!
+      eNew := mkApp eNew rhs
+      proof := mkApp proof rhs
+      mvarIdsNewInsts := mvarIdsNewInsts.push rhs.mvarId!
+    | .heq | .fixedNoParam => unreachable!
+  let proof' ← args[congrThm.argKinds.size:].foldlM (init := proof) mkCongrFun
+  return (proof', mvarIdNew?.get!, mvarIdsNewInsts)
+
+/--
+Implements `arg` for foralls. If `domain` is true, accesses the domain, otherwise accesses the codomain.
+-/
+def congrArgForall (tacticName : String) (domain : Bool) (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List MVarId) := do
+  let .forallE n t b bi := lhs | unreachable!
+  if domain then
+    if !b.hasLooseBVars then
+      let (t', g) ← mkConvGoalFor t (← mvarId.getTag)
+      mvarId.assign <| ← mkAppM ``implies_congr #[g, ← mkEqRefl b]
+      resolveRhs tacticName rhs (.forallE n t' b bi)
+      return [g.mvarId!]
+    else if ← isProp b <&&> isProp lhs then
+      let (_rhs, g) ← mkConvGoalFor t (← mvarId.getTag)
+      let proof ← mkAppM ``forall_prop_congr_dom #[g, .lam n t b .default]
+      resolveRhsFromProof tacticName rhs proof
+      mvarId.assign proof
+      return [g.mvarId!]
     else
-      let i := i - 1
-      let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false)
-      selectIdx "arg" mvarIds i
+      throwError m!"'{tacticName}' conv tactic failed, cannot select domain"
+  else
+    withLocalDeclD (← mkFreshUserName n) t fun arg => do
+      let u ← getLevel t
+      let q := b.instantiate1 arg
+      let (q', g) ← mkConvGoalFor q (← mvarId.getTag)
+      let v ← getLevel q
+      let proof := mkAppN (.const ``pi_congr [u, v])
+        #[t, .lam n t b .default, ← mkLambdaFVars #[arg] q', ← mkLambdaFVars #[arg] g]
+      resolveRhsFromProof tacticName rhs proof
+      mvarId.assign proof
+      return [g.mvarId!]
+
+/-- Implementation of `arg i`. -/
+def congrArgN (tacticName : String) (mvarId : MVarId) (i : Int) (explicit : Bool) : MetaM (List MVarId) := mvarId.withContext do
+  let (lhs, rhs) ← getLhsRhsCore mvarId
+  let lhs := (← instantiateMVars lhs).cleanupAnnotations
+  if lhs.isForall then
+    if i < -2 || i == 0 || i > 2 then throwError "invalid '{tacticName}' conv tactic, index is out of bounds for pi type"
+    let domain := i == 1 || i == -2
+    return ← congrArgForall tacticName domain mvarId lhs rhs
+  else if lhs.isApp then
+    lhs.withApp fun f xs => do
+      let (f, xs) ← applyArgs f xs i
+      let (proof, mvarIdNew, mvarIdsNewInsts) ← mkCongrArgZeroThm tacticName (← mvarId.getTag) f xs
+      resolveRhsFromProof tacticName rhs proof
+      mvarId.assign proof
+      return mvarIdNew :: mvarIdsNewInsts.toList
+  else
+    throwError "invalid '{tacticName}' conv tactic, application or implication expected{indentExpr lhs}"
+where
+  applyArgs (f : Expr) (xs : Array Expr) (i : Int) : MetaM (Expr × Array Expr) := do
+    if explicit then
+      let i := if i > 0 then i - 1 else i + xs.size
+      if i < 0 || i ≥ xs.size then
+        throwError "invalid '{tacticName}' tactic, application has {xs.size} arguments but the index is out of bounds"
+      let idx := i.natAbs
+      return (mkAppN f xs[0:idx], xs[idx:])
+    else
+      let mut fType ← inferType f
+      let mut j := 0
+      let mut explicitIdxs := #[]
+      for k in [0:xs.size] do
+        unless fType.isForall do
+          fType ← withTransparency .all <| whnf (fType.instantiateRevRange j k xs)
+          j := k
+        let .forallE _ _ b bi := fType | failure
+        fType := b
+        if bi.isExplicit then
+          explicitIdxs := explicitIdxs.push k
+      let i := if i > 0 then i - 1 else i + explicitIdxs.size
+      if i < 0 || i ≥ explicitIdxs.size then
+        throwError "invalid '{tacticName}' tactic, application has {xs.size} explicit argument(s) but the index is out of bounds"
+      let idx := explicitIdxs[i.natAbs]!
+      return (mkAppN f xs[0:idx], xs[idx:])
+
+def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit := do
+  if i == 0 then
+    replaceMainGoal [← congrFunN (← getMainGoal)]
+  else
+    replaceMainGoal (← congrArgN tacticName (← getMainGoal) i explicit)
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.arg] def elabArg : Tactic := fun stx => do
+  match stx with
+  | `(conv| arg $[@%$tk?]? $[-%$neg?]? $i:num) =>
+    let i : Int := if neg?.isSome then -i.getNat else i.getNat
+    evalArg "arg" i (explicit := tk?.isSome)
   | _ => throwUnsupportedSyntax
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do
+  evalArg "lhs" (-2) false
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do
+  evalArg "rhs" (-1) false
+
 @[builtin_tactic Lean.Parser.Tactic.Conv.«fun»] def evalFun : Tactic := fun _ => do
   let mvarId ← getMainGoal
   mvarId.withContext do
@@ -163,9 +249,7 @@ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
       | throwError "invalid 'fun' conv tactic, application expected{indentExpr lhs}"
     let (g, mvarNew) ← mkConvGoalFor f
     mvarId.assign (← Meta.mkCongrFun mvarNew a)
-    let rhs' := .app g a
-    unless ← isDefEqGuarded rhs rhs' do
-      throwError "invalid 'fun' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+    resolveRhs "fun" rhs (.app g a)
     replaceMainGoal [mvarNew.mvarId!]
 
 def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId) := do
@@ -209,9 +293,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
         let (qa, mvarNew) ← mkConvGoalFor pa
         let q ← mkLambdaFVars #[a] qa
         let h ← mkLambdaFVars #[a] mvarNew
-        let rhs' ← mkForallFVars #[a] qa
-        unless (← isDefEqGuarded rhs rhs') do
-          throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+        resolveRhs "ext" rhs (← mkForallFVars #[a] qa)
         return (q, h, mvarNew)
       let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
       mvarId.assign proof
@@ -238,4 +320,22 @@ private def ext (userName? : Option Name) : TacticM Unit := do
     for id in ids do
       withRef id <| ext id.getId
 
+-- syntax (name := enter) "enter" " [" enterArg,+ "]" : conv
+@[builtin_tactic Lean.Parser.Tactic.Conv.enter] def evalEnter : Tactic := fun stx => do
+  let token := stx[0]
+  let lbrak := stx[1]
+  let enterArgsAndSeps := stx[2].getArgs
+  -- show initial state up to (incl.) `[`
+  withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
+  let numEnterArgs := (enterArgsAndSeps.size + 1) / 2
+  for i in [:numEnterArgs] do
+    let enterArg := enterArgsAndSeps[2 * i]!
+    let sep := enterArgsAndSeps.getD (2 * i + 1) .missing
+    -- show state up to (incl.) next `,` and show errors on `enterArg`
+    withTacticInfoContext (mkNullNode #[enterArg, sep]) <| withRef enterArg do
+      match enterArg with
+      | `(Parser.Tactic.Conv.enterArg| $arg:argArg) => evalTactic (← `(conv| arg $arg))
+      | `(Parser.Tactic.Conv.enterArg| $id:ident)   => evalTactic (← `(conv| ext $id))
+      | _ => pure ()
+
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Induction.lean

@@ -208,15 +208,28 @@ private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM N
 private def isWildcard (altStx : Syntax) : Bool :=
   getAltName altStx == `_
 
-private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
+private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit := do
+  let mut seenNames : Array Name := #[]
   for h : i in [:altsSyntax.size] do
     let altStx := altsSyntax[i]
     if getAltName altStx == `_ && i != altsSyntax.size - 1 then
       withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative"
     let altName := getAltName altStx
     if altName != `_ then
+      if seenNames.contains altName then
+        throwErrorAt altStx s!"duplicate alternative name '{altName}'"
+      seenNames := seenNames.push altName
       unless alts.any (·.name == altName) do
-        throwErrorAt altStx "invalid alternative name '{altName}'"
+        let unhandledAlts := alts.filter fun alt => !seenNames.contains alt.name
+        let msg :=
+          if unhandledAlts.isEmpty then
+            m!"invalid alternative name '{altName}', no unhandled alternatives"
+          else
+            let unhandledAltsMessages := unhandledAlts.map (m!"{·.name}")
+            let unhandledAlts := MessageData.orList unhandledAltsMessages.toList
+            m!"invalid alternative name '{altName}', expected {unhandledAlts}"
+        throwErrorAt altStx msg
+
 
 /-- Given the goal `altMVarId` for a given alternative that introduces `numFields` new variables,
     return the number of explicit variables. Recall that when the `@` is not used, only the explicit variables can

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

@@ -696,9 +696,9 @@ the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
 def omegaDefault : TacticM Unit := omegaTactic {}
 
 @[builtin_tactic Lean.Parser.Tactic.omega]
-def evalOmega : Tactic := fun
-  | `(tactic| omega $[$cfg]?) => do
-    let cfg ← elabOmegaConfig (mkOptionalNode cfg)
+def evalOmega : Tactic
+  | `(tactic| omega $cfg:optConfig) => do
+    let cfg ← elabOmegaConfig cfg
     omegaTactic cfg
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Tactic/Simp.lean

@@ -85,7 +85,7 @@ private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.Disc
 /-
   `optConfig` is of the form `("(" "config" ":=" term ")")?`
 -/
-def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.Config := do
+def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Config := do
   match kind with
   | .simp    => elabSimpConfigCore optConfig
   | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
@@ -437,7 +437,7 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
   Simp.reportDiag stats
 
 /-
-  "simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
+  "simp" optConfig (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
   (location)?
 -/
 @[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -25,11 +25,11 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 @[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
   match stx with
   | `(tactic|
-      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
+      simp?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
     let stx ← if bang.isSome then
-      `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| simp!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
-      `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
     let stats ← dischargeWrapper.with fun discharge? =>
       simpLocation ctx (simprocs := simprocs) discharge? <|
@@ -41,11 +41,11 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 
 @[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
+  | `(tactic| simp_all?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
-      `(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
+      `(tactic| simp_all!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
     else
-      `(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
+      `(tactic| simp_all%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
     let { ctx, .. } ← mkSimpContext stx (eraseLocal := true)
       (kind := .simpAll) (ignoreStarArg := true)
     let (result?, stats) ← simpAll (← getMainGoal) ctx
@@ -81,11 +81,11 @@ where
 
 @[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
+  | `(tactic| dsimp?%$tk $[!%$bang]? $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
-      `(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| dsimp!%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
     else
-      `(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, .. } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
     let stats ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)

src/Lean/Elab/Tactic/Simpa.lean

@@ -31,9 +31,9 @@ deriving instance Repr for UseImplicitLambdaResult
 
 @[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
   match stx with
-  | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
+  | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]?
         $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
-    let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
+    let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
     let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
@@ -96,11 +96,11 @@ deriving instance Repr for UseImplicitLambdaResult
         g.assumption; pure stats
       if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
         let stx ← match ← mkSimpOnly stx stats.usedTheorems with
-          | `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
+          | `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
             if unfold.isSome then
-              `(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
+              `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
             else
-              `(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
+              `(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
           | _ => unreachable!
         TryThis.addSuggestion tk stx (origSpan? := ← getRef)
       return stats.diag

src/Lean/Elab/Tactic/SolveByElim.lean

@@ -68,7 +68,7 @@ def processSyntax (cfg : SolveByElimConfig := {}) (only star : Bool) (add remove
 @[builtin_tactic Lean.Parser.Tactic.applyAssumption]
 def evalApplyAssumption : Tactic := fun stx =>
   match stx with
-  | `(tactic| apply_assumption $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+  | `(tactic| apply_assumption $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
     let (star, add, remove) := parseArgs t
     let use := parseUsing use
     let cfg ← elabConfig (mkOptionalNode cfg)
@@ -86,7 +86,7 @@ See `Lean.MVarId.applyRules` for a `MetaM` level analogue of this tactic.
 @[builtin_tactic Lean.Parser.Tactic.applyRules]
 def evalApplyRules : Tactic := fun stx =>
   match stx with
-  | `(tactic| apply_rules $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+  | `(tactic| apply_rules $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
     let (star, add, remove) := parseArgs t
     let use := parseUsing use
     let cfg ← elabApplyRulesConfig (mkOptionalNode cfg)
@@ -95,16 +95,15 @@ def evalApplyRules : Tactic := fun stx =>
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.solveByElim]
-def evalSolveByElim : Tactic := fun stx =>
-  match stx with
-  | `(tactic| solve_by_elim $[*%$s]? $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+def evalSolveByElim : Tactic
+  | `(tactic| solve_by_elim $[*%$s]? $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
     let (star, add, remove) := parseArgs t
     let use := parseUsing use
     let goals ← if s.isSome then
       getGoals
     else
       pure [← getMainGoal]
-    let cfg ← elabConfig (mkOptionalNode cfg)
+    let cfg ← elabConfig cfg
     let [] ← processSyntax cfg o.isSome star add remove use goals |
       throwError "solve_by_elim unexpectedly returned subgoals"
     pure ()

src/Lean/Environment.lean

@@ -328,7 +328,7 @@ private def invalidExtMsg := "invalid environment extension has been accessed"
 
 unsafe def setState {σ} (ext : Ext σ) (exts : Array EnvExtensionState) (s : σ) : Array EnvExtensionState :=
   if h : ext.idx < exts.size then
-    exts.set ⟨ext.idx, h⟩ (unsafeCast s)
+    exts.set ext.idx (unsafeCast s)
   else
     have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
     panic! invalidExtMsg
@@ -638,20 +638,21 @@ end TagDeclarationExtension
 /-- Environment extension for mapping declarations to values.
     Declarations must only be inserted into the mapping in the module where they were declared. -/
 
-def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
+def MapDeclarationExtension (α : Type) := PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
 
 def mkMapDeclarationExtension (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
-  registerSimplePersistentEnvExtension {
-    name          := name,
-    addImportedFn := fun _ => {},
-    addEntryFn    := fun s n => s.insert n.1 n.2 ,
-    toArrayFn     := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
+  registerPersistentEnvExtension {
+    name            := name,
+    mkInitial       := pure {}
+    addImportedFn   := fun _ => pure {}
+    addEntryFn      := fun s (n, v) => s.insert n v
+    exportEntriesFn := fun s => s.toArray
   }
 
 namespace MapDeclarationExtension
 
 instance : Inhabited (MapDeclarationExtension α) :=
-  inferInstanceAs (Inhabited (SimplePersistentEnvExtension ..))
+  inferInstanceAs (Inhabited (PersistentEnvExtension ..))
 
 def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
   have : Inhabited Environment := ⟨env⟩

src/Lean/Expr.lean

@@ -1836,6 +1836,27 @@ The delaborator uses `pp` options.
 def setPPUniverses (e : Expr) (flag : Bool) :=
   e.setOption `pp.universes flag
 
+/--
+Annotate `e` with `pp.piBinderTypes := flag`
+The delaborator uses `pp` options.
+-/
+def setPPPiBinderTypes (e : Expr) (flag : Bool) :=
+  e.setOption `pp.piBinderTypes flag
+
+/--
+Annotate `e` with `pp.funBinderTypes := flag`
+The delaborator uses `pp` options.
+-/
+def setPPFunBinderTypes (e : Expr) (flag : Bool) :=
+  e.setOption `pp.funBinderTypes flag
+
+/--
+Annotate `e` with `pp.explicit := flag`
+The delaborator uses `pp` options.
+-/
+def setPPNumericTypes (e : Expr) (flag : Bool) :=
+  e.setOption `pp.numericTypes flag
+
 /--
 If `e` is an application `f a_1 ... a_n` annotate `f`, `a_1` ... `a_n` with `pp.explicit := false`,
 and annotate `e` with `pp.explicit := true`.

src/Lean/Message.lean

@@ -279,6 +279,14 @@ def ofList : List MessageData → MessageData
 def ofArray (msgs : Array MessageData) : MessageData :=
   ofList msgs.toList
 
+/-- Puts `MessageData` into a comma-separated list with `"or"` at the back (no Oxford comma).
+Best used on non-empty lists; returns `"– none –"` for an empty list.  -/
+def orList (xs : List MessageData) : MessageData :=
+  match xs with
+  | [] => "– none –"
+  | [x] => "'" ++ x ++ "'"
+  | _ => joinSep (xs.dropLast.map (fun x => "'" ++ x ++ "'")) ", " ++ " or '" ++ xs.getLast! ++ "'"
+
 /-- Puts `MessageData` into a comma-separated list with `"and"` at the back (no Oxford comma).
 Best used on non-empty lists; returns `"– none –"` for an empty list.  -/
 def andList (xs : List MessageData) : MessageData :=

src/Lean/Meta/ArgsPacker.lean

@@ -56,7 +56,7 @@ Given a telescope of FVars of type `tᵢ`, iterates `PSigma` to produce the type
 `t₁ ⊗' t₂ …`.
 -/
 def packType (xs : Array Expr) : MetaM Expr := do
-  let mut d ← inferType xs.back
+  let mut d ← inferType xs.back!
   for x in xs.pop.reverse do
     d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)]
   return d
@@ -217,7 +217,7 @@ Helpers for iterated `PSum`.
 
 /-- Given types `#[t₁, t₂,…]`, returns the type `t₁ ⊕' t₂ …`. -/
 def packType (ds : Array Expr) : MetaM Expr := do
-  let mut r := ds.back
+  let mut r := ds.back!
   for d in ds.pop.reverse do
     r ← mkAppM ``PSum #[d, r]
   return r
@@ -335,7 +335,7 @@ def uncurryTypeND (types : Array Expr) : MetaM Expr := do
     unless type.isArrow do
       throwError "Mutual.uncurryTypeND: Expected non-dependent types, got {type}"
   let codomains := types.map (·.bindingBody!)
-  let t' := codomains.back
+  let t' := codomains.back!
   codomains.pop.forM fun t =>
     unless ← isDefEq t t' do
       throwError "Mutual.uncurryTypeND: Expected equal codomains, but got {t} and {t'}"

src/Lean/Meta/Check.lean

@@ -37,8 +37,9 @@ private def getFunctionDomain (f : Expr) : MetaM (Expr × BinderInfo) := do
   | _                    => throwFunctionExpected f
 
 /--
-Given two expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true` to
-expose "implicit" differences. For example, suppose `a` and `b` are of the form
+Given two expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true`
+and other `pp` options to expose "implicit" differences.
+For example, suppose `a` and `b` are of the form
 ```lean
 @HashMap Nat Nat eqInst hasInst1
 @HashMap Nat Nat eqInst hasInst2
@@ -67,7 +68,8 @@ has type
 but is expected to have type
   @HashMap Nat Nat eqInst hasInst2
 ```
-Remark: this method implements a simple heuristic, we should extend it as we find other counterintuitive
+
+Remark: this method implements simple heuristics; we should extend it as we find other counterintuitive
 error messages.
 -/
 partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
@@ -123,6 +125,15 @@ where
                 firstExplicitDiff? := firstExplicitDiff? <|> some i
               else
                 firstImplicitDiff? := firstImplicitDiff? <|> some i
+          -- Some special cases
+          let fn? : Option Name :=
+            match a.getAppFn, b.getAppFn with
+            | .const ca .., .const cb .. => if ca == cb then ca else none
+            | _, _ => none
+          if fn? == ``OfNat.ofNat && as.size ≥ 3 && firstImplicitDiff? == some 0 then
+            -- Even if there is an explicit diff, it is better to see that the type is different.
+            return (a.setPPNumericTypes true, b.setPPNumericTypes true)
+          -- General case
           if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
             let (ai, bi) ← visit as[i]! bs[i]!
             as := as.set! i ai
@@ -133,6 +144,28 @@ where
             return (a, b)
           else
             return (a.setPPExplicit true, b.setPPExplicit true)
+      | .forallE na ta ba bia, .forallE nb tb bb bib =>
+        if !(← isDefEq ta tb) then
+          let (ta, tb) ← visit ta tb
+          let a := Expr.forallE na ta ba bia
+          let b := Expr.forallE nb tb bb bib
+          return (a.setPPPiBinderTypes true, b.setPPPiBinderTypes true)
+        else
+          -- Then bodies must not be defeq.
+          withLocalDeclD na ta fun arg => do
+            let (ba', bb') ← visit (ba.instantiate1 arg) (bb.instantiate1 arg)
+            return (Expr.forallE na ta (ba'.abstract #[arg]) bia, Expr.forallE nb tb (bb'.abstract #[arg]) bib)
+      | .lam na ta ba bia, .lam nb tb bb bib =>
+        if !(← isDefEq ta tb) then
+          let (ta, tb) ← visit ta tb
+          let a := Expr.lam na ta ba bia
+          let b := Expr.lam nb tb bb bib
+          return (a.setPPFunBinderTypes true, b.setPPFunBinderTypes true)
+        else
+          -- Then bodies must not be defeq.
+          withLocalDeclD na ta fun arg => do
+            let (ba', bb') ← visit (ba.instantiate1 arg) (bb.instantiate1 arg)
+            return (Expr.lam na ta (ba'.abstract #[arg]) bia, Expr.lam nb tb (bb'.abstract #[arg]) bib)
       | _, _ => return (a, b)
     catch _ =>
       return (a, b)

src/Lean/Meta/Closure.lean

@@ -226,7 +226,7 @@ partial def pickNextToProcessAux (lctx : LocalContext) (i : Nat) (toProcess : Ar
   if h : i < toProcess.size then
     let elem' := toProcess.get ⟨i, h⟩
     if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then
-      pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ elem) elem'
+      pickNextToProcessAux lctx (i+1) (toProcess.set i elem) elem'
     else
       pickNextToProcessAux lctx (i+1) toProcess elem
   else
@@ -239,7 +239,7 @@ def pickNextToProcess? : ClosureM (Option ToProcessElement) := do
     pure none
   else
     modifyGet fun s =>
-      let elem      := s.toProcess.back
+      let elem      := s.toProcess.back!
       let toProcess := s.toProcess.pop
       let (elem, toProcess) := pickNextToProcessAux lctx 0 toProcess elem
       (some elem, { s with toProcess := toProcess })

src/Lean/Meta/CongrTheorems.lean

@@ -231,6 +231,29 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) :
       result := result.push .eq
   return fixKindsForDependencies info result
 
+/--
+Variant of `getCongrSimpKinds` for rewriting just argument 0.
+If it is possible to rewrite, the 0th `CongrArgKind` is `CongrArgKind.eq`,
+and otherwise it is `CongrArgKind.fixed`. This is used for the `arg` conv tactic.
+-/
+def getCongrSimpKindsForArgZero (info : FunInfo) : MetaM (Array CongrArgKind) := do
+  let mut result := #[]
+  for h : i in [:info.paramInfo.size] do
+    if info.resultDeps.contains i then
+      result := result.push .fixed
+    else if i == 0 then
+      result := result.push .eq
+    else if info.paramInfo[i].isProp then
+      result := result.push .cast
+    else if info.paramInfo[i].isInstImplicit then
+      if shouldUseSubsingletonInst info result i then
+        result := result.push .subsingletonInst
+      else
+        result := result.push .fixed
+    else
+      result := result.push .fixed
+  return fixKindsForDependencies info result
+
 /--
   Create a congruence theorem that is useful for the simplifier and `congr` tactic.
 -/

src/Lean/Meta/DiscrTree.lean

@@ -426,7 +426,7 @@ partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (conf
   if todo.isEmpty then
     return keys
   else
-    let e    := todo.back
+    let e    := todo.back!
     let todo := todo.pop
     let (k, todo) ← pushArgs root todo e config noIndexAtArgs
     mkPathAux false todo (keys.push k) config noIndexAtArgs
@@ -460,7 +460,7 @@ where
   loop (i : Nat) : Array α :=
     if h : i < vs.size then
       if v == vs[i] then
-        vs.set ⟨i,h⟩ v
+        vs.set i v
       else
         loop (i+1)
     else
@@ -603,7 +603,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
     else if cs.isEmpty then
       return result
     else
-      let e     := todo.back
+      let e     := todo.back!
       let todo  := todo.pop
       let first := cs[0]! /- Recall that `Key.star` is the minimal key -/
       let (k, args) ← getMatchKeyArgs e (root := false) config
@@ -748,7 +748,7 @@ where
       else if cs.isEmpty then
         return result
       else
-        let e     := todo.back
+        let e     := todo.back!
         let todo  := todo.pop
         let (k, args) ← getUnifyKeyArgs e (root := false) config
         let visitStar (result : Array α) : MetaM (Array α) :=

src/Lean/Meta/ExprDefEq.lean

@@ -430,7 +430,7 @@ where
   hasLetDeclsInBetween : MetaM Bool := do
     let check (lctx : LocalContext) : Bool := Id.run do
       let start := lctx.getFVar! xs[0]! |>.index
-      let stop  := lctx.getFVar! xs.back |>.index
+      let stop  := lctx.getFVar! xs.back! |>.index
       for i in [start+1:stop] do
         match lctx.getAt? i with
         | some localDecl =>
@@ -488,7 +488,7 @@ where
   collectLetDeps : MetaM FVarIdHashSet := do
     let lctx ← getLCtx
     let start := lctx.getFVar! xs[0]! |>.index
-    let stop  := lctx.getFVar! xs.back |>.index
+    let stop  := lctx.getFVar! xs.back! |>.index
     let s := xs.foldl (init := {}) fun s x => s.insert x.fvarId!
     let (_, s) ← collectLetDepsAux stop |>.run start |>.run s
     return s
@@ -500,7 +500,7 @@ where
     let s ← collectLetDeps
     /- Convert `s` into the array `ys` -/
     let start := lctx.getFVar! xs[0]! |>.index
-    let stop  := lctx.getFVar! xs.back |>.index
+    let stop  := lctx.getFVar! xs.back! |>.index
     let mut ys := #[]
     for i in [start:stop+1] do
       match lctx.getAt? i with
@@ -1072,7 +1072,7 @@ private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v :
     if args.isEmpty then
       pure false
     else
-      Meta.isExprDefEqAux args.back a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
+      Meta.isExprDefEqAux args.back! a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
   | _            => pure false
 
 /--
@@ -1178,7 +1178,7 @@ private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patter
             if argsPrefix.isEmpty then
               defaultCase
             else
-              let some v ← mkLambdaFVarsWithLetDeps #[argsPrefix.back] v | defaultCase
+              let some v ← mkLambdaFVarsWithLetDeps #[argsPrefix.back!] v | defaultCase
               go argsPrefix.pop v
           match (← checkAssignment mvarId argsPrefix v) with
           | none      => cont
@@ -1205,7 +1205,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
       if h : i < args.size then
         let arg := args.get ⟨i, h⟩
         let arg ← simpAssignmentArg arg
-        let args := args.set ⟨i, h⟩ arg
+        let args := args.set i arg
         match arg with
         | Expr.fvar fvarId =>
           if args[0:i].any fun prevArg => prevArg == arg then
@@ -1975,7 +1975,7 @@ where
       assign `?m`.
       -/
       return false
-    let ctorVal := getStructureCtor (← getEnv) structName
+    let some ctorVal := getStructureLikeCtor? (← getEnv) structName | return false
     if ctorVal.numFields != 1 then
       return false -- It is not a structure with a single field.
     let sType ← whnf (← inferType s)
@@ -2013,7 +2013,7 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do
 /-- Return `true` if the type of the given expression is an inductive datatype with a single constructor with no fields. -/
 private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do
   let tType ← whnf (← inferType t)
-  matchConstStruct tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do
+  matchConstStructureLike tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do
     if ctorVal.numFields != 0 then
       return false
     else if (← useEtaStruct ctorVal.induct) then