chore: fix apply? error reporting when out of heartbeats

This PR fixes a bug where structural recursion did not work when indices
of the recursive argument appeared as function parameters in a different
order than in the argument's type's definition.

Fixes #6015.

.github/workflows/pr-body.yml

@@ -1,6 +1,7 @@
 name: Check PR body for changelog convention
 
 on:
+  merge_group:
   pull_request:
     types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
 
@@ -9,6 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR body
+        if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
           script: |

nix/bootstrap.nix

@@ -170,7 +170,7 @@ lib.warn "The Nix-based build is deprecated" rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi' -j$NIX_BUILD_CORES
+         ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
           mkdir $out

src/Init/Core.lean

@@ -1922,12 +1922,12 @@ represents an element of `Squash α` the same as `α` itself
 `Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
 while `Nonempty.rec` can only do the same when `β` is a proposition.
 -/
-def Squash (α : Type u) := Quot (fun (_ _ : α) => True)
+def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
 
 /-- The canonical quotient map into `Squash α`. -/
-def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
+def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x
 
-theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
+theorem Squash.ind {α : Sort u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
   Quot.ind h
 
 /-- If `β` is a subsingleton, then a function `α → β` lifts to `Squash α → β`. -/

src/Init/Data.lean

@@ -42,3 +42,4 @@ import Init.Data.PLift
 import Init.Data.Zero
 import Init.Data.NeZero
 import Init.Data.Function
+import Init.Data.RArray

src/Init/Data/Array.lean

@@ -18,3 +18,4 @@ import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Set
+import Init.Data.Array.Monadic

src/Init/Data/Array/Attach.lean

@@ -10,6 +10,16 @@ import Init.Data.List.Attach
 
 namespace Array
 
+/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+  `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+  but is defined only when all members of `l` satisfy `P`, using the proof
+  to apply `f`.
+
+We replace this at runtime with a more efficient version via
+-/
+def pmap {P : α → Prop} (f : ∀ a, P a → β) (l : Array α) (H : ∀ a ∈ l, P a) : Array β :=
+  (l.toList.pmap f (fun a m => H a (mem_def.mpr m))).toArray
+
 /--
 Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
 `Array {x // P x}` is the same as the input `Array α`.
@@ -35,6 +45,10 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
   simp [attach]
 
+@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
+    l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by
+  simp [pmap]
+
 @[simp] theorem toList_attachWith {l : Array α} {P : α → Prop} {H : ∀ x ∈ l, P x} :
    (l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H) := by
   simp [attachWith]
@@ -43,6 +57,29 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
   simp [attach]
 
+@[simp] theorem toList_pmap {l : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
+    (l.pmap f H).toList = l.toList.pmap f (fun a m => H a (mem_def.mpr m)) := by
+  simp [pmap]
+
+/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : Array α) (H : ∀ a ∈ l, P a) :
+    Array β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
+
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+  funext α β p f L h'
+  cases L
+  simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith]
+  apply List.pmap_congr_left
+  intro a m h₁ h₂
+  congr
+
+@[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
+    l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
+      l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  simp only [List.attachWith, List.attach, List.map_pmap]
+  apply List.pmap_congr_left
+  simp
+
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -83,7 +120,7 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
 
 @[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
   cases l
-  simp
+  simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]
 
 @[simp] theorem unattach_attachWith {p : α → Prop} {l : Array α}
     {H : ∀ a ∈ l, p a} :

src/Init/Data/Array/Basic.lean

@@ -166,13 +166,14 @@ count of 1 when called.
 -/
 @[extern "lean_array_fswap"]
 def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
-  let v₁ := a.get i
-  let v₂ := a.get j
+  let v₁ := a[i]
+  let v₂ := a[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)
 
 @[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[j]).set j a[i]
+    (Nat.lt_of_lt_of_eq j.isLt (size_set a i a[j] _).symm)).size = a.size
   rw [size_set, size_set]
 
 /--
@@ -246,10 +247,10 @@ def get? (a : Array α) (i : Nat) : Option α :=
   if h : i < a.size then some a[i] else none
 
 def back? (a : Array α) : Option α :=
-  a.get? (a.size - 1)
+  a[a.size - 1]?
 
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
-  let e := a.get i
+  let e := a[i]
   let a := a.set i v
   (e, a)
 
@@ -273,24 +274,22 @@ def take (a : Array α) (n : Nat) : Array α :=
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩
-    let v                := a.get idx
+    let v                := a[i]
     -- Replace a[i] by `box(0)`.  This ensures that `v` remains unshared if possible.
     -- Note: we assume that arrays have a uniform representation irrespective
     -- of the element type, and that it is valid to store `box(0)` in any array.
-    let a'               := a.set idx (unsafeCast ())
+    let a'               := a.set i (unsafeCast ())
     let v ← f v
-    pure <| a'.set idx v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
+    pure <| a'.set i v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
   else
     pure a
 
 @[implemented_by modifyMUnsafe]
 def modifyM [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx := ⟨i, h⟩
-    let v   := a.get idx
+    let v   := a[i]
     let v ← f v
-    pure <| a.set idx v
+    pure <| a.set i v
   else
     pure a
 
@@ -443,6 +442,8 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
+@[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
+
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
@@ -455,15 +456,15 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt)))
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
   as.mapFinIdxM fun i a => f i a
 
 @[inline]
-def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
+def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
   for a in as do
     match (← f a) with
     | some b => return b
@@ -471,14 +472,14 @@ def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as
   return none
 
 @[inline]
-def findM? {α : Type} {m : Type → Type} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) := do
+def findM? {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
     if (← p a) then
       return a
   return none
 
 @[inline]
-def findIdxM? [Monad m] (as : Array α) (p : α → m Bool) : m (Option Nat) := do
+def findIdxM? [Monad m] (p : α → m Bool) (as : Array α) : m (Option Nat) := do
   let mut i := 0
   for a in as do
     if (← p a) then
@@ -530,7 +531,7 @@ def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
   return !(← as.anyM (start := start) (stop := stop) fun v => return !(← p v))
 
 @[inline]
-def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) :=
+def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) :=
   let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
     | 0,   _ => pure none
     | i+1, h => do
@@ -544,7 +545,7 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
   find as.size (Nat.le_refl _)
 
 @[inline]
-def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) :=
+def findRevM? {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) :=
   as.findSomeRevM? fun a => return if (← p a) then some a else none
 
 @[inline]
@@ -573,7 +574,7 @@ def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size →
   Id.run <| as.mapFinIdxM f
 
 @[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
+def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
@@ -581,29 +582,29 @@ def zipWithIndex (arr : Array α) : Array (α × Nat) :=
   arr.mapIdx fun i a => (a, i)
 
 @[inline]
-def find? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
+def find? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
   Id.run <| as.findM? p
 
 @[inline]
-def findSome? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
+def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
   Id.run <| as.findSomeM? f
 
 @[inline]
-def findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : α → Option β) : β :=
-  match findSome? a f with
+def findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (a : Array α) : β :=
+  match a.findSome? f with
   | some b => b
   | none   => panic! "failed to find element"
 
 @[inline]
-def findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
+def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
   Id.run <| as.findSomeRevM? f
 
 @[inline]
-def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
+def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
   Id.run <| as.findRevM? p
 
 @[inline]
-def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
+def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (j : Nat) :=
     if h : j < as.size then
@@ -618,8 +619,7 @@ def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
-    if a.get idx == v then some idx
+    if a[i] == v then some ⟨i, h⟩
     else indexOfAux a v (i+1)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
@@ -744,7 +744,7 @@ where
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
-    if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
+    if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
       popWhile p as.pop
     else
       as
@@ -756,7 +756,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
-      let a := as.get ⟨i, h⟩
+      let a := as[i]
       if p a then
         go (i+1) (r.push a)
       else

src/Init/Data/Array/Bootstrap.lean

@@ -15,26 +15,26 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_eq_foldlM_toList.aux [Monad m]
+theorem foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · 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]
+    simp [foldlM_toList.aux f arr i (j+1) H]
     rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-theorem foldlM_eq_foldlM_toList [Monad m]
+@[simp] theorem foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.toList.foldlM f init := by
-  simp [foldlM, foldlM_eq_foldlM_toList.aux]
+    arr.toList.foldlM f init = arr.foldlM f init := by
+  simp [foldlM, foldlM_toList.aux]
 
-theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.toList.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
+@[simp] theorem foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.toList.foldl f init = arr.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_toList ..
 
 theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
