chore: basic functionality tests for modify/alter

.github/ISSUE_TEMPLATE/bug_report.md

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

.github/workflows/ci.yml

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

RELEASES.md

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

flake.nix

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

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 15)
+set(LEAN_VERSION_MINOR 12)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init.lean

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

src/Init/Control/Basic.lean

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

src/Init/Conv.lean

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

src/Init/Data/Array.lean

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

src/Init/Data/Array/Basic.lean

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

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

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

src/Init/Data/Array/DecidableEq.lean

@@ -13,9 +13,9 @@ import Init.ByCases
 namespace Array
 
 theorem rel_of_isEqvAux
-    {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
+    (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
     (heqv : Array.isEqvAux a b hsz r i hi)
-    {j : Nat} (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
+    (j : Nat) (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
   induction i with
   | zero => contradiction
   | succ i ih =>
@@ -28,7 +28,7 @@ theorem rel_of_isEqvAux
       subst hj'
       exact heqv.left
 
-theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
+theorem isEqvAux_of_rel (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
     (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
   induction i with
   | zero => simp [Array.isEqvAux]
@@ -36,18 +36,18 @@ theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size
     simp only [isEqvAux, Bool.and_eq_true]
     exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
 
-theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} :
+theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
     Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
   simp only [isEqv]
   split <;> rename_i h
-  · exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩
+  · exact fun h' => ⟨h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
 theorem isEqv_iff_rel (a b : Array α) (r) :
     Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
-  ⟨rel_of_isEqv, fun ⟨h, w⟩ => by
+  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
     simp only [isEqv, ← h, ↓reduceDIte]
-    exact isEqvAux_of_rel h (by simp [h]) w⟩
+    exact isEqvAux_of_rel r a b h a.size (by simp [h]) w⟩
 
 theorem isEqv_eq_decide (a b : Array α) (r) :
     Array.isEqv a b r =
@@ -67,7 +67,7 @@ theorem isEqv_eq_decide (a b : Array α) (r) :
   simp [isEqv_eq_decide, List.isEqv_eq_decide]
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
-  have ⟨h, h'⟩ := rel_of_isEqv h
+  have ⟨h, h'⟩ := rel_of_isEqv (fun x y => x = y) a b h
   exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
 
 theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :

src/Init/Data/Array/Lemmas.lean

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

src/Init/Data/Array/MapIdx.lean

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

src/Init/Data/Array/Set.lean

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

src/Init/Data/BitVec/Basic.lean

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

src/Init/Data/BitVec/Bitblast.lean

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

src/Init/Data/BitVec/Lemmas.lean

@@ -1792,7 +1792,7 @@ theorem setWidth_succ (x : BitVec w) :
     · simp_all
     · omega
 
-@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]
+@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
 theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
   simp
 
@@ -2146,6 +2146,19 @@ 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
@@ -2886,14 +2899,6 @@ theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) :=
   simp only [intMin, getLsbD_twoPow, boolToPropSimps]
   omega
 
-theorem getMsbD_intMin {w i : Nat} :
-    (intMin w).getMsbD i = (decide (0 < w) && decide (i = 0)) := by
-  simp only [getMsbD, getLsbD_intMin]
-  match w, i with
-  | 0,   _    => simp
-  | w+1, 0    => simp
-  | w+1, i+1  => simp; omega
-
 /--
 The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
 -/
@@ -2916,21 +2921,6 @@ theorem toInt_intMin {w : Nat} :
     rw [Nat.mul_comm]
     simp [w_pos]
 
-theorem toInt_intMin_le (x : BitVec w) :
-    (intMin w).toInt ≤ x.toInt := by
-  cases w
-  case zero => simp [@of_length_zero x]
-  case succ w =>
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
-    have : 0 < 2 ^ w := Nat.two_pow_pos w
-    rw [Int.emod_eq_of_lt (by omega) (by omega)]
-    rw [BitVec.toInt_eq_toNat_bmod]
-    rw [show (2 ^ w : Nat) = ((2 ^ (w + 1) : Nat) : Int) / 2 by omega]
-    apply Int.le_bmod (by omega)
-
-theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by
-  simp only [BitVec.sle, toInt_intMin_le x, decide_True]
-
 @[simp]
 theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   by_cases h : 0 < w
@@ -2938,10 +2928,6 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   · simp only [Nat.not_lt, Nat.le_zero_eq] at h
     simp [bv_toNat, h]
 
-@[simp]
-theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by
-  simp [BitVec.abs, bv_toNat]
-
 theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
     (-x).toInt = -(x.toInt) := by
   simp only [ne_eq, toNat_eq, toNat_intMin] at rs
@@ -2958,10 +2944,6 @@ theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
   have := @Nat.two_pow_pred_mul_two w (by omega)
   split <;> split <;> omega
 
-theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by
-  simp only [msb_eq_decide, toNat_intMin, decide_eq_decide]
-  by_cases h : 0 < w <;> simp_all
-
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
@@ -3054,38 +3036,6 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
     BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
   omega
 
-/-! ### neg -/
-
-theorem msb_eq_toInt {x : BitVec w}:
-    x.msb = decide (x.toInt < 0) := by
-  by_cases h : x.msb <;>
-  · simp [h, toInt_eq_msb_cond]
-    omega
-
-theorem msb_eq_toNat {x : BitVec w}:
-    x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by
-  simp only [msb_eq_decide, ge_iff_le]
-
-/-! ### abs -/
-
-theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
-
-@[simp, bv_toNat]
-theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
-  simp only [BitVec.abs, neg_eq]
-  by_cases h : x.msb = true
-  · simp only [h, ↓reduceIte, toNat_neg]
-    have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
-    rw [Nat.mod_eq_of_lt (by omega)]
-  · simp [h]
-
-theorem getLsbD_abs {i : Nat} {x : BitVec w} :
-   getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by
-  by_cases h : x.msb <;> simp [BitVec.abs, h]
-
-theorem getMsbD_abs {i : Nat} {x : BitVec w} :
-    getMsbD (x.abs) i = if x.msb then getMsbD (-x) i else getMsbD x i := by
-  by_cases h : x.msb <;> simp [BitVec.abs, h]
 
 /-! ### Decidable quantifiers -/
 

src/Init/Data/ByteArray/Basic.lean

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

src/Init/Data/Fin/Fold.lean

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

src/Init/Data/FloatArray/Basic.lean

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

src/Init/Data/Hashable.lean

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

src/Init/Data/Int/DivModLemmas.lean

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

src/Init/Data/Int/Order.lean

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

src/Init/Data/List.lean

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

src/Init/Data/List/Basic.lean

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

src/Init/Data/List/Control.lean

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

src/Init/Data/List/Count.lean

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

src/Init/Data/List/Find.lean

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

src/Init/Data/List/Impl.lean

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

src/Init/Data/List/Lemmas.lean

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

src/Init/Data/List/MapIdx.lean

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

src/Init/Data/List/Monadic.lean

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

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

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

src/Init/Data/List/OfFn.lean

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

src/Init/Data/List/Pairwise.lean

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

src/Init/Data/List/Sublist.lean

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

src/Init/Data/Nat/Dvd.lean

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

src/Init/Data/Nat/Lemmas.lean

@@ -651,8 +651,8 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
   | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
 
 theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
-  rw (occs := .pos [1]) [← mod_add_div a n]
-  rw (occs := .pos [1]) [← mod_add_div b n]
+  rw (config := {occs := .pos [1]}) [← mod_add_div a n]
+  rw (config := {occs := .pos [1]}) [← mod_add_div b n]
   rw [Nat.add_mul, Nat.mul_add, Nat.mul_add,
     Nat.mul_assoc, Nat.mul_assoc, ← Nat.mul_add n, add_mul_mod_self_left,
     Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]

src/Init/Data/Option/Instances.lean

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

src/Init/Data/Range.lean

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

src/Init/Data/Sum/Lemmas.lean

@@ -17,11 +17,11 @@ open Function
 
 namespace Sum
 
-protected theorem «forall» {p : α ⊕ β → Prop} :
+@[simp] protected theorem «forall» {p : α ⊕ β → Prop} :
     (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
   ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
 
-protected theorem «exists» {p : α ⊕ β → Prop} :
+@[simp] protected theorem «exists» {p : α ⊕ β → Prop} :
     (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
   ⟨ fun
     | ⟨inl a, h⟩ => Or.inl ⟨a, h⟩
@@ -116,7 +116,7 @@ theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
 
 theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
     Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
-  simp [funext_iff, Sum.forall]
+  simp [funext_iff]
 
 /-! ### `Sum.map` -/
 

src/Init/Data/UInt/Basic.lean

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

src/Init/Meta.lean

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

src/Init/Prelude.lean

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

src/Init/PropLemmas.lean

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

src/Init/SimpLemmas.lean

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

src/Init/Syntax.lean

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

src/Init/Tactics.lean

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

src/Init/TacticsExtra.lean

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

src/Init/WFTactics.lean

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

src/Lean/Compiler/IR/ElimDeadVars.lean

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

src/Lean/Compiler/IR/EmitLLVM.lean

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

src/Lean/Compiler/IR/ExpandResetReuse.lean

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

src/Lean/Compiler/IR/PushProj.lean

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

src/Lean/Compiler/IR/SimpCase.lean

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

src/Lean/Compiler/LCNF/InferType.lean

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

src/Lean/Data/HashMap.lean

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

src/Lean/Data/HashSet.lean

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

src/Lean/Data/KVMap.lean

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

src/Lean/Data/Lsp/Utf16.lean

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

src/Lean/Data/PersistentArray.lean

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

src/Lean/Data/Position.lean

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

src/Lean/Data/RBMap.lean

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

src/Lean/Data/Xml/Parser.lean

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

src/Lean/Elab/App.lean

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

src/Lean/Elab/Arg.lean

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

src/Lean/Elab/BuiltinCommand.lean

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

src/Lean/Elab/BuiltinEvalCommand.lean

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

src/Lean/Elab/Do.lean

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

src/Lean/Elab/Inductive.lean

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

src/Lean/Elab/Level.lean

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

src/Lean/Elab/PreDefinition/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,12 +22,7 @@ namespace Lean.Elab.Command
 
 register_builtin_option structureDiamondWarning : Bool := {
   defValue := false
-  descr    := "if true, enable warnings when a structure has diamond inheritance"
-}
-
-register_builtin_option structure.strictResolutionOrder : Bool := {
-  defValue := false
-  descr := "if true, require a strict resolution order for structures"
+  descr    := "enable/disable warning messages for structure diamonds"
 }
 
 open Meta
@@ -811,16 +806,9 @@ 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
@@ -940,6 +928,8 @@ 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)
@@ -948,23 +938,6 @@ 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
@@ -1030,8 +1003,6 @@ 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. -/
@@ -1069,8 +1040,6 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
     pure view
   elabStructureViewPostprocessing view
 
-builtin_initialize
-  registerTraceClass `Elab.structure
-  registerTraceClass `Elab.structure.resolutionOrder
+builtin_initialize registerTraceClass `Elab.structure
 
 end Lean.Elab.Command

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

@@ -112,6 +112,7 @@ 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 }
@@ -177,33 +178,6 @@ 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.
 -/
@@ -222,7 +196,7 @@ def acNormalizePass : Pass := fun goal => do
 /--
 The normalization passes used by `bv_normalize` and thus `bv_decide`.
 -/
-def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
+def defaultPipeline : List Pass := [rewriteRulesPass]
 
 def passPipeline : MetaM (List Pass) := do
   let opts ← getOptions
@@ -248,8 +222,8 @@ def evalBVNormalize : Tactic := fun
   | `(tactic| bv_normalize) => do
     let g ← getMainGoal
     match ← bvNormalize g with
-    | some newGoal => replaceMainGoal [newGoal]
-    | none => replaceMainGoal []
+    | some newGoal => setGoals [newGoal]
+    | none => setGoals []
   | _ => 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, Kyle Miller
+Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Eval
@@ -10,174 +10,25 @@ import Lean.Elab.SyntheticMVars
 import Lean.Linter.MissingDocs
 
 namespace Lean.Elab.Tactic
-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 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 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,8 +11,6 @@ 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₁
@@ -74,14 +72,6 @@ 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
@@ -92,7 +82,9 @@ 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
-    resolveRhsFromProof "congr" rhs proof
+    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'}"
     mvarId.assign proof
     return mvarIdsNew.toList ++ mvarIdsNewInsts.toList
   else
@@ -101,7 +93,42 @@ 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))
 
-/-- Implementation of `arg 0`. -/
+-- 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` -/
 def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let (lhs, rhs) ← getLhsRhsCore mvarId
   let lhs := (← instantiateMVars lhs).cleanupAnnotations
@@ -109,137 +136,24 @@ 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 (init := mvarNew) Meta.mkCongrFun)
-    resolveRhs "arg 0" rhs (mkAppN g xs)
+    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'}"
     return mvarNew.mvarId!
 
-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
-      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
+@[builtin_tactic Lean.Parser.Tactic.Conv.arg] def evalArg : 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)
+  | `(conv| arg $[@%$tk?]? $i:num) =>
+    let i := i.getNat
+    if i == 0 then
+      replaceMainGoal [← congrFunN (← getMainGoal)]
+    else
+      let i := i - 1
+      let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false)
+      selectIdx "arg" mvarIds i
   | _ => 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
@@ -249,7 +163,9 @@ def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit :=
       | throwError "invalid 'fun' conv tactic, application expected{indentExpr lhs}"
     let (g, mvarNew) ← mkConvGoalFor f
     mvarId.assign (← Meta.mkCongrFun mvarNew a)
-    resolveRhs "fun" rhs (.app g a)
+    let rhs' := .app g a
+    unless ← isDefEqGuarded rhs rhs' do
+      throwError "invalid 'fun' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
     replaceMainGoal [mvarNew.mvarId!]
 
 def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId) := do
