fix: Context.setConfig must update metaConfig and indexConfig fields

This PR fixes a bug at `Context.setConfig`. It was not propagating
the configuration to the redundant fields (cache) `metaConfig` and `indexConfig`.

src/Init/Data/Array/Attach.lean

@@ -10,12 +10,13 @@ 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`.
+/--
+`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
+We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
 -/
 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
@@ -73,6 +74,17 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   intro a m h₁ h₂
   congr
 
+@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+
+@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : Array α) (h : ∀ b ∈ l.push a, P b) :
+    pmap f (l.push a) h =
+      (pmap f l (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
+  simp [pmap]
+
+@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+
+@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+
 @[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
@@ -80,6 +92,353 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   apply List.pmap_congr_left
   simp
 
+@[simp]
+theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : Array α) (H) :
+    @pmap _ _ p (fun a _ => f a) l H = map f l := by
+  cases l; simp
+
+theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : Array α) {H₁ H₂}
+    (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by
+  cases l
+  simp only [mem_toArray] at h
+  simp only [List.pmap_toArray, mk.injEq]
+  rw [List.pmap_congr_left _ h]
+
+theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) :
+    map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
+  cases l
+  simp [List.map_pmap]
+
+theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) :
+    pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h) := by
+  cases l
+  simp [List.pmap_map]
+
+theorem attach_congr {l₁ l₂ : Array α} (h : l₁ = l₂) :
+    l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
+  subst h
+  simp
+
+theorem attachWith_congr {l₁ l₂ : Array α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
+    l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h) := by
+  subst w
+  simp
+
+@[simp] theorem attach_push {a : α} {l : Array α} :
+    (l.push a).attach =
+      (l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
+  cases l
+  rw [attach_congr (List.push_toArray _ _)]
+  simp [Function.comp_def]
+
+@[simp] theorem attachWith_push {a : α} {l : Array α} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
+    (l.push a).attachWith P H =
+      (l.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
+  cases l
+  simp [attachWith_congr (List.push_toArray _ _)]
+
+theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
+    pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
+  cases l
+  simp [List.pmap_eq_map_attach]
+
+theorem attach_map_coe (l : Array α) (f : α → β) :
+    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
+  cases l
+  simp [List.attach_map_coe]
+
+theorem attach_map_val (l : Array α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
+  attach_map_coe _ _
+
+@[simp]
+theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l := by
+  cases l; simp
+
+theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
+    ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
+  cases l; simp
+
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
+    ((l.attachWith p H).map fun i => f i.val) = l.map f :=
+  attachWith_map_coe _ _ _
+
+@[simp]
+theorem attachWith_map_subtype_val {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) :
+    (l.attachWith p H).map Subtype.val = l := by
+  cases l; simp
+
+@[simp]
+theorem mem_attach (l : Array α) : ∀ x, x ∈ l.attach
+  | ⟨a, h⟩ => by
+    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
+    rcases this with ⟨⟨_, _⟩, m, rfl⟩
+    exact m
+
+@[simp]
+theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
+    b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
+  simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
+
+theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h : a ∈ l) :
+    f a (H a h) ∈ pmap f l H := by
+  rw [mem_pmap]
+  exact ⟨a, h, rfl⟩
+
+@[simp]
+theorem size_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).size = l.size := by
+  cases l; simp
+
+@[simp]
+theorem size_attach {L : Array α} : L.attach.size = L.size := by
+  cases L; simp
+
+@[simp]
+theorem size_attachWith {p : α → Prop} {l : Array α} {H} : (l.attachWith p H).size = l.size := by
+  cases l; simp
+
+@[simp]
+theorem pmap_eq_empty_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = #[] ↔ l = #[] := by
+  cases l; simp
+
+theorem pmap_ne_empty_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Array α}
+    (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ #[] ↔ xs ≠ #[] := by
+  cases xs; simp
+
+theorem pmap_eq_self {l : Array α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a)
+    (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
+  cases l; simp [List.pmap_eq_self]
+
+@[simp]
+theorem attach_eq_empty_iff {l : Array α} : l.attach = #[] ↔ l = #[] := by
+  cases l; simp
+
+theorem attach_ne_empty_iff {l : Array α} : l.attach ≠ #[] ↔ l ≠ #[] := by
+  cases l; simp
+
+@[simp]
+theorem attachWith_eq_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
+    l.attachWith P H = #[] ↔ l = #[] := by
+  cases l; simp
+
+theorem attachWith_ne_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
+    l.attachWith P H ≠ #[] ↔ l ≠ #[] := by
+  cases l; simp
+
+@[simp]
+theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) (n : Nat) :
+    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
+  cases l; simp
+
+@[simp]
+theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) {n : Nat}
+    (hn : n < (pmap f l h).size) :
+    (pmap f l h)[n] =
+      f (l[n]'(@size_pmap _ _ p f l h ▸ hn))
+        (h _ (getElem_mem (@size_pmap _ _ p f l h ▸ hn))) := by
+  cases l; simp
+
+@[simp]
+theorem getElem?_attachWith {xs : Array α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
+    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
+  getElem?_pmap ..
+
+@[simp]
+theorem getElem?_attach {xs : Array α} {i : Nat} :
+    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
+  getElem?_attachWith
+
+@[simp]
+theorem getElem_attachWith {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
+    {i : Nat} (h : i < (xs.attachWith P H).size) :
+    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
+  getElem_pmap ..
+
+@[simp]
+theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
+    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
+  getElem_attachWith h
+
+theorem foldl_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
+    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
+  rw [pmap_eq_map_attach, foldl_map]
+
+theorem foldr_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
+    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
+  rw [pmap_eq_map_attach, foldr_map]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+See however `foldl_subtype` below.
+-/
+theorem foldl_attach (l : Array α) (f : β → α → β) (b : β) :
+    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
+  rcases l with ⟨l⟩
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
+    List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
+  congr
+  ext
+  simpa using fun a => List.mem_of_getElem? a
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+See however `foldr_subtype` below.
+-/
+theorem foldr_attach (l : Array α) (f : α → β → β) (b : β) :
+    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
+  rcases l with ⟨l⟩
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
+    List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
+  congr
+  ext
+  simpa using fun a => List.mem_of_getElem? a
+
+theorem attach_map {l : Array α} (f : α → β) :
+    (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
+  cases l
+  ext <;> simp
+
+theorem attachWith_map {l : Array α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
+    (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
+      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
+  cases l
+  ext
+  · simp
+  · simp only [List.map_toArray, List.attachWith_toArray, List.getElem_toArray,
+      List.getElem_attachWith, List.getElem_map, Function.comp_apply]
+    erw [List.getElem_attachWith] -- Why is `erw` needed here?
+
+theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+    (f : { x // P x } → β) :
+    (l.attachWith P H).map f =
+      l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
+  cases l
+  ext <;> simp
+
+/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
+theorem map_attach {l : Array α} (f : { x // x ∈ l } → β) :
+    l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
+  cases l
+  ext <;> simp
+
+theorem attach_filterMap {l : Array α} {f : α → Option β} :
+    (l.filterMap f).attach = l.attach.filterMap
+      fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
+  cases l
+  rw [attach_congr (List.filterMap_toArray f _)]
+  simp [List.attach_filterMap, List.map_filterMap, Function.comp_def]
+
+theorem attach_filter {l : Array α} (p : α → Bool) :
+    (l.filter p).attach = l.attach.filterMap
+      fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none := by
+  cases l
+  rw [attach_congr (List.filter_toArray p _)]
+  simp [List.attach_filter, List.map_filterMap, Function.comp_def]
+
+-- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
+-- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
+
+theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
+    pmap f (pmap g l H₁) H₂ =
+      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
+        (fun a _ => H₁ a a.2) := by
+  cases l
+  simp [List.pmap_pmap, List.pmap_map]
+
+@[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : Array ι)
+    (h : ∀ a ∈ l₁ ++ l₂, p a) :
+    (l₁ ++ l₂).pmap f h =
+      (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
+        l₂.pmap f fun a ha => h a (mem_append_right l₁ ha) := by
+  cases l₁
+  cases l₂
+  simp
+
+theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ : Array α)
+    (h₁ : ∀ a ∈ l₁, p a) (h₂ : ∀ a ∈ l₂, p a) :
+    ((l₁ ++ l₂).pmap f fun a ha => (mem_append.1 ha).elim (h₁ a) (h₂ a)) =
+      l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
+  pmap_append f l₁ l₂ _
+
+@[simp] theorem attach_append (xs ys : Array α) :
+    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
+      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
+  cases xs
+  cases ys
+  rw [attach_congr (List.append_toArray _ _)]
+  simp [List.attach_append, Function.comp_def]
+
+@[simp] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+    {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
+    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
+      ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
+  simp [attachWith, attach_append, map_pmap, pmap_append]
+
+@[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
+    (H : ∀ (a : α), a ∈ xs.reverse → P a) :
+    xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
+  induction xs <;> simp_all
+
+theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
+  rw [pmap_reverse]
+
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+    {H : ∀ (a : α), a ∈ xs.reverse → P a} :
+    xs.reverse.attachWith P H =
+      (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
+  cases xs
+  simp
+
+theorem reverse_attachWith {P : α → Prop} {xs : Array α}
+    {H : ∀ (a : α), a ∈ xs → P a} :
+    (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
+  cases xs
+  simp
+
+@[simp] theorem attach_reverse (xs : Array α) :
+    xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  cases xs
+  rw [attach_congr (List.reverse_toArray _)]
+  simp
+
+theorem reverse_attach (xs : Array α) :
+    xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  cases xs
+  simp
+
+@[simp] theorem back?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
+    (H : ∀ (a : α), a ∈ xs → P a) :
+    (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
+  cases xs
+  simp
+
+@[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+    {H : ∀ (a : α), a ∈ xs → P a} :
+    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back?_eq_some h)⟩) := by
+  cases xs
+  simp
+
+@[simp]
+theorem back?_attach {xs : Array α} :
+    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back?_eq_some h⟩ := by
+  cases xs
+  simp
+
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -128,6 +487,15 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
   cases l
   simp
 
+@[simp] theorem getElem?_unattach {p : α → Prop} {l : Array { x // p x }} (i : Nat) :
+    l.unattach[i]? = l[i]?.map Subtype.val := by
+  simp [unattach]
+
+@[simp] theorem getElem_unattach
+    {p : α → Prop} {l : Array { x // p x }} (i : Nat) (h : i < l.unattach.size) :
+    l.unattach[i] = (l[i]'(by simpa using h)).1 := by
+  simp [unattach]
+
 /-! ### Recognizing higher order functions using a function that only depends on the value. -/
 
 /--

src/Init/Data/Array/Basic.lean

@@ -613,8 +613,15 @@ def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
-def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-  a.findIdx? fun a => a == v
+@[inline]
+def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
+    if h : j < as.size then
+      if p as[j] then some ⟨j, h⟩ else loop (j + 1)
+    else none
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
+  loop 0
 
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
@@ -627,6 +634,10 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
 
+@[deprecated indexOf? (since := "2024-11-20")]
+def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
+  a.findIdx? fun a => a == v
+
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
   Id.run <| as.anyM p start stop
@@ -766,48 +777,62 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
-/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
+/--
+Remove the element at a given index from an array without a runtime bounds checks,
+using a `Nat` index and a tactic-provided bound.
 
-  This function takes worst case O(n) time because
-  it has to backshift all elements at positions greater than `i`.-/
+This function takes worst case O(n) time because
+it has to backshift all elements at positions greater than `i`.-/
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
-  if h : i.val + 1 < a.size then
-    let a' := a.swap ⟨i.val + 1, h⟩ i
-    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
-    a'.feraseIdx i'
+def eraseIdx (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
+  if h' : i + 1 < a.size then
+    let a' := a.swap ⟨i + 1, h'⟩ ⟨i, h⟩
+    a'.eraseIdx (i + 1) (by simp [a', h'])
   else
     a.pop
-termination_by a.size - i.val
-decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
+termination_by a.size - i
+decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
-  induction a, i using Array.feraseIdx.induct with
-  | @case1 a i h a' _ ih =>
-    unfold feraseIdx
-    simp [h, a', ih]
-  | case2 a i h =>
-    unfold feraseIdx
-    simp [h]
+@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) (h) : (a.eraseIdx i h).size = a.size - 1 := by
+  induction a, i, h using Array.eraseIdx.induct with
+  | @case1 a i h h' a' ih =>
+    unfold eraseIdx
+    simp [h', a', ih]
+  | case2 a i h h' =>
+    unfold eraseIdx
+    simp [h']
 
 /-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
 
   This function takes worst case O(n) time because
   it has to backshift all elements at positions greater than `i`.-/
-def eraseIdx (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
+def eraseIdxIfInBounds (a : Array α) (i : Nat) : Array α :=
+  if h : i < a.size then a.eraseIdx i h else a
+
+/-- Remove the element at a given index from an array, or panic if the index is out of bounds.
+
+This function takes worst case O(n) time because
+it has to backshift all elements at positions greater than `i`. -/
+def eraseIdx! (a : Array α) (i : Nat) : Array α :=
+  if h : i < a.size then a.eraseIdx i h else panic! "invalid index"
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with
   | none   => as
-  | some i => as.feraseIdx i
+  | some i => as.eraseIdx i
+
+/-- Erase the first element that satisfies the predicate `p`. -/
+def eraseP (as : Array α) (p : α → Bool) : Array α :=
+  match as.findIdx? p with
+  | none   => as
+  | some i => as.eraseIdxIfInBounds i
 
 /-- Insert element `a` at position `i`. -/
-@[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
+@[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (as : Array α) (j : Fin as.size) :=
-    if i.1 < j then
+    if i < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
@@ -818,12 +843,23 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
 
+@[deprecated insertIdx (since := "2024-11-20")] abbrev insertAt := @insertIdx
+
 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
-def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
+def insertIdx! (as : Array α) (i : Nat) (a : α) : Array α :=
   if h : i ≤ as.size then
-    insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
+    insertIdx as i a
   else panic! "invalid index"
 
+@[deprecated insertIdx! (since := "2024-11-20")] abbrev insertAt! := @insertIdx!
+
+/-- Insert element `a` at position `i`, or do nothing if `as.size < i`. -/
+def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
+  if h : i ≤ as.size then
+    insertIdx as i a
+  else
+    as
+
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then

src/Init/Data/Array/BinSearch.lean

@@ -52,7 +52,7 @@ namespace Array
     let mid    := (lo + hi)/2
     let midVal := as.get! mid
     if lt midVal k then
-      if mid == lo then do let v ← add (); pure <| as.insertAt! (lo+1) v
+      if mid == lo then do let v ← add (); pure <| as.insertIdx! (lo+1) v
       else binInsertAux lt merge add as k mid hi
     else if lt k midVal then
       binInsertAux lt merge add as k lo mid
@@ -67,7 +67,7 @@ namespace Array
     (k : α) : m (Array α) :=
   let _ := Inhabited.mk k
   if as.isEmpty then do let v ← add (); pure <| as.push v
-  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertAt! 0 v
+  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertIdx! 0 v
   else if !lt (as.get! 0) k then as.modifyM 0 <| merge
   else if lt as.back! k then do let v ← add (); pure <| as.push v
   else if !lt k as.back! then as.modifyM (as.size - 1) <| merge

src/Init/Data/Array/Find.lean

@@ -272,4 +272,10 @@ theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
     ((mkArray n a).find? p).get h = a := by
   simp [mkArray_eq_toArray_replicate]
 
+theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
+    (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
+    (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
+  simp only [pmap_eq_map_attach, find?_map]
+  rfl
+
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -23,6 +23,9 @@ import Init.TacticsExtra
 
 namespace Array
 
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
 theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := rfl
@@ -36,12 +39,21 @@ theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? =
   · rw [getElem?_neg a i h]
     simp_all
 
+@[simp] theorem none_eq_getElem?_iff {a : Array α} {i : Nat} : none = a[i]? ↔ a.size ≤ i := by
+  simp [eq_comm (a := none)]
+
 theorem getElem?_eq {a : Array α} {i : Nat} :
     a[i]? = if h : i < a.size then some a[i] else none := by
   split
   · simp_all [getElem?_eq_getElem]
   · simp_all
 
+theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b ↔ ∃ h : i < a.size, a[i] = b := by
+  simp [getElem?_eq]
+
+theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? ↔ ∃ h : i < a.size, a[i] = b := by
+  rw [eq_comm, getElem?_eq_some_iff]
+
 theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
   rw [getElem?_eq]
   split <;> simp_all
@@ -66,6 +78,35 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
 @[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
 @[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
 
+@[simp] theorem mem_push {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y := by
+  simp [mem_def]
+
+theorem mem_push_self {a : Array α} {x : α} : x ∈ a.push x :=
+  mem_push.2 (Or.inr rfl)
+
+theorem mem_push_of_mem {a : Array α} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y :=
+  mem_push.2 (Or.inl h)
+
+theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (n : Nat) (h : n < l.size), l[n]'h = a := by
+  cases l
+  simp [List.getElem_of_mem (by simpa using h)]
+
+theorem getElem?_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a :=
+  let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
+
+theorem mem_of_getElem? {l : Array α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
+  let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
+
+theorem mem_iff_getElem {a} {l : Array α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.size), l[n]'h = a :=
+  ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
+
+theorem mem_iff_getElem? {a} {l : Array α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by
+  simp [getElem?_eq_some_iff, mem_iff_getElem]
+
+theorem forall_getElem {l : Array α} {p : α → Prop} :
+    (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by
+  cases l; simp [List.forall_getElem]
+
 @[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
   simp [getElem!_def, get!, getD]
   split <;> rename_i h
@@ -93,9 +134,6 @@ We prefer to pull `List.toArray` outwards.
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [mem_def]
-
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -583,7 +621,7 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
     (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
   simp [getElem?_def]
 
-/-- # mkArray -/
+/-! # mkArray -/
 
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
   List.length_replicate ..
@@ -599,25 +637,12 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
     (mkArray n v)[i]? = if i < n then some v else none := by
   simp [getElem?_def]
 
-/-- # mem -/
+/-! # mem -/
 
 @[simp] theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
 
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
-theorem getElem_of_mem {a : α} {as : Array α} :
-    a ∈ as → (∃ (n : Nat) (h : n < as.size), as[n]'h = a) := by
-  intro ha
-  rcases List.getElem_of_mem ha.val with ⟨i, hbound, hi⟩
-  exists i
-  exists hbound
-
-theorem getElem?_of_mem {a : α} {as : Array α} :
-    a ∈ as → ∃ (n : Nat), as[n]? = some a := by
-  intro ha
-  rcases List.getElem?_of_mem ha.val with ⟨i, hi⟩
-  exists i
-
 @[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
@@ -634,7 +659,7 @@ theorem getElem?_of_mem {a : α} {as : Array α} :
     (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
   split <;> simp_all
 
-/-- # get lemmas -/
+/-! # get lemmas -/
 
 theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :
     idx < a.size :=
@@ -659,10 +684,6 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp only [get!_eq_getElem?, get?_eq_getElem?]
 
-theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
-  cases as
-  simp [List.getElem?_eq_some_iff]
-
 theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
   simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
 
@@ -672,6 +693,10 @@ theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD de
 @[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
   simp [back!_eq_back?]
 
+theorem mem_of_back?_eq_some {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
+  cases xs
+  simpa using List.mem_of_getLast?_eq_some (by simpa using h)
+
 theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
   rw [getElem?_pos, getElem_push_lt]
@@ -1025,6 +1050,10 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
 @[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
   simp only [mem_def, toList_map, List.mem_map]
 
+theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
+
+theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩
+
 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_toList, ← List.foldrM_reverse]
@@ -1215,6 +1244,12 @@ theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] :=
 @[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
   simp only [mem_def, toList_append, List.mem_append]
 
+theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inl h)
+
+theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
+  mem_append.2 (Or.inr h)
+
 @[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
   simp only [size, toList_append, List.length_append]
 
@@ -1602,9 +1637,9 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
 
 /-! ### eraseIdx -/
 
-theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
-    a.feraseIdx i = a.eraseIdx i.1 := by
-  simp [eraseIdx]
+theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) :
+    a.eraseIdx i h = a.eraseIdxIfInBounds i := by
+  simp [eraseIdxIfInBounds, h]
 
 /-! ### isPrefixOf -/
 
@@ -1834,16 +1869,15 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
-@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
-    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
-  rw [feraseIdx]
-  split <;> rename_i h
-  · rw [feraseIdx_toArray]
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
+    l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
+  split <;> rename_i h'
+  · rw [eraseIdx_toArray]
     simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
     rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
     simp
-  · rcases i with ⟨i, w⟩
-    simp at h w
+  · simp at h h'
     have t : i = l.length - 1 := by omega
     simp [t]
 termination_by l.length - i
@@ -1853,9 +1887,9 @@ decreasing_by
   simp
   omega
 
-@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
-    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
-  rw [Array.eraseIdx]
+@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdxIfInBounds]
   split
   · simp
   · simp_all [eraseIdx_eq_self.2]
@@ -1874,13 +1908,13 @@ namespace Array
     (as.takeWhile p).toList = as.toList.takeWhile p := by
   induction as; simp
 
-@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
-    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) (h : i < as.size) :
+    (as.eraseIdx i h).toList = as.toList.eraseIdx i := by
   induction as
   simp
 
-@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
-    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
+@[simp] theorem toList_eraseIdxIfInBounds (as : Array α) (i : Nat) :
+    (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i := by
   induction as
   simp
 
@@ -1914,6 +1948,26 @@ theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : Li
   specialize h (ass.toList.map toList)
   simpa [← toList_map, Function.comp_def, map_id] using h
 
+theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) :
+    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
+  cases l; simp [List.foldl_map]
+
+theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : Array α₁) (init : β) :
+    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
+  cases l; simp [List.foldr_map]
+
+theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : Array α) (init : γ) :
+    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
+  cases l
+  simp [List.foldl_filterMap]
+  rfl
+
+theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : Array α) (init : γ) :
+    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
+  cases l
+  simp [List.foldr_filterMap]
+  rfl
+
 /-! ### flatten -/
 
 @[simp] theorem flatten_empty : flatten (#[] : Array (Array α)) = #[] := rfl
@@ -1928,6 +1982,12 @@ theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : Li
   | nil => simp
   | cons xs xss ih => simp [ih]
 
+/-! ### reverse -/
+
+@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
+  cases as
+  simp
+
 /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
 
 @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse

src/Init/Data/BitVec/Lemmas.lean

@@ -2611,7 +2611,7 @@ theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   apply getLsbD_ge
   omega
 
-/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsbD i`. -/
+/-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
 theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateLeft r).getLsbD i =
       cond (i < r)
@@ -2638,6 +2638,56 @@ theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
       if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)] := by
   simp [← BitVec.getLsbD_eq_getElem, h]
 
+/-- If `w ≤ x < 2 * w`, then `x % w = x - w` -/
+theorem mod_eq_sub_of_le_of_lt {x w : Nat} (x_le : w ≤ x) (x_lt : x < 2 * w) :
+    x % w = x - w := by
+  rw [Nat.mod_eq_sub_mod, Nat.mod_eq_of_lt (by omega)]
+  omega
+
+theorem getMsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
+    (x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i) := by
+  rw [rotateLeftAux, getMsbD_or]
+  simp [show i < w - r by omega, Nat.add_comm]
+
+theorem getMsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
+    (x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r))) := by
+  simp [rotateLeftAux, getMsbD_or, show i + r ≥ w by omega, show ¬i < w - r by omega]
+
+/-- When `r < w`, we give a formula for `(x.rotateLeft r).getMsbD i`. -/
+theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
+    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
+  rcases w with rfl | w
+  · simp
+  · rw [BitVec.rotateLeft_eq_rotateLeftAux_of_lt (by omega)]
+    by_cases h : n < (w + 1) - r
+    · simp [getMsbD_rotateLeftAux_of_lt h, Nat.mod_eq_of_lt, show r + n < (w + 1) by omega, show n < w + 1 by omega]
+    · simp [getMsbD_rotateLeftAux_of_ge <| Nat.ge_of_not_lt h]
+      by_cases h₁ : n < w + 1
+      · simp only [h₁, decide_true, Bool.true_and]
+        have h₂ : (r + n) < 2 * (w + 1) := by omega
+        rw [mod_eq_sub_of_le_of_lt (by omega) (by omega)]
+        congr 1
+        omega
+      · simp [h₁]
+
+theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :
+    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
+  rcases w with rfl | w
+  · simp
+  · by_cases h : r < w
+    · rw [getMsbD_rotateLeft_of_lt (by omega)]
+    · rw [← rotateLeft_mod_eq_rotateLeft, getMsbD_rotateLeft_of_lt (by apply Nat.mod_lt; simp)]
+      simp
+
+@[simp]
+theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
+    (x.rotateLeft m).msb = x.getMsbD (m % w) := by
+  simp only [BitVec.msb, getMsbD_rotateLeft]
+  by_cases h : w = 0
+  · simp [h]
+  · simp
+    omega
+
 /-! ## Rotate Right -/
 
 /--
@@ -2699,7 +2749,7 @@ theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
   simp only [rotateRight, Nat.mod_mod]
 
 /-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
-theorem getLsbD_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
+theorem getLsbD_rotateRight_of_lt {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateRight r).getLsbD i =
       cond (i < w - r)
       (x.getLsbD (r + i))
@@ -2717,7 +2767,7 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
       (decide (i < w) && x.getLsbD (i - (w - (r % w)))) := by
   rcases w with ⟨rfl, w⟩
   · simp
-  · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_le (Nat.mod_lt _ (by omega))]
+  · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_lt (Nat.mod_lt _ (by omega))]
 
 @[simp]
 theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
@@ -2725,6 +2775,56 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
   simp only [← BitVec.getLsbD_eq_getElem]
   simp [getLsbD_rotateRight, h]
 
+theorem getMsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
+    (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r)) := by
+  rw [rotateRightAux, getMsbD_or, getMsbD_ushiftRight]
+  simp [show i < r by omega]
+
+theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
+    (x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r)) := by
+  simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) ≥ w by omega]
+
+/-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/
+@[simp]
+theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w):
+    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
+    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
+  rcases w with rfl | w
+  · simp
+  · rw [rotateRight_eq_rotateRightAux_of_lt (by omega)]
+    by_cases h : n < m
+    · simp only [getMsbD_rotateRightAux_of_lt h, show n < w + 1 by omega, decide_true,
+        show m % (w + 1) = m by rw [Nat.mod_eq_of_lt hr], h, ↓reduceIte,
+        show (w + 1 + n - m) < (w + 1) by omega, Nat.mod_eq_of_lt, Bool.true_and]
+      congr 1
+      omega
+    · simp [h, getMsbD_rotateRightAux_of_ge <| Nat.ge_of_not_lt h]
+      by_cases h₁ : n < w + 1
+      · simp [h, h₁, decide_true, Bool.true_and, Nat.mod_eq_of_lt hr]
+      · simp [h₁]
+
+@[simp]
+theorem getMsbD_rotateRight {w n m : Nat} {x : BitVec w} :
+    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
+    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
+  rcases w with rfl | w
+  · simp
+  · by_cases h₀ : m < w
+    · rw [getMsbD_rotateRight_of_lt (by omega)]
+    · rw [← rotateRight_mod_eq_rotateRight, getMsbD_rotateRight_of_lt (by apply Nat.mod_lt; simp)]
+      simp
+
+@[simp]
+theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
+    (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w) := by
+  simp only [BitVec.msb, getMsbD_rotateRight]
+  by_cases h₀ : 0 < w
+  · simp only [h₀, decide_true, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, Bool.true_and,
+    ite_eq_left_iff, Nat.not_lt, Nat.le_zero_eq]
+    intro h₁
+    simp [h₁]
+  · simp [show w = 0 by omega]
+
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

src/Init/Data/Float.lean

@@ -31,7 +31,7 @@ opaque floatSpec : FloatSpec := {
 structure Float where
   val : floatSpec.float
 
-instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
+instance : Nonempty Float := ⟨{ val := floatSpec.val }⟩
 
 @[extern "lean_float_add"] opaque Float.add : Float → Float → Float
 @[extern "lean_float_sub"] opaque Float.sub : Float → Float → Float
@@ -136,6 +136,9 @@ instance : ToString Float where
 
 @[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
 
+instance : Inhabited Float where
+  default := UInt64.toFloat 0
+
 instance : Repr Float where
   reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
 

src/Init/Data/List/Attach.lean

@@ -13,7 +13,7 @@ namespace List
   `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`. -/
-@[simp] def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
+def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
   | [], _ => []
   | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
 
@@ -46,6 +46,11 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
   exact go L h'
 
+@[simp] theorem pmap_nil {P : α → Prop} (f : ∀ a, P a → β) : pmap f [] (by simp) = [] := rfl
+
+@[simp] theorem pmap_cons {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : List α) (h : ∀ b ∈ a :: l, P b) :
+    pmap f (a :: l) h = f a (forall_mem_cons.1 h).1 :: pmap f l (forall_mem_cons.1 h).2 := rfl
+
 @[simp] theorem attach_nil : ([] : List α).attach = [] := rfl
 
 @[simp] theorem attachWith_nil : ([] : List α).attachWith P H = [] := rfl
@@ -148,7 +153,7 @@ theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h :
   exact ⟨a, h, rfl⟩
 
 @[simp]
-theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pmap f l H) = length l := by
+theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).length = l.length := by
   induction l
   · rfl
   · simp only [*, pmap, length]
@@ -199,7 +204,7 @@ theorem attachWith_ne_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l,
 
 @[simp]
 theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (getElem?_mem H) := by
+    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
   induction l generalizing n with
   | nil => simp
   | cons hd tl hl =>
@@ -215,7 +220,7 @@ theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
       · simp_all
 
 theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (get?_mem H) := by
+    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
   simp only [get?_eq_getElem?]
   simp [getElem?_pmap, h]
 
@@ -238,18 +243,18 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h :
     (hn : n < (pmap f l h).length) :
     get (pmap f l h) ⟨n, hn⟩ =
       f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
-        (h _ (get_mem l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)) := by
+        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
   simp only [get_eq_getElem]
   simp [getElem_pmap]
 
 @[simp]
 theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
-    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (getElem?_mem a)) :=
+    (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
   getElem?_pmap ..
 
 @[simp]
 theorem getElem?_attach {xs : List α} {i : Nat} :
-    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) :=
+    xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
   getElem?_attachWith
 
 @[simp]
@@ -333,6 +338,7 @@ This is useful when we need to use `attach` to show termination.
 
 Unfortunately this can't be applied by `simp` because of the higher order unification problem,
 and even when rewriting we need to specify the function explicitly.
+See however `foldl_subtype` below.
 -/
 theorem foldl_attach (l : List α) (f : β → α → β) (b : β) :
     l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
@@ -348,6 +354,7 @@ This is useful when we need to use `attach` to show termination.
 
 Unfortunately this can't be applied by `simp` because of the higher order unification problem,
 and even when rewriting we need to specify the function explicitly.
+See however `foldr_subtype` below.
 -/
 theorem foldr_attach (l : List α) (f : α → β → β) (b : β) :
     l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
@@ -452,16 +459,16 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ :
   pmap_append f l₁ l₂ _
 
 @[simp] theorem attach_append (xs ys : List α) :
-    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_left ys h⟩) ++
-      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_right xs h⟩ := by
+    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
+      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   simp only [attach, attachWith, pmap, map_pmap, pmap_append]
   congr 1 <;>
   exact pmap_congr_left _ fun _ _ _ _ => rfl
 
 @[simp] theorem attachWith_append {P : α → Prop} {xs ys : List α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
-    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_of_mem_left ys h)) ++
-      ys.attachWith P (fun a h => H a (mem_append_of_mem_right xs h)) := by
+    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
+      ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp only [attachWith, attach_append, map_pmap, pmap_append]
 
 @[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
@@ -598,6 +605,15 @@ def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) := l.map (
   | nil => simp
   | cons a l ih => simp [ih, Function.comp_def]
 
+@[simp] theorem getElem?_unattach {p : α → Prop} {l : List { x // p x }} (i : Nat) :
+    l.unattach[i]? = l[i]?.map Subtype.val := by
+  simp [unattach]
+
+@[simp] theorem getElem_unattach
+    {p : α → Prop} {l : List { x // p x }} (i : Nat) (h : i < l.unattach.length) :
+    l.unattach[i] = (l[i]'(by simpa using h)).1 := by
+  simp [unattach]
+
 /-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
 
 /--

src/Init/Data/List/Basic.lean

@@ -726,13 +726,13 @@ theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : List α} (h :
 instance [BEq α] [LawfulBEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
 
-theorem mem_append_of_mem_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
+theorem mem_append_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
   intro h
   induction h with
   | head => apply Mem.head
   | tail => apply Mem.tail; assumption
 
-theorem mem_append_of_mem_right {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs := by
+theorem mem_append_right {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs := by
   intro h
   induction as with
   | nil  => simp [h]

src/Init/Data/List/Control.lean

@@ -256,7 +256,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
       have : a ∈ as := by
         have ⟨bs, h⟩ := h
         subst h
-        exact mem_append_of_mem_right _ (Mem.head ..)
+        exact mem_append_right _ (Mem.head ..)
       match (← f a this b) with
       | ForInStep.done b  => pure b
       | ForInStep.yield b =>

src/Init/Data/List/Lemmas.lean

@@ -394,9 +394,9 @@ theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = s
 theorem mem_cons_self (a : α) (l : List α) : a ∈ a :: l := .head ..
 
 theorem mem_concat_self (xs : List α) (a : α) : a ∈ xs ++ [a] :=
-  mem_append_of_mem_right xs (mem_cons_self a _)
+  mem_append_right xs (mem_cons_self a _)
 
-theorem mem_append_cons_self : a ∈ xs ++ a :: ys := mem_append_of_mem_right _ (mem_cons_self _ _)
+theorem mem_append_cons_self : a ∈ xs ++ a :: ys := mem_append_right _ (mem_cons_self _ _)
 
 theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
     ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as := by
@@ -507,12 +507,16 @@ theorem get_mem : ∀ (l : List α) n, get l n ∈ l
   | _ :: _, ⟨0, _⟩ => .head ..
   | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
 
-theorem getElem?_mem {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
+theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
-theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
+@[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem?
+
+theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
   let ⟨_, e⟩ := get?_eq_some.1 e; e ▸ get_mem ..
 
+@[deprecated mem_of_get? (since := "2024-09-06")] abbrev get?_mem := @mem_of_get?
+
 theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.length), l[n]'h = a :=
   ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩
 
@@ -1997,11 +2001,8 @@ theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t
 theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
   propext mem_append
 
-theorem mem_append_left {a : α} {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inl h)
-
-theorem mem_append_right {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inr h)
+@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left
+@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right
 
 theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
   ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩

src/Init/Data/List/Sublist.lean

@@ -417,7 +417,7 @@ theorem Sublist.of_sublist_append_left (w : ∀ a, a ∈ l → a ∉ l₂) (h :
   obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
   have : l₂' = [] := by
     rw [eq_nil_iff_forall_not_mem]
-    exact fun x m => w x (mem_append_of_mem_right l₁' m) (h₂.mem m)
+    exact fun x m => w x (mem_append_right l₁' m) (h₂.mem m)
   simp_all
 
 theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h : l <+ l₁ ++ l₂) : l <+ l₂ := by
@@ -425,7 +425,7 @@ theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h :
   obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
   have : l₁' = [] := by
     rw [eq_nil_iff_forall_not_mem]
-    exact fun x m => w x (mem_append_of_mem_left l₂' m) (h₁.mem m)
+    exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)
   simp_all
 
 theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂ := by

src/Init/Meta.lean

@@ -431,21 +431,20 @@ def getSubstring? (stx : Syntax) (withLeading := true) (withTrailing := true) :
     }
   | _, _ => none
 
-@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
-  if i == 0 then
-    none
-  else
-    let i := i - 1
-    let v := a[i]!
+@[specialize] private partial def updateLast {α} (a : Array α) (f : α → Option α) (i : Fin (a.size + 1)) : Option (Array α) :=
+  match i with
+  | 0 => none
+  | ⟨i + 1, h⟩ =>
+    let v := a[i]'(Nat.succ_lt_succ_iff.mp h)
     match f v with
-    | some v => some <| a.set! i v
-    | none   => updateLast a f i
+    | some v => some <| a.set i v (Nat.succ_lt_succ_iff.mp h)
+    | none   => updateLast a f ⟨i, Nat.lt_of_succ_lt h⟩
 
 partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
   | atom _ val             => some <| atom info val
   | ident _ rawVal val pre => some <| ident info rawVal val pre
   | node info' k args      =>
-    match updateLast args (setTailInfoAux info) args.size with
+    match updateLast args (setTailInfoAux info) ⟨args.size, by simp⟩ with
     | some args => some <| node info' k args
     | none      => none
   | _                      => none

src/Init/NotationExtra.lean

@@ -22,28 +22,28 @@ syntax explicitBinders            := (ppSpace bracketedExplicitBinders)+ <|> unb
 
 open TSyntax.Compat in
 def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
-  let rec loop (i : Nat) (acc : Syntax) := do
+  let rec loop (i : Nat) (h : i ≤ idents.size) (acc : Syntax) := do
     match i with
     | 0   => pure acc
-    | i+1 =>
-      let ident := idents[i]![0]
+    | i + 1 =>
+      let ident := idents[i][0]
       let acc ← match ident.isIdent, type? with
         | true,  none      => `($combinator fun $ident => $acc)
         | true,  some type => `($combinator fun $ident : $type => $acc)
         | false, none      => `($combinator fun _ => $acc)
         | false, some type => `($combinator fun _ : $type => $acc)
-      loop i acc
-  loop idents.size body
+      loop i (Nat.le_of_succ_le h) acc
+  loop idents.size (by simp) body
 
 def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax :=
-  let rec loop (i : Nat) (acc : Syntax) := do
+  let rec loop (i : Nat) (h : i ≤ binders.size) (acc : Syntax) := do
     match i with
     | 0   => pure acc
     | i+1 =>
-      let idents := binders[i]![1].getArgs
-      let type   := binders[i]![3]
-      loop i (← expandExplicitBindersAux combinator idents (some type) acc)
-  loop binders.size body
+      let idents := binders[i][1].getArgs
+      let type   := binders[i][3]
+      loop i (Nat.le_of_succ_le h) (← expandExplicitBindersAux combinator idents (some type) acc)
+  loop binders.size (by simp) body
 
 def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
   let combinator := mkCIdentFrom (← getRef) combinatorDeclName

src/Init/System/Uri.lean

@@ -29,13 +29,13 @@ def decodeUri (uri : String) : String := Id.run do
   let len := rawBytes.size
   let mut i := 0
   let percent := '%'.toNat.toUInt8
-  while i < len do
-    let c := rawBytes[i]!
-    (decoded, i) := if c == percent && i + 1 < len then
-      let h1 := rawBytes[i + 1]!
+  while h : i < len do
+    let c := rawBytes[i]
+    (decoded, i) := if h₁ : c == percent ∧ i + 1 < len then
+      let h1 := rawBytes[i + 1]
       if let some hd1 := hexDigitToUInt8? h1 then
-        if i + 2 < len then
-          let h2 := rawBytes[i + 2]!
+        if h₂ : i + 2 < len then
+          let h2 := rawBytes[i + 2]
           if let some hd2 := hexDigitToUInt8? h2 then
             -- decode the hex digits into a byte.
             (decoded.push (hd1 * 16 + hd2), i + 3)

src/Lean/Compiler/IR/EmitC.lean

@@ -271,9 +271,9 @@ def emitTag (x : VarId) (xType : IRType) : M Unit := do
     emit x
 
 def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
-  if alts.size != 2 then none
-  else match alts[0]! with
-    | Alt.ctor c b => some (c.cidx, b, alts[1]!.body)
+  if h : alts.size ≠ 2 then none
+  else match alts[0] with
+    | Alt.ctor c b => some (c.cidx, b, alts[1].body)
     | _            => none
 
 def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit := do

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1172,8 +1172,8 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
     (needsPackedArgs? : Bool)  (llvmfn : LLVM.Value llvmctx) (params : Array Param) : M llvmctx Unit := do
   if needsPackedArgs? then do
       let argsp ← LLVM.getParam llvmfn 0 -- lean_object **args
-      for i in List.range params.size do
-          let param := params[i]!
+      for h : i in [:params.size] do
+          let param := params[i]
           -- argsi := (args + i)
           let argsi ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argsp #[← constIntUnsigned i] s!"packed_arg_{i}_slot"
           let llvmty ← toLLVMType param.ty
@@ -1182,15 +1182,16 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
           -- slot for arg[i] which is always void* ?
           let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}"
           LLVM.buildStore builder pv alloca
-          addVartoState params[i]!.x alloca llvmty
+          addVartoState param.x alloca llvmty
   else
       let n ← LLVM.countParams llvmfn
-      for i in (List.range n.toNat) do
-        let llvmty ← toLLVMType params[i]!.ty
+      for i in [:n.toNat] do
+        let param := params[i]!
+        let llvmty ← toLLVMType param.ty
         let alloca ← buildPrologueAlloca builder  llvmty s!"arg_{i}"
         let arg ← LLVM.getParam llvmfn (UInt64.ofNat i)
         let _ ← LLVM.buildStore builder arg alloca
-        addVartoState params[i]!.x alloca llvmty
+        addVartoState param.x alloca llvmty
 
 def emitDeclAux (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d : Decl) : M llvmctx Unit := do
   let env ← getEnv

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -54,7 +54,7 @@ abbrev Mask := Array (Option VarId)
 partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
   let done (_ : Unit)        := (bs ++ keep.reverse, mask)
   let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
-  if bs.size < 2 then done ()
+  if h : bs.size < 2 then done ()
   else
     let b := bs.back!
     match b with
@@ -62,7 +62,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
     | .vdecl _ _ (.uproj _ _) _   => keepInstr b
     | .inc z n c p _ =>
       if n == 0 then done () else
-      let b' := bs[bs.size - 2]!
+      let b' := bs[bs.size - 2]
       match b' with
       | .vdecl w _ (.proj i x) _ =>
         if w == z && y == x then

src/Lean/Compiler/LCNF/Basic.lean

@@ -366,10 +366,10 @@ to be updated.
 @[implemented_by updateFunDeclCoreImp] opaque FunDeclCore.updateCore (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
 def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
-  let found (i : Nat) := (cases.alts[i]!, { cases with alts := cases.alts.eraseIdx i })
-  if let some i := cases.alts.findIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
+  let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
+  if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
     found i
-  else if let some i := cases.alts.findIdx? fun | .default _ => true | _ => false then
+  else if let some i := cases.alts.findFinIdx? fun | .default _ => true | _ => false then
     found i
   else
     unreachable!

src/Lean/Compiler/LCNF/PassManager.lean

@@ -134,9 +134,9 @@ def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassIns
 
 def installAfter (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where
   install passes :=
-    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]!
-      return passes.insertAt! (idx + 1) (p passUnderTest)
+    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]
+      return passes.insertIdx (idx + 1) (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
@@ -145,9 +145,9 @@ def installAfterEach (targetName : Name) (p : Pass → Pass) : PassInstaller :=
 
 def installBefore (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0): PassInstaller where
   install passes :=
-    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]!
-      return passes.insertAt! idx (p passUnderTest)
+    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]
+      return passes.insertIdx idx (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -152,8 +152,8 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
       let specArgs? := getSpecializationArgs? (← getEnv) decl.name
       let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i
       let mut paramsInfo : Array SpecParamInfo := #[]
-      for i in [:decl.params.size] do
-        let param := decl.params[i]!
+      for h :i in [:decl.params.size] do
+        let param := decl.params[i]
         let info ←
           if contains i then
             pure .user
@@ -181,14 +181,14 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
       declsInfo := declsInfo.push paramsInfo
   if declsInfo.any fun paramsInfo => paramsInfo.any (· matches .user | .fixedInst | .fixedHO) then
     let m := mkFixedParamsMap decls
-    for i in [:decls.size] do
-      let decl := decls[i]!
+    for hi : i in [:decls.size] do
+      let decl := decls[i]
       let mut paramsInfo := declsInfo[i]!
       let some mask := m.find? decl.name | unreachable!
       trace[Compiler.specialize.info] "{decl.name} {mask}"
       paramsInfo := paramsInfo.zipWith mask fun info fixed => if fixed || info matches .user then info else .other
       for j in [:paramsInfo.size] do
-        let mut info  := paramsInfo[j]!
+        let mut info := paramsInfo[j]!
         if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then
           paramsInfo := paramsInfo.set! j .other
       if paramsInfo.any fun info => info matches .fixedInst | .fixedHO | .user then

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -499,8 +499,8 @@ where
       match app with
       | .fvar f =>
         let mut argsNew := #[]
-        for i in [arity : args.size] do
-          argsNew := argsNew.push (← visitAppArg args[i]!)
+        for h :i in [arity : args.size] do
+          argsNew := argsNew.push (← visitAppArg args[i])
         letValueToArg <| .fvar f argsNew
       | .erased | .type .. => return .erased
 

src/Lean/Compiler/Specialize.lean

@@ -26,13 +26,14 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
       if let some idx := arg.isNatLit? then
         if idx == 0 then throwErrorAt arg "invalid specialization argument index, index must be greater than 0"
         let idx := idx - 1
-        if idx >= argNames.size then
+        if h : idx >= argNames.size then
           throwErrorAt arg "invalid argument index, `{declName}` has #{argNames.size} arguments"
-        if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]!}` has already been specified as a specialization candidate"
-        result := result.push idx
+        else
+          if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]}` has already been specified as a specialization candidate"
+          result := result.push idx
       else
         let argName := arg.getId
-        if let some idx := argNames.getIdx? argName then
+        if let some idx := argNames.indexOf? argName then
           if result.contains idx then throwErrorAt arg "invalid specialization argument name `{argName}`, it has already been specified as a specialization candidate"
           result := result.push idx
         else

src/Lean/Data/PersistentHashMap.lean

@@ -233,10 +233,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let keys' := keys.feraseIdx idx
-      have keq := keys.size_feraseIdx idx
-      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
-      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
+      let keys' := keys.eraseIdx idx
+      have keq := keys.size_eraseIdx idx _
+      let vals' := vals.eraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_eraseIdx (Eq.ndrec idx heq) _
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       Node.collision keys' vals' (keq.trans (this.trans veq.symm))
     | none     => n

src/Lean/Elab/App.lean

@@ -1347,7 +1347,7 @@ where
     let mut unusableNamedArgs := unusableNamedArgs
     for x in xs, bInfo in bInfos do
       let xDecl ← x.mvarId!.getDecl
-      if let some idx := remainingNamedArgs.findIdx? (·.name == xDecl.userName) then
+      if let some idx := remainingNamedArgs.findFinIdx? (·.name == xDecl.userName) then
         /- If there is named argument with name `xDecl.userName`, then it is accounted for and we can't make use of it. -/
         remainingNamedArgs := remainingNamedArgs.eraseIdx idx
       else
@@ -1355,9 +1355,9 @@ where
           /- We found a type of the form (baseName ...).
              First, we check if the current argument is an explicit one,
              and if the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
-          if argIdx ≤ args.size && bInfo.isExplicit then
+          if h : argIdx ≤ args.size ∧ bInfo.isExplicit then
             /- We can insert `e` as an explicit argument -/
-            return (args.insertAt! argIdx (Arg.expr e), namedArgs)
+            return (args.insertIdx argIdx (Arg.expr e), namedArgs)
           else
             /- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible
                if there isn't an argument with the same name occurring before it. -/

src/Lean/Elab/BuiltinCommand.lean

@@ -211,7 +211,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
         else
           `(bracketedBinderF| {$id $[: $ty?]?})
       for id in ids.reverse do
-        if let some idx := binderIds.findIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
+        if let some idx := binderIds.findFinIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
           binderIds := binderIds.eraseIdx idx
           modifiedVarDecls := true
           varDeclsNew := varDeclsNew.push (← mkBinder id explicit)

src/Lean/Elab/Deriving/Util.lean

@@ -49,9 +49,9 @@ invoking ``mkInstImplicitBinders `BarClass foo #[`α, `n, `β]`` gives `` `([Bar
 def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) :=
   forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do
     let mut binders := #[]
-    for i in [:xs.size] do
+    for h : i in [:xs.size] do
       try
-        let x := xs[i]!
+        let x := xs[i]
         let c ← mkAppM className #[x]
         if (← isTypeCorrect c) then
           let argName := argNames[i]!
@@ -86,8 +86,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
 
 def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
   let mut letDecls := #[]
-  for i in [:ctx.typeInfos.size] do
-    let indVal       := ctx.typeInfos[i]!
+  for h : i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]
     let auxFunName   := ctx.auxFunNames[i]!
     let currArgNames ← mkInductArgNames indVal
     let numParams    := indVal.numParams

src/Lean/Elab/Do.lean

@@ -796,10 +796,10 @@ Note that we are not restricting the macro power since the
 actions to be in the same universe.
 -/
 private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
-  if elems.size == 0 then
+  if elems.size = 0 then
     mkUnit
-  else if elems.size == 1 then
-    return elems[0]!
+  else if h : elems.size = 1 then
+    return elems[0]
   else
     elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
       ``(MProd.mk $elem $tuple)
@@ -831,10 +831,10 @@ def isDoExpr? (doElem : Syntax) : Option Syntax :=
   We use this method when expanding the `for-in` notation.
 -/
 private def destructTuple (uvars : Array Var) (x : Syntax) (body : Syntax) : MacroM Syntax := do
-  if uvars.size == 0 then
+  if uvars.size = 0 then
     return body
-  else if uvars.size == 1 then
-    `(let $(uvars[0]!):ident := $x; $body)
+  else if h : uvars.size = 1 then
+    `(let $(uvars[0]):ident := $x; $body)
   else
     destruct uvars.toList x body
 where
@@ -1314,9 +1314,9 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
     else if liftMethodDelimiter k then
       return stx
     -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
-    else if args.size >= 2 && (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
+    else if h : args.size >= 2 ∧ (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
       let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
-      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]!
+      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]
       let args := args.set! 1 arg1
       return Syntax.node i k args
     else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
@@ -1518,7 +1518,7 @@ mutual
   -/
   partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
     let doForDecls := doFor[1].getSepArgs
-    if doForDecls.size > 1 then
+    if h : doForDecls.size > 1 then
       /-
         Expand
         ```

src/Lean/Elab/Frontend.lean

@@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
 where
   go initialSnap t commands :=
     let snap := t.get
-    let commands := commands.push snap.data
+    let commands := commands.push snap
     if let some next := snap.nextCmdSnap? then
       go initialSnap next.task commands
     else
@@ -115,9 +115,9 @@ where
       -- snapshots as they subsume any info trees reported incrementally by their children.
       let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
       return {
-        commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
-        parserState := snap.data.parserState
-        cmdPos := snap.data.parserState.pos
+        commandState := { snap.finishedSnap.get.cmdState with messages, infoState.trees := trees }
+        parserState := snap.parserState
+        cmdPos := snap.parserState.pos
         commands := commands.map (·.stx)
         inputCtx, initialSnap
       }
@@ -164,8 +164,8 @@ def runFrontend
     | return (← mkEmptyEnvironment, false)
 
   if let some out := trace.profiler.output.get? opts then
-    let traceState := cmdState.traceState
-    let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
+    let traceStates := snaps.getAll.map (·.traces)
+    let profile ← Firefox.Profile.export mainModuleName.toString startTime traceStates opts
     IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
 
   let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)

src/Lean/Elab/Inductive.lean

@@ -173,15 +173,15 @@ private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
       throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
 private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
-  if views.size > 1 then
-    let levelNames := views[0]!.levelNames
+  if h : views.size > 1 then
+    let levelNames := views[0].levelNames
     for view in views do
       unless view.levelNames == levelNames do
         throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
 private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
-  if rs.size > 1 then
-    let levelNames := rs[0]!.levelNames
+  if h : rs.size > 1 then
+    let levelNames := rs[0].levelNames
     for r in rs do
       unless r.levelNames == levelNames do
         throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
@@ -433,8 +433,8 @@ where
         let mut args := e.getAppArgs
         unless args.size ≥ params.size do
           throwError "unexpected inductive type occurrence{indentExpr e}"
-        for i in [:params.size] do
-          let param := params[i]!
+        for h : i in [:params.size] do
+          let param := params[i]
           let arg := args[i]!
           unless (← isDefEq param arg) do
             throwError "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
@@ -694,8 +694,8 @@ private def collectLevelParamsInInductive (indTypes : List InductiveType) : Arra
 private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := Id.run do
   let levelParams := levelNames.map mkLevelParam;
   let mut m : ExprMap Expr := {}
-  for i in [:views.size] do
-    let view    := views[i]!
+  for h : i in [:views.size] do
+    let view    := views[i]
     let indFVar := indFVars[i]!
     m := m.insert indFVar (mkConst view.declName levelParams)
   return m
@@ -856,9 +856,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
     withInductiveLocalDecls rs fun params indFVars => do
       trace[Elab.inductive] "indFVars: {indFVars}"
       let mut indTypesArray := #[]
-      for i in [:views.size] do
+      for h : i in [:views.size] do
         let indFVar := indFVars[i]!
-        Term.addLocalVarInfo views[i]!.declId indFVar
+        Term.addLocalVarInfo views[i].declId indFVar
         let r     := rs[i]!
         /- At this point, because of `withInductiveLocalDecls`, the only fvars that are in context are the ones related to the first inductive type.
            Because of this, we need to replace the fvars present in each inductive type's header of the mutual block with those of the first inductive.

src/Lean/Elab/LetRec.lean

@@ -87,8 +87,8 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
   view.decls.mapM fun view => do
     forallBoundedTelescope view.type view.binderIds.size fun xs type => do
       -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
-      for i in [0:view.binderIds.size] do
-        addLocalVarInfo view.binderIds[i]! xs[i]!
+      for h : i in [0:view.binderIds.size] do
+        addLocalVarInfo view.binderIds[i] xs[i]!
       withDeclName view.declName do
         withInfoContext' view.valStx
           (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·))

src/Lean/Elab/Match.lean

@@ -282,8 +282,8 @@ where
         let dArg := dArgs[i]!
         unless (← isDefEq tArg dArg) do
           return i :: (← goType tArg dArg)
-      for i in [info.numParams : tArgs.size] do
-        let tArg := tArgs[i]!
+      for h : i in [info.numParams : tArgs.size] do
+        let tArg := tArgs[i]
         let dArg := dArgs[i]!
         unless (← isDefEq tArg dArg) do
           return i :: (← goIndex tArg dArg)

src/Lean/Elab/Open.lean

@@ -49,12 +49,12 @@ private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) :
       exs := exs.push ex
   if exs.size == nss.length then
     withRef idStx do
-      if exs.size == 1 then
-        throw exs[0]!
+      if h : exs.size = 1 then
+        throw exs[0]
       else
         throwErrorWithNestedErrors "failed to open" exs
-  if result.size == 1 then
-    return result[0]!
+  if h : result.size = 1 then
+    return result[0]
   else
     withRef idStx do throwError "ambiguous identifier '{idStx.getId}', possible interpretations: {result.map mkConst}"
 

src/Lean/Elab/PatternVar.lean

@@ -332,9 +332,9 @@ where
     else
       let accessible := isNextArgAccessible ctx
       let (d, ctx)   := getNextParam ctx
-      match ctx.namedArgs.findIdx? fun namedArg => namedArg.name == d.1 with
+      match ctx.namedArgs.findFinIdx? fun namedArg => namedArg.name == d.1 with
       | some idx =>
-        let arg := ctx.namedArgs[idx]!
+        let arg := ctx.namedArgs[idx]
         let ctx := { ctx with namedArgs := ctx.namedArgs.eraseIdx idx }
         let ctx ← pushNewArg accessible ctx arg.val
         processCtorAppContext ctx

src/Lean/Elab/PreDefinition/Basic.lean

@@ -244,8 +244,8 @@ def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do
     lambdaTelescope preDef.value fun xs _ => return xs.size
   forallBoundedTelescope preDefs[0]!.type arities[0]!  fun _ type₀ => do
     let u₀ ← getLevel type₀
-    for i in [1:preDefs.size] do
-      forallBoundedTelescope preDefs[i]!.type arities[i]! fun _ typeᵢ =>
+    for h : i in [1:preDefs.size] do
+      forallBoundedTelescope preDefs[i].type arities[i]! fun _ typeᵢ =>
       unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do
         withOptions (fun o => pp.sanitizeNames.set o false) do
           throwError m!"invalid mutual definition, result types must be in the same universe " ++

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

@@ -292,9 +292,9 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
     let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
-    let some poss := positions.find? (·.contains fnIdx)
+    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
-    let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
+    let brecOn ← PProdN.proj size idx brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)
 
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -53,10 +53,10 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
     (hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
   assert! extraParams ≤ arity
 
-  if hint.vars.size > extraParams then
+  if h : hint.vars.size > extraParams then
     let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
       m!"{funName} only binds {parameters extraParams}."
-    if let `($ident:ident) := hint.vars[0]! then
+    if let `($ident:ident) := hint.vars[0] then
       if ident.getId.isSuffixOf funName then
           msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
             "expects the function name here.)"

src/Lean/Elab/PreDefinition/TerminationHint.lean

@@ -90,10 +90,10 @@ lambda of `value`, and throws appropriate errors.
 -/
 def TerminationBy.checkVars (funName : Name) (extraParams : Nat) (tb : TerminationBy) : MetaM Unit := do
   unless tb.synthetic do
-    if tb.vars.size > extraParams then
+    if h : tb.vars.size > extraParams then
       let mut msg := m!"{parameters tb.vars.size} bound in `termination_by`, but the body of " ++
         m!"{funName} only binds {parameters extraParams}."
-      if let `($ident:ident) := tb.vars[0]! then
+      if let `($ident:ident) := tb.vars[0] then
         if ident.getId.isSuffixOf funName then
             msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
               "expects the function name here.)"

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

@@ -21,8 +21,8 @@ open Meta
 private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition)  : TermElabM Unit := do
   let us := preDefNonRec.levelParams.map mkLevelParam
   let all := preDefs.toList.map (·.declName)
-  for fidx in [:preDefs.size] do
-    let preDef := preDefs[fidx]!
+  for h : fidx in [:preDefs.size] do
+    let preDef := preDefs[fidx]
     let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
       let value := mkAppN (mkConst preDefNonRec.declName us) xs
       let value ← argsPacker.curryProj value fidx

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

@@ -40,7 +40,7 @@ private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames
     return TransformStep.done e
   let declName := f.constName!
   let us       := f.constLevels!
-  if let some fidx := funNames.getIdx? declName then
+  if let some fidx := funNames.indexOf? declName then
     let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
     let e' ← withAppN arity e fun args => do
       let fixedArgs := args[:fixedPrefix]

src/Lean/Elab/Quotation.lean

@@ -58,7 +58,7 @@ partial def mkTuple : Array Syntax → TermElabM Syntax
   | #[]  => `(Unit.unit)
   | #[e] => return e
   | es   => do
-    let stx ← mkTuple (es.eraseIdx 0)
+    let stx ← mkTuple (es.eraseIdxIfInBounds 0)
     `(Prod.mk $(es[0]!) $stx)
 
 def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name × List String) :=

src/Lean/Elab/Syntax.lean

@@ -19,12 +19,12 @@ def expandOptPrecedence (stx : Syntax) : MacroM (Option Nat) :=
     return some (← evalPrec stx[0][1])
 
 private def mkParserSeq (ds : Array (Term × Nat)) : TermElabM (Term × Nat) := do
-  if ds.size == 0 then
+  if h₀ : ds.size = 0 then
     throwUnsupportedSyntax
-  else if ds.size == 1 then
-    pure ds[0]!
+  else if h₁ : ds.size = 1 then
+    pure ds[0]
   else
-    let mut (r, stackSum) := ds[0]!
+    let mut (r, stackSum) := ds[0]
     for (d, stackSz) in ds[1:ds.size] do
       r ← `(ParserDescr.binary `andthen $r $d)
       stackSum := stackSum + stackSz
@@ -142,7 +142,7 @@ where
     let args := stx.getArgs
     if (← checkLeftRec stx[0]) then
       if args.size == 1 then throwErrorAt stx "invalid atomic left recursive syntax"
-      let args := args.eraseIdx 0
+      let args := args.eraseIdxIfInBounds 0
       let args ← args.mapM fun arg => withNestedParser do process arg
       mkParserSeq args
     else

src/Lean/Elab/SyntheticMVars.lean

@@ -149,8 +149,8 @@ where
         -- Succeeded. Collect new TC problems
         trace[Elab.defaultInstance] "isDefEq worked {mkMVar mvarId} : {← inferType (mkMVar mvarId)} =?= {candidate} : {← inferType candidate}"
         let mut pending := []
-        for i in [:bis.size] do
-          if bis[i]! == BinderInfo.instImplicit then
+        for h : i in [:bis.size] do
+          if bis[i] == BinderInfo.instImplicit then
             pending := mvars[i]!.mvarId! :: pending
         synthesizePending pending
       else

src/Lean/Elab/Tactic/Basic.lean

@@ -218,7 +218,7 @@ where
                     let old ← snap.old?
                     -- If the kind is equal, we can assume the old version was a macro as well
                     guard <| old.stx.isOfKind stx.getKind
-                    let state ← old.val.get.data.finished.get.state?
+                    let state ← old.val.get.finished.get.state?
                     guard <| state.term.meta.core.nextMacroScope == nextMacroScope
                     -- check absence of traces; see Note [Incremental Macros]
                     guard <| state.term.meta.core.traceState.traces.size == 0
@@ -226,9 +226,10 @@ where
                     return old.val.get
                   Language.withAlwaysResolvedPromise fun promise => do
                     -- Store new unfolding in the snapshot tree
-                    snap.new.resolve <| .mk {
+                    snap.new.resolve {
                       stx := stx'
                       diagnostics := .empty
+                      inner? := none
                       finished := .pure {
                         diagnostics := .empty
                         state? := (← Tactic.saveState)
@@ -240,7 +241,7 @@ where
                       new := promise
                       old? := do
                         let old ← old?
-                        return ⟨old.data.stx, (← old.data.next.get? 0)⟩
+                        return ⟨old.stx, (← old.next.get? 0)⟩
                     } }) do
                       evalTactic stx'
                   return

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -60,7 +60,7 @@ where
     if let some snap := (← readThe Term.Context).tacSnap? then
       if let some old := snap.old? then
         let oldParsed := old.val.get
-        oldInner? := oldParsed.data.inner? |>.map (⟨oldParsed.data.stx, ·⟩)
+        oldInner? := oldParsed.inner? |>.map (⟨oldParsed.stx, ·⟩)
     -- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script
     Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do
       let some snap := (← readThe Term.Context).tacSnap?
@@ -70,10 +70,10 @@ where
       if let some old := snap.old? then
         -- `tac` must be unchanged given the narrow above; let's reuse `finished`'s state!
         let oldParsed := old.val.get
-        if let some state := oldParsed.data.finished.get.state? then
+        if let some state := oldParsed.finished.get.state? then
           reusableResult? := some ((), state)
           -- only allow `next` reuse in this case
-          oldNext? := oldParsed.data.next.get? 0 |>.map (⟨old.stx, ·⟩)
+          oldNext? := oldParsed.next.get? 0 |>.map (⟨old.stx, ·⟩)
 
       -- For `tac`'s snapshot task range, disregard synthetic info as otherwise
       -- `SnapshotTree.findInfoTreeAtPos` might choose the wrong snapshot: for example, when
@@ -89,7 +89,7 @@ where
       withAlwaysResolvedPromise fun next => do
         withAlwaysResolvedPromise fun finished => do
           withAlwaysResolvedPromise fun inner => do
-            snap.new.resolve <| .mk {
+            snap.new.resolve {
               desc := tac.getKind.toString
               diagnostics := .empty
               stx := tac

src/Lean/Elab/Tactic/Induction.lean

@@ -282,10 +282,11 @@ where
         -- them, eventually put each of them back in `Context.tacSnap?` in `applyAltStx`
         withAlwaysResolvedPromise fun finished => do
           withAlwaysResolvedPromises altStxs.size fun altPromises => do
-            tacSnap.new.resolve <| .mk {
+            tacSnap.new.resolve {
               -- save all relevant syntax here for comparison with next document version
               stx := mkNullNode altStxs
               diagnostics := .empty
+              inner? := none
               finished := { range? := none, task := finished.result }
               next := altStxs.zipWith altPromises fun stx prom =>
                 { range? := stx.getRange?, task := prom.result }
@@ -298,7 +299,7 @@ where
                 let old := old.val.get
                 -- use old version of `mkNullNode altsSyntax` as guard, will be compared with new
                 -- version and picked apart in `applyAltStx`
-                return ⟨old.data.stx, (← old.data.next[i]?)⟩
+                return ⟨old.stx, (← old.next[i]?)⟩
               new := prom
             }
             finished.resolve { diagnostics := .empty, state? := (← saveState) }
@@ -340,9 +341,9 @@ where
     for h : altStxIdx in [0:altStxs.size] do
       let altStx := altStxs[altStxIdx]
       let altName := getAltName altStx
-      if let some i := alts.findIdx? (·.1 == altName) then
+      if let some i := alts.findFinIdx? (·.1 == altName) then
         -- cover named alternative
-        applyAltStx tacSnaps altStxIdx altStx alts[i]!
+        applyAltStx tacSnaps altStxIdx altStx alts[i]
         alts := alts.eraseIdx i
       else if !alts.isEmpty && isWildcard altStx then
         -- cover all alternatives

src/Lean/Elab/Term.lean

@@ -230,7 +230,7 @@ instance : ToSnapshotTree TacticFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- Snapshot just before execution of a tactic. -/
-structure TacticParsedSnapshotData (TacticParsedSnapshot : Type) extends Language.Snapshot where
+structure TacticParsedSnapshot extends Language.Snapshot where
   /-- Syntax tree of the tactic, stored and compared for incremental reuse. -/
   stx      : Syntax
   /-- Task for nested incrementality, if enabled for tactic. -/
@@ -240,16 +240,9 @@ structure TacticParsedSnapshotData (TacticParsedSnapshot : Type) extends Languag
   /-- Tasks for subsequent, potentially parallel, tactic steps. -/
   next     : Array (SnapshotTask TacticParsedSnapshot) := #[]
 deriving Inhabited
-
-/-- State after execution of a single synchronous tactic step. -/
-inductive TacticParsedSnapshot where
-  | mk (data : TacticParsedSnapshotData TacticParsedSnapshot)
-deriving Inhabited
-abbrev TacticParsedSnapshot.data : TacticParsedSnapshot → TacticParsedSnapshotData TacticParsedSnapshot
-  | .mk data => data
 partial instance : ToSnapshotTree TacticParsedSnapshot where
   toSnapshotTree := go where
-    go := fun ⟨s⟩ => ⟨s.toSnapshot,
+    go := fun s => ⟨s.toSnapshot,
       s.inner?.toArray.map (·.map (sync := true) go) ++
       #[s.finished.map (sync := true) toSnapshotTree] ++
       s.next.map (·.map (sync := true) go)⟩

src/Lean/Environment.lean

@@ -317,8 +317,8 @@ partial def ensureExtensionsArraySize (exts : Array EnvExtensionState) : IO (Arr
 where
   loop (i : Nat) (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do
     let envExtensions ← envExtensionsRef.get
-    if i < envExtensions.size then
-      let s ← envExtensions[i]!.mkInitial
+    if h : i < envExtensions.size then
+      let s ← envExtensions[i].mkInitial
       let exts := exts.push s
       loop (i + 1) exts
     else
@@ -726,7 +726,6 @@ def mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Name Nat) := do
   let descrs ← persistentEnvExtensionsRef.get
   let mut result := {}
   for h : i in [startingAt : descrs.size] do
-    have : i < descrs.size := h.upper
     let descr := descrs[i]
     result := result.insert descr.name i
   return result
@@ -740,7 +739,6 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/
   let extNameIdx ← mkExtNameMap startingAt
   for h : modIdx in [:mods.size] do
-    have : modIdx < mods.size := h.upper
     let mod := mods[modIdx]
     for (extName, entries) in mod.entries do
       if let some entryIdx := extNameIdx[extName]? then
@@ -860,7 +858,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.empty (capacity := numConsts)
   let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.empty (capacity := numConsts)
   for h : modIdx in [0:s.moduleData.size] do
-    let mod := s.moduleData[modIdx]'h.upper
+    let mod := s.moduleData[modIdx]
     for cname in mod.constNames, cinfo in mod.constants do
       match constantMap.getThenInsertIfNew? cname cinfo with
       | (cinfoPrev?, constantMap') =>

src/Lean/Language/Basic.lean

@@ -56,6 +56,11 @@ structure Snapshot where
   /-- General elaboration metadata produced by this step. -/
   infoTree? : Option Elab.InfoTree := none
   /--
+  Trace data produced by this step. Currently used only by `trace.profiler.output`, otherwise we
+  depend on the elaborator adding traces to `diagnostics` eventually.
+  -/
+  traces : TraceState := {}
+  /--
   Whether it should be indicated to the user that a fatal error (which should be part of
   `diagnostics`) occurred that prevents processing of the remainder of the file.
   -/

src/Lean/Language/Lean.lean

@@ -348,7 +348,7 @@ where
         if let some (some processed) ← old.processedResult.get? then
           -- ...and the edit location is after the next command (see note [Incremental Parsing])...
           if let some nextCom ← processed.firstCmdSnap.get? then
-            if (← isBeforeEditPos nextCom.data.parserState.pos) then
+            if (← isBeforeEditPos nextCom.parserState.pos) then
               -- ...go immediately to next snapshot
               return (← unchanged old old.stx oldSuccess.parserState)
 
@@ -470,20 +470,20 @@ where
       -- from `old`
       if let some oldNext := old.nextCmdSnap? then do
         let newProm ← IO.Promise.new
-        let _ ← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
+        let _ ← old.finishedSnap.bindIO (sync := true) fun oldFinished =>
           -- also wait on old command parse snapshot as parsing is cheap and may allow for
           -- elaboration reuse
           oldNext.bindIO (sync := true) fun oldNext => do
             parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx
             return .pure ()
-        prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result })
+        prom.resolve <| { old with nextCmdSnap? := some { range? := none, task := newProm.result } }
       else prom.resolve old  -- terminal command, we're done!
 
     -- fast path, do not even start new task for this snapshot
     if let some old := old? then
       if let some nextCom ← old.nextCmdSnap?.bindM (·.get?) then
-        if (← isBeforeEditPos nextCom.data.parserState.pos) then
-          return (← unchanged old old.data.parserState)
+        if (← isBeforeEditPos nextCom.parserState.pos) then
+          return (← unchanged old old.parserState)
 
     let beginPos := parserState.pos
     let scope := cmdState.scopes.head!
@@ -500,7 +500,7 @@ where
       -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
       -- only that whitespace changes, which is wasteful but still necessary because it may
       -- influence the range of error messages such as from a trailing `exact`
-      if stx.eqWithInfo old.data.stx then
+      if stx.eqWithInfo old.stx then
         -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
         return (← unchanged old parserState)
       -- on first change, make sure to cancel old invocation
@@ -515,11 +515,12 @@ where
       -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
       -- (as no-one should look at this result in that case) but anything containing `Environment`
       -- is not `Inhabited`
-      prom.resolve <| .mk (nextCmdSnap? := none) {
+      prom.resolve <| {
         diagnostics := .empty, stx := .missing, parserState
         elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
         finishedSnap := .pure { diagnostics := .empty, cmdState }
         tacticCache := (← IO.mkRef {})
+        nextCmdSnap? := none
       }
       return
 
@@ -537,29 +538,30 @@ where
       -- irrelevant in this case.
       let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
       let finishedSnap := { range? := endRange?, task := finishedPromise.result }
-      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
+      let tacticCache ← old?.map (·.tacticCache) |>.getDM (IO.mkRef {})
 
       let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
       let next? ← if Parser.isTerminalCommand stx then pure none
         -- for now, wait on "command finished" snapshot before parsing next command
         else some <$> IO.Promise.new
+      let nextCmdSnap? := next?.map
+        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })
       let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
-      let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
-        diagnostics
-        stx := .missing
-        parserState := {}
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
-        tacticCache
-      } else {
-        diagnostics, stx, parserState, tacticCache
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
-      }
-      prom.resolve <| .mk (nextCmdSnap? := next?.map
-        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
+      if minimalSnapshots && !Parser.isTerminalCommand stx then
+        prom.resolve {
+          diagnostics, finishedSnap, tacticCache, nextCmdSnap?
+          stx := .missing
+          parserState := {}
+          elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+        }
+      else
+        prom.resolve {
+          diagnostics, stx, parserState, tacticCache, nextCmdSnap?
+          elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+          finishedSnap
+        }
       let cmdState ← doElab stx cmdState beginPos
-        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
+        { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise }
         finishedPromise tacticCache ctx
       if let some next := next? then
         -- We're definitely off the fast-forwarding path now
@@ -571,7 +573,7 @@ where
       LeanProcessingM Command.State := do
     let ctx ← read
     let scope := cmdState.scopes.head!
-    let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
+    let cmdStateRef ← IO.mkRef { cmdState with messages := .empty, traceState := {} }
     /-
     The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
     has exclusive access to the cache, we create a fresh reference here. Before this change, the
@@ -613,6 +615,7 @@ where
     finishedPromise.resolve {
       diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
       infoTree? := infoTree
+      traces := cmdState.traceState
       cmdState := if cmdline then {
         env := Runtime.markPersistent cmdState.env
         maxRecDepth := 0
@@ -644,6 +647,6 @@ where goCmd snap :=
   if let some next := snap.nextCmdSnap? then
     goCmd next.get
   else
-    snap.data.finishedSnap.get.cmdState
+    snap.finishedSnap.get.cmdState
 
 end Lean

src/Lean/Language/Lean/Types.lean

@@ -34,7 +34,7 @@ instance : ToSnapshotTree CommandFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- State after a command has been parsed. -/
-structure CommandParsedSnapshotData extends Snapshot where
+structure CommandParsedSnapshot extends Snapshot where
   /-- Syntax tree of the command. -/
   stx : Syntax
   /-- Resulting parser state. -/
@@ -48,27 +48,14 @@ structure CommandParsedSnapshotData extends Snapshot where
   finishedSnap : SnapshotTask CommandFinishedSnapshot
   /-- Cache for `save`; to be replaced with incrementality. -/
   tacticCache : IO.Ref Tactic.Cache
+  /-- Next command, unless this is a terminal command. -/
+  nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot)
 deriving Nonempty
-
-/-- State after a command has been parsed. -/
--- workaround for lack of recursive structures
-inductive CommandParsedSnapshot where
-  /-- Creates a command parsed snapshot. -/
-  | mk (data : CommandParsedSnapshotData)
-    (nextCmdSnap? : Option (SnapshotTask CommandParsedSnapshot))
-deriving Nonempty
-/-- The snapshot data. -/
-abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
-  | mk data _ => data
-/-- Next command, unless this is a terminal command. -/
-abbrev CommandParsedSnapshot.nextCmdSnap? : CommandParsedSnapshot →
-    Option (SnapshotTask CommandParsedSnapshot)
-  | mk _ next? => next?
 partial instance : ToSnapshotTree CommandParsedSnapshot where
   toSnapshotTree := go where
-    go s := ⟨s.data.toSnapshot,
-      #[s.data.elabSnap.map (sync := true) toSnapshotTree,
-        s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
+    go s := ⟨s.toSnapshot,
+      #[s.elabSnap.map (sync := true) toSnapshotTree,
+        s.finishedSnap.map (sync := true) toSnapshotTree] |>
         pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
 
 /-- State after successful importing. -/

src/Lean/Message.lean

@@ -244,8 +244,8 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
       | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}"
     formatAux nCtx ctx? msg
 
-protected def format (msgData : MessageData) : IO Format :=
-  formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData
+protected def format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : IO Format :=
+  formatAux { currNamespace := Name.anonymous, openDecls := [] } ctx? msgData
 
 protected def toString (msgData : MessageData) : IO String := do
   return toString (← msgData.format)

src/Lean/Meta/CongrTheorems.lean

@@ -122,8 +122,8 @@ def mkHCongr (f : Expr) : MetaM CongrTheorem := do
 private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do
   let mut kinds := kinds
   for i in [:info.paramInfo.size] do
-    for j in [i+1:info.paramInfo.size] do
-      if info.paramInfo[j]!.backDeps.contains i then
+    for hj : j in [i+1:info.paramInfo.size] do
+      if info.paramInfo[j].backDeps.contains i then
         if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then
           -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed.
           kinds := kinds.set! i CongrArgKind.fixed

src/Lean/Meta/ExprDefEq.lean

@@ -255,8 +255,8 @@ private def isDefEqArgsFirstPass
     (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : MetaM DefEqArgsFirstPassResult := do
   let mut postponedImplicit := #[]
   let mut postponedHO := #[]
-  for i in [:paramInfo.size] do
-    let info := paramInfo[i]!
+  for h : i in [:paramInfo.size] do
+    let info := paramInfo[i]
     let a₁ := args₁[i]!
     let a₂ := args₂[i]!
     if info.dependsOnHigherOrderOutParam || info.higherOrderOutParam then
@@ -939,29 +939,6 @@ def check (hasCtxLocals : Bool) (mctx : MetavarContext) (lctx : LocalContext) (m
 
 end CheckAssignmentQuick
 
-/--
-Auxiliary function used at `typeOccursCheckImp`.
-Given `type`, it tries to eliminate "dependencies". For example, suppose we are trying to
-perform the assignment `?m := f (?n a b)` where
-```
-?n : let k := g ?m; A -> h k ?m -> C
-```
-If we just perform occurs check `?m` at the type of `?n`, we get a failure, but
-we claim these occurrences are ok because the type `?n a b : C`.
-In the example above, `typeOccursCheckImp` invokes this function with `n := 2`.
-Note that we avoid using `whnf` and `inferType` at `typeOccursCheckImp` to minimize the
-performance impact of this extra check.
-
-See test `typeOccursCheckIssue.lean` for an example where this refinement is needed.
-The test is derived from a Mathlib file.
--/
-private partial def skipAtMostNumBinders (type : Expr) (n : Nat) : Expr :=
-  match type, n with
-  | .forallE _ _ b _, n+1 => skipAtMostNumBinders b n
-  | .mdata _ b,       n   => skipAtMostNumBinders b n
-  | .letE _ _ v b _,  n   => skipAtMostNumBinders (b.instantiate1 v) n
-  | type,             _   => type
-
 /-- `typeOccursCheck` implementation using unsafe (i.e., pointer equality) features. -/
 private unsafe def typeOccursCheckImp (mctx : MetavarContext) (mvarId : MVarId) (v : Expr) : Bool :=
   if v.hasExprMVar then
@@ -982,19 +959,11 @@ where
     -- this function assumes all assigned metavariables have already been
     -- instantiated.
     go.run' mctx
-  visitMVar (mvarId' : MVarId) (numArgs : Nat := 0) : Bool :=
+  visitMVar (mvarId' : MVarId) : Bool :=
     if let some mvarDecl := mctx.findDecl? mvarId' then
-      occursCheck (skipAtMostNumBinders mvarDecl.type numArgs)
+      occursCheck mvarDecl.type
     else
       false
-  visitApp (e : Expr) : StateM (PtrSet Expr) Bool :=
-    e.withApp fun f args => do
-      unless (← args.allM visit) do
-        return false
-      if f.isMVar then
-        return visitMVar f.mvarId! args.size
-      else
-        visit f
   visit (e : Expr) : StateM (PtrSet Expr) Bool := do
     if !e.hasExprMVar then
       return true
@@ -1003,7 +972,7 @@ where
     else match e with
       | .mdata _ b       => visit b
       | .proj _ _ s      => visit s
-      | .app ..          => visitApp e
+      | .app f a         => visit f <&&> visit a
       | .lam _ d b _     => visit d <&&> visit b
       | .forallE _ d b _ => visit d <&&> visit b
       | .letE _ t v b _  => visit t <&&> visit v <&&> visit b

src/Lean/Meta/ForEachExpr.lean

@@ -93,8 +93,8 @@ def setMVarUserNamesAt (e : Expr) (isTarget : Array Expr) : MetaM (Array MVarId)
   forEachExpr (← instantiateMVars e) fun e => do
     if e.isApp then
       let args := e.getAppArgs
-      for i in [:args.size] do
-        let arg := args[i]!
+      for h : i in [:args.size] do
+        let arg := args[i]
         if arg.isMVar && isTarget.contains arg then
           let mvarId := arg.mvarId!
           if (← mvarId.getDecl).userName.isAnonymous then

src/Lean/Meta/IndPredBelow.lean

@@ -83,7 +83,7 @@ where
       forallTelescopeReducing t fun xs s => do
         let motiveType ← instantiateForall motive xs[:numParams]
         withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do
-          mkForallFVars (xs.insertAt! numParams motive) s)
+          mkForallFVars (xs.insertIdxIfInBounds numParams motive) s)
 
   motiveType (indVal : InductiveVal) : MetaM Expr :=
     forallTelescopeReducing indVal.type fun xs _ => do

src/Lean/Meta/Match/MatchEqs.lean

@@ -129,9 +129,9 @@ where
           let typeNew := b.instantiate1 y
           if let some (_, lhs, rhs) ← matchEq? d then
             if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-               let some j  := ys.getIdx? lhs | unreachable!
+               let some j  := ys.indexOf? lhs | unreachable!
                let ys      := ys.eraseIdx j
-               let some k  := args.getIdx? lhs | unreachable!
+               let some k  := args.indexOf? lhs | unreachable!
                let mask    := mask.set! k false
                let args    := args.map fun arg => if arg == lhs then rhs else arg
                let arg     ← mkEqRefl rhs
@@ -557,8 +557,8 @@ where
         let mut minorBodyNew := minor
         -- We have to extend the mapping to make sure `convertTemplate` can "fix" occurrences of the refined minor premises
         let mut m ← read
-        for i in [:isAlt.size] do
-          if isAlt[i]! then
+        for h : i in [:isAlt.size] do
+          if isAlt[i] then
             -- `convertTemplate` will correct occurrences of the alternative
             let alt := args[6+i]! -- Recall that `Eq.ndrec` has 6 arguments
             let some (_, numParams, argMask) := m.find? alt.fvarId! | unreachable!

src/Lean/Meta/RecursorInfo.lean

@@ -107,7 +107,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     if motiveArgs.isEmpty then
       throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
     let major := motiveArgs.back!
-    match xs.getIdx? major with
+    match xs.indexOf? major with
     | some majorPos => pure (major, majorPos, true)
     | none          => throwError "ill-formed recursor '{declName}'"
 

src/Lean/Meta/Tactic/Clear.lean

@@ -27,7 +27,7 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
       throwTacticEx `clear mvarId m!"target depends on '{mkFVar fvarId}'"
     let lctx := lctx.erase fvarId
     let localInsts ← getLocalInstances
-    let localInsts := match localInsts.findIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
+    let localInsts := match localInsts.findFinIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
       | none => localInsts
       | some idx => localInsts.eraseIdx idx
     let newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type MetavarKind.syntheticOpaque tag

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -148,13 +148,13 @@ def mkCustomEliminator (elimName : Name) (induction : Bool) : MetaM CustomElimin
   let info ← getConstInfo elimName
   forallTelescopeReducing info.type fun xs _ => do
     let mut typeNames := #[]
-    for i in [:elimInfo.targetsPos.size] do
-      let targetPos := elimInfo.targetsPos[i]!
+    for hi : i in [:elimInfo.targetsPos.size] do
+      let targetPos := elimInfo.targetsPos[i]
       let x := xs[targetPos]!
       /- Return true if there is another target that depends on `x`. -/
       let isImplicitTarget : MetaM Bool := do
-        for j in [i+1:elimInfo.targetsPos.size] do
-          let y := xs[elimInfo.targetsPos[j]!]!
+        for hj : j in [i+1:elimInfo.targetsPos.size] do
+          let y := xs[elimInfo.targetsPos[j]]!
           let yType ← inferType y
           if (← dependsOn yType x.fvarId!) then
             return true

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -58,8 +58,9 @@ private partial def loop : M Bool := do
   modify fun s => { s with modified := false }
   let simprocs := (← get).simprocs
   -- simplify entries
-  for i in [:(← get).entries.size] do
-    let entry := (← get).entries[i]!
+  let entries := (← get).entries
+  for h : i in [:entries.size] do
+    let entry := entries[i]
     let ctx := (← get).ctx
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -146,8 +146,12 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
     indexConfig := mkIndexConfig config
   }
 
-def Context.setConfig (context : Context) (config : Config) : Context :=
-  { context with config }
+def Context.setConfig (context : Context) (config : Config) : MetaM Context := do
+  return { context with
+    config
+    metaConfig := (← mkMetaConfig config)
+    indexConfig := (← mkIndexConfig config)
+  }
 
 def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
   { c with simpTheorems }

src/Lean/Meta/Tactic/Split.lean

@@ -140,8 +140,8 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N
           let matcherApp := { matcherApp with discrs := discrVars }
           foundRef.set true
           let mut altsNew := #[]
-          for i in [:matcherApp.alts.size] do
-            let alt := matcherApp.alts[i]!
+          for h : i in [:matcherApp.alts.size] do
+            let alt := matcherApp.alts[i]
             let altNumParams := matcherApp.altNumParams[i]!
             let altNew ← lambdaTelescope alt fun xs body => do
               if xs.size < altNumParams || xs.size < numDiscrEqs then

src/Lean/Meta/Tactic/TryThis.lean

@@ -114,7 +114,7 @@ apply the replacement.
     unless params.range.start.line ≤ stxRange.end.line do return result
     let mut result := result
     for h : i in [:suggestionTexts.size] do
-      let (newText, title?) := suggestionTexts[i]'h.2
+      let (newText, title?) := suggestionTexts[i]
       let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
       result := result.push {
         eager.title := title

src/Lean/MetavarContext.lean

@@ -248,9 +248,7 @@ instance : Hashable LocalInstance where
 
 /-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`. -/
 def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : LocalInstances :=
-  match localInsts.findIdx? (fun inst => inst.fvar.fvarId! == fvarId) with
-  | some idx => localInsts.eraseIdx idx
-  | _        => localInsts
+  localInsts.eraseP (fun inst => inst.fvar.fvarId! == fvarId)
 
 /-- A kind for the metavariable that determines its unification behaviour.
 For more information see the large comment at the beginning of this file. -/
@@ -1061,7 +1059,7 @@ mutual
 
     Note: It is assumed that `xs` is the result of calling `collectForwardDeps` on a subset of variables in `lctx`.
   -/
-  private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) : M Expr := do
+  private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) (usedLetOnly : Bool) : M Expr := do
     let e ← abstractRangeAux xs xs.size e
     xs.size.foldRevM (init := e) fun i e => do
       let x := xs[i]!
@@ -1072,16 +1070,25 @@ mutual
           let type ← abstractRangeAux xs i type
           return Lean.mkForall n bi type e
         | LocalDecl.ldecl _ _ n type value nonDep _ =>
-          let type := type.headBeta
-          let type  ← abstractRangeAux xs i type
-          let value ← abstractRangeAux xs i value
-          let e := mkLet n type value e nonDep
-          match kind with
-          | MetavarKind.syntheticOpaque =>
-            -- See "Gruesome details" section in the beginning of the file
-            let e := e.liftLooseBVars 0 1
-            return mkForall n BinderInfo.default type e
-          | _ => pure e
+          if !usedLetOnly || e.hasLooseBVar 0 then
+            let type := type.headBeta
+            let type  ← abstractRangeAux xs i type
+            let value ← abstractRangeAux xs i value
+            let e := mkLet n type value e nonDep
+            match kind with
+            | MetavarKind.syntheticOpaque =>
+              -- See "Gruesome details" section in the beginning of the file
+              let e := e.liftLooseBVars 0 1
+              return mkForall n BinderInfo.default type e
+            | _ => pure e
+          else
+            match kind with
+            | MetavarKind.syntheticOpaque =>
+              let type := type.headBeta
+              let type  ← abstractRangeAux xs i type
+              return mkForall n BinderInfo.default type e
+            | _ =>
+              return e.lowerLooseBVars 1 1
       else
         -- `xs` may contain metavariables as "may dependencies" (see `findExprDependsOn`)
         let mvarDecl := (← get).mctx.getDecl x.mvarId!
@@ -1101,7 +1108,7 @@ mutual
 
     See details in the comment at the top of the file.
   -/
-  private partial def elimMVar (xs : Array Expr) (mvarId : MVarId) (args : Array Expr) : M (Expr × Array Expr) := do
+  private partial def elimMVar (xs : Array Expr) (mvarId : MVarId) (args : Array Expr) (usedLetOnly : Bool) : M (Expr × Array Expr) := do
     let mvarDecl  := (← getMCtx).getDecl mvarId
     let mvarLCtx  := mvarDecl.lctx
     let toRevert  := getInScope mvarLCtx xs
@@ -1129,7 +1136,7 @@ mutual
       let newMVarLCtx   := reduceLocalContext mvarLCtx toRevert
       let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x
       -- Remark: we must reset the cache before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs`
-      let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
+      let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type usedLetOnly
       let newMVarId    := { name := (← get).ngen.curr }
       let newMVar      := mkMVar newMVarId
       let result       := mkMVarApp mvarLCtx newMVar toRevert newMVarKind
@@ -1170,7 +1177,8 @@ mutual
         if (← read).mvarIdsToAbstract.contains mvarId then
           return mkAppN f (← args.mapM (visit xs))
         else
-          return (← elimMVar xs mvarId args).1
+          -- We set `usedLetOnly := true` to avoid unnecessary let binders in the new metavariable type.
+          return (← elimMVar xs mvarId args (usedLetOnly := true)).1
     | _ =>
       return mkAppN (← visit xs f) (← args.mapM (visit xs))
 
@@ -1192,7 +1200,9 @@ partial def elimMVarDeps (xs : Array Expr) (e : Expr) : M Expr :=
 -/
 partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr) :=
   withFreshCache do
-    elimMVar xs mvarId #[]
+    -- We set `usedLetOnly := false`, because in the `revert` tactic
+    -- we expect that reverting a let variable always results in a let binder.
+    elimMVar xs mvarId #[] (usedLetOnly := false)
 
 /--
   Similar to `Expr.abstractRange`, but handles metavariables correctly.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -349,7 +349,7 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
     if idx == 0 then
       -- If it's the first argument, then we can tag `obj.field` with the first app.
       head ← withBoundedAppFn (numArgs - 1) <| annotateTermInfo head
-    return Syntax.mkApp head (argStxs.eraseIdx idx)
+    return Syntax.mkApp head (argStxs.eraseIdxIfInBounds idx)
   else
     return Syntax.mkApp fnStx argStxs
 
@@ -876,7 +876,7 @@ def delabLam : Delab :=
           -- "default" binder group is the only one that expects binder names
           -- as a term, i.e. a single `Syntax.ident` or an application thereof
           let stxCurNames ←
-            if curNames.size > 1 then
+            if h : curNames.size > 1 then
               `($(curNames.get! 0) $(curNames.eraseIdx 0)*)
             else
               pure $ curNames.get! 0;

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -57,8 +57,8 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
   -- Search for the first argument that could be used for field notation
   -- and make sure it is the first explicit argument.
   forallBoundedTelescope info.type args.size fun params _ => do
-    for i in [0:params.size] do
-      let fvarId := params[i]!.fvarId!
+    for h : i in [0:params.size] do
+      let fvarId := params[i].fvarId!
       -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation.
       -- Plus, recursors tend to be riskier when using dot notation.
       if (← fvarId.getUserName) == `motive then

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -308,12 +308,12 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
     let args := e.getAppArgs
     let fType ← replaceLPsWithVars (← inferType e.getAppFn)
     let (mvars, bInfos, resultType) ← forallMetaBoundedTelescope fType e.getAppArgs.size
-    for i in [:mvars.size] do
+    for h : i in [:mvars.size] do
       if bInfos[i]! == BinderInfo.instImplicit then
-        inspectOutParams args[i]! mvars[i]!
+        inspectOutParams args[i]! mvars[i]
       else if bInfos[i]! == BinderInfo.default then
-        if ← isTrivialBottomUp args[i]! then tryUnify args[i]! mvars[i]!
-        else if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! (some mvars[i]!) fuel then tryUnify args[i]! mvars[i]!
+        if ← isTrivialBottomUp args[i]! then tryUnify args[i]! mvars[i]
+        else if ← typeUnknown mvars[i] <&&> canBottomUp args[i]! (some mvars[i]) fuel then tryUnify args[i]! mvars[i]
     if ← (pure (isHBinOp e) <&&> (valUnknown mvars[0]! <||> valUnknown mvars[1]!)) then tryUnify mvars[0]! mvars[1]!
     if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
     return !(← valUnknown resultType)
@@ -487,22 +487,22 @@ mutual
     collectBottomUps := do
       let { args, mvars, bInfos, ..} ← read
       for target in [fun _ => none, fun i => some mvars[i]!] do
-        for i in [:args.size] do
+        for h : i in [:args.size] do
           if bInfos[i]! == BinderInfo.default then
-            if ← typeUnknown mvars[i]! <&&> canBottomUp args[i]! (target i) then
+            if ← typeUnknown mvars[i]! <&&> canBottomUp args[i] (target i) then
               tryUnify args[i]! mvars[i]!
               modify fun s => { s with bottomUps := s.bottomUps.set! i true }
 
     checkOutParams := do
       let { args, mvars, bInfos, ..} ← read
-      for i in [:args.size] do
-        if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i]! mvars[i]!
+      for h : i in [:args.size] do
+        if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i] mvars[i]!
 
     collectHigherOrders := do
       let { args, mvars, bInfos, ..} ← read
-      for i in [:args.size] do
+      for h : i in [:args.size] do
         if !(bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
-        if !(← isHigherOrder (← inferType args[i]!)) then continue
+        if !(← isHigherOrder (← inferType args[i])) then continue
         if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue
 
         if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && !(← valUnknown mvars[i]!)
@@ -520,9 +520,9 @@ mutual
       -- motivation: prevent levels from printing in
       -- Boo.mk : {α : Type u_1} → {β : Type u_2} → α → β → Boo.{u_1, u_2} α β
       let { args, mvars, bInfos, ..} ← read
-      for i in [:args.size] do
+      for h : i in [:args.size] do
         if bInfos[i]! == BinderInfo.default then
-          if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i]! then
+          if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i] then
             tryUnify args[i]! mvars[i]!
             modify fun s => { s with bottomUps := s.bottomUps.set! i true }
 

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -33,9 +33,9 @@ def findCompletionCmdDataAtPos
     (pos : String.Pos)
     : Task (Option (Syntax × Elab.InfoTree)) :=
   findCmdDataAtPos doc (pos := pos) fun s => Id.run do
-    let some tailPos := s.data.stx.getTailPos?
+    let some tailPos := s.stx.getTailPos?
       | return false
-    return pos.byteIdx <= tailPos.byteIdx + s.data.stx.getTrailingSize
+    return pos.byteIdx <= tailPos.byteIdx + s.stx.getTrailingSize
 
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do

src/Lean/Server/FileWorker/Utils.lean

@@ -28,10 +28,10 @@ private partial def mkCmdSnaps (initSnap : Language.Lean.InitialSnapshot) :
     } <| .delayed <| headerSuccess.firstCmdSnap.task.bind go
 where
   go cmdParsed :=
-    cmdParsed.data.finishedSnap.task.map fun finished =>
+    cmdParsed.finishedSnap.task.map fun finished =>
       .ok <| .cons {
-        stx := cmdParsed.data.stx
-        mpState := cmdParsed.data.parserState
+        stx := cmdParsed.stx
+        mpState := cmdParsed.parserState
         cmdState := finished.cmdState
       } (match cmdParsed.nextCmdSnap? with
         | some next => .delayed <| next.task.bind go

src/Lean/Server/Requests.lean

@@ -204,7 +204,7 @@ partial def findInfoTreeAtPos
   findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun
     | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun
       | some infoTree => .pure <| some infoTree
-      | none          => cmdParsed.data.finishedSnap.task.map (sync := true) fun s =>
+      | none          => cmdParsed.finishedSnap.task.map (sync := true) fun s =>
         -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
         assert! s.cmdState.infoState.trees.size == 1
         some s.cmdState.infoState.trees[0]!
@@ -225,11 +225,11 @@ def findCmdDataAtPos
     : Task (Option (Syntax × Elab.InfoTree)) :=
   findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun
     | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun
-      | some infoTree => .pure <| some (cmdParsed.data.stx, infoTree)
-      | none          => cmdParsed.data.finishedSnap.task.map (sync := true) fun s =>
+      | some infoTree => .pure <| some (cmdParsed.stx, infoTree)
+      | none          => cmdParsed.finishedSnap.task.map (sync := true) fun s =>
         -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
         assert! s.cmdState.infoState.trees.size == 1
-        some (cmdParsed.data.stx, s.cmdState.infoState.trees[0]!)
+        some (cmdParsed.stx, s.cmdState.infoState.trees[0]!)
     | none => .pure none
 
 /--
@@ -244,7 +244,7 @@ def findInfoTreeAtPosWithTrailingWhitespace
     : Task (Option Elab.InfoTree) :=
   -- NOTE: use `>=` since the cursor can be *after* the input (and there is no interesting info on
   -- the first character of the subsequent command if any)
-  findInfoTreeAtPos doc (·.data.parserState.pos ≥ pos) pos
+  findInfoTreeAtPos doc (·.parserState.pos ≥ pos) pos
 
 open Elab.Command in
 def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do

src/Lean/Structure.lean

@@ -383,7 +383,7 @@ partial def computeStructureResolutionOrder [Monad m] [MonadEnv m]
   -- `resOrders` contains the resolution orders to merge.
   -- The parent list is inserted as a pseudo resolution order to ensure immediate parents come out in order,
   -- and it is added first to be the primary ordering constraint when there are ordering errors.
-  let mut resOrders := parentResOrders.insertAt 0 parentNames |>.filter (!·.isEmpty)
+  let mut resOrders := parentResOrders.insertIdx 0 parentNames |>.filter (!·.isEmpty)
 
   let mut resOrder : Array Name := #[structName]
   let mut defects : Array StructureResolutionOrderConflict := #[]

src/Lean/Syntax.lean

@@ -248,11 +248,11 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
   | Syntax.atom info val               => Syntax.atom (info.updateTrailing trailing) val
   | Syntax.ident info rawVal val pre   => Syntax.ident (info.updateTrailing trailing) rawVal val pre
   | n@(Syntax.node info k args)        =>
-    if args.size == 0 then n
+    if h : args.size = 0 then n
     else
      let i    := args.size - 1
-     let last := updateTrailing trailing args[i]!
-     let args := args.set! i last;
+     let last := updateTrailing trailing args[i]
+     let args := args.set i last;
      Syntax.node info k args
   | s => s
 

src/Lean/Util/Profiler.lean

@@ -12,7 +12,23 @@ namespace Lean.Firefox
 
 /-! Definitions from https://github.com/firefox-devtools/profiler/blob/main/src/types/profile.js -/
 
-abbrev Milliseconds := Float
+structure Milliseconds where
+  ms : Float
+deriving Inhabited
+
+instance : Coe Float Milliseconds := ⟨fun s => .mk (s * 1000)⟩
+instance : OfScientific Milliseconds := ⟨fun m s e => .mk (OfScientific.ofScientific m s e)⟩
+instance : ToJson Milliseconds where toJson x := toJson x.ms
+instance : FromJson Milliseconds where fromJson? j := Milliseconds.mk <$> fromJson? j
+instance : Add Milliseconds where add x y := ⟨x.ms + y.ms⟩
+
+structure Microseconds where
+  μs : Float
+
+instance : Coe Float Microseconds := ⟨fun s => .mk (s * 1000000)⟩
+instance : OfScientific Microseconds := ⟨fun m s e => .mk (OfScientific.ofScientific m s e)⟩
+instance : ToJson Microseconds where toJson x := toJson x.μs
+instance : FromJson Microseconds where fromJson? j := Microseconds.mk <$> fromJson? j
 
 structure Category where
   name : String
@@ -20,14 +36,22 @@ structure Category where
   subcategories : Array String := #[]
 deriving FromJson, ToJson
 
+structure SampleUnits where
+  time : String := "ms"
+  eventDelay : String := "ms"
+  threadCPUDelta : String := "µs"
+deriving FromJson, ToJson
+
 structure ProfileMeta where
-  interval : Milliseconds := 0  -- should be irrelevant with `tracing-ms`
+  interval : Milliseconds := 0.0  -- should be irrelevant with `tracing-ms`
   startTime : Milliseconds
   categories : Array Category := #[]
   processType : Nat := 0
   product : String := "lean"
   preprocessedProfileVersion : Nat := 48
   markerSchema : Array Json := #[]
+  -- without this field, no CPU usage is shown
+  sampleUnits : SampleUnits := {}
 deriving FromJson, ToJson
 
 structure StackTable where
@@ -43,6 +67,7 @@ structure SamplesTable where
   time : Array Milliseconds
   weight : Array Milliseconds
   weightType : String := "tracing-ms"
+  threadCPUDelta : Array Float
   length : Nat
 deriving FromJson, ToJson
 
@@ -109,11 +134,22 @@ def categories : Array Category := #[
   { name := "Meta", color := "yellow" }
 ]
 
+/-- Returns first `startTime` in the trace tree, if any. -/
+private partial def getFirstStart? : MessageData → Option Float
+    | .trace data _ children => do
+      if data.startTime != 0 then
+        return data.startTime
+      if let some startTime := children.findSome? getFirstStart? then
+        return startTime
+      none
+    | .withContext _ msg => getFirstStart? msg
+    | _ => none
+
 private partial def addTrace (pp : Bool) (thread : ThreadWithMaps) (trace : MessageData) :
     IO ThreadWithMaps :=
-  (·.2) <$> StateT.run (go none trace) thread
+  (·.2) <$> StateT.run (go none none trace) thread
 where
-  go parentStackIdx? : _ → StateT ThreadWithMaps IO Unit
+  go parentStackIdx? ctx? : _ → StateT ThreadWithMaps IO Unit
     | .trace data msg children => do
       if data.startTime == 0 then
         return  -- no time data, skip
@@ -121,7 +157,7 @@ where
       if !data.tag.isEmpty then
         funcName := s!"{funcName}: {data.tag}"
       if pp then
-        funcName := s!"{funcName}: {← msg.format}"
+        funcName := s!"{funcName}: {← msg.format ctx?}"
       let strIdx ← modifyGet fun thread =>
         if let some idx := thread.stringMap[funcName]? then
           (idx, thread)
@@ -165,40 +201,34 @@ where
             stackMap := thread.stackMap.insert (frameIdx, parentStackIdx?) thread.stackMap.size })
       modify fun thread => { thread with lastTime := data.startTime }
       for c in children do
-        if let some nextStart := getNextStart? c then
+        if let some nextStart := getFirstStart? c then
           -- add run time slice between children/before first child
+          -- a "slice" is always a pair of samples as otherwise Firefox Profiler interpolates
+          -- between adjacent samples in undesirable ways
           modify fun thread => { thread with samples := {
-            stack := thread.samples.stack.push stackIdx
-            time := thread.samples.time.push (thread.lastTime * 1000)
-            weight := thread.samples.weight.push ((nextStart - thread.lastTime) * 1000)
-            length := thread.samples.length + 1
+            stack := thread.samples.stack.push stackIdx |>.push stackIdx
+            time := thread.samples.time.push thread.lastTime |>.push nextStart
+            weight := thread.samples.weight.push 0.0 |>.push (nextStart - thread.lastTime)
+            threadCPUDelta := thread.samples.threadCPUDelta.push 0.0 |>.push (nextStart - thread.lastTime)
+            length := thread.samples.length + 2
           } }
-          go (some stackIdx) c
+          go (some stackIdx) ctx? c
       -- add remaining slice after last child
       modify fun thread => { thread with
         lastTime := data.stopTime
         samples := {
-          stack := thread.samples.stack.push stackIdx
-          time := thread.samples.time.push (thread.lastTime * 1000)
-          weight := thread.samples.weight.push ((data.stopTime - thread.lastTime) * 1000)
-          length := thread.samples.length + 1
+          stack := thread.samples.stack.push stackIdx |>.push stackIdx
+          time := thread.samples.time.push thread.lastTime |>.push data.stopTime
+          weight := thread.samples.weight.push 0.0 |>.push (data.stopTime - thread.lastTime)
+          threadCPUDelta := thread.samples.threadCPUDelta.push 0.0 |>.push (data.stopTime - thread.lastTime)
+          length := thread.samples.length + 2
         } }
-    | .withContext _ msg => go parentStackIdx? msg
+    | .withContext ctx msg => go parentStackIdx? (some ctx) msg
     | _ => return
-  /-- Returns first `startTime` in the trace tree, if any. -/
-  getNextStart?
-    | .trace data _ children => do
-      if data.startTime != 0 then
-        return data.startTime
-      if let some startTime := children.findSome? getNextStart? then
-        return startTime
-      none
-    | .withContext _ msg => getNextStart? msg
-    | _ => none
 
 def Thread.new (name : String) : Thread := {
   name
-  samples := { stack := #[], time := #[], weight := #[], length := 0 }
+  samples := { stack := #[], time := #[], weight := #[], threadCPUDelta := #[], length := 0 }
   stackTable := { frame := #[], «prefix» := #[], category := #[], subcategory := #[], length := 0 }
   frameTable := { func := #[], length := 0 }
   stringArray := #[]
@@ -207,17 +237,39 @@ def Thread.new (name : String) : Thread := {
     length := 0 }
 }
 
-def Profile.export (name : String) (startTime : Milliseconds) (traceState : TraceState)
+def Profile.export (name : String) (startTime : Float) (traceStates : Array TraceState)
     (opts : Options) : IO Profile := do
-  let thread := Thread.new name
-  -- wrap entire trace up to current time in `runFrontend` node
-  let trace := .trace {
-    cls := `runFrontend, startTime, stopTime := (← IO.monoNanosNow).toFloat / 1000000000,
-    collapsed := true } "" (traceState.traces.toArray.map (·.msg))
-  let thread ← addTrace (Lean.trace.profiler.output.pp.get opts) { thread with } trace
+  let tids := traceStates.groupByKey (·.tid)
+  let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
+  let threads ← tids.toArray.qsort (fun (t1, _) (t2, _) => t1 < t2) |>.mapM fun (tid, traceStates) => do
+    let mut thread := { Thread.new (if tid = 0 then name else toString tid) with isMainThread := tid = 0 }
+    let traces := traceStates.map (·.traces.toArray)
+    -- sort traces of thread by start time
+    let traces := traces.qsort (fun tr1 tr2 =>
+      let f tr := tr.get? 0 |>.bind (getFirstStart? ·.msg) |>.getD 0
+      f tr1 < f tr2)
+    let mut traces := traces.flatMap id |>.map (·.msg)
+    if tid = 0 then
+      -- wrap entire trace up to current time in `runFrontend` node
+      traces := #[.trace {
+        cls := `runFrontend, startTime, stopTime,
+        collapsed := true } "" traces]
+    for trace in traces do
+      if thread.lastTime > 0.0 then
+        if let some nextStart := getFirstStart? trace then
+          -- add 0% CPU run time slice between traces
+          thread := { thread with samples := {
+            stack := thread.samples.stack.push 0 |>.push 0
+            time := thread.samples.time.push thread.lastTime |>.push nextStart
+            weight := thread.samples.weight.push 0.0 |>.push 0.0
+            threadCPUDelta := thread.samples.threadCPUDelta.push 0.0 |>.push 0.0
+            length := thread.samples.length + 2
+          } }
+      thread ← addTrace (Lean.trace.profiler.output.pp.get opts) thread trace
+    return thread
   return {
     meta := { startTime, categories }
-    threads := #[thread.toThread]
+    threads := threads.map (·.toThread)
   }
 
 structure ThreadWithCollideMaps extends ThreadWithMaps where
@@ -240,19 +292,20 @@ where
         if let some idx := thread.sampleMap[stackIdx]? then
           -- imperative to preserve linear use of arrays here!
           let ⟨⟨⟨t1, t2, t3, samples, t5, t6, t7, t8, t9, t10⟩, o2, o3, o4, o5⟩, o6⟩ := thread
-          let ⟨s1, s2, weight, s3, s4⟩ := samples
+          let ⟨s1, s2, weight, s3, s4, s5⟩ := samples
           let weight := weight.set! idx <| weight[idx]! + add.samples.weight[oldSampleIdx]!
-          let samples := ⟨s1, s2, weight, s3, s4⟩
+          let samples := ⟨s1, s2, weight, s3, s4, s5⟩
           ⟨⟨⟨t1, t2, t3, samples, t5, t6, t7, t8, t9, t10⟩, o2, o3, o4, o5⟩, o6⟩
         else
           -- imperative to preserve linear use of arrays here!
           let ⟨⟨⟨t1, t2, t3, samples, t5, t6, t7, t8, t9, t10⟩, o2, o3, o4, o5⟩, sampleMap⟩ :=
             thread
-          let ⟨stack, time, weight, _, length⟩ := samples
+          let ⟨stack, time, weight, _, threadCPUDelta, length⟩ := samples
           let samples := {
               stack := stack.push stackIdx
               time := time.push time.size.toFloat
               weight := weight.push add.samples.weight[oldSampleIdx]!
+              threadCPUDelta := threadCPUDelta.push 1
               length := length + 1
             }
           let sampleMap := sampleMap.insert stackIdx sampleMap.size

src/Lean/Util/Trace.lean

@@ -64,6 +64,8 @@ structure TraceElem where
   deriving Inhabited
 
 structure TraceState where
+  /-- Thread ID, used by `trace.profiler.output`. -/
+  tid     : UInt64 := 0
   traces  : PersistentArray TraceElem := {}
   deriving Inhabited
 

src/lake/Lake/Toml/Data/Dict.lean

@@ -36,7 +36,7 @@ def mkEmpty (capacity : Nat) : RBDict α β cmp :=
 def ofArray (items : Array (α × β)) : RBDict α β cmp := Id.run do
   let mut indices := mkRBMap α Nat cmp
   for h : i in [0:items.size] do
-    indices := indices.insert (items[i]'h.upper).1 i
+    indices := indices.insert items[i].1 i
   return {items, indices}
 
 protected def beq [BEq (α × β)] (self other : RBDict α β cmp) : Bool :=

tests/compiler/float.lean

@@ -15,6 +15,7 @@ def tst1 : IO Unit := do
   IO.println (Float.ofInt 0)
   IO.println (Float.ofInt 42)
   IO.println (Float.ofInt (-42))
+  IO.println (default : Float)
   IO.println (0 / 0 : Float).toUInt8
   IO.println (0 / 0 : Float).toUInt16
   IO.println (0 / 0 : Float).toUInt32

tests/compiler/float.lean.expected.out

@@ -13,6 +13,7 @@ true
 0.000000
 42.000000
 -42.000000
+0.000000
 0
 0
 0

tests/lean/interactive/completionDocString.lean

@@ -1,2 +1,2 @@
-#eval Array.insertAt
-                  --^ textDocument/completion
+#eval Array.insertIdx
+                   --^ textDocument/completion

tests/lean/interactive/completionDocString.lean.expected.out

@@ -1,19 +1,32 @@
 {"textDocument": {"uri": "file:///completionDocString.lean"},
- "position": {"line": 0, "character": 20}}
+ "position": {"line": 0, "character": 21}}
 {"items":
  [{"sortText": "0",
-   "label": "insertAt",
+   "label": "insertIdx",
    "kind": 3,
    "documentation":
    {"value": "Insert element `a` at position `i`. ", "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDocString.lean"},
-     "position": {"line": 0, "character": 20}},
-    "id": {"const": {"declName": "Array.insertAt"}},
+     "position": {"line": 0, "character": 21}},
+    "id": {"const": {"declName": "Array.insertIdx"}},
     "cPos": 0}},
   {"sortText": "1",
-   "label": "insertAt!",
+   "label": "insertIdxIfInBounds",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "Insert element `a` at position `i`, or do nothing if `as.size < i`. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDocString.lean"},
+     "position": {"line": 0, "character": 21}},
+    "id": {"const": {"declName": "Array.insertIdxIfInBounds"}},
+    "cPos": 0}},
+  {"sortText": "2",
+   "label": "insertIdx!",
    "kind": 3,
    "documentation":
    {"value":
@@ -22,7 +35,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDocString.lean"},
-     "position": {"line": 0, "character": 20}},
-    "id": {"const": {"declName": "Array.insertAt!"}},
+     "position": {"line": 0, "character": 21}},
+    "id": {"const": {"declName": "Array.insertIdx!"}},
     "cPos": 0}}],
  "isIncomplete": true}

tests/lean/interactive/hover.lean.expected.out

@@ -573,7 +573,7 @@
  {"start": {"line": 269, "character": 2}, "end": {"line": 269, "character": 3}},
  "contents":
  {"value":
-  "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
+  "```lean\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 272, "character": 4}}

tests/lean/run/array_isEqvAux.lean

@@ -36,9 +36,9 @@ example : #[0, 1, 2].popWhile (· % 2 = 0) = #[0, 1] := by decide
 
 example : #[0, 1, 2].takeWhile (· % 2 = 0) = #[0] := by decide
 
-example : #[0, 1, 2].feraseIdx ⟨1, by decide⟩ = #[0, 2] := by decide
+example : #[0, 1, 2].eraseIdx 1 = #[0, 2] := by decide
 
-example : #[0, 1, 2].insertAt ⟨1, by decide⟩ 3 = #[0, 3, 1, 2] := by decide
+example : #[0, 1, 2].insertIdx 1 3 = #[0, 3, 1, 2] := by decide
 
 example : #[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true := by decide
 

tests/lean/run/meta5.lean

@@ -9,7 +9,7 @@ withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
   let mvar ← mkFreshExprMVar (mkConst `Nat) MetavarKind.syntheticOpaque;
   trace[Meta.debug] mvar;
   let r ← mkLambdaFVars #[y, x] mvar;
-  trace[Message.debug] r;
+  trace[Meta.debug] r;
   let v := mkApp2 (mkConst `Nat.add) x y;
   mvar.mvarId!.assign v;
   trace[Meta.debug] mvar;
@@ -24,15 +24,15 @@ set_option trace.Meta.debug true
 
 /--
 info: [Meta.debug] ?_
+[Meta.debug] fun y =>
+      let x := 0;
+      ?_
 [Meta.debug] x.add y
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
 [Meta.debug] ?_uniq.3037 : Nat
-[Meta.debug] ?_uniq.3038 : Nat →
-      Nat →
-        let x := 0;
-        Nat
+[Meta.debug] ?_uniq.3038 : Nat → Nat → Nat
 -/
 #guard_msgs in
 #eval tst1