@@ -51,23 +51,23 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-theorem foldrM_eq_foldrM_toList [Monad m]
+@[simp] theorem foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.toList.foldrM f init := by
+    arr.toList.foldrM f init = arr.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.toList.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
+@[simp] theorem foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.toList.foldr f init = arr.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
 @[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
 @[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
-  simp [toListAppend, foldr_eq_foldr_toList]
+  simp [toListAppend, ← foldr_toList]
 
 @[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
-  simp [toListImpl, foldr_eq_foldr_toList]
+  simp [toListImpl, ← foldr_toList]
 
 @[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
@@ -76,7 +76,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
 @[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [foldl_eq_foldl_toList]
+  rw [← foldl_toList]
   induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
@@ -98,20 +98,44 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
-@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
-abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
+@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
+theorem foldrM_eq_foldrM_toList [Monad m]
+    (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.toList.foldrM f init := by
+  simp
 
-@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
-abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
+@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
+theorem foldlM_eq_foldlM_toList [Monad m]
+    (f : β → α → m β) (init : β) (arr : Array α) :
+    arr.foldlM f init = arr.toList.foldlM f init:= by
+  simp
+
+@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
+theorem foldr_eq_foldr_toList
+    (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init := by
+  simp
+
+@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
+theorem foldl_eq_foldl_toList
+    (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init:= by
+  simp
+
+@[deprecated foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_toList
+
+@[deprecated foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_toList
 
 @[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
 abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
 
-@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
+@[deprecated foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_toList
 
-@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
-abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
+@[deprecated foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_toList
 
 @[deprecated push_toList (since := "2024-09-09")]
 abbrev push_data := @push_toList

src/Init/Data/Array/Find.lean

@@ -0,0 +1,275 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Find
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+
+/-!
+# Lemmas about `Array.findSome?`, `Array.find?`.
+-/
+
+namespace Array
+
+open Nat
+
+/-! ### findSome? -/
+
+@[simp] theorem findSomeRev?_push_of_isSome (l : Array α) (h : (f a).isSome) : (l.push a).findSomeRev? f = f a := by
+  cases l; simp_all
+
+@[simp] theorem findSomeRev?_push_of_isNone (l : Array α) (h : (f a).isNone) : (l.push a).findSomeRev? f = l.findSomeRev? f := by
+  cases l; simp_all
+
+theorem exists_of_findSome?_eq_some {f : α → Option β} {l : Array α} (w : l.findSome? f = some b) :
+    ∃ a, a ∈ l ∧ f a = b := by
+  cases l; simp_all [List.exists_of_findSome?_eq_some]
+
+@[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
+  cases l; simp
+
+@[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : Array α} :
+    (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
+  cases l; simp
+
+theorem findSome?_eq_some_iff {f : α → Option β} {l : Array α} {b : β} :
+    l.findSome? f = some b ↔ ∃ (l₁ : Array α) (a : α) (l₂ : Array α), l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none := by
+  cases l
+  simp only [List.findSome?_toArray, List.findSome?_eq_some_iff]
+  constructor
+  · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
+    exact ⟨l₁.toArray, a, l₂.toArray, by simp_all⟩
+  · rintro ⟨l₁, a, l₂, h₀, h₁, h₂⟩
+    exact ⟨l₁.toList, a, l₂.toList, by simpa using congrArg toList h₀, h₁, by simpa⟩
+
+@[simp] theorem findSome?_guard (l : Array α) : findSome? (Option.guard fun x => p x) l = find? p l := by
+  cases l; simp
+
+@[simp] theorem getElem?_zero_filterMap (f : α → Option β) (l : Array α) : (l.filterMap f)[0]? = l.findSome? f := by
+  cases l; simp [← List.head?_eq_getElem?]
+
+@[simp] theorem getElem_zero_filterMap (f : α → Option β) (l : Array α) (h) :
+    (l.filterMap f)[0] = (l.findSome? f).get (by cases l; simpa [List.length_filterMap_eq_countP] using h) := by
+  cases l; simp [← List.head_eq_getElem, ← getElem?_zero_filterMap]
+
+@[simp] theorem back?_filterMap (f : α → Option β) (l : Array α) : (l.filterMap f).back? = l.findSomeRev? f := by
+  cases l; simp
+
+@[simp] theorem back!_filterMap [Inhabited β] (f : α → Option β) (l : Array α) :
+    (l.filterMap f).back! = (l.findSomeRev? f).getD default := by
+  cases l; simp
+
+@[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (l : Array α) :
+    (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
+  cases l; simp
+
+theorem findSome?_map (f : β → γ) (l : Array β) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
+  cases l; simp [List.findSome?_map]
+
+theorem findSome?_append {l₁ l₂ : Array α} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f) := by
+  cases l₁; cases l₂; simp [List.findSome?_append]
+
+theorem getElem?_zero_flatten (L : Array (Array α)) :
+    (flatten L)[0]? = L.findSome? fun l => l[0]? := by
+  cases L using array_array_induction
+  simp [← List.head?_eq_getElem?, List.head?_flatten, List.findSome?_map, Function.comp_def]
+
+theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.size) :
+    (L.findSome? fun l => l[0]?).isSome := by
+  cases L using array_array_induction
+  simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
+    List.findSome?_isSome_iff, List.isSome_getElem?]
+  simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
+    Nat.sum_pos_iff_exists_pos, List.mem_map] at h
+  obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
+  exact ⟨xs, m, by simpa using h⟩
+
+theorem getElem_zero_flatten {L : Array (Array α)} (h) :
+    (flatten L)[0] = (L.findSome? fun l => l[0]?).get (getElem_zero_flatten.proof h) := by
+  have t := getElem?_zero_flatten L
+  simp [getElem?_eq_getElem, h] at t
+  simp [← t]
+
+theorem back?_flatten {L : Array (Array α)} :
+    (flatten L).back? = (L.findSomeRev? fun l => l.back?) := by
+  cases L using array_array_induction
+  simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]
+
+theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
+  simp [mkArray_eq_toArray_replicate, List.findSome?_replicate]
+
+@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
+  simp [findSome?_mkArray, Nat.ne_of_gt h]
+
+-- Argument is unused, but used to decide whether `simp` should unfold.
+@[simp] theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) :
+   findSome? f (mkArray n a) = if n = 0 then none else f a := by
+  simp [findSome?_mkArray]
+
+@[simp] theorem findSome?_mkArray_of_isNone (h : (f a).isNone) :
+    findSome? f (mkArray n a) = none := by
+  rw [Option.isNone_iff_eq_none] at h
+  simp [findSome?_mkArray, h]
+
+/-! ### find? -/
+
+@[simp] theorem find?_singleton (a : α) (p : α → Bool) :
+    #[a].find? p = if p a then some a else none := by
+  simp [singleton_eq_toArray_singleton]
+
+@[simp] theorem findRev?_push_of_pos (l : Array α) (h : p a) :
+    findRev? p (l.push a) = some a := by
+  cases l; simp [h]
+
+@[simp] theorem findRev?_cons_of_neg (l : Array α) (h : ¬p a) :
+    findRev? p (l.push a) = findRev? p l := by
+  cases l; simp [h]
+
+@[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
+  cases l; simp
+
+theorem find?_eq_some_iff_append {xs : Array α} :
+    xs.find? p = some b ↔ p b ∧ ∃ (as bs : Array α), xs = as.push b ++ bs ∧ ∀ a ∈ as, !p a := by
+  rcases xs with ⟨xs⟩
+  simp only [List.find?_toArray, List.find?_eq_some_iff_append, Bool.not_eq_eq_eq_not,
+    Bool.not_true, exists_and_right, and_congr_right_iff]
+  intro w
+  constructor
+  · rintro ⟨as, ⟨⟨x, rfl⟩, h⟩⟩
+    exact ⟨as.toArray, ⟨x.toArray, by simp⟩ , by simpa using h⟩
+  · rintro ⟨as, ⟨⟨x, h'⟩, h⟩⟩
+    exact ⟨as.toList, ⟨x.toList, by simpa using congrArg Array.toList h'⟩,
+      by simpa using h⟩
+
+@[simp]
+theorem find?_push_eq_some {xs : Array α} :
+    (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
+  cases xs; simp
+
+@[simp] theorem find?_isSome {xs : Array α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
+  cases xs; simp
+
+theorem find?_some {xs : Array α} (h : find? p xs = some a) : p a := by
+  cases xs
+  simp at h
+  exact List.find?_some h
+
+theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a ∈ xs := by
+  cases xs
+  simp at h
+  simpa using List.mem_of_find?_eq_some h
+
+theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
+  cases xs
+  simp [List.get_find?_mem]
+
+@[simp] theorem find?_filter {xs : Array α} (p q : α → Bool) :
+    (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
+  cases xs; simp
+
+@[simp] theorem getElem?_zero_filter (p : α → Bool) (l : Array α) :
+    (l.filter p)[0]? = l.find? p := by
+  cases l; simp [← List.head?_eq_getElem?]
+
+@[simp] theorem getElem_zero_filter (p : α → Bool) (l : Array α) (h) :
+    (l.filter p)[0] =
+      (l.find? p).get (by cases l; simpa [← List.countP_eq_length_filter] using h) := by
+  cases l
+  simp [List.getElem_zero_eq_head]
+
+@[simp] theorem back?_filter (p : α → Bool) (l : Array α) : (l.filter p).back? = l.findRev? p := by
+  cases l; simp
+
+@[simp] theorem back!_filter [Inhabited α] (p : α → Bool) (l : Array α) :
+    (l.filter p).back! = (l.findRev? p).get! := by
+  cases l; simp [Option.get!_eq_getD]
+
+@[simp] theorem find?_filterMap (xs : Array α) (f : α → Option β) (p : β → Bool) :
+    (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
+  cases xs; simp
+
+@[simp] theorem find?_map (f : β → α) (xs : Array β) :
+    find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
+  cases xs; simp
+
+@[simp] theorem find?_append {l₁ l₂ : Array α} :
+    (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
+  cases l₁
+  cases l₂
+  simp
+
+@[simp] theorem find?_flatten (xs : Array (Array α)) (p : α → Bool) :
+    xs.flatten.find? p = xs.findSome? (·.find? p) := by
+  cases xs using array_array_induction
+  simp [List.findSome?_map, Function.comp_def]
+
+theorem find?_flatten_eq_none {xs : Array (Array α)} {p : α → Bool} :
+    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
+  simp
+
+/--
+If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
+some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
+Moreover, no earlier array in `xs` has an element satisfying `p`.
+-/
+theorem find?_flatten_eq_some {xs : Array (Array α)} {p : α → Bool} {a : α} :
+    xs.flatten.find? p = some a ↔
+      p a ∧ ∃ (as : Array (Array α)) (ys zs : Array α) (bs : Array (Array α)),
+        xs = as.push (ys.push a ++ zs) ++ bs ∧
+        (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
+  cases xs using array_array_induction
+  simp only [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some]
+  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
+  intro w
+  constructor
+  · rintro ⟨as, ys, ⟨⟨zs, bs, rfl⟩, h₁, h₂⟩⟩
+    exact ⟨as.toArray.map List.toArray, ys.toArray,
+      ⟨zs.toArray, bs.toArray.map List.toArray, by simp⟩, by simpa using h₁, by simpa using h₂⟩
+  · rintro ⟨as, ys, ⟨⟨zs, bs, h⟩, h₁, h₂⟩⟩
+    replace h := congrArg (·.map Array.toList) (congrArg Array.toList h)
+    simp [Function.comp_def] at h
+    exact ⟨as.toList.map Array.toList, ys.toList,
+      ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
+        by simpa using h₁, by simpa using h₂⟩
+
+@[simp] theorem find?_flatMap (xs : Array α) (f : α → Array β) (p : β → Bool) :
+    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
+  cases xs
+  simp [List.find?_flatMap, Array.flatMap_toArray]
+
+theorem find?_flatMap_eq_none {xs : Array α} {f : α → Array β} {p : β → Bool} :
+    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
+  simp
+
+theorem find?_mkArray :
+    find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
+  simp [mkArray_eq_toArray_replicate, List.find?_replicate]
+
+@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
+    find? p (mkArray n a) = if p a then some a else none := by
+  simp [find?_mkArray, Nat.ne_of_gt h]
+
+@[simp] theorem find?_mkArray_of_pos (h : p a) :
+    find? p (mkArray n a) = if n = 0 then none else some a := by
+  simp [find?_mkArray, h]
+
+@[simp] theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none := by
+  simp [find?_mkArray, h]
+
+-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
+theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
+    (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
+  simp [mkArray_eq_toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
+
+@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α → Bool} :
+    (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+  simp [mkArray_eq_toArray_replicate]
+
+@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
+    ((mkArray n a).find? p).get h = a := by
+  simp [mkArray_eq_toArray_replicate]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -76,6 +76,8 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
+theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
+
 end Array
 
 namespace List
@@ -111,6 +113,9 @@ We prefer to pull `List.toArray` outwards.
 @[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 (l : List α) : l.toArray.back? = l.getLast? := by
+  simp [back?, List.getLast?_eq_getElem?]
+
 @[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
     (h : i ≤ l.length) (b : β) :
     Array.forIn'.loop l.toArray f i h b =
@@ -146,15 +151,15 @@ theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List
 
 theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
-  rw [foldlM_eq_foldlM_toList]
+  rw [foldlM_toList]
 
 theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
-  rw [foldr_eq_foldr_toList]
+  rw [foldr_toList]
 
 theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
-  rw [foldl_eq_foldl_toList]
+  rw [foldl_toList]
 
 /-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
@@ -169,21 +174,21 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     (h : stop = l.toArray.size) :
     l.toArray.foldlM f init 0 stop = l.foldlM f init := by
   subst h
-  rw [foldlM_eq_foldlM_toList]
+  rw [foldlM_toList]
 
 /-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
     (h : start = l.toArray.size) :
     l.toArray.foldr f init start 0 = l.foldr f init := by
   subst h
-  rw [foldr_eq_foldr_toList]
+  rw [foldr_toList]
 
 /-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
     (h : stop = l.toArray.size) :
     l.toArray.foldl f init 0 stop = l.foldl f init := by
   subst h
-  rw [foldl_eq_foldl_toList]
+  rw [foldl_toList]
 
 @[simp] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
@@ -197,6 +202,9 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
   induction l generalizing as <;> simp [*]
 
+@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
+  rw [foldr_eq_foldl_reverse, foldl_push]
+
 @[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
@@ -210,7 +218,7 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 
 theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
     (i : Nat) (h) :
-    findSomeRevM?.find l.toArray f i h = (l.take i).reverse.findSomeM? f := by
+    findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by
   induction i generalizing l with
   | zero => simp [Array.findSomeRevM?.find.eq_def]
   | succ i ih =>
@@ -357,7 +365,8 @@ namespace Array
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
+  simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
+    List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
 
 /--
 Variant of `foldrM_push` with `h : start = arr.size + 1`
@@ -383,11 +392,11 @@ rather than `(arr.push a).size` as the argument.
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
 
 @[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
+  rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
-  rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
+  rw [mapM, aux, ← foldlM_toList]; rfl
 where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
@@ -402,7 +411,7 @@ where
 
 @[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
   rw [map, mapM_eq_foldlM]
-  apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
+  apply congrArg toList (foldl_toList (fun bs a => push bs (f a)) #[] arr).symm |>.trans
   have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
     induction l generalizing arr <;> simp [*]
   simp [H]
@@ -450,7 +459,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
-@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
+@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
 
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
@@ -581,6 +590,8 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
 
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
+theorem mkArray_eq_toArray_replicate (n : Nat) (v : α) : mkArray n v = (List.replicate n v).toArray := rfl
+
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
     (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
 
@@ -590,7 +601,7 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
 
 /-- # mem -/
 
-theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
+@[simp] theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
 
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
@@ -609,19 +620,19 @@ theorem getElem?_of_mem {a : α} {as : Array α} :
 
 @[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
     (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
-  split <;> simp_all [mem_def]
+  split <;> simp_all
 
 @[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Array α} :
     (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h := by
-  split <;> simp_all [mem_def]
+  split <;> simp_all
 
 @[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
     (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l := by
-  split <;> simp_all [mem_def]
+  split <;> simp_all
 
 @[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
     (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
-  split <;> simp_all [mem_def]
+  split <;> simp_all
 
 /-- # get lemmas -/
 
@@ -730,11 +741,11 @@ theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
 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[j]).set j a[i] := by
   simp [swap, fin_cast_val]
 
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
-    (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
+    (a.swap i j).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
 
 theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
     if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
@@ -1016,7 +1027,7 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
-  rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
+  rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
@@ -1141,7 +1152,7 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
     (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
-  rw [foldl_eq_foldl_toList]
+  rw [← foldl_toList]
   generalize l.toList = l
   suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
       a.toList ++ List.filter p l by
@@ -1172,7 +1183,7 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
 @[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
     (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
-  rw [foldlM_eq_foldlM_toList]
+  rw [← foldlM_toList]
   generalize l.toList = l
   have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
     a.toList ++ List.filterMap f l := ?_
@@ -1207,6 +1218,14 @@ theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] :=
 @[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
   simp only [size, toList_append, List.length_append]
 
+@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by
+  cases as
+  simp
+
+@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by
+  cases as
+  simp
+
 theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
     (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
   cases as; cases bs
@@ -1251,7 +1270,7 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
 @[simp] theorem toList_flatten {l : Array (Array α)} :
     l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
-  simp only [foldl_eq_foldl_toList]
+  simp only [← foldl_toList]
   generalize l.toList = l
   have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
   exact this #[]
@@ -1470,7 +1489,7 @@ termination_by stop - start
 
 -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
 theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
-    any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
+    as.any p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
   dsimp [any, anyM, Id.run]
   split
   · rw [anyM_loop_iff_exists]; rfl
@@ -1482,7 +1501,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
       exact ⟨i, by omega, by omega, h⟩
 
 theorem any_eq_true {p : α → Bool} {as : Array α} :
-    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
+    as.any p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
 
 theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
@@ -1502,20 +1521,20 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
   rw [List.allM_eq_not_anyM_not]
 
 theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
-    all as p start stop = !(any as (!p ·) start stop) := by
+    as.all p start stop = !(as.any (!p ·) start stop) := by
   dsimp [all, allM]
   rfl
 
 theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
-    all as p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
+    as.all p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
   rw [all_eq_not_any_not]
-  suffices ¬(any as (!p ·) start stop = true) ↔
+  suffices ¬(as.any (!p ·) start stop = true) ↔
       ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] by
     simp_all
   rw [any_iff_exists]
   simp
 
-theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
+theorem all_eq_true {p : α → Bool} {as : Array α} : as.all p ↔ ∀ i : Fin as.size, p as[i] := by
   simp [all_iff_forall, Fin.isLt]
 
 theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
@@ -1865,6 +1884,50 @@ namespace Array
   induction as
   simp
 
+/-! ### map -/
+
+@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Array α} :
+    (as.map f).map g = as.map (g ∘ f) := by
+  cases as; simp
+
+@[simp] theorem map_id_fun : map (id : α → α) = id := by
+  funext l
+  induction l <;> simp_all
+
+/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
+@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
+
+-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
+theorem map_id (as : Array α) : map (id : α → α) as = as := by
+  cases as <;> simp_all
+
+/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
+-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
+theorem map_id' (as : Array α) : map (fun (a : α) => a) as = as := map_id as
+
+/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
+theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (as : Array α) : map f as = as := by
+  simp [show f = id from funext h]
+
+theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : List (List α)), P (xss.map List.toArray).toArray)
+    (ass : Array (Array α)) : P ass := by
+  specialize h (ass.toList.map toList)
+  simpa [← toList_map, Function.comp_def, map_id] using h
+
+/-! ### flatten -/
+
+@[simp] theorem flatten_empty : flatten (#[] : Array (Array α)) = #[] := rfl
+
+@[simp] theorem flatten_toArray_map_toArray (xss : List (List α)) :
+    (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
+  simp [flatten]
+  suffices ∀ as, List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray by
+    simpa using this #[]
+  intro as
+  induction xss generalizing as with
+  | nil => simp
+  | cons xs xss ih => simp [ih]
+
 /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
 
 @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse
@@ -1929,6 +1992,27 @@ namespace Array
   cases as
   simp
 
+@[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
+
+@[simp] theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
+    (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
+  simp [flatMap]
+  suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
+      f a ++ List.foldl (fun bs a => bs ++ f a) cs as by
+    erw [empty_append] -- Why doesn't this work via `simp`?
+    simpa using this #[]
+  intro cs
+  induction as generalizing cs <;> simp_all
+
+@[simp] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) :
+    as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    apply ext'
+    simp [ih]
+
+
 end Array
 
 /-! ### Deprecations -/
@@ -2037,8 +2121,8 @@ abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
 
 @[deprecated getElem_modify (since := "2024-08-08")]
 theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
-    (arr.modify x f).get ⟨i, h⟩ =
-    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
+    (arr.modify x f).get i h =
+    if x = i then f (arr.get i (by simpa using h)) else arr.get i (by simpa using h) := by
   simp [getElem_modify h]
 
 @[deprecated toList_filter (since := "2024-09-09")]

src/Init/Data/Array/MapIdx.lean

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

src/Init/Data/Array/Mem.lean

@@ -14,12 +14,12 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
 
-theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
   cases as with | _ as =>
-  exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
+  simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)
 
 @[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
-  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _ h
 
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions

src/Init/Data/Array/Monadic.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.List.Monadic
+
+/-!
+# Lemmas about `Array.forIn'` and `Array.forIn`.
+-/
+
+namespace Array
+
+open Nat
+
+/-! ## Monadic operations -/
+
+/-! ### mapM -/
+
+theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Array α) :
+    mapM f l = l.foldlM (fun acc a => return (acc.push (← f a))) #[] := by
+  rcases l with ⟨l⟩
+  simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']
+  rw [List.mapM_eq_reverse_foldlM_cons]
+  simp only [bind_pure_comp, Functor.map_map]
+  suffices ∀ (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
+      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l by
+    exact this []
+  intro k
+  induction l generalizing k with
+  | nil => simp
+  | cons a as ih =>
+    simp [ih, List.foldlM_cons]
+
+/-! ### foldlM and foldrM -/
+
+theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) :
+    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
+  cases l
+  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_map]
+
+theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Array β₁)
+    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
+  cases l
+  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldrM_map]
+
+theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Array α) (init : γ) :
+    (l.filterMap f).foldlM g init =
+      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
+  cases l
+  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_filterMap]
+  rfl
+
+theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Array α) (init : γ) :
+    (l.filterMap f).foldrM g init =
+      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
+  cases l
+  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldrM_filterMap]
+  rfl
+
+theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Array α) (init : β) :
+    (l.filter p).foldlM g init =
+      l.foldlM (fun x y => if p y then g x y else pure x) init := by
+  cases l
+  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_filter]
+
+theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Array α) (init : β) :
+    (l.filter p).foldrM g init =
+      l.foldrM (fun x y => if p x then g x y else pure y) init := by
+  cases l
+  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldrM_filter]
+
+/-! ### forIn' -/
+
+/--
+We can express a for loop over an array 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 : Array α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
+    forIn' l init f = ForInStep.value <$>
+      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
+        | .yield b => f a m b
+        | .done b => pure (.done b)) (ForInStep.yield init) := by
+  cases l
+  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
+  simp only [List.forIn'_toArray, List.forIn'_eq_foldlM, List.attachWith_mem_toArray, size_toArray,
+    List.length_map, List.length_attach, List.foldlM_toArray', List.foldlM_map]
+  congr
+
+/-- We can express a for loop over an array which always yields as a fold. -/
+@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Array α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
+    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
+      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
+  cases l
+  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_map]
+
+theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' l init (fun a m b => pure (.yield (f a m b))) =
+      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
+  cases l
+  simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
+
+@[simp] theorem forIn'_yield_eq_foldl
+    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
+  cases l
+  simp [List.foldl_map]
+
+/--
+We can express a for loop over an array 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 : Array α) :
+    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
+  cases l
+  simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']
+  congr
+
+/-- We can express a for loop over an array which always yields as a fold. -/
+@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Array α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
+    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
+      l.foldlM (fun b a => g a b <$> f a b) init := by
+  cases l
+  simp [List.foldlM_map]
+
+theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : Array α) (f : α → β → β) (init : β) :
+    forIn l init (fun a b => pure (.yield (f a b))) =
+      pure (f := m) (l.foldl (fun b a => f a b) init) := by
+  cases l
+  simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
+
+@[simp] theorem forIn_yield_eq_foldl
+    (l : Array α) (f : α → β → β) (init : β) :
+    forIn (m := Id) l init (fun a b => .yield (f a b)) =
+      l.foldl (fun b a => f a b) init := by
+  cases l
+  simp [List.foldl_map]
+
+end Array

src/Init/Data/Array/Subarray.lean

@@ -15,15 +15,6 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array (since := "2024-04-13")]
-abbrev Subarray.as (s : Subarray α) : Array α := s.array
-
-@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
-theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
-
-@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
-
 namespace Subarray
 
 def size (s : Subarray α) : Nat :=
@@ -48,7 +39,7 @@ instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
-  if h : i < s.size then s.get ⟨i, h⟩ else v₀
+  if h : i < s.size then s[i] else v₀
 
 abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
   getD s i default

src/Init/Data/BitVec/Basic.lean

@@ -29,9 +29,6 @@ section Nat
 
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
-@[deprecated isLt (since := "2024-03-12")]
-theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
-
 /-- Theorem for normalizing the bit vector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
 @[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

src/Init/Data/BitVec/Bitblast.lean

@@ -76,7 +76,7 @@ to prove the correctness of the circuit that is built by `bv_decide`.
 def blastMul (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w
 theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment) :
    ...
-   ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
+   ⟦(blastMul aig input).aig, (blastMul aig input).vec[idx], assign.toAIGAssignment⟧
      =
    (lhs * rhs).getLsbD idx
 ```
@@ -403,7 +403,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} :
       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]
+        bne_right_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)⟩
@@ -419,7 +419,7 @@ theorem getMsbD_neg {i : Nat} {x : BitVec w} :
     simp [hi]; omega
   case pos =>
     have h₁ : w - 1 - i < w := by omega
-    simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide]
+    simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_right_inj, decide_eq_decide]
     constructor
     · rintro ⟨j, hj, h⟩
       refine ⟨w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h⟩

src/Init/Data/Bool.lean

@@ -238,8 +238,8 @@ theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by simp
 @[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
 instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
-@[simp] theorem bne_left_inj  : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z := by decide
-@[simp] theorem bne_right_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y := by decide
+@[simp] theorem bne_right_inj  : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z := by decide
+@[simp] theorem bne_left_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y := by decide
 
 theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide
 
@@ -295,9 +295,9 @@ theorem xor_right_comm : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = ((x ^^ z) ^^ y) :
 
 theorem xor_assoc : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = (x ^^ (y ^^ z)) := bne_assoc
 
-theorem xor_left_inj : ∀ {x y z : Bool}, (x ^^ y) = (x ^^ z) ↔ y = z := bne_left_inj
+theorem xor_right_inj : ∀ {x y z : Bool}, (x ^^ y) = (x ^^ z) ↔ y = z := bne_right_inj
 
-theorem xor_right_inj : ∀ {x y z : Bool}, (x ^^ z) = (y ^^ z) ↔ x = y := bne_right_inj
+theorem xor_left_inj : ∀ {x y z : Bool}, (x ^^ z) = (y ^^ z) ↔ x = y := bne_left_inj
 
 /-! ### le/lt -/
 

src/Init/Data/ByteArray/Basic.lean

@@ -42,7 +42,7 @@ def usize (a : @& ByteArray) : USize :=
   a.size.toUSize
 
 @[extern "lean_byte_array_uget"]
-def uget : (a : @& ByteArray) → (i : USize) → i.toNat < a.size → UInt8
+def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, h => bs[i]
 
 @[extern "lean_byte_array_get"]
@@ -50,11 +50,11 @@ def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs.get! i
 
 @[extern "lean_byte_array_fget"]
-def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
-  | ⟨bs⟩, i => bs.get i
+def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
+  | ⟨bs⟩, i, _ => bs[i]
 
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i
 
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
@@ -64,11 +64,11 @@ def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
 @[extern "lean_byte_array_fset"]
-def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
-  | ⟨bs⟩, i, b => ⟨bs.set i.1 b i.2⟩
+def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
+  | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
 
 @[extern "lean_byte_array_uset"]
-def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray
+def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
 @[extern "lean_byte_array_hash"]
@@ -144,7 +144,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
       have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
       have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
       have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-      match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
+      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
@@ -178,7 +178,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
         match i with
         | 0    => pure b
         | i'+1 =>
-          loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
+          loop i' (j+1) (← f b as[j])
       else
         pure b
     loop (stop - start) start init

src/Init/Data/Fin/Lemmas.lean

@@ -642,7 +642,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
   ext
   simp
 
-@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ ↑i) : (subNat 1 i h).succ = i := by
+@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by
   ext
   simp
   omega

src/Init/Data/Float.lean

@@ -47,6 +47,25 @@ def Float.lt : Float → Float → Prop := fun a b =>
 def Float.le : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
+/--
+Raw transmutation from `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+-/
+@[extern "lean_float_of_bits"] opaque Float.ofBits : UInt64 → Float
+
+/--
+Raw transmutation to `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+
+Note that this function is distinct from `Float.toUInt64`, which attempts
+to preserve the numeric value, and not the bitwise value.
+-/
+@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64
+
 instance : Add Float := ⟨Float.add⟩
 instance : Sub Float := ⟨Float.sub⟩
 instance : Mul Float := ⟨Float.mul⟩

src/Init/Data/FloatArray/Basic.lean

@@ -46,8 +46,8 @@ def uget : (a : @& FloatArray) → (i : USize) → i.toNat < a.size → Float
   | ⟨ds⟩, i, h => ds[i]
 
 @[extern "lean_float_array_fget"]
-def get : (ds : @& FloatArray) → (@& Fin ds.size) → Float
-  | ⟨ds⟩, i => ds.get i
+def get : (ds : @& FloatArray) → (i : @& Nat) → (h : i < ds.size := by get_elem_tactic) → Float
+  | ⟨ds⟩, i, h => ds.get i h
 
 @[extern "lean_float_array_get"]
 def get! : (@& FloatArray) → (@& Nat) → Float
@@ -55,23 +55,23 @@ def get! : (@& FloatArray) → (@& Nat) → Float
 
 def get? (ds : FloatArray) (i : Nat) : Option Float :=
   if h : i < ds.size then
-    ds.get ⟨i, h⟩
+    some (ds.get i h)
   else
     none
 
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i h
 
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
 @[extern "lean_float_array_uset"]
-def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
+def uset : (a : FloatArray) → (i : USize) → Float → (h : i.toNat < a.size := by get_elem_tactic) → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩
 
 @[extern "lean_float_array_fset"]
-def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
-  | ⟨ds⟩, i, d => ⟨ds.set i.1 d i.2⟩
+def set : (ds : FloatArray) → (i : @& Nat) → Float → (h : i < ds.size := by get_elem_tactic) → FloatArray
+  | ⟨ds⟩, i, d, h => ⟨ds.set i d h⟩
 
 @[extern "lean_float_array_set"]
 def set! : FloatArray → (@& Nat) → Float → FloatArray
@@ -83,7 +83,7 @@ def isEmpty (s : FloatArray) : Bool :=
 partial def toList (ds : FloatArray) : List Float :=
   let rec loop (i r) :=
     if h : i < ds.size then
-      loop (i+1) (ds.get ⟨i, h⟩ :: r)
+      loop (i+1) (ds[i] :: r)
     else
       r.reverse
   loop 0 []
@@ -115,7 +115,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA
       have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
       have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
       have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-      match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
+      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
@@ -149,7 +149,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float →
         match i with
         | 0    => pure b
         | i'+1 =>
-          loop i' (j+1) (← f b (as.get ⟨j, Nat.lt_of_lt_of_le hlt h⟩))
+          loop i' (j+1) (← f b (as[j]'(Nat.lt_of_lt_of_le hlt h)))
       else
         pure b
     loop (stop - start) start init

src/Init/Data/Int/Lemmas.lean

@@ -329,22 +329,22 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
 /- ## add/sub injectivity -/
 
 @[simp]
-protected theorem add_right_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by
+protected theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by
   apply Iff.intro
   · intro p
     rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p]
   · exact congrArg (· + k)
 
 @[simp]
-protected theorem add_left_inj {i j : Int} (k : Int) : (k + i = k + j) ↔ i = j := by
+protected theorem add_right_inj {i j : Int} (k : Int) : (k + i = k + j) ↔ i = j := by
   simp [Int.add_comm k]
 
 @[simp]
-protected theorem sub_left_inj {i j : Int} (k : Int) : (k - i = k - j) ↔ i = j := by
+protected theorem sub_right_inj {i j : Int} (k : Int) : (k - i = k - j) ↔ i = j := by
   simp [Int.sub_eq_add_neg, Int.neg_inj]
 
 @[simp]
-protected theorem sub_right_inj {i j : Int} (k : Int) : (i - k = j - k) ↔ i = j := by
+protected theorem sub_left_inj {i j : Int} (k : Int) : (i - k = j - k) ↔ i = j := by
   simp [Int.sub_eq_add_neg]
 
 /- ## Ring properties -/

src/Init/Data/List/Basic.lean

@@ -551,7 +551,7 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
 /-! ### flatten -/
 
 /--
-`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
+`O(|flatten L|)`. `flatten L` concatenates all the lists in `L` into one list.
 * `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
 -/
 def flatten : List (List α) → List α

src/Init/Data/List/Find.lean

@@ -10,7 +10,8 @@ import Init.Data.List.Sublist
 import Init.Data.List.Range
 
 /-!
-# Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, and `List.indexOf`.
+Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `List.indexOf`,
+and `List.lookup`.
 -/
 
 namespace List
@@ -95,22 +96,22 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
     · simp only [Option.guard_eq_none] at h
       simp [ih, h]
 
-@[simp] theorem filterMap_head? (f : α → Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f := by
+@[simp] theorem head?_filterMap (f : α → Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [filterMap_cons, findSome?_cons]
     split <;> simp [*]
 
-@[simp] theorem filterMap_head (f : α → Option β) (l : List α) (h) :
-    (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none])  := by
+@[simp] theorem head_filterMap (f : α → Option β) (l : List α) (h) :
+    (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem filterMap_getLast? (f : α → Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f := by
+@[simp] theorem getLast?_filterMap (f : α → Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f := by
   rw [getLast?_eq_head?_reverse]
   simp [← filterMap_reverse]
 
-@[simp] theorem filterMap_getLast (f : α → Option β) (l : List α) (h) :
+@[simp] theorem getLast_filterMap (f : α → Option β) (l : List α) (h) :
     (l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast_eq_some]
 
@@ -291,18 +292,18 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
     · simp only [find?_cons]
       split <;> simp_all
 
-@[simp] theorem filter_head? (p : α → Bool) (l : List α) : (l.filter p).head? = l.find? p := by
-  rw [← filterMap_eq_filter, filterMap_head?, findSome?_guard]
+@[simp] theorem head?_filter (p : α → Bool) (l : List α) : (l.filter p).head? = l.find? p := by
+  rw [← filterMap_eq_filter, head?_filterMap, findSome?_guard]
 
-@[simp] theorem filter_head (p : α → Bool) (l : List α) (h) :
+@[simp] theorem head_filter (p : α → Bool) (l : List α) (h) :
     (l.filter p).head h = (l.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem filter_getLast? (p : α → Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p := by
+@[simp] theorem getLast?_filter (p : α → Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p := by
   rw [getLast?_eq_head?_reverse]
   simp [← filter_reverse]
 
-@[simp] theorem filter_getLast (p : α → Bool) (l : List α) (h) :
+@[simp] theorem getLast_filter (p : α → Bool) (l : List α) (h) :
     (l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast_eq_some]
 

src/Init/Data/List/Impl.lean

@@ -91,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
 @[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
 
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
+  funext α β f init l; simp [foldrTR, ← Array.foldr_toList, -Array.size_toArray]
 
 /-! ### flatMap  -/
 
@@ -331,7 +331,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_toList]
+  rw [← Array.foldr_toList]
   simp [go]
 
 /-! ## Other list operations -/

src/Init/Data/List/Lemmas.lean

@@ -372,6 +372,17 @@ theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? =
 @[deprecated getElem?_concat_length (since := "2024-06-12")]
 theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
 
+@[simp] theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
+  by_cases h : n < l.length
+  · simp_all
+  · simp [h]
+    simp_all
+
+@[simp] theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
+  by_cases h : n < l.length
+  · simp_all
+  · simp [h]
+
 /-! ### mem -/
 
 @[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := nofun
@@ -1025,6 +1036,10 @@ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
   | _ :: _ :: _, _ => by
     simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]
 
+theorem getElem_length_sub_one_eq_getLast (l : List α) (h) :
+    l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
+  rw [← getLast_eq_getElem]
+
 @[deprecated getLast_eq_getElem (since := "2024-07-15")]
 theorem getLast_eq_get (l : List α) (h : l ≠ []) :
     getLast l h = l.get ⟨l.length - 1, by
@@ -1045,7 +1060,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
 
 @[simp] theorem getLast_singleton (a h) : @getLast α [a] h = a := rfl
 
-theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
+theorem getLast!_cons_eq_getLastD [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
   simp [getLast!, getLast_eq_getLastD]
 
 @[simp] theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
@@ -1109,7 +1124,12 @@ theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
 
 /-! ### getLast! -/
 
-@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
+theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
+
+@[simp] theorem getLast!_eq_getLast?_getD [Inhabited α] {l : List α} : getLast! l = (getLast? l).getD default := by
+  cases l with
+  | nil => simp [getLast!_nil]
+  | cons _ _ => simp [getLast!, getLast?_eq_getLast]
 
 theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
   | _ :: _, rfl => rfl
@@ -1144,6 +1164,11 @@ theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_p
   | nil => simp at h
   | cons _ _ => simp
 
+theorem getElem_zero_eq_head (l : List α) (h) : l[0] = head l (by simpa [length_pos] using h) := by
+  cases l with
+  | nil => simp at h
+  | cons _ _ => simp
+
 theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h

src/Init/Data/Nat/Lemmas.lean

@@ -1029,3 +1029,12 @@ instance decidableExistsLT [h : DecidablePred p] : DecidablePred fun n => ∃ m
 instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Nat, m ≤ n ∧ p m :=
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
+
+/-! ### Results about `List.sum` specialized to `Nat` -/
+
+protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [← ih]
+    omega

src/Init/Data/Nat/Linear.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.ByCases
 import Init.Data.Prod
+import Init.Data.RArray
 
 namespace Nat.Linear
 
@@ -15,7 +16,7 @@ namespace Nat.Linear
 
 abbrev Var := Nat
 
-abbrev Context := List Nat
+abbrev Context := Lean.RArray Nat
 
 /--
   When encoding polynomials. We use `fixedVar` for encoding numerals.
@@ -23,12 +24,7 @@ abbrev Context := List Nat
 def fixedVar := 100000000 -- Any big number should work here
 
 def Var.denote (ctx : Context) (v : Var) : Nat :=
-  bif v == fixedVar then 1 else go ctx v
-where
-  go : List Nat → Nat → Nat
-   | [],    _   => 0
-   | a::_,  0   => a
-   | _::as, i+1 => go as i
+  bif v == fixedVar then 1 else ctx.get v
 
 inductive Expr where
   | num  (v : Nat)
@@ -52,25 +48,23 @@ def Poly.denote (ctx : Context) (p : Poly) : Nat :=
   | [] => 0
   | (k, v) :: p => Nat.add (Nat.mul k (v.denote ctx)) (denote ctx p)
 
-def Poly.insertSorted (k : Nat) (v : Var) (p : Poly) : Poly :=
+def Poly.insert (k : Nat) (v : Var) (p : Poly) : Poly :=
   match p with
   | [] => [(k, v)]
-  | (k', v') :: p => bif Nat.blt v v' then (k, v) :: (k', v') :: p else (k', v') :: insertSorted k v p
+  | (k', v') :: p =>
+    bif Nat.blt v v' then
+      (k, v) :: (k', v') :: p
+    else bif Nat.beq v v' then
+      (k + k', v') :: p
+    else
+      (k', v') :: insert k v p
 
-def Poly.sort (p : Poly) : Poly :=
-  let rec go (p : Poly) (r : Poly) : Poly :=
+def Poly.norm (p : Poly) : Poly := go p []
+where
+  go (p : Poly) (r : Poly) : Poly :=
     match p with
     | [] => r
-    | (k, v) :: p => go p (r.insertSorted k v)
-  go p []
-
-def Poly.fuse (p : Poly) : Poly :=
-  match p with
-  | []  => []
-  | (k, v) :: p =>
-    match fuse p with
-    | [] => [(k, v)]
-    | (k', v') :: p' => bif v == v' then (Nat.add k k', v)::p' else (k, v) :: (k', v') :: p'
+    | (k, v) :: p => go p (r.insert k v)
 
 def Poly.mul (k : Nat) (p : Poly) : Poly :=
   bif k == 0 then
@@ -146,15 +140,17 @@ def Poly.combineAux (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
 def Poly.combine (p₁ p₂ : Poly) : Poly :=
   combineAux hugeFuel p₁ p₂
 
-def Expr.toPoly : Expr → Poly
-  | Expr.num k    => bif k == 0 then [] else [ (k, fixedVar) ]
-  | Expr.var i    => [(1, i)]
-  | Expr.add a b  => a.toPoly ++ b.toPoly
-  | Expr.mulL k a => a.toPoly.mul k
-  | Expr.mulR a k => a.toPoly.mul k
-
-def Poly.norm (p : Poly) : Poly :=
-  p.sort.fuse
+def Expr.toPoly (e : Expr) :=
+  go 1 e []
+where
+  -- Implementation note: This assembles the result using difference lists
+  -- to avoid `++` on lists.
+  go (coeff : Nat) : Expr → (Poly → Poly)
+    | Expr.num k    => bif k == 0 then id else ((coeff * k, fixedVar) :: ·)
+    | Expr.var i    => ((coeff, i) :: ·)
+    | Expr.add a b  => go coeff a ∘ go coeff b
+    | Expr.mulL k a
+    | Expr.mulR a k => bif k == 0 then id else go (coeff * k) a
 
 def Expr.toNormPoly (e : Expr) : Poly :=
   e.toPoly.norm
@@ -201,7 +197,7 @@ def PolyCnstr.denote (ctx : Context) (c : PolyCnstr) : Prop :=
     Poly.denote_le ctx (c.lhs, c.rhs)
 
 def PolyCnstr.norm (c : PolyCnstr) : PolyCnstr :=
-  let (lhs, rhs) := Poly.cancel c.lhs.sort.fuse c.rhs.sort.fuse
+  let (lhs, rhs) := Poly.cancel c.lhs.norm c.rhs.norm
   { eq := c.eq, lhs, rhs }
 
 def PolyCnstr.isUnsat (c : PolyCnstr) : Bool :=
@@ -268,24 +264,32 @@ def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
   { c with lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
-attribute [local simp] Poly.denote Expr.denote Poly.insertSorted Poly.sort Poly.sort.go Poly.fuse Poly.cancelAux
+attribute [local simp] Poly.denote Expr.denote Poly.insert Poly.norm Poly.norm.go Poly.cancelAux
 attribute [local simp] Poly.mul Poly.mul.go
 
-theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (v : Var) (p : Poly) : (p.insertSorted k v).denote ctx = p.denote ctx + k * v.denote ctx := by
+theorem Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
+    (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
   match p with
   | [] => simp
-  | (k', v') :: p => by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]
+  | (k', v') :: p =>
+    by_cases h₁ : Nat.blt v v'
+    · simp [h₁]
+    · by_cases h₂ : Nat.beq v v'
+      · simp only [insert, h₁, h₂, cond_false, cond_true]
+        simp [Nat.eq_of_beq_eq_true h₂]
+      · simp only [insert, h₁, h₂, cond_false, cond_true]
+        simp [denote_insert]
 
-attribute [local simp] Poly.denote_insertSorted
+attribute [local simp] Poly.denote_insert
 
-theorem Poly.denote_sort_go (ctx : Context) (p : Poly) (r : Poly) : (sort.go p r).denote ctx = p.denote ctx + r.denote ctx := by
+theorem Poly.denote_norm_go (ctx : Context) (p : Poly) (r : Poly) : (norm.go p r).denote ctx = p.denote ctx + r.denote ctx := by
   match p with
   | [] => simp
-  | (k, v):: p => simp [denote_sort_go]
+  | (k, v):: p => simp [denote_norm_go]
 
-attribute [local simp] Poly.denote_sort_go
+attribute [local simp] Poly.denote_norm_go
 
-theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.sort.denote ctx = m.denote ctx := by
+theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.norm.denote ctx = m.denote ctx := by
   simp
 
 attribute [local simp] Poly.denote_sort
@@ -316,18 +320,6 @@ theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.revers
 
 attribute [local simp] Poly.denote_reverse
 
-theorem Poly.denote_fuse (ctx : Context) (p : Poly) : p.fuse.denote ctx = p.denote ctx := by
-  match p with
-  | [] => rfl
-  | (k, v) :: p =>
-    have ih := denote_fuse ctx p
-    simp
-    split
-    case _ h => simp [← ih, h]
-    case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ← ih, h]; rw [eq_of_beq he]
-
-attribute [local simp] Poly.denote_fuse
-
 theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx := by
   simp
   by_cases h : k == 0 <;> simp [h]; simp [eq_of_beq h]
@@ -516,13 +508,25 @@ theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p
 
 attribute [local simp] Poly.denote_combine
 
+theorem Expr.denote_toPoly_go (ctx : Context) (e : Expr) :
+  (toPoly.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
+  induction k, e using Expr.toPoly.go.induct generalizing p with
+  | case1 k k' =>
+    simp only [toPoly.go]
+    by_cases h : k' == 0
+    · simp [h, eq_of_beq h]
+    · simp [h, Var.denote]
+  | case2 k i => simp [toPoly.go]
+  | case3 k a b iha ihb => simp [toPoly.go, iha, ihb]
+  | case4 k k' a ih
+  | case5 k a k' ih =>
+    simp only [toPoly.go, denote, mul_eq]
+    by_cases h : k' == 0
+    · simp [h, eq_of_beq h]
+    · simp [h, cond_false, ih, Nat.mul_assoc]
+
 theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
-  induction e with
-  | num k => by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]; simp [eq_of_beq h]
-  | var i => simp [toPoly]
-  | add a b iha ihb => simp [toPoly, iha, ihb]
-  | mulL k a ih => simp [toPoly, ih, -Poly.mul]
-  | mulR k a ih => simp [toPoly, ih, -Poly.mul]
+  simp [toPoly, Expr.denote_toPoly_go]
 
 attribute [local simp] Expr.denote_toPoly
 
@@ -554,8 +558,8 @@ theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denot
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
   by_cases h : eq = true <;> simp [h]
-  · simp [Poly.denote_eq, Expr.toPoly]
-  · simp [Poly.denote_le, Expr.toPoly]
+  · simp [Poly.denote_eq]
+  · simp [Poly.denote_le]
 
 attribute [local simp] ExprCnstr.denote_toPoly
 

src/Init/Data/Option/Basic.lean

@@ -16,22 +16,22 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[deprecated getM (since := "2024-04-17")]
--- `[Monad m]` is not needed here.
-def toMonad [Monad m] [Alternative m] : Option α → m α := getM
-
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
   | none   => false
 
-@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome
+@[simp] theorem isSome_none : @isSome α none = false := rfl
+@[simp] theorem isSome_some : isSome (some a) = true := rfl
 
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
   | some _ => false
   | none   => true
 
+@[simp] theorem isNone_none : @isNone α none = true := rfl
+@[simp] theorem isNone_some : isNone (some a) = false := rfl
+
 /--
 `x?.isEqSome y` is equivalent to `x? == some y`, but avoids an allocation.
 -/
@@ -134,6 +134,10 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
 @[inline] def get {α : Type u} : (o : Option α) → isSome o → α
   | some x, _ => x
 
+@[simp] theorem some_get : ∀ {x : Option α} (h : isSome x), some (x.get h) = x
+| some _, _ => rfl
+@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
+
 /-- `guard p a` returns `some a` if `p a` holds, otherwise `none`. -/
 @[inline] def guard (p : α → Prop) [DecidablePred p] (a : α) : Option α :=
   if p a then some a else none

src/Init/Data/Option/Lemmas.lean

@@ -36,11 +36,6 @@ theorem get_of_mem : ∀ {o : Option α} (h : isSome o), a ∈ o → o.get h = a
 
 theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun
 
-@[simp] theorem some_get : ∀ {x : Option α} (h : isSome x), some (x.get h) = x
-| some _, _ => rfl
-
-@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
-
 theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x := by
   cases x; {contradiction}; rw [getD_some]
 
@@ -60,7 +55,9 @@ theorem get_eq_getD {fallback : α} : (o : Option α) → {h : o.isSome} → o.g
 theorem some_get! [Inhabited α] : (o : Option α) → o.isSome → some (o.get!) = o
   | some _, _ => rfl
 
-theorem get!_eq_getD_default [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
+theorem get!_eq_getD [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
+
+@[deprecated get!_eq_getD (since := "2024-11-18")] abbrev get!_eq_getD_default := @get!_eq_getD
 
 theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
   some.inj <| ha ▸ hb
@@ -73,19 +70,11 @@ theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a
 theorem eq_none_iff_forall_not_mem : o = none ↔ ∀ a, a ∉ o :=
   ⟨fun e a h => by rw [e] at h; (cases h), fun h => ext <| by simp; exact h⟩
 
-@[simp] theorem isSome_none : @isSome α none = false := rfl
-
-@[simp] theorem isSome_some : isSome (some a) = true := rfl
-
 theorem isSome_iff_exists : isSome x ↔ ∃ a, x = some a := by cases x <;> simp [isSome]
 
 theorem isSome_eq_isSome : (isSome x = isSome y) ↔ (x = none ↔ y = none) := by
   cases x <;> cases y <;> simp
 
-@[simp] theorem isNone_none : @isNone α none = true := rfl
-
-@[simp] theorem isNone_some : isNone (some a) = false := rfl
-
 @[simp] theorem not_isSome : isSome a = false ↔ a.isNone = true := by
   cases a <;> simp
 

src/Init/Data/RArray.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Init.PropLemmas
+
+namespace Lean
+
+/--
+A `RArray` can model `Fin n → α` or `Array α`, but is optimized for a fast kernel-reducible `get`
+operation.
+
+The primary intended use case is the “denote” function of a typical proof by reflection proof, where
+only the `get` operation is necessary. It is not suitable as a general-purpose data structure.
+
+There is no well-formedness invariant attached to this data structure, to keep it concise; it's
+semantics is given through `RArray.get`. In that way one can also view an `RArray` as a decision
+tree implementing `Nat → α`.
+
+See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for functions that construct an
+`RArray`.
+
+It is not universe-polymorphic. ; smaller proof objects and no complication with the `ToExpr` type
+class.
+-/
+inductive RArray (α : Type) : Type where
+  | leaf : α → RArray α
+  | branch : Nat → RArray α → RArray α → RArray α
+
+variable {α : Type}
+
+/-- The crucial operation, written with very little abstractional overhead -/
+noncomputable def RArray.get (a : RArray α) (n : Nat) : α :=
+  RArray.rec (fun x => x) (fun p _ _ l r => (Nat.ble p n).rec l r) a
+
+private theorem RArray.get_eq_def (a : RArray α) (n : Nat) :
+  a.get n = match a with
+    | .leaf x => x
+    | .branch p l r => (Nat.ble p n).rec (l.get n) (r.get n) := by
+  conv => lhs; unfold RArray.get
+  split <;> rfl
+
+/-- `RArray.get`, implemented conventionally -/
+def RArray.getImpl (a : RArray α) (n : Nat) : α :=
+  match a with
+  | .leaf x => x
+  | .branch p l r => if n < p then l.getImpl n else r.getImpl n
+
+@[csimp]
+theorem RArray.get_eq_getImpl : @RArray.get = @RArray.getImpl := by
+  funext α a n
+  induction a with
+  | leaf _ => rfl
+  | branch p l r ihl ihr =>
+    rw [RArray.getImpl, RArray.get_eq_def]
+    simp only [ihl, ihr, ← Nat.not_le, ← Nat.ble_eq, ite_not]
+    cases hnp : Nat.ble p n <;> rfl
+
+instance : GetElem (RArray α) Nat α (fun _ _ => True) where
+  getElem a n _ := a.get n
+
+def RArray.size : RArray α → Nat
+  | leaf _ => 1
+  | branch _ l r => l.size + r.size
+
+end Lean

src/Init/Data/Repr.lean

@@ -162,7 +162,7 @@ private def reprArray : Array String := Id.run do
   List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
-  if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else
+  if h : n < 128 then Nat.reprArray.get n h else
   if h : n < USize.size then (USize.ofNatCore n h).repr
   else (toDigits 10 n).asString
 

src/Init/Data/SInt/Basic.lean

@@ -148,6 +148,9 @@ instance : ShiftLeft Int8   := ⟨Int8.shiftLeft⟩
 instance : ShiftRight Int8  := ⟨Int8.shiftRight⟩
 instance : DecidableEq Int8 := Int8.decEq
 
+@[extern "lean_bool_to_int8"]
+def Bool.toInt8 (b : Bool) : Int8 := if b then 1 else 0
+
 @[extern "lean_int8_dec_lt"]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -249,6 +252,9 @@ instance : ShiftLeft Int16   := ⟨Int16.shiftLeft⟩
 instance : ShiftRight Int16  := ⟨Int16.shiftRight⟩
 instance : DecidableEq Int16 := Int16.decEq
 
+@[extern "lean_bool_to_int16"]
+def Bool.toInt16 (b : Bool) : Int16 := if b then 1 else 0
+
 @[extern "lean_int16_dec_lt"]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -354,6 +360,9 @@ instance : ShiftLeft Int32   := ⟨Int32.shiftLeft⟩
 instance : ShiftRight Int32  := ⟨Int32.shiftRight⟩
 instance : DecidableEq Int32 := Int32.decEq
 
+@[extern "lean_bool_to_int32"]
+def Bool.toInt32 (b : Bool) : Int32 := if b then 1 else 0
+
 @[extern "lean_int32_dec_lt"]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -463,6 +472,9 @@ instance : ShiftLeft Int64   := ⟨Int64.shiftLeft⟩
 instance : ShiftRight Int64  := ⟨Int64.shiftRight⟩
 instance : DecidableEq Int64 := Int64.decEq
 
+@[extern "lean_bool_to_int64"]
+def Bool.toInt64 (b : Bool) : Int64 := if b then 1 else 0
+
 @[extern "lean_int64_dec_lt"]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -574,6 +586,9 @@ instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
 instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
 instance : DecidableEq ISize := ISize.decEq
 
+@[extern "lean_bool_to_isize"]
+def Bool.toISize (b : Bool) : ISize := if b then 1 else 0
+
 @[extern "lean_isize_dec_lt"]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))

src/Init/Data/Stream.lean

@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.array.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+      some (s.array[s.start]'(Nat.lt_of_lt_of_le h s.stop_le_array_size),
         { s with start := s.start + 1, start_le_stop := this })
     else
       none

src/Init/Data/String/Basic.lean

@@ -514,9 +514,6 @@ instance : Inhabited String := ⟨""⟩
 
 instance : Append String := ⟨String.append⟩
 
-@[deprecated push (since := "2024-04-06")]
-def str : String → Char → String := push
-
 @[inline] def pushn (s : String) (c : Char) (n : Nat) : String :=
   n.repeat (fun s => s.push c) s
 

src/Init/Data/String/Extra.lean

@@ -134,7 +134,7 @@ def toUTF8 (a : @& String) : ByteArray :=
 /-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/
 @[extern "lean_string_get_byte_fast"]
 def getUtf8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8 :=
-  (toUTF8 s).get ⟨n, size_toUTF8 _ ▸ h⟩
+  (toUTF8 s)[n]'(size_toUTF8 _ ▸ h)
 
 theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h

src/Init/Data/UInt/Basic.lean

@@ -56,6 +56,9 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
+@[extern "lean_bool_to_uint8"]
+def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0
+
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
@@ -116,6 +119,9 @@ instance : Xor UInt16       := ⟨UInt16.xor⟩
 instance : ShiftLeft UInt16  := ⟨UInt16.shiftLeft⟩
 instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 
+@[extern "lean_bool_to_uint16"]
+def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0
+
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
@@ -174,6 +180,9 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
+@[extern "lean_bool_to_uint32"]
+def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
+
 @[extern "lean_uint64_add"]
 def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint64_sub"]
@@ -278,5 +287,8 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
+@[extern "lean_bool_to_usize"]
+def Bool.toUSize (b : Bool) : USize := if b then 1 else 0
+
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe

src/Init/GetElem.lean

@@ -166,6 +166,12 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
   have : Decidable (dom c i) := .isFalse h
   simp [getElem!_def, getElem?_def, h]
 
+@[simp] theorem get_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) [Decidable (dom c i)] (h) :
+    c[i]?.get h = c[i]'(by simp only [getElem?_def] at h; split at h <;> simp_all) := by
+  simp only [getElem?_def] at h ⊢
+  split <;> simp_all
+
 namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
@@ -224,7 +230,7 @@ end List
 namespace Array
 
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
+  getElem xs i h := xs.get i h
 
 end Array
 

src/Init/Prelude.lean

@@ -938,8 +938,8 @@ and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypoth
 even though it has different types in the two cases.)
 
 We use this to be able to communicate the if-then-else condition to the branches.
-For example, `Array.get arr ⟨i, h⟩` expects a proof `h : i < arr.size` in order to
-avoid a bounds check, so you can write `if h : i < arr.size then arr.get ⟨i, h⟩ else ...`
+For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to
+avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...`
 to avoid the bounds check inside the if branch. (Of course in this case we have only
 lifted the check into an explicit `if`, but we could also use this proof multiple times
 or derive `i < arr.size` from some other proposition that we are checking in the `if`.)
@@ -2630,14 +2630,21 @@ def Array.empty {α : Type u} : Array α := mkEmpty 0
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 
-/-- Access an element from an array without bounds checks, using a `Fin` index. -/
+/--
+Access an element from an array without needing a runtime bounds checks,
+using a `Nat` index and a proof that it is in bounds.
+
+This function does not use `get_elem_tactic` to automatically find the proof that
+the index is in bounds. This is because the tactic itself needs to look up values in
+arrays. Use the indexing notation `a[i]` instead.
+-/
 @[extern "lean_array_fget"]
-def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
-  a.toList.get i
+def Array.get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
+  a.toList.get ⟨i, h⟩
 
 /-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
-  dite (LT.lt i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => v₀)
+  dite (LT.lt i a.size) (fun h => a.get i h) (fun _ => v₀)
 
 /-- Access an element from an array, or panic if the index is out of bounds. -/
 @[extern "lean_array_get"]
@@ -2695,7 +2702,7 @@ protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) :
       (fun hlt =>
         match i with
         | 0           => as
-        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get ⟨j, hlt⟩)))
+        | Nat.succ i' => loop i' (hAdd j 1) (as.push (bs.get j hlt)))
       (fun _ => as)
   loop bs.size 0 as
 
@@ -2710,7 +2717,7 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
       (fun hlt =>
         match i with
         | 0           => bs
-        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.get ⟨j, hlt⟩)))
+        | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.get j hlt)))
       (fun _ => bs)
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
@@ -2822,17 +2829,6 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabi
 instance [Monad m] : [Nonempty α] → Nonempty (m α)
   | ⟨x⟩ => ⟨pure x⟩
 
-/-- A fusion of Haskell's `sequence` and `map`. Used in syntax quotations. -/
-def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m β) : m (Array β) :=
-  let rec loop (i : Nat) (j : Nat) (bs : Array β) : m (Array β) :=
-    dite (LT.lt j as.size)
-      (fun hlt =>
-        match i with
-        | 0           => pure bs
-        | Nat.succ i' => Bind.bind (f (as.get ⟨j, hlt⟩)) fun b => loop i' (hAdd j 1) (bs.push b))
-      (fun _ => pure bs)
-  loop as.size 0 (Array.mkEmpty as.size)
-
 /--
 A function for lifting a computation from an inner `Monad` to an outer `Monad`.
 Like Haskell's [`MonadTrans`], but `n` does not have to be a monad transformer.

src/Init/System/IO.lean

@@ -802,6 +802,9 @@ def run (args : SpawnArgs) : IO String := do
 
 end Process
 
+/-- Returns the thread ID of the calling thread. -/
+@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt64
+
 structure AccessRight where
   read : Bool := false
   write : Bool := false

src/Init/Tactics.lean

@@ -466,7 +466,7 @@ hypotheses or the goal. It can have one of the forms:
 * `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
 * `at *`: target all hypotheses and the goal
 -/
-syntax location := withPosition(" at" (locationWildcard <|> locationHyp))
+syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)))
 
 /--
 * `change tgt'` will change the goal from `tgt` to `tgt'`,
@@ -1155,7 +1155,7 @@ Configuration for the `decide` tactic family.
 structure DecideConfig where
   /-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
   This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
-  however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/
+  however kernel reduction ignores transparency settings. -/
   kernel : Bool := false
   /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
   admitting the result via the axiom `Lean.ofReduceBool`.  This can be significantly more efficient,
@@ -1165,7 +1165,9 @@ structure DecideConfig where
   native : Bool := false
   /-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/
   zetaReduce : Bool := true
-  /-- If true (default: false), then when preprocessing reverts free variables. -/
+  /-- If true (default: false), then when preprocessing, removes irrelevant variables and reverts the local context.
+  A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
+  or if it is a proposition that refers to a relevant variable. -/
   revert : Bool := false
 
 /--
@@ -1240,17 +1242,6 @@ example : 1 + 1 = 2 := by rfl
 -/
 syntax (name := decide) "decide" optConfig : tactic
 
-/--
-`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
-It has the following properties:
-- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
-- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
-  and once during kernel type checking), the `decide!` tactic reduces it exactly once.
-
-The `decide!` syntax is short for `decide +kernel`.
--/
-syntax (name := decideBang) "decide!" optConfig : tactic
-
 /--
 `native_decide` is a synonym for `decide +native`.
 It will attempt to prove a goal of type `p` by synthesizing an instance

src/Lean/Compiler/ConstFolding.lean

@@ -133,8 +133,8 @@ def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option E
     return mkConst ``Bool.false
 
 def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
-def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
-def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
+def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
+def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
 
 def natFoldFns : List (Name × BinFoldFn) :=
   [(``Nat.add, foldNatAdd),

src/Lean/Compiler/IR/Checker.lean

@@ -135,8 +135,8 @@ def checkExpr (ty : IRType) : Expr → M Unit
     match xType with
     | IRType.object       => checkObjType ty
     | IRType.tobject      => checkObjType ty
-    | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
-    | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
+    | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys[i]) ty else throw "invalid proj index"
+    | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys[i]) ty else throw "invalid proj index"
     | _                   => throw s!"unexpected IR type '{xType}'"
   | Expr.uproj _ x          => checkObjVar x *> checkType ty (fun t => t == IRType.usize)
   | Expr.sproj _ _ x        => checkObjVar x *> checkScalarType ty

src/Lean/Data.lean

@@ -29,4 +29,4 @@ import Lean.Data.Xml
 import Lean.Data.NameTrie
 import Lean.Data.RBTree
 import Lean.Data.RBMap
-import Lean.Data.Rat
+import Lean.Data.RArray

src/Lean/Data/HashMap.lean

@@ -90,10 +90,9 @@ def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
 
 def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
   if h : i < source.size then
-     let idx : Fin source.size := ⟨i, h⟩
-     let es  : AssocList α β   := source.get idx
+     let es  : AssocList α β   := source[i]
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set idx AssocList.nil
+     let source                := source.set i AssocList.nil
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target

src/Lean/Data/HashSet.lean

@@ -80,10 +80,9 @@ def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
 
 def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
   if h : i < source.size then
-     let idx : Fin source.size := ⟨i, h⟩
-     let es  : List α   := source.get idx
+     let es  : List α   := source[i]
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set idx []
+     let source                := source.set i []
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else

src/Lean/Data/Lsp/Utf16.lean

@@ -66,7 +66,7 @@ namespace FileMap
 
 private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
   if h : line < text.positions.size then
-    text.positions.get ⟨line, h⟩
+    text.positions[line]
   else if text.positions.isEmpty then
     0
   else

src/Lean/Data/NameMap.lean

@@ -33,6 +33,16 @@ def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n
 instance : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (RBMap ..) ..)
 
+/-- `filter f m` returns the `NameMap` consisting of all
+"`key`/`val`"-pairs in `m` where `f key val` returns `true`. -/
+def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α := RBMap.filter f m
+
+/-- `filterMap f m` filters an `NameMap` and simultaneously modifies the filtered values.
+
+It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
+The resulting entries with non-`none` value are collected to form the output `NameMap`. -/
+def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := RBMap.filterMap f m
+
 end NameMap
 
 def NameSet := RBTree Name Name.quickCmp
@@ -53,6 +63,9 @@ def append (s t : NameSet) : NameSet :=
 instance : Append NameSet where
   append := NameSet.append
 
+/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`. -/
+def filter (f : Name → Bool) (s : NameSet) : NameSet := RBTree.filter f s
+
 end NameSet
 
 def NameSSet := SSet Name
@@ -73,6 +86,9 @@ instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
 def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
+
+/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/
+def filter (f : Name → Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s
 end NameHashSet
 
 def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=

src/Lean/Data/PersistentArray.lean

@@ -149,8 +149,8 @@ private def emptyArray {α : Type u} : Array (PersistentArrayNode α) :=
 partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (PersistentArrayNode α)
   | node cs =>
     if h : cs.size ≠ 0 then
-      let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.pred_lt h⟩
-      let last := cs.get idx
+      let idx := cs.size - 1
+      let last := cs[idx]
       let cs'  := cs.set idx default
       match popLeaf last with
       | (none,   _)       => (none, emptyArray)

src/Lean/Data/PersistentHashMap.lean

@@ -84,11 +84,10 @@ private theorem size_push {ks : Array α} {vs : Array β} (h : ks.size = vs.size
 partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat → α → β → CollisionNode α β
   | n@⟨Node.collision keys vals heq, _⟩, i, k, v =>
     if h : i < keys.size then
-      let idx : Fin keys.size := ⟨i, h⟩;
-      let k' := keys.get idx;
+      let k' := keys[i];
       if k == k' then
          let j : Fin vals.size := ⟨i, by rw [←heq]; assumption⟩
-         ⟨Node.collision (keys.set idx k) (vals.set j v) (size_set heq idx j k v), IsCollisionNode.mk _ _ _⟩
+         ⟨Node.collision (keys.set i k) (vals.set j v) (size_set heq ⟨i, h⟩ j k v), IsCollisionNode.mk _ _ _⟩
       else insertAtCollisionNodeAux n (i+1) k v
     else
       ⟨Node.collision (keys.push k) (vals.push v) (size_push heq k v), IsCollisionNode.mk _ _ _⟩

src/Lean/Data/Position.lean

@@ -97,7 +97,7 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
   let colPos :=
     if h : pos.line - 1 < text.positions.size then
-      text.positions.get ⟨pos.line - 1, h⟩
+      text.positions[pos.line - 1]
     else if text.positions.isEmpty then
       0
     else
@@ -110,7 +110,7 @@ This gives the same result as `map.ofPosition ⟨line, 0⟩`, but is more effici
 -/
 def lineStart (map : FileMap) (line : Nat) : String.Pos :=
   if h : line - 1 < map.positions.size then
-    map.positions.get ⟨line - 1, h⟩
+    map.positions[line - 1]
   else map.positions.back?.getD 0
 
 end FileMap

src/Lean/Data/RArray.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Init.Data.RArray
+import Lean.ToExpr
+
+/-!
+Auxillary definitions related to `Lean.RArray` that are typically only used in meta-code, in
+particular the `ToExpr` instance.
+-/
+
+namespace Lean
+
+-- This function could live in Init/Data/RArray.lean, but without omega it's tedious to implement
+def RArray.ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) : RArray α :=
+  go 0 n h (Nat.le_refl _)
+where
+  go (lb ub : Nat) (h1 : lb < ub) (h2 : ub ≤ n) : RArray α :=
+    if h : lb + 1 = ub then
+      .leaf (f ⟨lb, Nat.lt_of_lt_of_le h1 h2⟩)
+    else
+      let mid := (lb + ub)/2
+      .branch mid (go lb mid (by omega) (by omega)) (go mid ub (by omega) h2)
+
+def RArray.ofArray (xs : Array α) (h : 0 < xs.size) : RArray α :=
+  .ofFn (xs[·]) h
+
+/-- The correctness theorem for `ofFn` -/
+theorem RArray.get_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) :
+    (ofFn f h).get i = f i :=
+  go 0 n h (Nat.le_refl _) (Nat.zero_le _) i.2
+where
+  go lb ub h1 h2 (h3 : lb ≤ i.val) (h3 : i.val < ub) : (ofFn.go f lb ub h1 h2).get i = f i := by
+    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
+    case case1 =>
+      simp [ofFn.go, RArray.get_eq_getImpl, RArray.getImpl]
+      congr
+      omega
+    case case2 ih1 ih2 hiu =>
+      rw [ofFn.go]; simp only [↓reduceDIte, *]
+      simp [RArray.get_eq_getImpl, RArray.getImpl] at *
+      split
+      · rw [ih1] <;> omega
+      · rw [ih2] <;> omega
+
+@[simp]
+theorem RArray.size_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) :
+    (ofFn f h).size = n :=
+  go 0 n h (Nat.le_refl _)
+where
+  go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
+    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
+    case case1 => simp [ofFn.go, size]; omega
+    case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega
+
+section Meta
+open Lean
+
+def RArray.toExpr (ty : Expr) (f : α → Expr) : RArray α → Expr
+  | .leaf x  =>
+    mkApp2 (mkConst ``RArray.leaf) ty (f x)
+  | .branch p l r =>
+    mkApp4 (mkConst ``RArray.branch) ty (mkRawNatLit p) (l.toExpr ty f) (r.toExpr ty f)
+
+instance [ToExpr α] : ToExpr (RArray α) where
+  toTypeExpr := mkApp (mkConst ``RArray) (toTypeExpr α)
+  toExpr a := a.toExpr (toTypeExpr α) toExpr
+
+end Meta
+
+end Lean

src/Lean/Data/RBMap.lean

@@ -404,6 +404,24 @@ def intersectBy {γ : Type v₁} {δ : Type v₂} (mergeFn : α → β → γ
       | some b₂ => acc.insert a <| mergeFn a b₁ b₂
       | none => acc
 
+/--
+`filter f m` returns the `RBMap` consisting of all
+"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
+-/
+def filter (f : α → β → Bool) (m : RBMap α β cmp) : RBMap α β cmp :=
+  m.fold (fun r k v => if f k v then r.insert k v else r) {}
+
+/--
+`filterMap f m` filters an `RBMap` and simultaneously modifies the filtered values.
+
+It takes a function `f : α → β → Option γ` and applies `f k v` to the value with key `k`.
+The resulting entries with non-`none` value are collected to form the output `RBMap`.
+-/
+def filterMap (f : α → β → Option γ) (m : RBMap α β cmp) : RBMap α γ cmp :=
+  m.fold (fun r k v => match f k v with
+    | none => r
+    | some b => r.insert k b) {}
+
 end RBMap
 
 def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=

src/Lean/Data/RBTree.lean

@@ -114,6 +114,13 @@ def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
 def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
   t₂.fold .erase t₁
 
+/--
+`filter f m` returns the `RBTree` consisting of all
+`x` in `m` where `f x` returns `true`.
+-/
+def filter (f : α → Bool) (m : RBTree α cmp) : RBTree α cmp :=
+  RBMap.filter (fun a _ => f a) m
+
 end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=

src/Lean/Elab/App.lean

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

src/Lean/Elab/BuiltinCommand.lean

@@ -111,9 +111,8 @@ private def checkEndHeader : Name → List Scope → Option Name
 
 private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM Unit :=
   if h : i < cmds.size then
-    let cmd := cmds.get ⟨i, h⟩;
     catchInternalId unsupportedSyntaxExceptionId
-      (elabCommand cmd)
+      (elabCommand cmds[i])
       (fun _ => elabChoiceAux cmds (i+1))
   else
     throwUnsupportedSyntax

src/Lean/Elab/Command.lean

@@ -214,7 +214,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
+    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
     log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
   return log
 
@@ -555,7 +555,11 @@ private def getVarDecls (s : State) : Array Syntax :=
 instance {α} : Inhabited (CommandElabM α) where
   default := throw default
 
-private def mkMetaContext : Meta.Context := {
+/--
+The environment linter framework needs to be able to run linters with the same context
+as `liftTermElabM`, so we expose that context as a public function here.
+-/
+def mkMetaContext : Meta.Context := {
   config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }
 }
 

src/Lean/Elab/Declaration.lean

@@ -192,8 +192,7 @@ private def isMutualPreambleCommand (stx : Syntax) : Bool :=
 private partial def splitMutualPreamble (elems : Array Syntax) : Option (Array Syntax × Array Syntax) :=
   let rec loop (i : Nat) : Option (Array Syntax × Array Syntax) :=
     if h : i < elems.size then
-      let elem := elems.get ⟨i, h⟩
-      if isMutualPreambleCommand elem then
+      if isMutualPreambleCommand elems[i] then
         loop (i+1)
       else if i == 0 then
         none -- `mutual` block does not contain any preamble commands

src/Lean/Elab/Inductive.lean

@@ -133,7 +133,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
 private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) :=
   Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
     if h : i < views.size then
-      let view := views.get ⟨i, h⟩
+      let view := views[i]
       let acc ← Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
         match view.type? with
         | none         =>
@@ -250,7 +250,7 @@ private partial def withInductiveLocalDecls (rs : Array ElabHeaderResult) (x : A
   withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do
     let rec loop (i : Nat) (indFVars : Array Expr) := do
       if h : i < namesAndTypes.size then
-        let (declName, shortDeclName, type) := namesAndTypes.get ⟨i, h⟩
+        let (declName, shortDeclName, type) := namesAndTypes[i]
         Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
       else
         x params indFVars

src/Lean/Elab/LetRec.lean

@@ -77,7 +77,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
 private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : Array Expr → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
     if h : i < views.size then
-      let view := views.get ⟨i, h⟩
+      let view := views[i]
       withAuxDecl view.shortDeclName view.type view.declName fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars
@@ -90,9 +90,9 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       for i in [0:view.binderIds.size] do
         addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
-        withInfoContext' view.valStx (mkInfo := mkTermInfo `MutualDef.body view.valStx) do
-         let value ← elabTermEnsuringType view.valStx type
-         mkLambdaFVars xs value
+        withInfoContext' view.valStx (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·)) do
+          let value ← elabTermEnsuringType view.valStx type
+          mkLambdaFVars xs value
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
   let letRecsToLiftCurr := (← get).letRecsToLift

src/Lean/Elab/Match.lean

@@ -108,7 +108,7 @@ where
   /-- Elaborate discriminants inferring the match-type -/
   elabDiscrs (i : Nat) (discrs : Array Discr) : TermElabM ElabMatchTypeAndDiscrsResult := do
     if h : i < discrStxs.size then
-      let discrStx := discrStxs.get ⟨i, h⟩
+      let discrStx := discrStxs[i]
       let discr     ← elabAtomicDiscr discrStx
       let discr     ← instantiateMVars discr
       let userName ← mkUserNameFor discr
@@ -176,9 +176,8 @@ structure PatternVarDecl where
 private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array PatternVarDecl → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (decls : Array PatternVarDecl) (userNames : Array Name) := do
     if h : i < pVars.size then
-      let var := pVars.get ⟨i, h⟩
       let type ← mkFreshTypeMVar
-      withLocalDecl var.getId BinderInfo.default type fun x =>
+      withLocalDecl pVars[i].getId BinderInfo.default type fun x =>
         loop (i+1) (decls.push { fvarId := x.fvarId! }) (userNames.push Name.anonymous)
     else
       k decls
@@ -760,7 +759,7 @@ where
     | [] => k eqs
     | p::ps =>
       if h : i < discrs.size then
-        let discr := discrs.get ⟨i, h⟩
+        let discr := discrs[i]
         if let some h := discr.h? then
           withLocalDeclD h.getId (← mkEqHEq discr.expr (← p.toExpr)) fun eq => do
             addTermInfo' h eq (isBinder := true)

src/Lean/Elab/MutualDef.lean

@@ -77,7 +77,7 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
   if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
     throwError "'unsafe' subsumes 'partial'"
   if h : 0 < prevHeaders.size then
-    let firstHeader := prevHeaders.get ⟨0, h⟩
+    let firstHeader := prevHeaders[0]
     try
       unless newHeader.levelNames == firstHeader.levelNames do
         throwError "universe parameters mismatch"
@@ -273,7 +273,7 @@ where
 private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (k : Array Expr → TermElabM α) : TermElabM α :=
   let rec loop (i : Nat) (fvars : Array Expr) := do
     if h : i < headers.size then
-      let header := headers.get ⟨i, h⟩
+      let header := headers[i]
       if header.modifiers.isNonrec then
         loop (i+1) fvars
       else
@@ -417,7 +417,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- Store instantiated body in info tree for the benefit of the unused variables linter
           -- and other metaprograms that may want to inspect it without paying for the instantiation
           -- again
-          withInfoContext' valStx (mkInfo := mkTermInfo `MutualDef.body valStx) do
+          withInfoContext' valStx (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·)) do
             -- synthesize mvars here to force the top-level tactic block (if any) to run
             let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
             -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
@@ -936,7 +936,7 @@ end MutualClosure
 private def getAllUserLevelNames (headers : Array DefViewElabHeader) : List Name :=
   if h : 0 < headers.size then
     -- Recall that all top-level functions must have the same levels. See `check` method above
-    (headers.get ⟨0, h⟩).levelNames
+    headers[0].levelNames
   else
     []
 

src/Lean/Elab/PatternVar.lean

@@ -135,7 +135,7 @@ private def isNextArgAccessible (ctx : Context) : Bool :=
   | none =>
     if h : i < ctx.paramDecls.size then
       -- For `[match_pattern]` applications, only explicit parameters are accessible.
-      let d := ctx.paramDecls.get ⟨i, h⟩
+      let d := ctx.paramDecls[i]
       d.2.isExplicit
     else
       false

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -50,7 +50,9 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
+      else
+        let ctx ← Simp.mkContext (config := { dsimp := false })
+        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

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

@@ -45,7 +45,9 @@ where
       go mvarId
     else if let some mvarId ← simpIf? mvarId then
       go mvarId
-    else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
+    else
+      let ctx ← Simp.mkContext
+      match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>

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

@@ -243,7 +243,7 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
     recArgInfoss := recArgInfoss.push recArgInfos
   -- Put non-indices first
   recArgInfoss := recArgInfoss.map nonIndicesFirst
-  trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}"
+  trace[Elab.definition.structural] "recArgInfos:{indentD (.joinSep (recArgInfoss.flatten.toList.map (repr ·)) Format.line)}"
   -- Inductive groups to consider
   let groups ← inductiveGroups recArgInfoss.flatten
   trace[Elab.definition.structural] "inductive groups: {groups}"

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

@@ -27,7 +27,7 @@ constituents.
 structure IndGroupInfo where
   all       : Array Name
   numNested : Nat
-deriving BEq, Inhabited
+deriving BEq, Inhabited, Repr
 
 def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
   all       := indInfo.all.toArray
@@ -56,7 +56,7 @@ mutual structural recursion on such incompatible types.
 structure IndGroupInst extends IndGroupInfo where
   levels    : List Level
   params    : Array Expr
-deriving Inhabited
+deriving Inhabited, Repr
 
 def IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData :=
   mkAppN (.const igi.all[0]! igi.levels) igi.params

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

@@ -23,9 +23,9 @@ structure RecArgInfo where
   fnName       : Name
   /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/
   numFixed     : Nat
-  /-- position of the argument (counted including fixed prefix) we are recursing on -/
+  /-- position (counted including fixed prefix) of the argument we are recursing on -/
   recArgPos    : Nat
-  /-- position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on -/
+  /-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/
   indicesPos   : Array Nat
   /-- The inductive group (with parameters) of the argument's type -/
   indGroupInst : IndGroupInst
@@ -34,20 +34,23 @@ structure RecArgInfo where
   If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
   -/
   indIdx       : Nat
-deriving Inhabited
+deriving Inhabited, Repr
 
 /--
 If `xs` are the parameters of the functions (excluding fixed prefix), partitions them
 into indices and major arguments, and other parameters.
 -/
 def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
+  -- First indices and major arg, using the order they appear in `info.indicesPos`
   let mut indexMajorArgs := #[]
+  let indexMajorPos := info.indicesPos.push info.recArgPos
+  for j in indexMajorPos do
+    assert! info.numFixed ≤ j && j - info.numFixed < xs.size
+    indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]!
+  -- Then the other arguments, in the order they appear in `xs`
   let mut otherArgs := #[]
   for h : i in [:xs.size] do
-    let j := i + info.numFixed
-    if j = info.recArgPos || info.indicesPos.contains j then
-      indexMajorArgs := indexMajorArgs.push xs[i]
-    else
+    unless indexMajorPos.contains (i + info.numFixed) do
       otherArgs := otherArgs.push xs[i]
   return (indexMajorArgs, otherArgs)
 

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

@@ -57,7 +57,9 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
+      else
+        let ctx ← Simp.mkContext (config := { dsimp := false })
+        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

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

@@ -227,7 +227,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsP
     -- decreasing goals when the function has only one non fixed argument.
     -- This renaming is irrelevant if the function has multiple non fixed arguments. See `process*` functions above.
     let lctx := (← getLCtx).setUserName x.fvarId! varName
-    withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
+    withLCtx' lctx do
       let F   := xs[1]!
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do

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

@@ -166,7 +166,7 @@ def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool
 def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
   let mut lctx ←  getLCtx
   for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
-  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
+  withLCtx' lctx k
 
 /-- Create one measure for each (eligible) parameter of the given predefintion.  -/
 def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)

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

@@ -87,7 +87,7 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
     xs.mapM (·.fvarId!.getUserName)
 
 def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
-  let termArgs? := termArg?s.sequenceMap id -- Either all or none, checked by `elabTerminationByHints`
+  let termArgs? := termArg?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
   let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do

src/Lean/Elab/Quotation.lean

@@ -434,7 +434,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             else mkNullNode contents
           -- We use `no_error_if_unused%` in auxiliary `match`-syntax to avoid spurious error messages,
           -- the outer `match` is checking for unused alternatives
-          `(match ($(discrs).sequenceMap fun
+          `(match ($(discrs).mapM fun
                 | `($contents) => no_error_if_unused% some $tuple
                 | _            => no_error_if_unused% none) with
               | some $resId => $yes

src/Lean/Elab/StructInst.lean

@@ -11,21 +11,40 @@ import Lean.Elab.App
 import Lean.Elab.Binders
 import Lean.PrettyPrinter
 
+/-!
+# Structure instance elaborator
+
+A *structure instance* is notation to construct a term of a `structure`.
+Examples: `{ x := 2, y.z := true }`, `{ s with cache := c' }`, and `{ s with values[2] := v }`.
+Structure instances are the preferred way to invoke a `structure`'s constructor,
+since they hide Lean implementation details such as whether parents are represented as subobjects,
+and also they do correct processing of default values, which are complicated due to the fact that `structure`s can override default values of their parents.
+
+This module elaborates structure instance notation.
+Note that the `where` syntax to define structures (`Lean.Parser.Command.whereStructInst`)
+macro expands into the structure instance notation elaborated by this module.
+-/
+
 namespace Lean.Elab.Term.StructInst
 
 open Meta
 open TSyntax.Compat
 
-/-
-  Structure instances are of the form:
-
-      "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
-          >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
-          >> optEllipsis
-          >> optional (" : " >> termParser)
-          >> " }"
+/-!
+Recall that structure instances are of the form:
+```
+"{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
+    >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
+    >> optEllipsis
+    >> optional (" : " >> termParser)
+    >> " }"
+```
 -/
 
+/--
+Transforms structure instances such as `{ x := 0 : Foo }` into `({ x := 0 } : Foo)`.
+Structure instance notation makes use of the expected type.
+-/
 @[builtin_macro Lean.Parser.Term.structInst] def expandStructInstExpectedType : Macro := fun stx =>
   let expectedArg := stx[4]
   if expectedArg.isNone then
@@ -35,7 +54,10 @@ open TSyntax.Compat
     let stxNew   := stx.setArg 4 mkNullNode
     `(($stxNew : $expected))
 
-/-- Expand field abbreviations. Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }` -/
+/--
+Expands field abbreviation notation.
+Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }`.
+-/
 @[builtin_macro Lean.Parser.Term.structInst] def expandStructInstFieldAbbrev : Macro
   | `({ $[$srcs,* with]? $fields,* $[..%$ell]? $[: $ty]? }) =>
     if fields.getElems.raw.any (·.getKind == ``Lean.Parser.Term.structInstFieldAbbrev) then do
@@ -49,9 +71,12 @@ open TSyntax.Compat
   | _ => Macro.throwUnsupported
 
 /--
-  If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable, expand into `let src := sᵢ; { ..., src, ... with ... }`.
+If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable,
+expands into `let __src := sᵢ; { ..., __src, ... with ... }`.
+The significance of `__src` is that the variable is treated as an implementation-detail local variable,
+which can be unfolded by `simp` when `zetaDelta := false`.
 
-  Note that this one is not a `Macro` because we need to access the local context.
+Note that this one is not a `Macro` because we need to access the local context.
 -/
 private def expandNonAtomicExplicitSources (stx : Syntax) : TermElabM (Option Syntax) := do
   let sourcesOpt := stx[1]
@@ -100,27 +125,44 @@ where
           let r ← go sources (sourcesNew.push sourceNew)
           `(let __src := $source; $r)
 
-structure ExplicitSourceInfo where
+/--
+An *explicit source* is one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`.
+-/
+structure ExplicitSourceView where
+  /-- The syntax of the explicit source. -/
   stx        : Syntax
+  /-- The name of the structure for the type of the explicit source. -/
   structName : Name
   deriving Inhabited
 
-structure Source where
-  explicit : Array ExplicitSourceInfo -- `s₁ ... sₙ with`
-  implicit : Option Syntax -- `..`
+/--
+A view of the sources of fields for the structure instance notation.
+-/
+structure SourcesView where
+  /-- Explicit sources (i.e., one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`). -/
+  explicit : Array ExplicitSourceView
+  /-- The syntax for a trailing `..`. This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications. -/
+  implicit : Option Syntax
   deriving Inhabited
 
-def Source.isNone : Source → Bool
+/-- Returns `true` if the structure instance has no sources (neither explicit sources nor a `..`). -/
+def SourcesView.isNone : SourcesView → Bool
   | { explicit := #[], implicit := none } => true
   | _ => false
 
-/-- `optional (atomic (sepBy1 termParser ", " >> " with ")` -/
+/--
+Given an array of explicit sources, returns syntax of the form
+`optional (atomic (sepBy1 termParser ", " >> " with ")`
+-/
 private def mkSourcesWithSyntax (sources : Array Syntax) : Syntax :=
   let ref := sources[0]!
   let stx := Syntax.mkSep sources (mkAtomFrom ref ", ")
   mkNullNode #[stx, mkAtomFrom ref "with "]
 
-private def getStructSource (structStx : Syntax) : TermElabM Source :=
+/--
+Creates a structure source view from structure instance notation.
+-/
+private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
   withRef structStx do
     let explicitSource := structStx[1]
     let implicitSource := structStx[3]
@@ -138,10 +180,10 @@ private def getStructSource (structStx : Syntax) : TermElabM Source :=
     return { explicit, implicit }
 
 /--
-  We say a `{ ... }` notation is a `modifyOp` if it contains only one
-  ```
-  def structInstArrayRef := leading_parser "[" >> termParser >>"]"
-  ```
+We say a structure instance notation is a "modifyOp" if it contains only a single array update.
+```lean
+def structInstArrayRef := leading_parser "[" >> termParser >>"]"
+```
 -/
 private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
   let s? ← stx[2].getSepArgs.foldlM (init := none) fun s? arg => do
@@ -177,7 +219,11 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
   | none   => return none
   | some s => if s[0][0].getKind == ``Lean.Parser.Term.structInstArrayRef then return s? else return none
 
-private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceInfo) (expectedType? : Option Expr) : TermElabM Expr := do
+/--
+Given a `stx` that is a structure instance notation that's a modifyOp (according to `isModifyOp?`), elaborates it.
+Only supports structure instances with a single source.
+-/
+private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceView) (expectedType? : Option Expr) : TermElabM Expr := do
   if sources.size > 1 then
     throwError "invalid \{...} notation, multiple sources and array update is not supported."
   let cont (val : Syntax) : TermElabM Expr := do
@@ -204,12 +250,13 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
     cont val
 
 /--
-  Get structure name.
-  This method triest to postpone execution if the expected type is not available.
+Gets the structure name for the structure instance from the expected type and the sources.
+This method tries to postpone execution if the expected type is not available.
 
-  If the expected type is available and it is a structure, then we use it.
-  Otherwise, we use the type of the first source. -/
-private def getStructName (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
+If the expected type is available and it is a structure, then we use it.
+Otherwise, we use the type of the first source.
+-/
+private def getStructName (expectedType? : Option Expr) (sourceView : SourcesView) : TermElabM Name := do
   tryPostponeIfNoneOrMVar expectedType?
   let useSource : Unit → TermElabM Name := fun _ => do
     unless sourceView.explicit.isEmpty do
@@ -226,7 +273,7 @@ private def getStructName (expectedType? : Option Expr) (sourceView : Source) :
       unless isStructure (← getEnv) constName do
         throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}"
       return constName
-    | _                        => useSource ()
+    | _ => useSource ()
 where
   throwUnknownExpectedType :=
     throwError "invalid \{...} notation, expected type is not known"
@@ -237,72 +284,92 @@ where
     else
       throwError "invalid \{...} notation, {kind} type is not of the form (C ...){indentExpr type}"
 
+/--
+A component of a left-hand side for a field appearing in structure instance syntax.
+-/
 inductive FieldLHS where
+  /-- A name component for a field left-hand side. For example, `x` and `y` in `{ x.y := v }`. -/
   | fieldName  (ref : Syntax) (name : Name)
+  /-- A numeric index component for a field left-hand side. For example `3` in `{ x.3 := v }`. -/
   | fieldIndex (ref : Syntax) (idx : Nat)
+  /-- An array indexing component for a field left-hand side. For example `[3]` in `{ arr[3] := v }`. -/
   | modifyOp   (ref : Syntax) (index : Syntax)
   deriving Inhabited
 
-instance : ToFormat FieldLHS := ⟨fun lhs =>
-  match lhs with
-  | .fieldName _ n  => format n
-  | .fieldIndex _ i => format i
-  | .modifyOp _ i   => "[" ++ i.prettyPrint ++ "]"⟩
+instance : ToFormat FieldLHS where
+  format
+    | .fieldName _ n  => format n
+    | .fieldIndex _ i => format i
+    | .modifyOp _ i   => "[" ++ i.prettyPrint ++ "]"
 
+/--
+`FieldVal StructInstView` is a representation of a field value in the structure instance.
+-/
 inductive FieldVal (σ : Type) where
-  | term  (stx : Syntax) : FieldVal σ
+  /-- A `term` to use for the value of the field. -/
+  | term (stx : Syntax)  : FieldVal σ
+  /-- A `StructInstView` to use for the value of a subobject field. -/
   | nested (s : σ)       : FieldVal σ
-  | default              : FieldVal σ -- mark that field must be synthesized using default value
+  /-- A field that was not provided and should be synthesized using default values. -/
+  | default              : FieldVal σ
   deriving Inhabited
 
+/--
+`Field StructInstView` is a representation of a field in the structure instance.
+-/
 structure Field (σ : Type) where
+  /-- The whole field syntax. -/
   ref   : Syntax
+  /-- The LHS decomposed into components. -/
   lhs   : List FieldLHS
+  /-- The value of the field. -/
   val   : FieldVal σ
+  /-- The elaborated field value, filled in at `elabStruct`.
+  Missing fields use a metavariable for the elaborated value and are later solved for in `DefaultFields.propagate`. -/
   expr? : Option Expr := none
   deriving Inhabited
 
+/--
+Returns if the field has a single component in its LHS.
+-/
 def Field.isSimple {σ} : Field σ → Bool
   | { lhs := [_], .. } => true
   | _                  => false
 
-inductive Struct where
-  /-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/
-  | mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source)
+/--
+The view for structure instance notation.
+-/
+structure StructInstView where
+  /-- The syntax for the whole structure instance. -/
+  ref : Syntax
+  /-- The name of the structure for the type of the structure instance. -/
+  structName : Name
+  /-- Used for default values, to propagate structure type parameters. It is initially empty, and then set at `elabStruct`. -/
+  params : Array (Name × Expr)
+  /-- The fields of the structure instance. -/
+  fields : List (Field StructInstView)
+  /-- The additional sources for fields for the structure instance. -/
+  sources : SourcesView
   deriving Inhabited
 
-abbrev Fields := List (Field Struct)
-
-def Struct.ref : Struct → Syntax
-  | ⟨ref, _, _, _, _⟩ => ref
-
-def Struct.structName : Struct → Name
-  | ⟨_, structName, _, _, _⟩ => structName
-
-def Struct.params : Struct → Array (Name × Expr)
-  | ⟨_, _, params, _, _⟩ => params
-
-def Struct.fields : Struct → Fields
-  | ⟨_, _, _, fields, _⟩ => fields
-
-def Struct.source : Struct → Source
-  | ⟨_, _, _, _, s⟩ => s
+/-- Abbreviation for the type of `StructInstView.fields`, namely `List (Field StructInstView)`. -/
+abbrev Fields := List (Field StructInstView)
 
 /-- `true` iff all fields of the given structure are marked as `default` -/
-partial def Struct.allDefault (s : Struct) : Bool :=
+partial def StructInstView.allDefault (s : StructInstView) : Bool :=
   s.fields.all fun { val := val,  .. } => match val with
     | .term _   => false
     | .default  => true
     | .nested s => allDefault s
 
-def formatField (formatStruct : Struct → Format) (field : Field Struct) : Format :=
+def formatField (formatStruct : StructInstView → Format) (field : Field StructInstView) : Format :=
   Format.joinSep field.lhs " . " ++ " := " ++
     match field.val with
     | .term v   => v.prettyPrint
     | .nested s => formatStruct s
     | .default  => "<default>"
 
-partial def formatStruct : Struct → Format
+partial def formatStruct : StructInstView → Format
   | ⟨_, _,          _, fields, source⟩ =>
     let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", "
     let implicitFmt := if source.implicit.isSome then " .. " else ""
@@ -311,31 +378,39 @@ partial def formatStruct : Struct → Format
     else
       "{" ++ format (source.explicit.map (·.stx)) ++ " with " ++ fieldsFmt ++ implicitFmt ++ "}"
 
-instance : ToFormat Struct     := ⟨formatStruct⟩
-instance : ToString Struct := ⟨toString ∘ format⟩
+instance : ToFormat StructInstView     := ⟨formatStruct⟩
+instance : ToString StructInstView := ⟨toString ∘ format⟩
 
-instance : ToFormat (Field Struct) := ⟨formatField formatStruct⟩
-instance : ToString (Field Struct) := ⟨toString ∘ format⟩
+instance : ToFormat (Field StructInstView) := ⟨formatField formatStruct⟩
+instance : ToString (Field StructInstView) := ⟨toString ∘ format⟩
+
+/--
+Converts a `FieldLHS` back into syntax. This assumes the `ref` fields have the correct structure.
 
-/-
 Recall that `structInstField` elements have the form
-```
-   def structInstField  := leading_parser structInstLVal >> " := " >> termParser
-   def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
-   def structInstArrayRef := leading_parser "[" >> termParser >>"]"
+```lean
+def structInstField  := leading_parser structInstLVal >> " := " >> termParser
+def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
+def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 ```
 -/
 -- Remark: this code relies on the fact that `expandStruct` only transforms `fieldLHS.fieldName`
-def FieldLHS.toSyntax (first : Bool) : FieldLHS → Syntax
+private def FieldLHS.toSyntax (first : Bool) : FieldLHS → Syntax
   | .modifyOp   stx _    => stx
   | .fieldName  stx name => if first then mkIdentFrom stx name else mkGroupNode #[mkAtomFrom stx ".", mkIdentFrom stx name]
   | .fieldIndex stx _    => if first then stx else mkGroupNode #[mkAtomFrom stx ".", stx]
 
-def FieldVal.toSyntax : FieldVal Struct → Syntax
+/--
+Converts a `FieldVal StructInstView` back into syntax. Only supports `.term`, and it assumes the `stx` field has the correct structure.
+-/
+private def FieldVal.toSyntax : FieldVal Struct → Syntax
   | .term stx => stx
-  | _                 => unreachable!
+  | _         => unreachable!
 
-def Field.toSyntax : Field Struct → Syntax
+/--
+Converts a `Field StructInstView` back into syntax. Used to construct synthetic structure instance notation for subobjects in `StructInst.expandStruct` processing.
+-/
+private def Field.toSyntax : Field Struct → Syntax
   | field =>
     let stx := field.ref
     let stx := stx.setArg 2 field.val.toSyntax
@@ -343,6 +418,7 @@ def Field.toSyntax : Field Struct → Syntax
     | first::rest => stx.setArg 0 <| mkNullNode #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
     | _ => unreachable!
 
+/-- Creates a view of a field left-hand side. -/
 private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
   if stx.getKind == ``Lean.Parser.Term.structInstArrayRef then
     return FieldLHS.modifyOp stx stx[1]
@@ -355,7 +431,12 @@ private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
       | some idx => return FieldLHS.fieldIndex stx idx
       | none     => Macro.throwError "unexpected structure syntax"
 
-private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : MacroM Struct := do
+/--
+Creates a structure instance view from structure instance notation
+and the computed structure name (from `Lean.Elab.Term.StructInst.getStructName`)
+and structure source view (from `Lean.Elab.Term.StructInst.getStructSources`).
+-/
+private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesView) : MacroM StructInstView := do
   /- Recall that `stx` is of the form
      ```
      leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
@@ -371,24 +452,18 @@ private def mkStructView (stx : Syntax) (structName : Name) (source : Source) :
     let val      := fieldStx[2]
     let first    ← toFieldLHS fieldStx[0][0]
     let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
-    return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field Struct }
-  return ⟨stx, structName, #[], fields, source⟩
+    return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field StructInstView }
+  return { ref := stx, structName, params := #[], fields, sources }
 
-def Struct.modifyFieldsM {m : Type → Type} [Monad m] (s : Struct) (f : Fields → m Fields) : m Struct :=
+def StructInstView.modifyFieldsM {m : Type → Type} [Monad m] (s : StructInstView) (f : Fields → m Fields) : m StructInstView :=
   match s with
-  | ⟨ref, structName, params, fields, source⟩ => return ⟨ref, structName, params, (← f fields), source⟩
+  | { ref, structName, params, fields, sources } => return { ref, structName, params, fields := (← f fields), sources }
 
-def Struct.modifyFields (s : Struct) (f : Fields → Fields) : Struct :=
+def StructInstView.modifyFields (s : StructInstView) (f : Fields → Fields) : StructInstView :=
   Id.run <| s.modifyFieldsM f
 
-def Struct.setFields (s : Struct) (fields : Fields) : Struct :=
-  s.modifyFields fun _ => fields
-
-def Struct.setParams (s : Struct) (ps : Array (Name × Expr)) : Struct :=
-  match s with
-  | ⟨ref, structName, _, fields, source⟩ => ⟨ref, structName, ps, fields, source⟩
-
-private def expandCompositeFields (s : Struct) : Struct :=
+/-- Expands name field LHSs with multi-component names into multi-component LHSs. -/
+private def expandCompositeFields (s : StructInstView) : StructInstView :=
   s.modifyFields fun fields => fields.map fun field => match field with
     | { lhs := .fieldName _ (.str Name.anonymous ..) :: _, .. } => field
     | { lhs := .fieldName ref n@(.str ..) :: rest, .. } =>
@@ -396,7 +471,8 @@ private def expandCompositeFields (s : Struct) : Struct :=
       { field with lhs := newEntries ++ rest }
     | _ => field
 
-private def expandNumLitFields (s : Struct) : TermElabM Struct :=
+/-- Replaces numeric index field LHSs with the corresponding named field, or throws an error if no such field exists. -/
+private def expandNumLitFields (s : StructInstView) : TermElabM StructInstView :=
   s.modifyFieldsM fun fields => do
     let env ← getEnv
     let fieldNames := getStructureFields env s.structName
@@ -407,28 +483,31 @@ private def expandNumLitFields (s : Struct) : TermElabM Struct :=
         else return { field with lhs := .fieldName ref fieldNames[idx - 1]! :: rest }
       | _ => return field
 
-/-- For example, consider the following structures:
-   ```
-   structure A where
-     x : Nat
+/--
+Expands fields that are actually represented as fields of subobject fields.
 
-   structure B extends A where
-     y : Nat
+For example, consider the following structures:
+```
+structure A where
+  x : Nat
 
-   structure C extends B where
-     z : Bool
-   ```
-   This method expands parent structure fields using the path to the parent structure.
-   For example,
-   ```
-   { x := 0, y := 0, z := true : C }
-   ```
-   is expanded into
-   ```
-   { toB.toA.x := 0, toB.y := 0, z := true : C }
-   ```
+structure B extends A where
+  y : Nat
+
+structure C extends B where
+  z : Bool
+```
+This method expands parent structure fields using the path to the parent structure.
+For example,
+```
+{ x := 0, y := 0, z := true : C }
+```
+is expanded into
+```
+{ toB.toA.x := 0, toB.y := 0, z := true : C }
+```
 -/
-private def expandParentFields (s : Struct) : TermElabM Struct := do
+private def expandParentFields (s : StructInstView) : TermElabM StructInstView := do
   let env ← getEnv
   s.modifyFieldsM fun fields => fields.mapM fun field => do match field with
     | { lhs := .fieldName ref fieldName :: _,    .. } =>
@@ -448,6 +527,11 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
 
 private abbrev FieldMap := Std.HashMap Name Fields
 
+/--
+Creates a hash map collecting all fields with the same first name component.
+Throws an error if there are multiple simple fields with the same name.
+Used by `StructInst.expandStruct` processing.
+-/
 private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
   fields.foldlM (init := {}) fun fieldMap field =>
     match field.lhs with
@@ -461,15 +545,16 @@ private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
       | _ => return fieldMap.insert fieldName [field]
     | _ => unreachable!
 
-private def isSimpleField? : Fields → Option (Field Struct)
+/--
+Given a value of the hash map created by `mkFieldMap`, returns true if the value corresponds to a simple field.
+-/
+private def isSimpleField? : Fields → Option (Field StructInstView)
   | [field] => if field.isSimple then some field else none
   | _       => none
 
-private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName : Name) : TermElabM Nat := do
-  match fieldNames.findIdx? fun n => n == fieldName with
-  | some idx => return idx
-  | none     => throwError "field '{fieldName}' is not a valid field of '{structName}'"
-
+/--
+Creates projection notation for the given structure field. Used
+-/
 def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
   if (findField? (← getEnv) structName fieldName).isNone then
     return none
@@ -478,7 +563,10 @@ def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (
       #[mkAtomFrom s "@",
         mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]]
 
-def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
+/--
+Finds a simple field of the given name.
+-/
+def findField? (fields : Fields) (fieldName : Name) : Option (Field StructInstView) :=
   fields.find? fun field =>
     match field.lhs with
     | [.fieldName _ n] => n == fieldName
@@ -486,7 +574,10 @@ def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
 
 mutual
 
-  private partial def groupFields (s : Struct) : TermElabM Struct := do
+  /--
+  Groups compound fields according to which subobject they are from.
+  -/
+  private partial def groupFields (s : StructInstView) : TermElabM StructInstView := do
     let env ← getEnv
     withRef s.ref do
     s.modifyFieldsM fun fields => do
@@ -499,14 +590,14 @@ mutual
           let field := fields.head!
           match Lean.isSubobjectField? env s.structName fieldName with
           | some substructName =>
-            let substruct := Struct.mk s.ref substructName #[] substructFields s.source
+            let substruct := { ref := s.ref, structName := substructName, params := #[], fields := substructFields, sources := s.sources }
             let substruct ← expandStruct substruct
             pure { field with lhs := [field.lhs.head!], val := FieldVal.nested substruct }
           | none =>
             let updateSource (structStx : Syntax) : TermElabM Syntax := do
-              let sourcesNew ← s.source.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
+              let sourcesNew ← s.sources.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
               let explicitSourceStx := if sourcesNew.isEmpty then mkNullNode else mkSourcesWithSyntax sourcesNew
-              let implicitSourceStx := s.source.implicit.getD mkNullNode
+              let implicitSourceStx := s.sources.implicit.getD mkNullNode
               return (structStx.setArg 1 explicitSourceStx).setArg 3 implicitSourceStx
             let valStx := s.ref -- construct substructure syntax using s.ref as template
             let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
@@ -518,7 +609,7 @@ mutual
   Adds in the missing fields using the explicit sources.
   Invariant: a missing field always comes from the first source that can provide it.
   -/
-  private partial def addMissingFields (s : Struct) : TermElabM Struct := do
+  private partial def addMissingFields (s : StructInstView) : TermElabM StructInstView := do
     let env ← getEnv
     let fieldNames := getStructureFields env s.structName
     let ref := s.ref.mkSynthetic
@@ -527,7 +618,7 @@ mutual
         match findField? s.fields fieldName with
         | some field => return field::fields
         | none       =>
-          let addField (val : FieldVal Struct) : TermElabM Fields := do
+          let addField (val : FieldVal StructInstView) : TermElabM Fields := do
             return { ref, lhs := [FieldLHS.fieldName ref fieldName], val := val } :: fields
           match Lean.isSubobjectField? env s.structName fieldName with
           | some substructName =>
@@ -535,8 +626,8 @@ mutual
             let downFields := getStructureFieldsFlattened env substructName false
             -- Filter out all explicit sources that do not share a leaf field keeping
             -- structure with no fields
-            let filtered := s.source.explicit.filter fun source =>
-              let sourceFields := getStructureFieldsFlattened env source.structName false
+            let filtered := s.sources.explicit.filter fun sources =>
+              let sourceFields := getStructureFieldsFlattened env sources.structName false
               sourceFields.any (fun name => downFields.contains name) || sourceFields.isEmpty
             -- Take the first such one remaining
             match filtered[0]? with
@@ -550,27 +641,30 @@ mutual
               -- No sources could provide this subobject in the proper order.
               -- Recurse to handle default values for fields.
               else
-                let substruct := Struct.mk ref substructName #[] [] s.source
+                let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources }
                 let substruct ← expandStruct substruct
                 addField (FieldVal.nested substruct)
             -- No sources could provide this subobject.
             -- Recurse to handle default values for fields.
             | none =>
-              let substruct := Struct.mk ref substructName #[] [] s.source
+              let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources }
               let substruct ← expandStruct substruct
               addField (FieldVal.nested substruct)
           -- Since this is not a subobject field, we are free to use the first source that can
             -- provide it.
           | none =>
-            if let some val ← s.source.explicit.findSomeM? fun source => mkProjStx? source.stx source.structName fieldName then
+            if let some val ← s.sources.explicit.findSomeM? fun source => mkProjStx? source.stx source.structName fieldName then
               addField (FieldVal.term val)
-            else if s.source.implicit.isSome then
+            else if s.sources.implicit.isSome then
               addField (FieldVal.term (mkHole ref))
             else
               addField FieldVal.default
-      return s.setFields fields.reverse
+      return { s with fields := fields.reverse }
 
-  private partial def expandStruct (s : Struct) : TermElabM Struct := do
+  /--
+  Expands all fields of the structure instance, consolidates compound fields into subobject fields, and adds missing fields.
+  -/
+  private partial def expandStruct (s : StructInstView) : TermElabM StructInstView := do
     let s := expandCompositeFields s
     let s ← expandNumLitFields s
     let s ← expandParentFields s
@@ -579,10 +673,17 @@ mutual
 
 end
 
+/--
+The constructor to use for the structure instance notation.
+-/
 structure CtorHeaderResult where
+  /-- The constructor function with applied structure parameters. -/
   ctorFn     : Expr
+  /-- The type of `ctorFn` -/
   ctorFnType : Expr
+  /-- Instance metavariables for structure parameters that are instance implicit. -/
   instMVars  : Array MVarId
+  /-- Type parameter names and metavariables for each parameter. Used to seed `StructInstView.params`. -/
   params     : Array (Name × Expr)
 
 private def mkCtorHeaderAux : Nat → Expr → Expr → Array MVarId → Array (Name × Expr) → TermElabM CtorHeaderResult
@@ -604,6 +705,7 @@ private partial def getForallBody : Nat → Expr → Option Expr
   | _+1, _                => none
   | 0,   type             => type
 
+/-- Attempts to use the expected type to solve for structure parameters. -/
 private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? : Option Expr) : TermElabM Unit := do
   match expectedType? with
   | none              => return ()
@@ -614,6 +716,7 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType?
         unless typeBody.hasLooseBVars do
           discard <| isDefEq expectedType typeBody
 
+/-- Elaborates the structure constructor using the expected type, filling in all structure parameters. -/
 private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
   let us ← mkFreshLevelMVars ctorVal.levelParams.length
   let val  := Lean.mkConst ctorVal.name us
@@ -623,32 +726,43 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr
   synthesizeAppInstMVars r.instMVars r.ctorFn
   return r
 
+/-- Annotates an expression that it is a value for a missing field. -/
 def markDefaultMissing (e : Expr) : Expr :=
   mkAnnotation `structInstDefault e
 
+/-- If the expression has been annotated by `markDefaultMissing`, returns the unannotated expression. -/
 def defaultMissing? (e : Expr) : Option Expr :=
   annotation? `structInstDefault e
 
+/-- Throws "failed to elaborate field" error. -/
 def throwFailedToElabField {α} (fieldName : Name) (structName : Name) (msgData : MessageData) : TermElabM α :=
   throwError "failed to elaborate field '{fieldName}' of '{structName}, {msgData}"
 
-def trySynthStructInstance? (s : Struct) (expectedType : Expr) : TermElabM (Option Expr) := do
+/-- If the struct has all-missing fields, tries to synthesize the structure using typeclass inference. -/
+def trySynthStructInstance? (s : StructInstView) (expectedType : Expr) : TermElabM (Option Expr) := do
   if !s.allDefault then
     return none
   else
     try synthInstance? expectedType catch _ => return none
 
+/-- The result of elaborating a `StructInstView` structure instance view. -/
 structure ElabStructResult where
+  /-- The elaborated value. -/
   val       : Expr
-  struct    : Struct
+  /-- The modified `StructInstView` view after elaboration. -/
+  struct    : StructInstView
+  /-- Metavariables for instance implicit fields. These will be registered after default value propagation. -/
   instMVars : Array MVarId
 
-private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do
+/--
+Main elaborator for structure instances.
+-/
+private partial def elabStructInstView (s : StructInstView) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do
   let env ← getEnv
   let ctorVal := getStructureCtor env s.structName
   if isPrivateNameFromImportedModule env ctorVal.name then
     throwError "invalid \{...} notation, constructor for `{s.structName}` is marked as private"
-  -- We store the parameters at the resulting `Struct`. We use this information during default value propagation.
+  -- We store the parameters at the resulting `StructInstView`. We use this information during default value propagation.
   let { ctorFn, ctorFnType, params, .. } ← mkCtorHeader ctorVal expectedType?
   let (e, _, fields, instMVars) ← s.fields.foldlM (init := (ctorFn, ctorFnType, [], #[])) fun (e, type, fields, instMVars) field => do
     match field.lhs with
@@ -657,7 +771,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
       trace[Elab.struct] "elabStruct {field}, {type}"
       match type with
       | .forallE _ d b bi =>
-        let cont (val : Expr) (field : Field Struct) (instMVars := instMVars) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
+        let cont (val : Expr) (field : Field StructInstView) (instMVars := instMVars) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
           pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo {
             projName := s.structName.append fieldName, fieldName, lctx := (← getLCtx), val, stx := ref }
           let e     := mkApp e val
@@ -671,7 +785,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
           match (← trySynthStructInstance? s d) with
           | some val => cont val { field with val := FieldVal.term (mkHole field.ref) }
           | none     =>
-            let { val, struct := sNew, instMVars := instMVarsNew } ← elabStruct s (some d)
+            let { val, struct := sNew, instMVars := instMVarsNew } ← elabStructInstView s (some d)
             let val ← ensureHasType d val
             cont val { field with val := FieldVal.nested sNew } (instMVars ++ instMVarsNew)
         | .default  =>
@@ -700,17 +814,21 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
               cont (markDefaultMissing val) field
       | _ => withRef field.ref <| throwFailedToElabField fieldName s.structName m!"unexpected constructor type{indentExpr type}"
     | _ => throwErrorAt field.ref "unexpected unexpanded structure field"
-  return { val := e, struct := s.setFields fields.reverse |>.setParams params, instMVars }
+  return { val := e, struct := { s with fields := fields.reverse, params }, instMVars }
 
 namespace DefaultFields
 
+/--
+Context for default value propagation.
+-/
 structure Context where
-  -- We must search for default values overridden in derived structures
-  structs : Array Struct := #[]
+  /-- The current path through `.nested` subobject structures. We must search for default values overridden in derived structures. -/
+  structs : Array StructInstView := #[]
+  /-- The collection of structures that could provide a default value. -/
   allStructNames : Array Name := #[]
   /--
   Consider the following example:
-  ```
+  ```lean
   structure A where
     x : Nat := 1
 
@@ -736,22 +854,29 @@ structure Context where
   -/
   maxDistance : Nat := 0
 
+/--
+State for default value propagation
+-/
 structure State where
+  /-- Whether progress has been made so far on this round of the propagation loop. -/
   progress : Bool := false
 
-partial def collectStructNames (struct : Struct) (names : Array Name) : Array Name :=
+/-- Collects all structures that may provide default values for fields. -/
+partial def collectStructNames (struct : StructInstView) (names : Array Name) : Array Name :=
   let names := names.push struct.structName
   struct.fields.foldl (init := names) fun names field =>
     match field.val with
     | .nested struct => collectStructNames struct names
     | _ => names
 
-partial def getHierarchyDepth (struct : Struct) : Nat :=
+/-- Gets the maximum nesting depth of subobjects. -/
+partial def getHierarchyDepth (struct : StructInstView) : Nat :=
   struct.fields.foldl (init := 0) fun max field =>
     match field.val with
     | .nested struct => Nat.max max (getHierarchyDepth struct + 1)
     | _ => max
 
+/-- Returns whether the field is still missing. -/
 def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool := do
   if let some expr := field.expr? then
     if let some (.mvar mvarId) := defaultMissing? expr then
@@ -759,40 +884,51 @@ def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool :=
         return true
   return false
 
-partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : Struct) : m (Option (Field Struct)) :=
+/-- Returns a field that is still missing. -/
+partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Option (Field StructInstView)) :=
   struct.fields.findSomeM? fun field => do
    match field.val with
    | .nested struct => findDefaultMissing? struct
    | _ => return if (← isDefaultMissing? field) then field else none
 
-partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : Struct) : m (Array (Field Struct)) :=
+/-- Returns all fields that are still missing. -/
+partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Array (Field StructInstView)) :=
   go struct *> get |>.run' #[]
 where
-  go (struct : Struct) : StateT (Array (Field Struct)) m Unit :=
+  go (struct : StructInstView) : StateT (Array (Field StructInstView)) m Unit :=
     for field in struct.fields do
       if let .nested struct := field.val then
         go struct
       else if (← isDefaultMissing? field) then
         modify (·.push field)
 
-def getFieldName (field : Field Struct) : Name :=
+/-- Returns the name of the field. Assumes all fields under consideration are simple and named. -/
+def getFieldName (field : Field StructInstView) : Name :=
   match field.lhs with
   | [.fieldName _ fieldName] => fieldName
   | _ => unreachable!
 
 abbrev M := ReaderT Context (StateRefT State TermElabM)
 
+/-- Returns whether we should interrupt the round because we have made progress allowing nonzero depth. -/
 def isRoundDone : M Bool := do
   return (← get).progress && (← read).maxDistance > 0
 
-def getFieldValue? (struct : Struct) (fieldName : Name) : Option Expr :=
+/-- Returns the `expr?` for the given field. -/
+def getFieldValue? (struct : StructInstView) (fieldName : Name) : Option Expr :=
   struct.fields.findSome? fun field =>
     if getFieldName field == fieldName then
       field.expr?
     else
       none
 
-partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Expr)
+/-- Instantiates a default value from the given default value declaration, if applicable. -/
+partial def mkDefaultValue? (struct : StructInstView) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
+  withRef struct.ref do
+  let us ← mkFreshLevelMVarsFor cinfo
+  process (← instantiateValueLevelParams cinfo us)
+where
+  process : Expr → TermElabM (Option Expr)
   | .lam n d b c => withRef struct.ref do
     if c.isExplicit then
       let fieldName := n
@@ -801,29 +937,26 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
       | some val =>
         let valType ← inferType val
         if (← isDefEq valType d) then
-          mkDefaultValueAux? struct (b.instantiate1 val)
+          process (b.instantiate1 val)
         else
           return none
     else
       if let some (_, param) := struct.params.find? fun (paramName, _) => paramName == n then
         -- Recall that we did not use to have support for parameter propagation here.
         if (← isDefEq (← inferType param) d) then
-          mkDefaultValueAux? struct (b.instantiate1 param)
+          process (b.instantiate1 param)
         else
           return none
       else
         let arg ← mkFreshExprMVar d
-        mkDefaultValueAux? struct (b.instantiate1 arg)
+        process (b.instantiate1 arg)
   | e =>
     let_expr id _ a := e | return some e
     return some a
 
-def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
-  withRef struct.ref do
-  let us ← mkFreshLevelMVarsFor cinfo
-  mkDefaultValueAux? struct (← instantiateValueLevelParams cinfo us)
-
-/-- Reduce default value. It performs beta reduction and projections of the given structures. -/
+/--
+Reduces a default value. It performs beta reduction and projections of the given structures to reduce them to the provided values for fields.
+-/
 partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
   match e with
   | .forallE ..   =>
@@ -880,12 +1013,15 @@ where
     else
       k
 
-partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
+/--
+Attempts to synthesize a default value for a missing field `fieldName` using default values from each structure in `structs`.
+-/
+def tryToSynthesizeDefault (structs : Array StructInstView) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
   let rec loop (i : Nat) (dist : Nat) := do
     if dist > maxDistance then
       return false
     else if h : i < structs.size then
-      let struct := structs.get ⟨i, h⟩
+      let struct := structs[i]
       match getDefaultFnForField? (← getEnv) struct.structName fieldName with
       | some defFn =>
         let cinfo ← getConstInfo defFn
@@ -900,14 +1036,25 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
           | none   =>
             let mvarDecl ← getMVarDecl mvarId
             let val ← ensureHasType mvarDecl.type val
-            mvarId.assign val
-            return true
+            /-
+            We must use `checkedAssign` here to ensure we do not create a cyclic
+            assignment. See #3150.
+            This can happen when there are holes in the the fields the default value
+            depends on.
+            Possible improvement: create a new `_` instead of returning `false` when
+            `checkedAssign` fails. Reason: the field will not be needed after the
+            other `_` are resolved by the user.
+            -/
+            mvarId.checkedAssign val
       | _ => loop (i+1) dist
     else
       return false
   loop 0 0
 
-partial def step (struct : Struct) : M Unit :=
+/--
+Performs one step of default value synthesis.
+-/
+partial def step (struct : StructInstView) : M Unit :=
   unless (← isRoundDone) do
     withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do
       for field in struct.fields do
@@ -924,7 +1071,10 @@ partial def step (struct : Struct) : M Unit :=
                   modify fun _ => { progress := true }
             | _ => pure ()
 
-partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M Unit := do
+/--
+Main entry point to default value synthesis in the `M` monad.
+-/
+partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : StructInstView) : M Unit := do
   match (← findDefaultMissing? struct) with
   | none       => return () -- Done
   | some field =>
@@ -947,16 +1097,22 @@ partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M
       else
         propagateLoop hierarchyDepth (d+1) struct
 
-def propagate (struct : Struct) : TermElabM Unit :=
+/--
+Synthesizes default values for all missing fields, if possible.
+-/
+def propagate (struct : StructInstView) : TermElabM Unit :=
   let hierarchyDepth := getHierarchyDepth struct
   let structNames := collectStructNames struct #[]
   propagateLoop hierarchyDepth 0 struct { allStructNames := structNames } |>.run' {}
 
 end DefaultFields
 
-private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source) : TermElabM Expr := do
-  let structName ← getStructName expectedType? source
-  let struct ← liftMacroM <| mkStructView stx structName source
+/--
+Main entry point to elaborator for structure instance notation, unless the structure instance is a modifyOp.
+-/
+private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sources : SourcesView) : TermElabM Expr := do
+  let structName ← getStructName expectedType? sources
+  let struct ← liftMacroM <| mkStructView stx structName sources
   let struct ← expandStruct struct
   trace[Elab.struct] "{struct}"
   /- We try to synthesize pending problems with `withSynthesize` combinator before trying to use default values.
@@ -974,7 +1130,7 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
 
      TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior.
   -/
-  let { val := r, struct, instMVars } ← withSynthesize (postpone := .yes) <| elabStruct struct expectedType?
+  let { val := r, struct, instMVars } ← withSynthesize (postpone := .yes) <| elabStructInstView struct expectedType?
   trace[Elab.struct] "before propagate {r}"
   DefaultFields.propagate struct
   synthesizeAppInstMVars instMVars r
@@ -984,13 +1140,13 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
   match (← expandNonAtomicExplicitSources stx) with
   | some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   | none =>
-    let sourceView ← getStructSource stx
+    let sourcesView ← getStructSources stx
     if let some modifyOp ← isModifyOp? stx then
-      if sourceView.explicit.isEmpty then
+      if sourcesView.explicit.isEmpty then
         throwError "invalid \{...} notation, explicit source is required when using '[<index>] := <value>'"
-      elabModifyOp stx modifyOp sourceView.explicit expectedType?
+      elabModifyOp stx modifyOp sourcesView.explicit expectedType?
     else
-      elabStructInstAux stx expectedType? sourceView
+      elabStructInstAux stx expectedType? sourcesView
 
 builtin_initialize
   registerTraceClass `Elab.struct

src/Lean/Elab/Structure.lean

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

src/Lean/Elab/Syntax.lean

@@ -233,11 +233,15 @@ where
     return (← `((with_annotate_term $(stx[0]) @ParserDescr.sepBy1) $p $sep $psep $(quote allowTrailingSep)), 1)
 
   isValidAtom (s : String) : Bool :=
+    -- Pretty-printing instructions shouldn't affect validity
+    let s := s.trim
     !s.isEmpty &&
-    s.front != '\'' &&
+    (s.front != '\'' || "''".isPrefixOf s) &&
     s.front != '\"' &&
+    !(isIdBeginEscape s.front) &&
     !(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (s.get ⟨1⟩) || isIdBeginEscape (s.get ⟨1⟩))) &&
-    !s.front.isDigit
+    !s.front.isDigit &&
+    !(s.any Char.isWhitespace)
 
   processAtom (stx : Syntax) := do
     match stx[0].isStrLit? with

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

@@ -163,7 +163,9 @@ builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofN
 A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
 the goal fully, indicated by returning `none`.
 -/
-abbrev Pass := MVarId → MetaM (Option MVarId)
+structure Pass where
+  name : Name
+  run : MVarId → MetaM (Option MVarId)
 
 namespace Pass
 
@@ -174,7 +176,8 @@ the goal anymore.
 partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Option MVarId) := do
   let runPass (goal? : Option MVarId) (pass : Pass) : MetaM (Option MVarId) := do
     let some goal := goal? | return none
-    pass goal
+    withTraceNode `bv (fun _ => return s!"Running pass: {pass.name}") do
+      pass.run goal
 
   let some newGoal := ← passes.foldlM (init := some goal) runPass | return none
   if goal != newGoal then
@@ -187,83 +190,156 @@ partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Optio
 /--
 Responsible for applying the Bitwuzla style rewrite rules.
 -/
-def rewriteRulesPass (maxSteps : Nat) : Pass := fun goal => do
-  let bvThms ← bvNormalizeExt.getTheorems
-  let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
-  let sevalThms ← getSEvalTheorems
-  let sevalSimprocs ← Simp.getSEvalSimprocs
+def rewriteRulesPass (maxSteps : Nat) : Pass where
+  name := `rewriteRules
+  run goal := do
+    let bvThms ← bvNormalizeExt.getTheorems
+    let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
+    let sevalThms ← getSEvalTheorems
+    let sevalSimprocs ← Simp.getSEvalSimprocs
 
-  let simpCtx : Simp.Context := {
-    config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
-    simpTheorems := #[bvThms, sevalThms]
-    congrTheorems := (← getSimpCongrTheorems)
-  }
+    let simpCtx ← Simp.mkContext
+      (config := { failIfUnchanged := false, zetaDelta := true, maxSteps })
+      (simpTheorems := #[bvThms, sevalThms])
+      (congrTheorems := (← getSimpCongrTheorems))
 
-  let hyps ← goal.getNondepPropHyps
-  let ⟨result?, _⟩ ← simpGoal goal
-    (ctx := simpCtx)
-    (simprocs := #[bvSimprocs, sevalSimprocs])
-    (fvarIdsToSimp := hyps)
-  let some (_, newGoal) := result? | return none
-  return newGoal
-
-/--
-Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
-them to substitute occurences of `x` within other hypotheses
--/
-def embeddedConstraintPass (maxSteps : Nat) : 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, maxSteps }
-      simpTheorems := relevantHyps
-      congrTheorems := (← getSimpCongrTheorems)
-    }
-
-    let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps)
+    let ⟨result?, _⟩ ← simpGoal goal
+      (ctx := simpCtx)
+      (simprocs := #[bvSimprocs, sevalSimprocs])
+      (fvarIdsToSimp := hyps)
     let some (_, newGoal) := result? | return none
     return newGoal
 
 /--
-Normalize with respect to Associativity and Commutativity.
+Flatten out ands. That is look for hypotheses of the form `h : (x && y) = true` and replace them
+with `h.left : x = true` and `h.right : y = true`. This can enable more fine grained substitutions
+in embedded constraint substitution.
 -/
-def acNormalizePass : Pass := fun goal => do
-  let mut newGoal := goal
-  for hyp in (← goal.getNondepPropHyps) do
-    let result ← Lean.Meta.AC.acNfHypMeta newGoal hyp
+partial def andFlatteningPass : Pass where
+  name := `andFlattening
+  run goal := do
+    goal.withContext do
+      let hyps ← goal.getNondepPropHyps
+      let mut newHyps := #[]
+      let mut oldHyps := #[]
+      for fvar in hyps do
+        let hyp : Hypothesis := {
+          userName := (← fvar.getDecl).userName
+          type := ← fvar.getType
+          value := mkFVar fvar
+        }
+        let sizeBefore := newHyps.size
+        newHyps ← splitAnds hyp newHyps
+        if newHyps.size > sizeBefore then
+          oldHyps := oldHyps.push fvar
+      if newHyps.size == 0 then
+        return goal
+      else
+        let (_, goal) ← goal.assertHypotheses newHyps
+        -- Given that we collected the hypotheses in the correct order above the invariant is given
+        let goal ← goal.tryClearMany oldHyps
+        return goal
+where
+  splitAnds (hyp : Hypothesis) (hyps : Array Hypothesis) (first : Bool := true) :
+      MetaM (Array Hypothesis) := do
+    match ← trySplit hyp with
+    | some (left, right) =>
+      let hyps ← splitAnds left hyps false
+      splitAnds right hyps false
+    | none =>
+      if first then
+        return hyps
+      else
+        return hyps.push hyp
 
-    if let .some nextGoal := result then
-      newGoal := nextGoal
-    else
-      return none
-
-  return newGoal
+  trySplit (hyp : Hypothesis) : MetaM (Option (Hypothesis × Hypothesis)) := do
+    let typ := hyp.type
+    let_expr Eq α eqLhs eqRhs := typ | return none
+    let_expr Bool.and lhs rhs := eqLhs | return none
+    let_expr Bool.true := eqRhs | return none
+    let_expr Bool := α | return none
+    let mkEqTrue (lhs : Expr) : Expr :=
+      mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) lhs (mkConst ``Bool.true)
+    let leftHyp : Hypothesis := {
+      userName := hyp.userName,
+      type := mkEqTrue lhs,
+      value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_left) lhs rhs hyp.value
+    }
+    let rightHyp : Hypothesis := {
+      userName := hyp.userName,
+      type := mkEqTrue rhs,
+      value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_right) lhs rhs hyp.value
+    }
+    return some (leftHyp, rightHyp)
 
 /--
-The normalization passes used by `bv_normalize` and thus `bv_decide`.
+Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
+them to substitute occurences of `x` within other hypotheses. Additionally this drops all
+redundant top level hypotheses.
 -/
-def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
-  [
-    rewriteRulesPass cfg.maxSteps,
-    embeddedConstraintPass cfg.maxSteps
-  ]
+def embeddedConstraintPass (maxSteps : Nat) : Pass where
+  name := `embeddedConstraintSubsitution
+  run goal := do
+    goal.withContext do
+      let hyps ← goal.getNondepPropHyps
+      let mut relevantHyps : SimpTheoremsArray := #[]
+      let mut seen : Std.HashSet Expr := {}
+      let mut duplicates : Array FVarId := #[]
+      for hyp in hyps do
+        let typ ← hyp.getType
+        let_expr Eq α lhs rhs := typ | continue
+        let_expr Bool.true := rhs | continue
+        let_expr Bool := α | continue
+        if seen.contains lhs then
+          -- collect and later remove duplicates on the fly
+          duplicates := duplicates.push hyp
+        else
+          seen := seen.insert lhs
+          let localDecl ← hyp.getDecl
+          let proof  := localDecl.toExpr
+          relevantHyps ← relevantHyps.addTheorem (.fvar hyp) proof
+
+      let goal ← goal.tryClearMany duplicates
+
+      let simpCtx ← Simp.mkContext
+        (config := { failIfUnchanged := false, maxSteps })
+        (simpTheorems := relevantHyps)
+        (congrTheorems := (← getSimpCongrTheorems))
+
+      let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := ← goal.getNondepPropHyps)
+      let some (_, newGoal) := result? | return none
+      return newGoal
+
+/--
+Normalize with respect to Associativity and Commutativity.
+-/
+def acNormalizePass : Pass where
+  name := `ac_nf
+  run goal := do
+    let mut newGoal := goal
+    for hyp in (← goal.getNondepPropHyps) do
+      let result ← Lean.Meta.AC.acNfHypMeta newGoal hyp
+
+      if let .some nextGoal := result then
+        newGoal := nextGoal
+      else
+        return none
+
+    return newGoal
 
 def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
-  let mut passPipeline := defaultPipeline cfg
+  let mut passPipeline := [rewriteRulesPass cfg.maxSteps]
 
   if cfg.acNf then
     passPipeline := passPipeline ++ [acNormalizePass]
 
+  if cfg.andFlattening then
+    passPipeline := passPipeline ++ [andFlatteningPass]
+
+  if cfg.embeddedConstraintSubst then
+    passPipeline := passPipeline ++ [embeddedConstraintPass cfg.maxSteps]
+
   return passPipeline
 
 end Pass

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -308,7 +308,7 @@ def evalTacticSeq : Tactic :=
 
 partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   if h : i < tactics.size then
-    let tactic := tactics.get ⟨i, h⟩
+    let tactic := tactics[i]
     catchInternalId unsupportedSyntaxExceptionId
       (evalTactic tactic)
       (fun _ => evalChoiceAux tactics (i+1))

src/Lean/Elab/Tactic/Change.lean

@@ -13,6 +13,31 @@ open Meta
 # Implementation of the `change` tactic
 -/
 
+/--
+Elaborates the pattern `p` and ensures that it is defeq to `e`.
+Emulates `(show p from ?m : e)`, returning the type of `?m`, but `e` and `p` do not need to be types.
+Unlike `(show p from ?m : e)`, this can assign synthetic opaque metavariables appearing in `p`.
+-/
+def elabChange (e : Expr) (p : Term) : TacticM Expr := do
+  let p ← runTermElab do
+    let p ← Term.elabTermEnsuringType p (← inferType e)
+    unless ← isDefEq p e do
+      /-
+      Sometimes isDefEq can fail due to postponed elaboration problems.
+      We synthesize pending synthetic mvars while allowing typeclass instances to be postponed,
+      which might enable solving for them with an additional `isDefEq`.
+      -/
+      Term.synthesizeSyntheticMVars (postpone := .partial)
+      discard <| isDefEq p e
+    pure p
+  withAssignableSyntheticOpaque do
+    unless ← isDefEq p e do
+      let (p, tgt) ← addPPExplicitToExposeDiff p e
+      throwError "\
+        'change' tactic failed, pattern{indentExpr p}\n\
+        is not definitionally equal to target{indentExpr tgt}"
+    instantiateMVars p
+
 /-- `change` can be used to replace the main goal or its hypotheses with
 different, yet definitionally equal, goal or hypotheses.
 
@@ -38,15 +63,13 @@ the main goal. -/
   | `(tactic| change $newType:term $[$loc:location]?) => do
     withLocation (expandOptLocation (Lean.mkOptionalNode loc))
       (atLocal := fun h => do
-        let hTy ← h.getType
-        -- This is a hack to get the new type to elaborate in the same sort of way that
-        -- it would for a `show` expression for the goal.
-        let mvar ← mkFreshExprMVar none
-        let (_, mvars) ← elabTermWithHoles
-                          (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
+        let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChange (← h.getType) newType) (← getMainTag) `change
         liftMetaTactic fun mvarId => do
-          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
-      (atTarget := evalTactic <| ← `(tactic| refine_lift show $newType from ?_))
-      (failed := fun _ => throwError "change tactic failed")
+          return (← mvarId.changeLocalDecl h hTy') :: mvars)
+      (atTarget := do
+        let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChange (← getMainTarget) newType) (← getMainTag) `change
+        liftMetaTactic fun mvarId => do
+          return (← mvarId.replaceTargetDefEq tgt') :: mvars)
+      (failed := fun _ => throwError "'change' tactic failed")
 
 end Lean.Elab.Tactic

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.Conv.Basic
 
 namespace Lean.Elab.Tactic.Conv
@@ -15,11 +16,9 @@ open Meta
   | `(conv| change $e) => withMainContext do
     let lhs ← getLhs
     let mvarCounterSaved := (← getMCtx).mvarCounter
-    let r ← elabTermEnsuringType e (← inferType lhs)
-    logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-    unless (← isDefEqGuarded r lhs) do
-      throwError "invalid 'change' conv tactic, term{indentExpr r}\nis not definitionally equal to current left-hand-side{indentExpr lhs}"
-    changeLhs r
+    let lhs' ← elabChange lhs e
+    logUnassignedAndAbort (← filterOldMVars (← getMVars lhs') mvarCounterSaved)
+    changeLhs lhs'
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Conv

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

@@ -12,11 +12,10 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 private def getContext : MetaM Simp.Context := do
-  return {
-    simpTheorems  := {}
-    congrTheorems := (← getSimpCongrTheorems)
-    config        := Simp.neutralConfig
-  }
+  Simp.mkContext
+    (simpTheorems  := {})
+    (congrTheorems := (← getSimpCongrTheorems))
+    (config        := Simp.neutralConfig)
 
 partial def matchPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Option (Expr × Array Expr)) :=
   withNewMCtxDepth do
@@ -126,7 +125,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         pure (.occs #[] 0 ids.toList)
       | _ => throwUnsupportedSyntax
     let state ← IO.mkRef occs
-    let ctx := { ← getContext with config.memoize := occs matches .all _ }
+    let ctx := (← getContext).setMemoize (occs matches .all _)
     let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state })
     let subgoals ← match ← state.get with
     | .all #[] | .occs _ 0 _ =>

src/Lean/Elab/Tactic/DiscrTreeKey.lean

@@ -18,21 +18,22 @@ private def mkKey (e : Expr) (simp : Bool) : MetaM (Array Key) := do
   let (_, _, type) ← withReducible <| forallMetaTelescopeReducing e
   let type ← whnfR type
   if simp then
-    if let some (_, lhs, _) := type.eq? then
-      mkPath lhs simpDtConfig
-    else if let some (lhs, _) := type.iff? then
-      mkPath lhs simpDtConfig
-    else if let some (_, lhs, _) := type.ne? then
-      mkPath lhs simpDtConfig
-    else if let some p := type.not? then
-      match p.eq? with
-      | some (_, lhs, _) =>
-        mkPath lhs simpDtConfig
-      | _ => mkPath p simpDtConfig
-    else
-      mkPath type simpDtConfig
+    withSimpGlobalConfig do
+      if let some (_, lhs, _) := type.eq? then
+        mkPath lhs
+      else if let some (lhs, _) := type.iff? then
+        mkPath lhs
+      else if let some (_, lhs, _) := type.ne? then
+        mkPath lhs
+      else if let some p := type.not? then
+        match p.eq? with
+        | some (_, lhs, _) =>
+          mkPath lhs
+        | _ => mkPath p
+      else
+        mkPath type
   else
-    mkPath type {}
+    mkPath type
 
 private def getType (t : TSyntax `term) : TermElabM Expr := do
   if let `($id:ident) := t then

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -542,11 +542,6 @@ declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
   let cfg ← elabDecideConfig stx[1]
   evalDecideCore `decide cfg
 
-@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  let cfg := { cfg with kernel := true }
-  evalDecideCore `decide! cfg
-
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
   let cfg ← elabDecideConfig stx[1]
   let cfg := { cfg with native := true }

src/Lean/Elab/Tactic/Ext.lean

@@ -195,9 +195,6 @@ structure ExtTheorems where
   erased  : PHashSet Name := {}
   deriving Inhabited
 
-/-- Discrimation tree settings for the `ext` extension. -/
-def extExt.config : WhnfCoreConfig := {}
-
 /-- The environment extension to track `@[ext]` theorems. -/
 builtin_initialize extExtension :
     SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
@@ -211,7 +208,7 @@ builtin_initialize extExtension :
 ordered from high priority to low. -/
 @[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
   let extTheorems := extExtension.getState (← getEnv)
-  let arr ← extTheorems.tree.getMatch ty extExt.config
+  let arr ← extTheorems.tree.getMatch ty
   let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
   -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
   -- Most ext theorems have default priority.
@@ -258,7 +255,7 @@ builtin_initialize registerBuiltinAttribute {
       but this theorem proves{indentD declTy}"
     let some (ty, lhs, rhs) := declTy.eq? | failNotEq
     unless lhs.isMVar && rhs.isMVar do failNotEq
-    let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
+    let keys ← withReducible <| DiscrTree.mkPath ty
     let priority ← liftCommandElabM <| Elab.liftMacroM do evalPrio (prio.getD (← `(prio| default)))
     extExtension.add {declName, keys, priority} kind
     -- Realize iff theorem

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -40,7 +40,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
     | some suggestions =>
       if requireClose then throwError
         "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
-      reportOutOfHeartbeats `library_search ref
+      reportOutOfHeartbeats `apply? ref
       for (_, suggestionMCtx) in suggestions do
         withMCtx suggestionMCtx do
           addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)

src/Lean/Elab/Tactic/NormCast.lean

@@ -28,8 +28,10 @@ def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) :=
     unless ← isDefEq a'.expr b'.expr do return none
     a'.mkEqTrans (← b'.mkEqSymm b)
   withReducible do
-    (go (← Simp.mkDefaultMethods).toMethodsRef
-      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
+    let ctx ← Simp.mkContext
+        (simpTheorems := #[s])
+        (congrTheorems := ← Meta.getSimpCongrTheorems)
+    (go (← Simp.mkDefaultMethods).toMethodsRef ctx).run' {}
 
 /-- Proves `a = b` by simplifying using move and squash lemmas. -/
 def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
@@ -191,19 +193,25 @@ def derive (e : Expr) : MetaM Simp.Result := do
   -- step 1: pre-processing of numerals
   let r ← withTrace "pre-processing numerals" do
     let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
-    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
+    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
 
   -- step 2: casts are moved upwards and eliminated
   let r ← withTrace "moving upward, splitting and eliminating" do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
-    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
+    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
 
   let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
 
   -- step 3: casts are squashed
   let r ← withTrace "squashing" do
     let simpTheorems := #[← normCastExt.squash.getTheorems]
-    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems } simprocs).1
+    let ctx ← Simp.mkContext
+      (config := config)
+      (simpTheorems := simpTheorems)
+      (congrTheorems := congrTheorems)
+    r.mkEqTrans (← simp r.expr ctx simprocs).1
 
   return r
 
@@ -263,7 +271,7 @@ def evalConvNormCast : Tactic :=
 def evalPushCast : Tactic := fun stx => do
   let { ctx, simprocs, dischargeWrapper } ← withMainContext do
     mkSimpContext (simpTheorems := pushCastExt.getTheorems) stx (eraseLocal := false)
-  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
+  let ctx := ctx.setFailIfUnchanged false
   dischargeWrapper.with fun discharge? =>
     discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
 

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

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
-import Lean.Meta.Tactic.Cases
 import Lean.Elab.Tactic.Config
 
 /-!
@@ -520,23 +519,6 @@ partial def processFacts (p : MetaProblem) : OmegaM (MetaProblem × Nat) := do
 
 end MetaProblem
 
-/--
-Given `p : P ∨ Q` (or any inductive type with two one-argument constructors),
-split the goal into two subgoals:
-one containing the hypothesis `h : P` and another containing `h : Q`.
--/
-def cases₂ (mvarId : MVarId) (p : Expr) (hName : Name := `h) :
-    MetaM ((MVarId × FVarId) × (MVarId × FVarId)) := do
-  let mvarId ← mvarId.assert `hByCases (← inferType p) p
-  let (fvarId, mvarId) ← mvarId.intro1
-  let #[s₁, s₂] ← mvarId.cases fvarId #[{ varNames := [hName] }, { varNames := [hName] }] |
-    throwError "'cases' tactic failed, unexpected number of subgoals"
-  let #[Expr.fvar f₁ ..] ← pure s₁.fields
-    | throwError "'cases' tactic failed, unexpected new hypothesis"
-  let #[Expr.fvar f₂ ..] ← pure s₂.fields
-    | throwError "'cases' tactic failed, unexpected new hypothesis"
-  return ((s₁.mvarId, f₁), (s₂.mvarId, f₂))
-
 /--
 Helpful error message when omega cannot find a solution
 -/
@@ -628,33 +610,36 @@ mutual
 Split a disjunction in a `MetaProblem`, and if we find a new usable fact
 call `omegaImpl` in both branches.
 -/
-partial def splitDisjunction (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do
+partial def splitDisjunction (m : MetaProblem) : OmegaM Expr := do
   match m.disjunctions with
     | [] => throwError "omega could not prove the goal:\n{← formatErrorMessage m.problem}"
-    | h :: t =>
-      trace[omega] "Case splitting on {← inferType h}"
-      let ctx ← getMCtx
-      let (⟨g₁, h₁⟩, ⟨g₂, h₂⟩) ← cases₂ g h
-      trace[omega] "Adding facts:\n{← g₁.withContext <| inferType (.fvar h₁)}"
-      let m₁ := { m with facts := [.fvar h₁], disjunctions := t }
-      let r ← withoutModifyingState do
-        let (m₁, n) ← g₁.withContext m₁.processFacts
+    | h :: t => do
+      let hType ← whnfD (← inferType h)
+      trace[omega] "Case splitting on {hType}"
+      let_expr Or hType₁ hType₂ := hType | throwError "Unexpected disjunction {hType}"
+      let p?₁ ← withoutModifyingState do withLocalDeclD `h₁ hType₁ fun h₁ => do
+        withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₁}") do
+        let m₁ := { m with facts := [h₁], disjunctions := t }
+        let (m₁, n) ← m₁.processFacts
         if 0 < n then
-          omegaImpl m₁ g₁
-          pure true
+          let p₁ ← omegaImpl m₁
+          let p₁ ← mkLambdaFVars #[h₁] p₁
+          return some p₁
         else
-          pure false
-      if r then
-        trace[omega] "Adding facts:\n{← g₂.withContext <| inferType (.fvar h₂)}"
-        let m₂ := { m with facts := [.fvar h₂], disjunctions := t }
-        omegaImpl m₂ g₂
+          return none
+      if let some p₁ := p?₁ then
+         withLocalDeclD `h₂ hType₂ fun h₂ => do
+          withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₂}") do
+          let m₂ := { m with facts := [h₂], disjunctions := t }
+          let p₂ ← omegaImpl m₂
+          let p₂ ← mkLambdaFVars #[h₂] p₂
+          return mkApp6 (mkConst ``Or.elim) hType₁ hType₂ (mkConst ``False) h p₁ p₂
       else
         trace[omega] "No new facts found."
-        setMCtx ctx
-        splitDisjunction { m with disjunctions := t } g
+        splitDisjunction { m with disjunctions := t }
 
 /-- Implementation of the `omega` algorithm, and handling disjunctions. -/
-partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do
+partial def omegaImpl (m : MetaProblem) : OmegaM Expr := do
   let (m, _) ← m.processFacts
   guard m.facts.isEmpty
   let p := m.problem
@@ -663,12 +648,12 @@ partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withCont
   trace[omega] "After elimination:\nAtoms: {← atomsList}\n{p'}"
   match p'.possible, p'.proveFalse?, p'.proveFalse?_spec with
   | true, _, _ =>
-    splitDisjunction m g
+    splitDisjunction m
   | false, .some prf, _ =>
     trace[omega] "Justification:\n{p'.explanation?.get}"
     let prf ← instantiateMVars (← prf)
     trace[omega] "omega found a contradiction, proving {← inferType prf}"
-    g.assign prf
+    return prf
 
 end
 
@@ -677,7 +662,9 @@ Given a collection of facts, try prove `False` using the omega algorithm,
 and close the goal using that.
 -/
 def omega (facts : List Expr) (g : MVarId) (cfg : OmegaConfig := {}) : MetaM Unit :=
-  OmegaM.run (omegaImpl { facts } g) cfg
+  g.withContext do
+    let prf ← OmegaM.run (omegaImpl { facts }) cfg
+    g.assign prf
 
 open Lean Elab Tactic Parser.Tactic
 

src/Lean/Elab/Tactic/RCases.lean

@@ -526,7 +526,7 @@ where
   /-- Runs `rintroContinue` on `pats[i:]` -/
   loop i g fs clears a := do
     if h : i < pats.size then
-      rintroCore g fs clears a ref (pats.get ⟨i, h⟩) ty? (loop (i+1))
+      rintroCore g fs clears a ref pats[i] ty? (loop (i+1))
     else cont g fs clears a
 
 end

src/Lean/Elab/Tactic/Simp.lean

@@ -91,7 +91,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Co
   | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
   | .dsimp   => return { (← elabDSimpConfigCore optConfig) with }
 
-private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
+private def addDeclToUnfoldOrTheorem (config : Meta.ConfigWithKey) (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
   if e.isConst then
     let declName := e.constName!
     let info ← getConstInfo declName
@@ -108,7 +108,7 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     let fvarId := e.fvarId!
     let decl ← fvarId.getDecl
     if (← isProp decl.type) then
-      thms.add id #[] e (post := post) (inv := inv)
+      thms.add id #[] e (post := post) (inv := inv) (config := config)
     else if !decl.isLet then
       throwError "invalid argument, variable is not a proposition or let-declaration"
     else if inv then
@@ -116,9 +116,9 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     else
       return thms.addLetDeclToUnfold fvarId
   else
-    thms.add id #[] e (post := post) (inv := inv)
+    thms.add id #[] e (post := post) (inv := inv) (config := config)
 
-private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
+private def addSimpTheorem (config : Meta.ConfigWithKey) (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
   let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
@@ -132,7 +132,7 @@ private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (p
     else
       return some (#[], e)
   if let some (levelParams, proof) := thm? then
-    thms.add id levelParams proof (post := post) (inv := inv)
+    thms.add id levelParams proof (post := post) (inv := inv) (config := config)
   else
     return thms
 
@@ -212,7 +212,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             match (← resolveSimpIdTheorem? term) with
             | .expr e  =>
               let name ← mkFreshId
-              thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
+              thms ← addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
             | .simproc declName =>
               simprocs ← simprocs.add declName post
             | .ext (some ext₁) (some ext₂) _ =>
@@ -224,7 +224,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
               simprocs  := simprocs.push (← ext₂.getSimprocs)
             | .none    =>
               let name ← mkFreshId
-              thms ← addSimpTheorem thms (.stx name arg) term post inv
+              thms ← addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
           else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
             starArg := true
           else
@@ -234,7 +234,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             logException ex
           else
             throw ex
-      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
+      return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
     -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
     -- This affects `addSimpTheorem`.
     if (← read).recover then
@@ -311,10 +311,11 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     simpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
-    config      := (← elabSimpConfig stx[1] (kind := kind))
-    simpTheorems := #[simpTheorems], congrTheorems
-  }
+  let ctx ← Simp.mkContext
+     (config := (← elabSimpConfig stx[1] (kind := kind)))
+     (simpTheorems := #[simpTheorems])
+     congrTheorems
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) ctx
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else
@@ -328,8 +329,8 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     let hs ← getPropHyps
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
-        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    let ctx := { ctx with simpTheorems }
+        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr (config := ctx.indexConfig)
+    let ctx := ctx.setSimpTheorems simpTheorems
     return { ctx, simprocs, dischargeWrapper }
 
 register_builtin_option tactic.simp.trace : Bool := {

src/Lean/Elab/Tactic/Simpa.lean

@@ -36,9 +36,9 @@ deriving instance Repr for UseImplicitLambdaResult
     let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
-    let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
+    let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
     -- TODO: have `simpa` fail if it doesn't use `simp`.
-    let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
+    let ctx := ctx.setFailIfUnchanged false
     dischargeWrapper.with fun discharge? => do
       let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)

src/Lean/Elab/Tactic/Simproc.lean

@@ -25,7 +25,7 @@ def elabSimprocPattern (stx : Syntax) : MetaM Expr := do
 
 def elabSimprocKeys (stx : Syntax) : MetaM (Array Meta.SimpTheoremKey) := do
   let pattern ← elabSimprocPattern stx
-  DiscrTree.mkPath pattern simpDtConfig
+  withSimpGlobalConfig <| DiscrTree.mkPath pattern
 
 def checkSimprocType (declName : Name) : CoreM Bool := do
   let decl ← getConstInfo declName

src/Lean/Elab/Term.lean

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

src/Lean/Environment.lean

@@ -345,7 +345,7 @@ unsafe def setState {σ} (ext : Ext σ) (exts : Array EnvExtensionState) (s : σ
 
 unsafe def getState {σ} [Inhabited σ] (ext : Ext σ) (exts : Array EnvExtensionState) : σ :=
   if h : ext.idx < exts.size then
-    let s : EnvExtensionState := exts.get ⟨ext.idx, h⟩
+    let s : EnvExtensionState := exts[ext.idx]
     unsafeCast s
   else
     panic! invalidExtMsg

src/Lean/InternalExceptionId.lean

@@ -37,7 +37,7 @@ def InternalExceptionId.getName (id : InternalExceptionId) : IO Name :=  do
   let exs ← internalExceptionsRef.get
   let i := id.idx;
   if h : i < exs.size then
-    return exs.get ⟨i, h⟩
+    return exs[i]
   else
     throw <| IO.userError "invalid internal exception id"
 

src/Lean/Level.lean

@@ -320,7 +320,7 @@ private def accMax (result : Level) (prev : Level) (offset : Nat) : Level :=
  -/
 private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev : Level) (prevK : Nat) (result : Level) : Level :=
   if h : i < lvls.size then
-    let lvl   := lvls.get ⟨i, h⟩
+    let lvl   := lvls[i]
     let curr  := lvl.getLevelOffset
     let currK := lvl.getOffset
     if curr == prev then
@@ -335,7 +335,7 @@ private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev
   It finds the first position that is not an explicit universe. -/
 private partial def skipExplicit (lvls : Array Level) (i : Nat) : Nat :=
   if h : i < lvls.size then
-    let lvl := lvls.get ⟨i, h⟩
+    let lvl := lvls[i]
     if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i
   else
     i
@@ -349,7 +349,7 @@ It assumes `lvls` has been sorted using `normLt`.
 -/
 private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Nat) (i : Nat) : Bool :=
   if h : i < lvls.size then
-    let lvl := lvls.get ⟨i, h⟩
+    let lvl := lvls[i]
     if lvl.getOffset ≥ maxExplicit then true
     else isExplicitSubsumedAux lvls maxExplicit (i+1)
   else

src/Lean/Linter/UnusedVariables.lean

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

src/Lean/Message.lean

@@ -116,7 +116,7 @@ variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
 is true.
 
-This does not descend into lazily generated subtress (`.ofLazy`); message tags
+This does not descend into lazily generated subtrees (`.ofLazy`); message tags
 of interest (like those added by `logLinter`) are expected to be near the root
 of the `MessageData`, and not hidden inside `.ofLazy`.
 -/
@@ -130,6 +130,19 @@ partial def hasTag : MessageData → Bool
   | trace data msg msgs     => p data.cls || hasTag msg || msgs.any hasTag
   | _                       => false
 
+/--
+Returns the top-level tag of the message.
+If none, returns `Name.anonymous`.
+
+This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
+The message kind is expected to describe the whole message.
+-/
+def kind : MessageData → Name
+  | withContext _ msg       => kind msg
+  | withNamingContext _ msg => kind msg
+  | tagged n _              => n
+  | _                       => .anonymous
+
 /-- An empty message. -/
 def nil : MessageData :=
   ofFormat Format.nil
@@ -250,7 +263,7 @@ instance : Coe (Option Expr) MessageData := ⟨fun o => match o with | none => "
 
 partial def arrayExpr.toMessageData (es : Array Expr) (i : Nat) (acc : MessageData) : MessageData :=
   if h : i < es.size then
-    let e   := es.get ⟨i, h⟩;
+    let e   := es[i];
     let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e;
     toMessageData es (i+1) acc
   else
@@ -315,7 +328,7 @@ structure BaseMessage (α : Type u) where
   endPos        : Option Position := none
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
-  severity      : MessageSeverity := MessageSeverity.error
+  severity      : MessageSeverity := .error
   caption       : String          := ""
   /-- The content of the message. -/
   data          : α
@@ -328,7 +341,10 @@ abbrev Message := BaseMessage MessageData
 /-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
 serialized and is thus appropriate for use in pure contexts where the effectful
 `MessageData.toString` cannot be used. -/
-abbrev SerialMessage := BaseMessage String
+structure SerialMessage extends BaseMessage String where
+  /-- The message kind (i.e., the top-level tag). -/
+  kind          : Name
+  deriving ToJson, FromJson
 
 namespace SerialMessage
 
@@ -354,8 +370,12 @@ end SerialMessage
 
 namespace Message
 
+@[inherit_doc MessageData.kind] abbrev kind (msg : Message) :=
+  msg.data.kind
+
+/-- Serializes the message, converting its data into a string and saving its kind. -/
 @[inline] def serialize (msg : Message) : IO SerialMessage := do
-  return {msg with data := ← msg.data.toString}
+  return {msg with kind := msg.kind, data := ← msg.data.toString}
 
 protected def toString (msg : Message) (includeEndPos := false) : IO String := do
   -- Remark: The inline here avoids a new message allocation when `msg` is shared

src/Lean/Meta/ACLt.lean

@@ -32,6 +32,9 @@ inductive ReduceMode where
   | reduceSimpleOnly
   | none
 
+private def config : ConfigWithKey :=
+  { transparency := .reducible, iota := false, proj := .no : Config }.toConfigWithKey
+
 mutual
 
 /--
@@ -61,8 +64,8 @@ where
       -- Drawback: cost.
       return e
     else match mode with
-      | .reduce => DiscrTree.reduce e {}
-      | .reduceSimpleOnly => DiscrTree.reduce e { iota := false, proj := .no }
+      | .reduce => DiscrTree.reduce e
+      | .reduceSimpleOnly => withConfigWithKey config <| DiscrTree.reduce e
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do

src/Lean/Meta/AppBuilder.lean

@@ -352,7 +352,7 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat →
   | i, args, j, instMVars, Expr.forallE n d b bi => do
     let d  := d.instantiateRevRange j args.size args
     if h : i < xs.size then
-      match xs.get ⟨i, h⟩ with
+      match xs[i] with
       | none =>
         match bi with
         | BinderInfo.instImplicit => do

src/Lean/Meta/ArgsPacker.lean

@@ -196,13 +196,13 @@ where
       let packedArg := Unary.pack packedDomain args
       return e.beta #[packedArg]
   | [n] => do
-    withLocalDecl n .default domain fun x => do
+    withLocalDeclD n domain fun x => do
       let dummy := Expr.const ``Unit []
       mkLambdaFVars #[x] (← go packedDomain dummy (args.push x) [])
   | n :: ns =>
     match_expr domain with
     | PSigma a b =>
-      withLocalDecl n .default a fun x => do
+      withLocalDeclD n a fun x => do
         mkLambdaFVars #[x] (← go packedDomain (b.beta #[x]) (args.push x) ns)
     | _ => throwError "curryPSigma: Expected PSigma type, got {domain}"
 
@@ -319,7 +319,7 @@ def uncurryType (types : Array Expr) : MetaM Expr := do
     unless type.isForall do
       throwError "Mutual.uncurryType: Expected forall type, got {type}"
   let domain ← packType (types.map (·.bindingDomain!))
-  withLocalDeclD `x domain fun x => do
+  withLocalDeclD (← mkFreshUserName `x) domain fun x => do
     let codomain ← Mutual.mkCodomain types x
     mkForallFVars #[x] codomain
 
@@ -485,13 +485,14 @@ projects to the `i`th function of type,
 -/
 def curryProj (argsPacker : ArgsPacker) (e : Expr) (i : Nat) : MetaM Expr := do
   let n := argsPacker.numFuncs
-  let packedDomain := (← inferType e).bindingDomain!
+  let t ← inferType e
+  let packedDomain := t.bindingDomain!
   let unaryTypes ← Mutual.unpackType n packedDomain
   unless i < unaryTypes.length do
     throwError "curryProj: index out of range"
   let unaryType := unaryTypes[i]!
   -- unary : (x : a ⊗ b) → e[inl x]
-  let unary ← withLocalDecl `x .default unaryType fun x => do
+  let unary ← withLocalDeclD t.bindingName! unaryType fun x => do
       let packedArg ← Mutual.pack unaryTypes.length packedDomain i x
       mkLambdaFVars #[x] (e.beta #[packedArg])
   -- nary : (x : a) → (y : b) → e[inl (x,y)]