@@ -293,7 +209,9 @@ 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
-        resolveRhs "ext" rhs (← mkForallFVars #[a] qa)
+        let rhs' ← mkForallFVars #[a] qa
+        unless (← isDefEqGuarded rhs rhs') do
+          throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
         return (q, h, mvarNew)
       let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
       mvarId.assign proof
@@ -320,22 +238,4 @@ 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,28 +208,15 @@ 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 := do
-  let mut seenNames : Array Name := #[]
+private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
   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
-        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
-
+        throwErrorAt altStx "invalid alternative name '{altName}'"
 
 /-- 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
-  | `(tactic| omega $cfg:optConfig) => do
-    let cfg ← elabOmegaConfig cfg
+def evalOmega : Tactic := fun
+  | `(tactic| omega $[$cfg]?) => do
+    let cfg ← elabOmegaConfig (mkOptionalNode 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) : TacticM Meta.Simp.Config := do
+def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM 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" optConfig (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
+  "simp" (config)? (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]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
+      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
     let stx ← if bang.isSome then
-      `(tactic| simp!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
-      `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| simp%$tk $(config)? $(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]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
+  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
-      `(tactic| simp_all!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
+      `(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
     else
-      `(tactic| simp_all%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
+      `(tactic| simp_all%$tk $(config)? $(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]? $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
+  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
-      `(tactic| dsimp!%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
-      `(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
+      `(tactic| dsimp%$tk $(config)? $[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:optConfig $(disch)? $[only%$only]?
+  | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
         $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
-    let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
+    let stx ← `(tactic| simp $(cfg)? $(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:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
+          | `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
             if unfold.isSome then
-              `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
+              `(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
             else
-              `(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
+              `(tactic| simpa $(cfg)? $(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:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+  | `(tactic| apply_assumption $[$cfg]? $[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:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+  | `(tactic| apply_rules $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
     let (star, add, remove) := parseArgs t
     let use := parseUsing use
     let cfg ← elabApplyRulesConfig (mkOptionalNode cfg)
@@ -95,15 +95,16 @@ def evalApplyRules : Tactic := fun stx =>
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.solveByElim]
-def evalSolveByElim : Tactic
-  | `(tactic| solve_by_elim $[*%$s]? $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+def evalSolveByElim : Tactic := fun stx =>
+  match stx with
+  | `(tactic| solve_by_elim $[*%$s]? $[$cfg]? $[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 cfg
+    let cfg ← elabConfig (mkOptionalNode 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 (unsafeCast s)
+    exts.set ⟨ext.idx, h⟩ (unsafeCast s)
   else
     have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
     panic! invalidExtMsg
@@ -638,21 +638,20 @@ 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) := PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
+def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
 
 def mkMapDeclarationExtension (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
-  registerPersistentEnvExtension {
-    name            := name,
-    mkInitial       := pure {}
-    addImportedFn   := fun _ => pure {}
-    addEntryFn      := fun s (n, v) => s.insert n v
-    exportEntriesFn := fun s => s.toArray
+  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)
   }
 
 namespace MapDeclarationExtension
 
 instance : Inhabited (MapDeclarationExtension α) :=
-  inferInstanceAs (Inhabited (PersistentEnvExtension ..))
+  inferInstanceAs (Inhabited (SimplePersistentEnvExtension ..))
 
 def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
   have : Inhabited Environment := ⟨env⟩

src/Lean/Expr.lean

@@ -1836,27 +1836,6 @@ 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,14 +279,6 @@ 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,9 +37,8 @@ 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`
-and other `pp` options 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` 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
@@ -68,8 +67,7 @@ has type
 but is expected to have type
   @HashMap Nat Nat eqInst hasInst2
 ```
-
-Remark: this method implements simple heuristics; we should extend it as we find other counterintuitive
+Remark: this method implements a simple heuristic, we should extend it as we find other counterintuitive
 error messages.
 -/
 partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
@@ -125,15 +123,6 @@ 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
@@ -144,28 +133,6 @@ 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 elem) elem'
+      pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ 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,29 +231,6 @@ 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 v
+        vs.set ⟨i,h⟩ 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 arg
+        let args := args.set ⟨i, h⟩ 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 some ctorVal := getStructureLikeCtor? (← getEnv) structName | return false
+    let ctorVal := getStructureCtor (← getEnv) structName
     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)
-  matchConstStructureLike tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do
+  matchConstStruct tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do
     if ctorVal.numFields != 0 then
       return false
     else if (← useEtaStruct ctorVal.induct) then