import all

This PR upstreams existing lemmas about `Vector` from Batteries.

Thanks to @fgdorais for preparing these in
https://github.com/leanprover-community/batteries/pull/1062. Further
contributions to the `Vector` API welcome via PR here.

src/Init/Data/Array.lean

@@ -20,3 +20,4 @@ import Init.Data.Array.MapIdx
 import Init.Data.Array.Set
 import Init.Data.Array.Monadic
 import Init.Data.Array.FinRange
+import Init.Data.Array.Perm

src/Init/Data/Array/Lemmas.lean

@@ -21,15 +21,14 @@ import Init.TacticsExtra
 ## Theorems about `Array`.
 -/
 
+
+/-! ### Preliminaries about `Array` needed for `List.toArray` lemmas.
+
+This section contains only the bare minimum lemmas about `Array`
+that we need to write lemmas about `List.toArray`.
+-/
 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
-
 theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
   getElem?_pos ..
 
@@ -39,96 +38,26 @@ 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
-
-theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
-    have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
-    (a.push x)[i] = a[i] := by
-  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
-
-@[simp] theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
-  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
-  rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
-
-theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
-    (a.push x)[i] = if h : i < a.size then a[i] else x := by
-  by_cases h' : i < a.size
-  · simp [getElem_push_lt, h']
-  · simp at h
-    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
-
-@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
-@[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 (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
 
 @[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
   · simp [getElem?_eq_getElem h]
-    rfl
   · simp [getElem?_eq_none_iff.2 (by simpa using h)]
 
-theorem singleton_inj : #[a] = #[b] ↔ a = b := by
-  simp
-
-theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
 
 end Array
 
-namespace List
-
-open Array
-
 /-! ### Lemmas about `List.toArray`.
 
 We prefer to pull `List.toArray` outwards.
 -/
+namespace List
+
+open Array
 
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
@@ -419,10 +348,243 @@ theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → O
     Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by
   simp [Array.zipWithAll, zipWithAll_go_toArray]
 
+@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
+  apply ext'
+  simp
+
+theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
+    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
+  rw [takeWhile.go, takeWhile.go]
+  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+    getElem_toArray, getElem_cons_succ]
+  split
+  rw [takeWhile_go_succ]
+  rfl
+
+theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
+    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
+  induction l generalizing i r with
+  | nil => simp [takeWhile.go]
+  | cons a l ih =>
+    rw [takeWhile.go]
+    cases i with
+    | zero =>
+      simp [takeWhile_go_succ, ih, takeWhile_cons]
+      split <;> simp
+    | succ i =>
+      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+        getElem_toArray, getElem_cons_succ, drop_succ_cons]
+      split <;> rename_i h₁
+      · rw [takeWhile_go_succ, ih]
+        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
+        split <;> simp_all
+      · simp_all [drop_eq_nil_of_le]
+
+@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
+    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
+  simp [Array.takeWhile, takeWhile_go_toArray]
+
 end List
 
+
 namespace Array
 
+/-! ## Preliminaries -/
+
+/-! ### empty -/
+
+@[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by
+  cases xs <;> simp
+
+/-! ### size -/
+
+theorem eq_empty_of_size_eq_zero (h : l.size = 0) : l = #[] := by
+  cases l
+  simp_all
+
+theorem ne_empty_of_size_eq_add_one (h : l.size = n + 1) : l ≠ #[] := by
+  cases l
+  simpa using List.ne_nil_of_length_eq_add_one h
+
+theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by
+  cases l
+  simpa using List.ne_nil_of_length_pos h
+
+@[simp] theorem size_eq_zero : l.size = 0 ↔ l = #[] :=
+  ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
+
+theorem size_pos_of_mem {a : α} {l : Array α} (h : a ∈ l) : 0 < l.size := by
+  cases l
+  simp only [mem_toArray] at h
+  simpa using List.length_pos_of_mem h
+
+theorem exists_mem_of_size_pos {l : Array α} (h : 0 < l.size) : ∃ a, a ∈ l := by
+  cases l
+  simpa using List.exists_mem_of_length_pos h
+
+theorem size_pos_iff_exists_mem {l : Array α} : 0 < l.size ↔ ∃ a, a ∈ l :=
+  ⟨exists_mem_of_size_pos, fun ⟨_, h⟩ => size_pos_of_mem h⟩
+
+theorem exists_mem_of_size_eq_add_one {l : Array α} (h : l.size = n + 1) : ∃ a, a ∈ l := by
+  cases l
+  simpa using List.exists_mem_of_length_eq_add_one h
+
+theorem size_pos {l : Array α} : 0 < l.size ↔ l ≠ #[] :=
+  Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero)
+
+theorem size_eq_one {l : Array α} : l.size = 1 ↔ ∃ a, l = #[a] := by
+  cases l
+  simpa using List.length_eq_one
+
+/-! ### push -/
+
+theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by
+  cases xs
+  simp
+
+@[simp] theorem push_ne_self {a : α} {xs : Array α} : xs.push a ≠ xs := by
+  cases xs
+  simp
+
+@[simp] theorem ne_push_self {a : α} {xs : Array α} : xs ≠ xs.push a := by
+  rw [ne_eq, eq_comm]
+  simp
+
+theorem back_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : a = b := by
+  cases xs
+  cases ys
+  simp only [List.push_toArray, mk.injEq] at h
+  replace h := List.append_inj_right' h (by simp)
+  simpa using h
+
+theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys := by
+  cases xs
+  cases ys
+  simp at h
+  replace h := List.append_inj_left' h (by simp)
+  simp [h]
+
+theorem push_inj_left {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs = ys :=
+  ⟨pop_eq_of_push_eq, fun h => by simp [h]⟩
+
+theorem push_inj_right {a b : α} {xs : Array α} : xs.push a = xs.push b ↔ a = b :=
+  ⟨back_eq_of_push_eq, fun h => by simp [h]⟩
+
+theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
+  constructor
+  · intro h
+    exact ⟨back_eq_of_push_eq h, pop_eq_of_push_eq h⟩
+  · rintro ⟨rfl, rfl⟩
+    rfl
+
+theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
+    ∃ (ys : Array α) (a : α), xs = ys.push a := by
+  rcases xs with ⟨xs⟩
+  simp only [ne_eq, mk.injEq] at h
+  exact ⟨(xs.take (xs.length - 1)).toArray, xs.getLast h, by simp⟩
+
+theorem ne_empty_iff_exists_push {xs : Array α} :
+    xs ≠ #[] ↔ ∃ (ys : Array α) (a : α), xs = ys.push a :=
+  ⟨exists_push_of_ne_empty, fun ⟨_, _, eq⟩ => eq.symm ▸ push_ne_empty⟩
+
+theorem exists_push_of_size_pos {xs : Array α} (h : 0 < xs.size) :
+    ∃ (ys : Array α) (a : α), xs = ys.push a := by
+  replace h : xs ≠ #[] := size_pos.mp h
+  exact exists_push_of_ne_empty h
+
+theorem size_pos_iff_exists_push {xs : Array α} :
+    0 < xs.size ↔ ∃ (ys : Array α) (a : α), xs = ys.push a :=
+  ⟨exists_push_of_size_pos, fun ⟨_, _, eq⟩ => by simp [eq]⟩
+
+theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
+    ∃ (ys : Array α) (a : α), xs = ys.push a :=
+  exists_push_of_size_pos (by simp [h])
+
+/-! ## L[i] and L[i]? -/
+
+@[deprecated List.getElem_toArray (since := "2024-11-29")]
+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
+
+@[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
+
+theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+    have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
+    (a.push x)[i] = a[i] := by
+  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]
+
+@[simp] theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
+  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
+  rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]
+
+theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
+    (a.push x)[i] = if h : i < a.size then a[i] else x := by
+  by_cases h' : i < a.size
+  · simp [getElem_push_lt, h']
+  · simp at h
+    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
+
+@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
+@[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]
+
+theorem singleton_inj : #[a] = #[b] ↔ a = b := by
+  simp
+
+theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
+
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
 -- This is a duplicate of `List.toArray_toList`.
@@ -540,8 +702,6 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
-@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
-
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
 
@@ -860,11 +1020,6 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
   List.getElem_dropLast ..
 
-theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by
-  apply ext
-  · simp [h]
-  · intros; contradiction
-
 theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
     as = as.pop.push as.back! := by
   apply ext
@@ -1381,6 +1536,18 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
   · exact getElem?_append_left h
   · exact getElem?_append_right (by simpa using h)
 
+@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
+    xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by
+  cases as
+  cases bs
+  simp
+
+@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
+    as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs := by
+  cases as
+  cases bs
+  simp
+
 /-! ### flatten -/
 
 @[simp] theorem toList_flatten {l : Array (Array α)} :
@@ -1817,11 +1984,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
-    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem set_toArray (l : List α) (i : Fin l.toArray.size) (a : α) :
     l.toArray.set i a = (l.set i a).toArray := by
   apply ext'
@@ -1885,10 +2047,6 @@ theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p
   apply ext'
   simp
 
-@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
   apply ext'
   simp
@@ -1934,38 +2092,6 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
 @[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
   ext <;> simp
 
-theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
-    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
-  rw [takeWhile.go, takeWhile.go]
-  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
-    getElem_toArray, getElem_cons_succ]
-  split
-  rw [takeWhile_go_succ]
-  rfl
-
-theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
-    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
-  induction l generalizing i r with
-  | nil => simp [takeWhile.go]
-  | cons a l ih =>
-    rw [takeWhile.go]
-    cases i with
-    | zero =>
-      simp [takeWhile_go_succ, ih, takeWhile_cons]
-      split <;> simp
-    | succ i =>
-      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
-        getElem_toArray, getElem_cons_succ, drop_succ_cons]
-      split <;> rename_i h₁
-      · rw [takeWhile_go_succ, ih]
-        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
-        split <;> simp_all
-      · simp_all [drop_eq_nil_of_le]
-
-@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
-    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
-  simp [Array.takeWhile, takeWhile_go_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]

src/Init/Data/Array/Perm.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Nat.Perm
+import Init.Data.Array.Lemmas
+
+namespace Array
+
+open List
+
+/--
+`Perm as bs` asserts that `as` and `bs` are permutations of each other.
+
+This is a wrapper around `List.Perm`, and for now has much less API.
+For more complicated verification, use `perm_iff_toList_perm` and the `List` API.
+-/
+def Perm (as bs : Array α) : Prop :=
+  as.toList ~ bs.toList
+
+@[inherit_doc] scoped infixl:50 " ~ " => Perm
+
+theorem perm_iff_toList_perm {as bs : Array α} : as ~ bs ↔ as.toList ~ bs.toList := Iff.rfl
+
+@[simp] theorem perm_toArray (as bs : List α) : as.toArray ~ bs.toArray ↔ as ~ bs := by
+  simp [perm_iff_toList_perm]
+
+@[simp, refl] protected theorem Perm.refl (l : Array α) : l ~ l := by
+  cases l
+  simp
+
+protected theorem Perm.rfl {l : List α} : l ~ l := .refl _
+
+theorem Perm.of_eq {l₁ l₂ : Array α} (h : l₁ = l₂) : l₁ ~ l₂ := h ▸ .rfl
+
+protected theorem Perm.symm {l₁ l₂ : Array α} (h : l₁ ~ l₂) : l₂ ~ l₁ := by
+  cases l₁; cases l₂
+  simp only [perm_toArray] at h
+  simpa using h.symm
+
+protected theorem Perm.trans {l₁ l₂ l₃ : Array α} (h₁ : l₁ ~ l₂) (h₂ : l₂ ~ l₃) : l₁ ~ l₃ := by
+  cases l₁; cases l₂; cases l₃
+  simp only [perm_toArray] at h₁ h₂
+  simpa using h₁.trans h₂
+
+instance : Trans (Perm (α := α)) (Perm (α := α)) (Perm (α := α)) where
+  trans h₁ h₂ := Perm.trans h₁ h₂
+
+theorem perm_comm {l₁ l₂ : Array α} : l₁ ~ l₂ ↔ l₂ ~ l₁ := ⟨Perm.symm, Perm.symm⟩
+
+theorem Perm.push (x y : α) {l₁ l₂ : Array α} (p : l₁ ~ l₂) :
+    (l₁.push x).push y ~ (l₂.push y).push x := by
+  cases l₁; cases l₂
+  simp only [perm_toArray] at p
+  simp only [push_toArray, List.append_assoc, singleton_append, perm_toArray]
+  exact p.append (Perm.swap' _ _ Perm.nil)
+
+theorem swap_perm {as : Array α} {i j : Nat} (h₁ : i < as.size) (h₂ : j < as.size) :
+    as.swap i j ~ as := by
+  simp only [swap, perm_iff_toList_perm, toList_set]
+  apply set_set_perm
+
+end Array

src/Init/Data/Array/QSort.lean

@@ -4,46 +4,46 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.Array.Basic
+import Init.Data.Vector.Basic
 import Init.Data.Ord
 
 namespace Array
--- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget
 
-def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
-  if h : as.size = 0 then (0, as) else have : Inhabited α := ⟨as[0]'(by revert h; cases as.size <;> simp)⟩ -- TODO: remove
+private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
+    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {n : Nat // lo ≤ n} × Vector α n :=
   let mid := (lo + hi) / 2
-  let as  := if lt (as.get! mid) (as.get! lo) then as.swapIfInBounds lo mid else as
-  let as  := if lt (as.get! hi)  (as.get! lo) then as.swapIfInBounds lo hi  else as
-  let as  := if lt (as.get! mid) (as.get! hi) then as.swapIfInBounds mid hi else as
-  let pivot := as.get! hi
-  let rec loop (as : Array α) (i j : Nat) :=
+  let as  := if lt as[mid] as[lo] then as.swap lo mid else as
+  let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
+  let as  := if lt as[mid] as[hi] then as.swap mid hi else as
+  let pivot := as[hi]
+  let rec loop (as : Vector α n) (i j : Nat)
+      (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
     if h : j < hi then
-      if lt (as.get! j) pivot then
-        let as := as.swapIfInBounds i j
-        loop as (i+1) (j+1)
+      if lt as[j] pivot then
+        loop (as.swap i j) (i+1) (j+1)
       else
         loop as i (j+1)
     else
-      let as := as.swapIfInBounds i hi
-      (i, as)
-    termination_by hi - j
-    decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
+      (⟨i, ilo⟩, as.swap i hi)
   loop as lo lo
 
-@[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
-  let rec @[specialize] sort (as : Array α) (low high : Nat) :=
-    if low < high then
-      let p := qpartition as lt low high;
-      -- TODO: fix `partial` support in the equation compiler, it breaks if we use `let (mid, as) := partition as lt low high`
-      let mid := p.1
-      let as  := p.2
-      if mid >= high then as
+@[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
+    (low := 0) (high := as.size - 1) : Array α :=
+  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
+      (hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
+    if h₁ : lo < hi then
+      let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
+      if h₂ : mid ≥ hi then
+        as
       else
-        let as := sort as low mid
-        sort as (mid+1) high
+        sort (sort as lo mid) (mid+1) hi
     else as
-  sort as low high
+  if h : as.size = 0 then
+    as
+  else
+    let low := min low (as.size - 1)
+    let high := min high (as.size - 1)
+    sort ⟨as, rfl⟩ low high |>.toArray
 
 set_option linter.unusedVariables.funArgs false in
 /--

src/Init/Data/Fin/Basic.lean

@@ -36,12 +36,6 @@ def succ : Fin n → Fin (n + 1)
 
 variable {n : Nat}
 
-/--
-Returns `a` modulo `n + 1` as a `Fin n.succ`.
--/
-protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) :=
-  ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
-
 /--
 Returns `a` modulo `n` as a `Fin n`.
 
@@ -50,9 +44,12 @@ The assumption `NeZero n` ensures that `Fin n` is nonempty.
 protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
 
--- We intend to deprecate `Fin.ofNat` in favor of `Fin.ofNat'` (and later rename).
--- This is waiting on https://github.com/leanprover/lean4/pull/5323
--- attribute [deprecated Fin.ofNat' (since := "2024-09-16")] Fin.ofNat
+/--
+Returns `a` modulo `n + 1` as a `Fin n.succ`.
+-/
+@[deprecated Fin.ofNat' (since := "2024-11-27")]
+protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) :=
+  ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
 
 private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
   | 0,   h => Nat.mod_lt _ h

src/Init/Data/List/Lemmas.lean

@@ -83,44 +83,12 @@ open Nat
 @[simp] theorem nil_eq {α} {xs : List α} : [] = xs ↔ xs = [] := by
   cases xs <;> simp
 
-/-! ### cons -/
-
-theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun
-
-@[simp]
-theorem cons_ne_self (a : α) (l : List α) : a :: l ≠ l := mt (congrArg length) (Nat.succ_ne_self _)
-
-@[simp] theorem ne_cons_self {a : α} {l : List α} : l ≠ a :: l := by
-  rw [ne_eq, eq_comm]
-  simp
-
-theorem head_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : h₁ = h₂ := (cons.inj H).1
-
-theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (cons.inj H).2
-
-theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
-  ⟨tail_eq_of_cons_eq, congrArg _⟩
-
-@[deprecated cons_inj_right (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right
-
-theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
-  List.cons.injEq .. ▸ .rfl
-
-theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L
-  | c :: l', _ => ⟨c, l', rfl⟩
-
-theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
-  simp
-
 /-! ### length -/
 
 theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
 
 theorem ne_nil_of_length_eq_add_one (_ : length l = n + 1) : l ≠ [] := fun _ => nomatch l
 
-@[deprecated ne_nil_of_length_eq_add_one (since := "2024-06-16")]
-abbrev ne_nil_of_length_eq_succ := @ne_nil_of_length_eq_add_one
-
 theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l
 
 @[simp] theorem length_eq_zero : length l = 0 ↔ l = [] :=
@@ -156,6 +124,36 @@ theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
 theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
+/-! ### cons -/
+
+theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun
+
+@[simp]
+theorem cons_ne_self (a : α) (l : List α) : a :: l ≠ l := mt (congrArg length) (Nat.succ_ne_self _)
+
+@[simp] theorem ne_cons_self {a : α} {l : List α} : l ≠ a :: l := by
+  rw [ne_eq, eq_comm]
+  simp
+
+theorem head_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : h₁ = h₂ := (cons.inj H).1
+
+theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (cons.inj H).2
+
+theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
+  ⟨tail_eq_of_cons_eq, congrArg _⟩
+
+theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
+  List.cons.injEq .. ▸ .rfl
+
+theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L
+  | c :: l', _ => ⟨c, l', rfl⟩
+
+theorem ne_nil_iff_exists_cons {l : List α} : l ≠ [] ↔ ∃ b L, l = b :: L :=
+  ⟨exists_cons_of_ne_nil, fun ⟨_, _, eq⟩ => eq.symm ▸ cons_ne_nil _ _⟩
+
+theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
+  simp
+
 /-! ## L[i] and L[i]? -/
 
 /-! ### `get` and `get?`.
@@ -163,57 +161,29 @@ theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
 We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`.
 -/
 
-theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl
+@[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
 
-theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} :
-  (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
-
-theorem get_cons_succ' {as : List α} {i : Fin as.length} :
-  (a :: as).get i.succ = as.get i := rfl
-
-@[deprecated "Deprecated without replacement." (since := "2024-07-09")]
-theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl
-
-theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h)
-  | _::_, _ => rfl
-
-theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
-
-theorem get?_len_le : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
+theorem get?_eq_none : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
   | [], _, _ => rfl
-  | _ :: l, _+1, h => get?_len_le (l := l) <| Nat.le_of_succ_le_succ h
+  | _ :: l, _+1, h => get?_eq_none (l := l) <| Nat.le_of_succ_le_succ h
 
 theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩)
   | _ :: _, 0, _ => rfl
   | _ :: l, _+1, _ => get?_eq_get (l := l) _
 
-theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
+theorem get?_eq_some_iff : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
   ⟨fun e =>
-    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e
+    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_eq_none hn ▸ e
     ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
   fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩
 
-theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
-  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
+theorem get?_eq_none_iff : l.get? n = none ↔ length l ≤ n :=
+  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩), get?_eq_none⟩
 
 @[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
-  simp only [getElem?, decidableGetElem?]; split
+  simp only [getElem?_def]; split
   · exact (get?_eq_get ‹_›)
-  · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›)
-
-@[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
-
-theorem getElem?_eq_some {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i]'h = a := by
-  simpa using get?_eq_some
-
-/--
-If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
-`rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
-`i : Fin l.length` to `Fin l'.length` directly. The theorem `get_of_eq` can be used to make
-such a rewrite, with `rw [get_of_eq h]`.
--/
-theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
-    get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl
+  · exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›)
 
 /-! ### getD
 
@@ -224,42 +194,29 @@ Because of this, there is only minimal API for `getD`.
 @[simp] theorem getD_eq_getElem?_getD (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by
   simp [getD]
 
-@[deprecated getD_eq_getElem?_getD (since := "2024-06-12")]
-theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp
-
 /-! ### get!
 
 We simplify `l.get! n` to `l[n]!`.
 -/
 
-theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
-  | _a::_, 0, rfl => rfl
-  | _::l, _+1, e => get!_of_get? (l := l) e
-
 theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) n, l.get! n = l.getD n default
   | [], _      => rfl
   | _a::_, 0   => rfl
   | _a::l, n+1 => get!_eq_getD l n
 
-theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α)
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
-
 @[simp] theorem get!_eq_getElem! [Inhabited α] (l : List α) (n) : l.get! n = l[n]! := by
   simp [get!_eq_getD]
   rfl
 
-/-! ### getElem! -/
+/-! ### getElem!
 
-@[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
+We simplify `l[n]!` to `(l[n]?).getD default`.
+-/
 
-@[simp] theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
-  rw [getElem!_pos] <;> simp
-
-@[simp] theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[n+1]! = l[n]! := by
-  by_cases h : n < l.length
-  · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff]
-  · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff]
+@[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (n : Nat) :
+    l[n]! = (l[n]?).getD (default : α) := by
+  simp only [getElem!_def]
+  split <;> simp_all
 
 /-! ### getElem? and getElem -/
 
@@ -267,23 +224,19 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
   simp only [getElem?_def, h, ↓reduceDIte]
 
 theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
-  simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
+  simp only [← get?_eq_getElem?, get?_eq_some_iff, get_eq_getElem]
 
 theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.length, l[n] = a := by
   rw [eq_comm, getElem?_eq_some_iff]
 
 @[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
-  simp only [← get?_eq_getElem?, get?_eq_none]
+  simp only [← get?_eq_getElem?, get?_eq_none_iff]
 
 @[simp] theorem none_eq_getElem?_iff {l : List α} {n : Nat} : none = l[n]? ↔ length l ≤ n := by
   simp [eq_comm (a := none)]
 
 theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
-theorem getElem?_eq (l : List α) (i : Nat) :
-    l[i]? = if h : i < l.length then some l[i] else none := by
-  split <;> simp_all
-
 @[simp] theorem some_getElem_eq_getElem?_iff {α} (xs : List α) (i : Nat) (h : i < xs.length) :
     (some xs[i] = xs[i]?) ↔ True := by
   simp [h]
@@ -300,9 +253,6 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
     l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-@[deprecated getElem_eq_getElem?_get (since := "2024-09-04")] abbrev getElem_eq_getElem? :=
-  @getElem_eq_getElem?_get
-
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
 theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
@@ -314,11 +264,6 @@ theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
   cases i <;> simp
 
-theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => by
-    rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h]
-
 /--
 If one has `l[i]` in an expression and `h : l = l'`,
 `rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
@@ -332,20 +277,10 @@ theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length)
   match i, h with
   | 0, _ => rfl
 
-@[deprecated getElem_singleton (since := "2024-06-12")]
-theorem get_singleton (a : α) (n : Fin 1) : get [a] n = a := by simp
-
 theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos.mp h) :=
   match l, h with
   | _ :: _, _ => rfl
 
-theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {n : Nat}, l[n]? = some a → l[n]! = a
-  | _a::_, 0, _ => by
-    rw [getElem!_pos] <;> simp_all
-  | _::l, _+1, e => by
-    simp at e
-    simp_all [getElem!_of_getElem? (l := l) e]
-
 @[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ n : Nat, l₁[n]? = l₂[n]?) : l₁ = l₂ :=
   ext_get? fun n => by simp_all
 
@@ -356,11 +291,7 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
       simp_all [getElem?_eq_getElem]
     else by
       have h₁ := Nat.le_of_not_lt h₁
-      rw [getElem?_len_le h₁, getElem?_len_le]; rwa [← hl]
-
-theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
-    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
-  ext_getElem hl (by simp_all)
+      rw [getElem?_eq_none h₁, getElem?_eq_none]; rwa [← hl]
 
 @[simp] theorem getElem_concat_length : ∀ (l : List α) (a : α) (i) (_ : i = l.length) (w), (l ++ [a])[i]'w = a
   | [], a, _, h, _ => by subst h; simp
@@ -369,19 +300,11 @@ theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
 theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a := by
   simp
 
-@[deprecated getElem?_concat_length (since := "2024-06-12")]
-theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
+theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
+  simp
 
-@[simp] theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
-  by_cases h : n < l.length
-  · simp_all
-  · simp [h]
-    simp_all
-
-@[simp] theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
-  by_cases h : n < l.length
-  · simp_all
-  · simp [h]
+theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
+  simp
 
 /-! ### mem -/
 
@@ -493,42 +416,18 @@ theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (n : Nat) (h : n
   | _, _ :: _, .head .. => ⟨0, Nat.succ_pos _, rfl⟩
   | _, _ :: _, .tail _ m => let ⟨n, h, e⟩ := getElem_of_mem m; ⟨n+1, Nat.succ_lt_succ h, e⟩
 
-theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by
-  obtain ⟨n, h, e⟩ := getElem_of_mem h
-  exact ⟨⟨n, h⟩, e⟩
-
 theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a :=
   let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
 
-theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
-  let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
-
-theorem get_mem : ∀ (l : List α) n, get l n ∈ l
-  | _ :: _, ⟨0, _⟩ => .head ..
-  | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem 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 ..
 
-@[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 ..⟩
 
-theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
-  ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
-
 theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
-theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
-  simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]
-
 theorem forall_getElem {l : List α} {p : α → Prop} :
     (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by
   induction l with
@@ -579,18 +478,6 @@ theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 :=
 
 /-! ### any / all -/
 
-theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
-  induction l <;> simp_all
-
-theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
-  induction l <;> simp_all [eq_comm (a := a)]
-
-theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
-  induction l <;> simp_all
-
-theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
-  induction l <;> simp_all [eq_comm (a := a)]
-
 theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by induction l <;> simp [*]
 
 theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l → p x) := by induction l <;> simp [*]
@@ -615,6 +502,18 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
+theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
+  simp
+
+theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
+  simp
+
+theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
+  induction l <;> simp_all
+
+theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
+  induction l <;> simp_all [eq_comm (a := a)]
+
 /-! ### set -/
 
 -- As `List.set` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
@@ -632,19 +531,10 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
   | _ :: _, 0 => by simp
   | _ :: l, i + 1 => by simp [getElem_set_self]
 
-@[deprecated getElem_set_self (since := "2024-09-04")] abbrev getElem_set_eq := @getElem_set_self
-
-@[deprecated getElem_set_self (since := "2024-06-12")]
-theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
-    (l.set i a).get ⟨i, h⟩ = a := by
-  simp
-
 @[simp] theorem getElem?_set_self {l : List α} {i : Nat} {a : α} (h : i < l.length) :
     (l.set i a)[i]? = some a := by
   simp_all [getElem?_eq_some_iff]
 
-@[deprecated getElem?_set_self (since := "2024-09-04")] abbrev getElem?_set_eq := @getElem?_set_self
-
 /-- This differs from `getElem?_set_self` by monadically mapping `Function.const _ a` over the `Option`
 returned by `l[i]?`. -/
 theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} :
@@ -666,12 +556,6 @@ theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} :
     have g : i ≠ j := h ∘ congrArg (· + 1)
     simp [getElem_set_ne g]
 
-@[deprecated getElem_set_ne (since := "2024-06-12")]
-theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
-    (hj : j < (l.set i a).length) :
-    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by
-  simp [h]
-
 @[simp] theorem getElem?_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}  :
     (l.set i a)[j]? = l[j]? := by
   by_cases hj : j < (l.set i a).length
@@ -686,11 +570,6 @@ theorem getElem_set {l : List α} {m n} {a} (h) :
   else
     simp [h]
 
-@[deprecated getElem_set (since := "2024-06-12")]
-theorem get_set {l : List α} {m n} {a : α} (h) :
-    (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
-  simp [getElem_set]
-
 theorem getElem?_set {l : List α} {i j : Nat} {a : α} :
     (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]? := by
   if h : i = j then
@@ -710,6 +589,14 @@ theorem getElem?_set' {l : List α} {i j : Nat} {a : α} :
   · simp only [getElem?_set_self', Option.map_eq_map, ↓reduceIte, *]
   · simp only [ne_eq, not_false_eq_true, getElem?_set_ne, ↓reduceIte, *]
 
+@[simp] theorem set_getElem_self {as : List α} {i : Nat} (h : i < as.length) :
+    as.set i as[i] = as := by
+  apply ext_getElem
+  · simp
+  · intro n h₁ h₂
+    rw [getElem_set]
+    split <;> simp_all
+
 theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} :
     l.set n a = l := by
   induction l generalizing n with
@@ -724,8 +611,6 @@ theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α
 @[simp] theorem set_eq_nil_iff {l : List α} (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by
   cases l <;> cases n <;> simp [set]
 
-@[deprecated set_eq_nil_iff (since := "2024-09-05")] abbrev set_eq_nil := @set_eq_nil_iff
-
 theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
     (l.set n a).set m b = (l.set m b).set n a
   | _, _, [], _ => by simp
@@ -3445,17 +3330,137 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
     (l.insert a).all f = (f a && l.all f) := by
   simp [all_eq]
 
+/-! ### Legacy lemmas about `get`, `get?`, and `get!`.
+
+Hopefully these should not be needed, in favour of lemmas about `xs[i]`, `xs[i]?`, and `xs[i]!`,
+to which these simplify.
+
+We may consider deprecating or downstreaming these lemmas.
+-/
+
+theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl
+
+theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} :
+  (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
+
+theorem get_cons_succ' {as : List α} {i : Fin as.length} :
+  (a :: as).get i.succ = as.get i := rfl
+
+theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h)
+  | _::_, _ => rfl
+
+theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
+
+/--
+If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
+`rw [h]` will give a "motive is not type correct" error, as it cannot rewrite the
+`i : Fin l.length` to `Fin l'.length` directly. The theorem `get_of_eq` can be used to make
+such a rewrite, with `rw [get_of_eq h]`.
+-/
+theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
+    get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl
+
+theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
+  | _a::_, 0, rfl => rfl
+  | _::l, _+1, e => get!_of_get? (l := l) e
+
+theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α)
+  | [], _, _ => rfl
+  | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
+
+theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
+
+theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
+  rw [getElem!_pos] <;> simp
+
+theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[n+1]! = l[n]! := by
+  by_cases h : n < l.length
+  · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff]
+  · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff]
+
+theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {n : Nat}, l[n]? = some a → l[n]! = a
+  | _a::_, 0, _ => by
+    rw [getElem!_pos] <;> simp_all
+  | _::l, _+1, e => by
+    simp at e
+    simp_all [getElem!_of_getElem? (l := l) e]
+
+theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
+    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
+  ext_getElem hl (by simp_all)
+
+theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by
+  obtain ⟨n, h, e⟩ := getElem_of_mem h
+  exact ⟨⟨n, h⟩, e⟩
+
+theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
+  let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
+
+theorem get_mem : ∀ (l : List α) n, get l n ∈ l
+  | _ :: _, ⟨0, _⟩ => .head ..
+  | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
+
+theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
+  let ⟨_, e⟩ := get?_eq_some_iff.1 e; e ▸ get_mem ..
+
+theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
+  ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
+
+theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
+  simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]
+
 /-! ### Deprecations -/
 
+@[deprecated getD_eq_getElem?_getD (since := "2024-06-12")]
+theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp
+@[deprecated getElem_singleton (since := "2024-06-12")]
+theorem get_singleton (a : α) (n : Fin 1) : get [a] n = a := by simp
+@[deprecated getElem?_concat_length (since := "2024-06-12")]
+theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
+@[deprecated getElem_set_self (since := "2024-06-12")]
+theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
+    (l.set i a).get ⟨i, h⟩ = a := by
+  simp
+@[deprecated getElem_set_ne (since := "2024-06-12")]
+theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
+    (hj : j < (l.set i a).length) :
+    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by
+  simp [h]
+@[deprecated getElem_set (since := "2024-06-12")]
+theorem get_set {l : List α} {m n} {a : α} (h) :
+    (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
+  simp [getElem_set]
+@[deprecated cons_inj_right (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right
+@[deprecated ne_nil_of_length_eq_add_one (since := "2024-06-16")]
+abbrev ne_nil_of_length_eq_succ := @ne_nil_of_length_eq_add_one
+
+@[deprecated "Deprecated without replacement." (since := "2024-07-09")]
+theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl
+
+@[deprecated filter_flatten (since := "2024-08-26")]
+theorem join_map_filter (p : α → Bool) (l : List (List α)) :
+    (l.map (filter p)).flatten = (l.flatten).filter p := by
+  rw [filter_flatten]
+
+@[deprecated getElem_eq_getElem?_get (since := "2024-09-04")] abbrev getElem_eq_getElem? :=
+  @getElem_eq_getElem?_get
+@[deprecated flatten_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @flatten_eq_nil_iff
+@[deprecated flatten_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @flatten_ne_nil_iff
+@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons_iff := @flatten_eq_cons_iff
+@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff
+@[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff
+@[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem?
+@[deprecated mem_of_get? (since := "2024-09-06")] abbrev get?_mem := @mem_of_get?
+@[deprecated getElem_set_self (since := "2024-09-04")] abbrev getElem_set_eq := @getElem_set_self
+@[deprecated getElem?_set_self (since := "2024-09-04")] abbrev getElem?_set_eq := @getElem?_set_self
+@[deprecated set_eq_nil_iff (since := "2024-09-05")] abbrev set_eq_nil := @set_eq_nil_iff
 
 @[deprecated flatten_nil (since := "2024-10-14")] abbrev join_nil := @flatten_nil
 @[deprecated flatten_cons (since := "2024-10-14")] abbrev join_cons := @flatten_cons
 @[deprecated length_flatten (since := "2024-10-14")] abbrev length_join := @length_flatten
 @[deprecated flatten_singleton (since := "2024-10-14")] abbrev join_singleton := @flatten_singleton
 @[deprecated mem_flatten (since := "2024-10-14")] abbrev mem_join := @mem_flatten
-@[deprecated flatten_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @flatten_eq_nil_iff
 @[deprecated flatten_eq_nil_iff (since := "2024-10-14")] abbrev join_eq_nil_iff := @flatten_eq_nil_iff
-@[deprecated flatten_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @flatten_ne_nil_iff
 @[deprecated flatten_ne_nil_iff (since := "2024-10-14")] abbrev join_ne_nil_iff := @flatten_ne_nil_iff
 @[deprecated exists_of_mem_flatten (since := "2024-10-14")] abbrev exists_of_mem_join := @exists_of_mem_flatten
 @[deprecated mem_flatten_of_mem (since := "2024-10-14")] abbrev mem_join_of_mem := @mem_flatten_of_mem
@@ -3469,16 +3474,9 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
 @[deprecated filter_flatten (since := "2024-10-14")] abbrev filter_join := @filter_flatten
 @[deprecated flatten_filter_not_isEmpty (since := "2024-10-14")] abbrev join_filter_not_isEmpty := @flatten_filter_not_isEmpty
 @[deprecated flatten_filter_ne_nil (since := "2024-10-14")] abbrev join_filter_ne_nil := @flatten_filter_ne_nil
-@[deprecated filter_flatten (since := "2024-08-26")]
-theorem join_map_filter (p : α → Bool) (l : List (List α)) :
-    (l.map (filter p)).flatten = (l.flatten).filter p := by
-  rw [filter_flatten]
 @[deprecated flatten_append (since := "2024-10-14")] abbrev join_append := @flatten_append
 @[deprecated flatten_concat (since := "2024-10-14")] abbrev join_concat := @flatten_concat
 @[deprecated flatten_flatten (since := "2024-10-14")] abbrev join_join := @flatten_flatten
-@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons_iff := @flatten_eq_cons_iff
-@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff
-@[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff
 @[deprecated flatten_eq_append_iff (since := "2024-10-14")] abbrev join_eq_append_iff := @flatten_eq_append_iff
 @[deprecated eq_iff_flatten_eq (since := "2024-10-14")] abbrev eq_iff_join_eq := @eq_iff_flatten_eq
 @[deprecated flatten_replicate_nil (since := "2024-10-14")] abbrev join_replicate_nil := @flatten_replicate_nil
@@ -3513,4 +3511,18 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) :
 @[deprecated any_flatMap (since := "2024-10-16")] abbrev any_bind := @any_flatMap
 @[deprecated all_flatMap (since := "2024-10-16")] abbrev all_bind := @all_flatMap
 
+@[deprecated get?_eq_none (since := "2024-11-29")] abbrev get?_len_le := @get?_eq_none
+@[deprecated getElem?_eq_some_iff (since := "2024-11-29")]
+abbrev getElem?_eq_some := @getElem?_eq_some_iff
+@[deprecated get?_eq_some_iff (since := "2024-11-29")]
+abbrev get?_eq_some := @get?_eq_some_iff
+@[deprecated LawfulGetElem.getElem?_def (since := "2024-11-29")]
+theorem getElem?_eq (l : List α) (i : Nat) :
+    l[i]? = if h : i < l.length then some l[i] else none :=
+  getElem?_def _ _
+@[deprecated getElem?_eq_none (since := "2024-11-29")] abbrev getElem?_len_le := @getElem?_eq_none
+
+
+
+
 end List

src/Init/Data/List/MapIdx.lean

@@ -87,8 +87,8 @@ theorem mapFinIdx_eq_ofFn {as : List α} {f : Fin as.length → α → β} :
   apply ext_getElem <;> simp
 
 @[simp] theorem getElem?_mapFinIdx {l : List α} {f : Fin l.length → α → β} {i : Nat} :
-    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some] at m; exact m.1⟩ x := by
-  simp only [getElem?_eq, length_mapFinIdx, getElem_mapFinIdx]
+    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some_iff] at m; exact m.1⟩ x := by
+  simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx]
   split <;> simp
 
 @[simp]
@@ -126,7 +126,8 @@ theorem mapFinIdx_singleton {a : α} {f : Fin 1 → α → β} :
 
 theorem mapFinIdx_eq_enum_map {l : List α} {f : Fin l.length → α → β} :
     l.mapFinIdx f = l.enum.attach.map
-      fun ⟨⟨i, x⟩, m⟩ => f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some] at m; exact m.1⟩ x := by
+      fun ⟨⟨i, x⟩, m⟩ =>
+        f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1⟩ x := by
   apply ext_getElem <;> simp
 
 @[simp]
@@ -235,7 +236,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
     (mapIdx.go f l arr)[i]? =
       if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]?
   | [], arr, i => by
-    simp only [mapIdx.go, Array.toListImpl_eq, getElem?_eq, Array.length_toList,
+    simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList,
       Array.getElem_eq_getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
   | a :: l, arr, i => by
     rw [mapIdx.go, getElem?_mapIdx_go]

src/Init/Data/List/Nat.lean

@@ -15,3 +15,4 @@ import Init.Data.List.Nat.Find
 import Init.Data.List.Nat.BEq
 import Init.Data.List.Nat.Modify
 import Init.Data.List.Nat.InsertIdx
+import Init.Data.List.Nat.Perm

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

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Perm
+
+namespace List
+
+/-- Helper lemma for `set_set_perm`-/
+private theorem set_set_perm' {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : i + j < as.length)
+    (hj : 0 < j) :
+    (as.set i as[i + j]).set (i + j) as[i] ~ as := by
+  have : as =
+      as.take i ++ as[i] :: (as.take (i + j)).drop (i + 1) ++ as[i + j] :: as.drop (i + j + 1) := by
+    simp only [getElem_cons_drop, append_assoc, cons_append]
+    rw [← drop_append_of_le_length]
+    · simp
+    · simp; omega
+  conv => lhs; congr; congr; rw [this]
+  conv => rhs; rw [this]
+  rw [set_append_left _ _ (by simp; omega)]
+  rw [set_append_right _ _ (by simp; omega)]
+  rw [set_append_right _ _ (by simp; omega)]
+  simp only [length_append, length_take, length_set, length_cons, length_drop]
+  rw [(show i - min i as.length = 0 by omega)]
+  rw [(show i + j - (min i as.length + (min (i + j) as.length - (i + 1) + 1)) = 0 by omega)]
+  simp only [set_cons_zero]
+  simp only [append_assoc]
+  apply Perm.append_left
+  apply cons_append_cons_perm
+
+theorem set_set_perm {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j < as.length) :
+    (as.set i as[j]).set j as[i] ~ as := by
+  if h₃ : i = j then
+    simp [h₃]
+  else
+    if h₃ : i < j then
+      let j' := j - i
+      have t : j = i + j' := by omega
+      generalize j' = j' at t
+      subst t
+      exact set_set_perm' _ _ (by omega)
+    else
+      rw [set_comm _ _ _ (by omega)]
+      let i' := i - j
+      have t : i = j + i' := by omega
+      generalize i' = i' at t
+      subst t
+      apply set_set_perm' _ _ (by omega)
+
+end List

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

@@ -345,7 +345,7 @@ theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l
   rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
     simp [Nat.add_sub_cancel_left, Nat.le_add_right]
 
-theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
+theorem set_eq_take_append_cons_drop (l : List α) (n : Nat) (a : α) :
     l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l := by
   split <;> rename_i h
   · ext1 m

src/Init/Data/List/Perm.lean

@@ -39,6 +39,9 @@ protected theorem Perm.symm {l₁ l₂ : List α} (h : l₁ ~ l₂) : l₂ ~ l
   | swap => exact swap ..
   | trans _ _ ih₁ ih₂ => exact trans ih₂ ih₁
 
+instance : Trans (Perm (α := α)) (Perm (α := α)) (Perm (α := α)) where
+  trans h₁ h₂ := Perm.trans h₁ h₂
+
 theorem perm_comm {l₁ l₂ : List α} : l₁ ~ l₂ ↔ l₂ ~ l₁ := ⟨Perm.symm, Perm.symm⟩
 
 theorem Perm.swap' (x y : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : y :: x :: l₁ ~ x :: y :: l₂ :=
@@ -102,7 +105,7 @@ theorem perm_append_comm : ∀ {l₁ l₂ : List α}, l₁ ++ l₂ ~ l₂ ++ l
   | _ :: _, _ => (perm_append_comm.cons _).trans perm_middle.symm
 
 theorem perm_append_comm_assoc (l₁ l₂ l₃ : List α) :
-    Perm (l₁ ++ (l₂ ++ l₃)) (l₂ ++ (l₁ ++ l₃)) := by
+    (l₁ ++ (l₂ ++ l₃)) ~ (l₂ ++ (l₁ ++ l₃)) := by
   simpa only [List.append_assoc] using perm_append_comm.append_right _
 
 theorem concat_perm (l : List α) (a : α) : concat l a ~ a :: l := by simp
@@ -133,7 +136,7 @@ theorem Perm.nil_eq {l : List α} (p : [] ~ l) : [] = l := p.symm.eq_nil.symm
 
 theorem not_perm_nil_cons (x : α) (l : List α) : ¬[] ~ x :: l := (nomatch ·.symm.eq_nil)
 
-theorem not_perm_cons_nil {l : List α} {a : α} : ¬(Perm (a::l) []) :=
+theorem not_perm_cons_nil {l : List α} {a : α} : ¬((a::l) ~ []) :=
   fun h => by simpa using h.length_eq
 
 theorem Perm.isEmpty_eq {l l' : List α} (h : Perm l l') : l.isEmpty = l'.isEmpty := by
@@ -478,6 +481,15 @@ theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatt
 
 @[deprecated Perm.flatten (since := "2024-10-14")] abbrev Perm.join := @Perm.flatten
 
+theorem cons_append_cons_perm {a b : α} {as bs : List α} :
+    a :: as ++ b :: bs ~ b :: as ++ a :: bs := by
+  suffices [[a], as, [b], bs].flatten ~ [[b], as, [a], bs].flatten by simpa
+  apply Perm.flatten
+  calc
+    [[a], as, [b], bs] ~ [as, [a], [b], bs] := Perm.swap as [a] _
+    _ ~ [as, [b], [a], bs] := Perm.cons _ (Perm.swap [b] [a] _)
+    _ ~ [[b], as, [a], bs] := Perm.swap [b] as _
+
 theorem Perm.flatMap_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.flatMap f ~ l₂.flatMap f :=
   (p.map _).flatten
 

src/Init/Data/List/TakeDrop.lean

@@ -192,6 +192,24 @@ theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
   Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
     rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]
 
+@[simp] theorem take_append_getElem (l : List α) (i : Nat) (h : i < l.length) :
+    (l.take i) ++ [l[i]] = l.take (i+1) := by
+  simpa using take_concat_get l i h
+
+@[simp] theorem take_append_getLast (l : List α) (h : l ≠ []) :
+    (l.take (l.length - 1)) ++ [l.getLast h] = l := by
+  rw [getLast_eq_getElem]
+  cases l
+  · contradiction
+  · simp
+
+@[simp] theorem take_append_getLast? (l : List α) :
+    (l.take (l.length - 1)) ++ l.getLast?.toList = l := by
+  match l with
+  | [] => simp
+  | x :: xs =>
+    simpa using take_append_getLast (x :: xs) (by simp)
+
 @[deprecated take_succ_cons (since := "2024-07-25")]
 theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl
 

src/Init/Data/NeZero.lean

@@ -36,3 +36,7 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
 
 @[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False :=
   ⟨fun _ ↦ NeZero.ne (0 : α) rfl, fun h ↦ h.elim⟩
+
+instance {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] :
+    NeZero (if p then n else m) := by
+  split <;> infer_instance

src/Init/Data/UInt/Basic.lean

@@ -278,6 +278,16 @@ This function is overridden with a native implementation.
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize :=
   USize.ofNatCore n (Nat.lt_of_lt_of_le h le_usize_size)
+@[extern "lean_uint8_to_usize"]
+def UInt8.toUSize (a : UInt8) : USize :=
+  USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))
+@[extern "lean_usize_to_uint8"]
+def USize.toUInt8 (a : USize) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint16_to_usize"]
+def UInt16.toUSize (a : UInt16) : USize :=
+  USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))
+@[extern "lean_usize_to_uint16"]
+def USize.toUInt16 (a : USize) : UInt16 := a.toNat.toUInt16
 @[extern "lean_uint32_to_usize"]
 def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
 @[extern "lean_usize_to_uint32"]

src/Init/Data/UInt/Lemmas.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone
 -/
 prelude
 import Init.Data.UInt.Basic
@@ -9,129 +9,202 @@ import Init.Data.Fin.Lemmas
 import Init.Data.BitVec.Lemmas
 import Init.Data.BitVec.Bitblast
 
+open Lean in
 set_option hygiene false in
-macro "declare_uint_theorems" typeName:ident : command =>
-`(
-namespace $typeName
+macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
+  let mut cmds ← Syntax.getArgs <$> `(
+  namespace $typeName
 
-instance : Inhabited $typeName where
-  default := 0
+  theorem zero_def : (0 : $typeName) = ⟨0⟩ := rfl
+  theorem one_def : (1 : $typeName) = ⟨1⟩ := rfl
+  theorem sub_def (a b : $typeName) : a - b = ⟨a.toBitVec - b.toBitVec⟩ := rfl
+  theorem mul_def (a b : $typeName) : a * b = ⟨a.toBitVec * b.toBitVec⟩ := rfl
+  theorem mod_def (a b : $typeName) : a % b = ⟨a.toBitVec % b.toBitVec⟩ := rfl
+  theorem add_def (a b : $typeName) : a + b = ⟨a.toBitVec + b.toBitVec⟩ := rfl
 
-theorem zero_def : (0 : $typeName) = ⟨0⟩ := rfl
-theorem one_def : (1 : $typeName) = ⟨1⟩ := rfl
-theorem sub_def (a b : $typeName) : a - b = ⟨a.toBitVec - b.toBitVec⟩ := rfl
-theorem mul_def (a b : $typeName) : a * b = ⟨a.toBitVec * b.toBitVec⟩ := rfl
-theorem mod_def (a b : $typeName) : a % b = ⟨a.toBitVec % b.toBitVec⟩ := rfl
-theorem add_def (a b : $typeName) : a + b = ⟨a.toBitVec + b.toBitVec⟩ := rfl
+  @[simp] theorem toNat_mk : (mk a).toNat = a.toNat := rfl
 
-@[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
-  | ⟨_, _⟩ => rfl
+  @[simp] theorem toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
 
-theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
-  Nat.mod_eq_of_lt
+  @[simp] theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatCore n h).toNat = n := BitVec.toNat_ofNatLt ..
 
-theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
-  rw [toNat, toBitVec_eq_of_lt h]
+  @[simp] theorem val_val_eq_toNat (x : $typeName) : x.val.val = x.toNat := rfl
 
-theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
+  theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
 
-theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
+  @[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
+    | ⟨_, _⟩ => rfl
 
-@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := by simp [le_def, lt_def]
+  theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
+    Nat.mod_eq_of_lt
 
-@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := by simp [le_def, lt_def]
+  theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
+    rw [toNat, toBitVec_eq_of_lt h]
 
-@[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
+  theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
 
-@[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
+  theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
 
-protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
+  theorem le_iff_toNat_le {a b : $typeName} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
 
-protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
+  theorem lt_iff_toNat_lt {a b : $typeName} : a < b ↔ a.toNat < b.toNat := .rfl
 
-protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
+  @[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := by simp [le_def, lt_def]
 
-protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
+  @[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := by simp [le_def, lt_def]
 
-protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
+  @[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
 
-protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
-  cases a; cases b; simp_all
+  @[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
 
-open $typeName (eq_of_toBitVec_eq) in
-protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
-  rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
+  protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
 
-open $typeName (toBitVec_eq_of_eq) in
-protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
-  fun h' => absurd (toBitVec_eq_of_eq h') h
+  protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
 
-open $typeName (ne_of_toBitVec_ne) in
-protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
-  apply ne_of_toBitVec_ne
-  apply BitVec.ne_of_lt
-  simpa [lt_def] using h
+  protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
 
-@[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
+  protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
 
-@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
+  protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
 
-@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv  ..
+  protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
+    cases a; cases b; simp_all
 
-@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := BitVec.toNat_sub_of_le
+  open $typeName (eq_of_toBitVec_eq toBitVec_eq_of_eq) in
+  protected theorem toBitVec_inj {a b : $typeName} : a.toBitVec = b.toBitVec ↔ a = b :=
+    Iff.intro eq_of_toBitVec_eq toBitVec_eq_of_eq
 
-protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
+  open $typeName (eq_of_toBitVec_eq) in
+  protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
+    rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
 
-open $typeName (toNat_mod toNat_lt_size) in
-protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % ofNat m) < m := by
-  intro u h1
-  by_cases h2 : m < size
-  · rw [toNat_mod, toNat_ofNat_of_lt h2]
-    apply Nat.mod_lt _ h1
-  · apply Nat.lt_of_lt_of_le
-    · apply toNat_lt_size
-    · simpa using h2
+  open $typeName (eq_of_val_eq) in
+  protected theorem val_inj {a b : $typeName} : a.val = b.val ↔ a = b :=
+    Iff.intro eq_of_val_eq (congrArg val)
 
-open $typeName (toNat_mod_lt) in
-set_option linter.deprecated false in
-@[deprecated toNat_mod_lt (since := "2024-09-24")]
-protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
-  intro u
-  simp only [(· % ·)]
-  simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
-    Nat.reducePow]
-  rw [Nat.mod_eq_of_lt]
-  · apply Nat.mod_lt
-  · apply Nat.lt_of_le_of_lt
-    · apply Nat.mod_le
-    · apply Fin.is_lt
+  open $typeName (toBitVec_eq_of_eq) in
+  protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
+    fun h' => absurd (toBitVec_eq_of_eq h') h
 
-protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
-  simp only [lt_def, mod_def]
-  apply BitVec.umod_lt
+  open $typeName (ne_of_toBitVec_ne) in
+  protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
+    apply ne_of_toBitVec_ne
+    apply BitVec.ne_of_lt
+    simpa [lt_def] using h
 
-protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
-  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+  @[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
 
-@[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
+  @[simp] protected theorem toNat_add (a b : $typeName) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ $bits := BitVec.toNat_add ..
 
-@[simp]
-theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+  protected theorem toNat_sub (a b : $typeName) : (a - b).toNat = (2 ^ $bits - b.toNat + a.toNat) % 2 ^ $bits := BitVec.toNat_sub  ..
 
-@[simp]
-theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
+  @[simp] protected theorem toNat_mul (a b : $typeName) : (a * b).toNat = a.toNat * b.toNat % 2 ^ $bits := BitVec.toNat_mul  ..
 
-@[simp]
-theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
+  @[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
 
-end $typeName
-)
+  @[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv  ..
 
-declare_uint_theorems UInt8
-declare_uint_theorems UInt16
-declare_uint_theorems UInt32
-declare_uint_theorems UInt64
-declare_uint_theorems USize
+  @[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := BitVec.toNat_sub_of_le
+
+  protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
+
+  open $typeName (toNat_mod toNat_lt_size) in
+  protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % ofNat m) < m := by
+    intro u h1
+    by_cases h2 : m < size
+    · rw [toNat_mod, toNat_ofNat_of_lt h2]
+      apply Nat.mod_lt _ h1
+    · apply Nat.lt_of_lt_of_le
+      · apply toNat_lt_size
+      · simpa using h2
+
+  open $typeName (toNat_mod_lt) in
+  set_option linter.deprecated false in
+  @[deprecated toNat_mod_lt (since := "2024-09-24")]
+  protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
+    intro u
+    simp only [(· % ·)]
+    simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
+      Nat.reducePow]
+    rw [Nat.mod_eq_of_lt]
+    · apply Nat.mod_lt
+    · apply Nat.lt_of_le_of_lt
+      · apply Nat.mod_le
+      · apply Fin.is_lt
+
+  protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
+    simp only [lt_def, mod_def]
+    apply BitVec.umod_lt
+
+  protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
+    | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+  protected theorem toNat_inj : ∀ {a b : $typeName}, a.toNat = b.toNat ↔ a = b :=
+    Iff.intro toNat.inj (congrArg toNat)
+
+  open $typeName (toNat_inj) in
+  protected theorem le_antisymm_iff {a b : $typeName} : a = b ↔ a ≤ b ∧ b ≤ a :=
+    toNat_inj.symm.trans Nat.le_antisymm_iff
+
+  open $typeName (le_antisymm_iff) in
+  protected theorem le_antisymm {a b : $typeName} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b :=
+    le_antisymm_iff.2 ⟨h₁, h₂⟩
+
+  @[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
+
+  @[simp] protected theorem ofNat_toNat {x : $typeName} : ofNat x.toNat = x := by
+    apply toNat.inj
+    simp [Nat.mod_eq_of_lt x.toNat_lt_size]
+
+  @[simp]
+  theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+
+  @[simp]
+  theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
+
+  @[simp]
+  theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
+
+  )
+  if let some nbits := bits.raw.isNatLit? then
+    if nbits > 8 then
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUInt8 (x : $typeName) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl)
+    if nbits < 16 then
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUInt16 (x : $typeName) : x.toUInt16.toNat = x.toNat := rfl)
+    else if nbits > 16 then
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUInt16 (x : $typeName) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl)
+    if nbits < 32 then
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUInt32 (x : $typeName) : x.toUInt32.toNat = x.toNat := rfl)
+    else if nbits > 32 then
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUInt32 (x : $typeName) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl)
+    if nbits ≤ 32 then
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUSize (x : $typeName) : x.toUSize.toNat = x.toNat := rfl)
+    else
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUSize (x : $typeName) : x.toUSize.toNat = x.toNat % 2 ^ System.Platform.numBits := rfl)
+    if nbits < 64 then
+      cmds := cmds.push <| ←
+        `(@[simp] theorem toNat_toUInt64 (x : $typeName) : x.toUInt64.toNat = x.toNat := rfl)
+  cmds := cmds.push <| ← `(end $typeName)
+  return ⟨mkNullNode cmds⟩
+
+declare_uint_theorems UInt8 8
+declare_uint_theorems UInt16 16
+declare_uint_theorems UInt32 32
+declare_uint_theorems UInt64 64
+declare_uint_theorems USize System.Platform.numBits
+
+@[simp] theorem USize.toNat_ofNat32 {n : Nat} {h : n < 4294967296} : (ofNat32 n h).toNat = n := rfl
+
+@[simp] theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32  := rfl
+
+@[simp] theorem USize.toNat_toUInt64 (x : USize) : x.toUInt64.toNat = x.toNat := rfl
 
 theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : toNat (ofNat n) = n :=
   toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h le_usize_size)

src/Init/Data/Vector/Basic.lean

@@ -21,6 +21,9 @@ deriving Repr, DecidableEq
 
 attribute [simp] Vector.size_toArray
 
+/-- Convert `xs : Array α` to `Vector α xs.size`. -/
+abbrev Array.toVector (xs : Array α) : Vector α xs.size := .mk xs rfl
+
 namespace Vector
 
 /-- Syntax for `Vector α n` -/

src/Init/Data/Vector/Lemmas.lean

@@ -13,8 +13,6 @@ Lemmas about `Vector α n`
 
 namespace Vector
 
-theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
-
 @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
     (Vector.mk data size)[i] = data[i] := rfl
 
@@ -23,9 +21,6 @@ theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by sim
   cases xs
   simp
 
-theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
-    xs.toList[i] = xs[i]'(by simpa using h) := by simp
-
 @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
     (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
   simp [ofFn]
@@ -93,6 +88,157 @@ defeq issues in the implicit size argument.
     subst h
     simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero]
 
+
+/-! ### mk lemmas -/
+
+theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
+
+@[simp] theorem allDiff_mk [BEq α] (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).allDiff = a.allDiff := rfl
+
+@[simp] theorem mk_append_mk (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
+    Vector.mk a ha ++ Vector.mk b hb = Vector.mk (a ++ b) (by simp [ha, hb]) := rfl
+
+@[simp] theorem back!_mk [Inhabited α] (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).back! = a.back! := rfl
+
+@[simp] theorem back?_mk (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).back? = a.back? := rfl
+
+@[simp] theorem drop_mk (a : Array α) (h : a.size = n) (m) :
+    (Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl
+
+@[simp] theorem eraseIdx_mk (a : Array α) (h : a.size = n) (i) (h') :
+    (Vector.mk a h).eraseIdx i h' = Vector.mk (a.eraseIdx i) (by simp [h]) := rfl
+
+@[simp] theorem eraseIdx!_mk (a : Array α) (h : a.size = n) (i) (hi : i < n) :
+    (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx i) (by simp [h, hi]) := by
+  simp [Vector.eraseIdx!, hi]
+
+@[simp] theorem extract_mk (a : Array α) (h : a.size = n) (start stop) :
+    (Vector.mk a h).extract start stop = Vector.mk (a.extract start stop) (by simp [h]) := rfl
+
+@[simp] theorem indexOf?_mk [BEq α] (a : Array α) (h : a.size = n) (x : α) :
+    (Vector.mk a h).indexOf? x = (a.indexOf? x).map (Fin.cast h) := rfl
+
+@[simp] theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
+    Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r := by
+  simp [Vector.isEqv, Array.isEqv, ha, hb]
+
+@[simp] theorem mk_isPrefixOf_mk [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
+    (Vector.mk a ha).isPrefixOf (Vector.mk b hb) = a.isPrefixOf b := rfl
+
+@[simp] theorem map_mk (a : Array α) (h : a.size = n) (f : α → β) :
+    (Vector.mk a h).map f = Vector.mk (a.map f) (by simp [h]) := rfl
+
+@[simp] theorem reverse_mk (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).reverse = Vector.mk a.reverse (by simp [h]) := rfl
+
+@[simp] theorem set_mk (a : Array α) (h : a.size = n) (i x w) :
+    (Vector.mk a h).set i x = Vector.mk (a.set i x) (by simp [h]) := rfl
+
+@[simp] theorem set!_mk (a : Array α) (h : a.size = n) (i x) :
+    (Vector.mk a h).set! i x = Vector.mk (a.set! i x) (by simp [h]) := rfl
+
+@[simp] theorem setIfInBounds_mk (a : Array α) (h : a.size = n) (i x) :
+    (Vector.mk a h).setIfInBounds i x = Vector.mk (a.setIfInBounds i x) (by simp [h]) := rfl
+
+@[simp] theorem swap_mk (a : Array α) (h : a.size = n) (i j) (hi hj) :
+    (Vector.mk a h).swap i j = Vector.mk (a.swap i j) (by simp [h]) :=
+  rfl
+
+@[simp] theorem swapIfInBounds_mk (a : Array α) (h : a.size = n) (i j) :
+    (Vector.mk a h).swapIfInBounds i j = Vector.mk (a.swapIfInBounds i j) (by simp [h]) := rfl
+
+@[simp] theorem swapAt_mk (a : Array α) (h : a.size = n) (i x) (hi) :
+    (Vector.mk a h).swapAt i x =
+      ((a.swapAt i x).fst, Vector.mk (a.swapAt i x).snd (by simp [h])) :=
+  rfl
+
+@[simp] theorem swapAt!_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt! i x =
+    ((a.swapAt! i x).fst, Vector.mk (a.swapAt! i x).snd (by simp [h])) := rfl
+
+@[simp] theorem take_mk (a : Array α) (h : a.size = n) (m) :
+    (Vector.mk a h).take m = Vector.mk (a.take m) (by simp [h]) := rfl
+
+@[simp] theorem mk_zipWith_mk (f : α → β → γ) (a : Array α) (b : Array β)
+      (ha : a.size = n) (hb : b.size = n) : zipWith (Vector.mk a ha) (Vector.mk b hb) f =
+        Vector.mk (Array.zipWith a b f) (by simp [ha, hb]) := rfl
+
+/-! ### toArray lemmas -/
+
+@[simp] theorem toArray_append (a : Vector α m) (b : Vector α n) :
+    (a ++ b).toArray = a.toArray ++ b.toArray := rfl
+
+@[simp] theorem toArray_drop (a : Vector α n) (m) :
+    (a.drop m).toArray = a.toArray.extract m a.size := rfl
+
+@[simp] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
+
+@[simp] theorem toArray_mkEmpty (cap) :
+    (Vector.mkEmpty (α := α) cap).toArray = Array.mkEmpty cap := rfl
+
+@[simp] theorem toArray_eraseIdx (a : Vector α n) (i) (h) :
+    (a.eraseIdx i h).toArray = a.toArray.eraseIdx i (by simp [h]) := rfl
+
+@[simp] theorem toArray_eraseIdx! (a : Vector α n) (i) (hi : i < n) :
+    (a.eraseIdx! i).toArray = a.toArray.eraseIdx! i := by
+  cases a; simp_all [Array.eraseIdx!]
+
+@[simp] theorem toArray_extract (a : Vector α n) (start stop) :
+    (a.extract start stop).toArray = a.toArray.extract start stop := rfl
+
+@[simp] theorem toArray_map (f : α → β) (a : Vector α n) :
+    (a.map f).toArray = a.toArray.map f := rfl
+
+@[simp] theorem toArray_ofFn (f : Fin n → α) : (Vector.ofFn f).toArray = Array.ofFn f := rfl
+
+@[simp] theorem toArray_pop (a : Vector α n) : a.pop.toArray = a.toArray.pop := rfl
+
+@[simp] theorem toArray_push (a : Vector α n) (x) : (a.push x).toArray = a.toArray.push x := rfl
+
+@[simp] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
+
+@[simp] theorem toArray_reverse (a : Vector α n) : a.reverse.toArray = a.toArray.reverse := rfl
+
+@[simp] theorem toArray_set (a : Vector α n) (i x h) :
+    (a.set i x).toArray = a.toArray.set i x (by simpa using h):= rfl
+
+@[simp] theorem toArray_set! (a : Vector α n) (i x) :
+    (a.set! i x).toArray = a.toArray.set! i x := rfl
+
+@[simp] theorem toArray_setIfInBounds (a : Vector α n) (i x) :
+    (a.setIfInBounds i x).toArray = a.toArray.setIfInBounds i x := rfl
+
+@[simp] theorem toArray_singleton (x : α) : (Vector.singleton x).toArray = #[x] := rfl
+
+@[simp] theorem toArray_swap (a : Vector α n) (i j) (hi hj) : (a.swap i j).toArray =
+    a.toArray.swap i j (by simp [hi, hj]) (by simp [hi, hj]) := rfl
+
+@[simp] theorem toArray_swapIfInBounds (a : Vector α n) (i j) :
+    (a.swapIfInBounds i j).toArray = a.toArray.swapIfInBounds i j := rfl
+
+@[simp] theorem toArray_swapAt (a : Vector α n) (i x h) :
+    ((a.swapAt i x).fst, (a.swapAt i x).snd.toArray) =
+      ((a.toArray.swapAt i x (by simpa using h)).fst,
+        (a.toArray.swapAt i x (by simpa using h)).snd) := rfl
+
+@[simp] theorem toArray_swapAt! (a : Vector α n) (i x) :
+    ((a.swapAt! i x).fst, (a.swapAt! i x).snd.toArray) =
+      ((a.toArray.swapAt! i x).fst, (a.toArray.swapAt! i x).snd) := rfl
+
+@[simp] theorem toArray_take (a : Vector α n) (m) : (a.take m).toArray = a.toArray.take m := rfl
+
+@[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
+    (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
+
+/-! ### toList lemmas -/
+
+theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
+
+theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
+    xs.toList[i] = xs[i]'(by simpa using h) := by simp
+
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

src/Init/GetElem.lean

@@ -172,6 +172,16 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
   simp only [getElem?_def] at h ⊢
   split <;> simp_all
 
+@[simp] theorem isNone_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isNone = ¬dom c i := by
+  simp only [getElem?_def]
+  split <;> simp_all
+
+@[simp] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by
+  simp only [getElem?_def]
+  split <;> simp_all
+
 namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where

src/Init/MetaTypes.lean

@@ -224,7 +224,8 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  This option does not have any effect (yet).
+  If `implicitDefEqProofs := true`, `simp` does not create proof terms when the
+  input and output terms are definitionally equal.
   -/
   implicitDefEqProofs : Bool := true
   deriving Inhabited, BEq

src/Init/Notation.lean

@@ -48,6 +48,10 @@ def tactic : Category := {}
 For example, `let x ← e` is a `doElem`, and a `do` block consists of a list of `doElem`s. -/
 def doElem : Category := {}
 
+/-- `structInstFieldDecl` is the syntax category for value declarations for fields in structure instance notation.
+For example, the `:= 1` and `| 0 => 0 | n + 1 => n` in `{ x := 1, f | 0 => 0 | n + 1 => n }` are in the `structInstFieldDecl` class. -/
+def structInstFieldDecl : Category := {}
+
 /-- `level` is a builtin syntax category for universe levels.
 This is the `u` in `Sort u`: it can contain `max` and `imax`, addition with
 constants, and variables. -/

src/Init/Omega/IntList.lean

@@ -32,13 +32,9 @@ theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i) :
   cases xs[i]? <;> simp_all
 
 theorem get_of_length_le {xs : IntList} (h : xs.length ≤ i) : xs.get i = 0 := by
-  rw [get, List.get?_eq_none.mpr h]
+  rw [get, List.get?_eq_none_iff.mpr h]
   rfl
 
--- theorem lt_length_of_get_nonzero {xs : IntList} (h : xs.get i ≠ 0) : i < xs.length := by
---   revert h
---   simpa using mt get_of_length_le
-
 /-- Like `List.set`, but right-pad with zeroes as necessary first. -/
 def set (xs : IntList) (i : Nat) (y : Int) : IntList :=
   match xs, i with

src/Init/System/IO.lean

@@ -959,3 +959,25 @@ syntax "println! " (interpolatedStr(term) <|> term) : term
 macro_rules
   | `(println! $msg:interpolatedStr) => `((IO.println (s! $msg) : IO Unit))
   | `(println! $msg:term)            => `((IO.println $msg : IO Unit))
+
+/--
+  Marks given value and its object graph closure as multi-threaded if currently
+  marked single-threaded. This will make reference counter updates atomic and
+  thus more costly. It can still be useful to do eagerly when the value will be
+  shared between threads later anyway and there is available time budget to mark
+  it now. -/
+@[extern "lean_runtime_mark_multi_threaded"]
+def Runtime.markMultiThreaded (a : α) : BaseIO α := return a
+
+/--
+Marks given value and its object graph closure as persistent. This will remove
+reference counter updates but prevent the closure from being deallocated until
+the end of the process! It can still be useful to do eagerly when the value
+will be marked persistent later anyway and there is available time budget to
+mark it now or it would be unnecessarily marked multi-threaded in between.
+
+This function is only safe to use on objects (in the full closure) which are
+not used concurrently or which are already persistent.
+-/
+@[extern "lean_runtime_mark_persistent"]
+unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a

src/Init/System/Platform.lean

@@ -23,5 +23,14 @@ def isEmscripten : Bool := getIsEmscripten ()
 /-- The LLVM target triple of the current platform. Empty if missing at Lean compile time. -/
 def target : String := getTarget ()
 
+theorem numBits_pos : 0 < numBits := by
+  cases numBits_eq <;> next h => simp [h]
+
+theorem le_numBits : 32 ≤ numBits := by
+  cases numBits_eq <;> next h => simp [h]
+
+theorem numBits_le : numBits ≤ 64 := by
+  cases numBits_eq <;> next h => simp [h]
+
 end Platform
 end System

src/Init/Util.lean

@@ -79,25 +79,3 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 
 @[implemented_by withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
-
-/--
-  Marks given value and its object graph closure as multi-threaded if currently
-  marked single-threaded. This will make reference counter updates atomic and
-  thus more costly. It can still be useful to do eagerly when the value will be
-  shared between threads later anyway and there is available time budget to mark
-  it now. -/
-@[extern "lean_runtime_mark_multi_threaded"]
-def Runtime.markMultiThreaded (a : α) : α := a
-
-/--
-Marks given value and its object graph closure as persistent. This will remove
-reference counter updates but prevent the closure from being deallocated until
-the end of the process! It can still be useful to do eagerly when the value
-will be marked persistent later anyway and there is available time budget to
-mark it now or it would be unnecessarily marked multi-threaded in between.
-
-This function is only safe to use on objects (in the full closure) which are
-not used concurrently or which are already persistent.
--/
-@[extern "lean_runtime_mark_persistent"]
-unsafe def Runtime.markPersistent (a : α) : α := a

src/Lean/Elab/MutualDef.lean

@@ -282,52 +282,36 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
       k fvars
   loop 0 #[]
 
-private def expandWhereStructInst : Macro
-  | whereStx@`(Parser.Command.whereStructInst|where%$whereTk $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
-    let letIdDecls ← decls.mapM fun stx => match stx with
-      | `(letDecl|$_decl:letPatDecl) => Macro.throwErrorAt stx "patterns are not allowed here"
-      | `(letDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl (useExplicit := false)
-      | `(letDecl|$decl:letIdDecl)   => pure decl
-      | _                            => Macro.throwUnsupported
-    let structInstFields ← letIdDecls.mapM fun
-      | stx@`(letIdDecl|$id:ident $binders* $[: $ty?]? := $val) => withRef stx do
-        let mut val := val
-        if let some ty := ty? then
-          val ← `(($val : $ty))
-        -- HACK: this produces invalid syntax, but the fun elaborator supports letIdBinders as well
-        have : Coe (TSyntax ``letIdBinder) (TSyntax ``funBinder) := ⟨(⟨·⟩)⟩
-        val ← if binders.size > 0 then `(fun $binders* => $val) else pure val
-        `(structInstField|$id:ident := $val)
-      | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
-      | _ => Macro.throwUnsupported
+private def expandWhereStructInst : Macro := fun whereStx => do
+  let `(Parser.Command.whereStructInst| where%$whereTk $[$structInstFields];* $[$whereDecls?:whereDecls]?) := whereStx
+    | Macro.throwUnsupported
 
-    let startOfStructureTkInfo : SourceInfo :=
-      match whereTk.getPos? with
-      | some pos => .synthetic pos ⟨pos.byteIdx + 1⟩ true
-      | none => .none
-    -- Position the closing `}` at the end of the trailing whitespace of `where $[$_:letDecl];*`.
-    -- We need an accurate range of the generated structure instance in the generated `TermInfo`
-    -- so that we can determine the expected type in structure field completion.
-    let structureStxTailInfo :=
-      whereStx[1].getTailInfo?
-      <|> whereStx[0].getTailInfo?
-    let endOfStructureTkInfo : SourceInfo :=
-      match structureStxTailInfo with
-      | some (SourceInfo.original _ _ trailing _) =>
-        let tokenPos := trailing.str.prev trailing.stopPos
-        let tokenEndPos := trailing.stopPos
-        .synthetic tokenPos tokenEndPos true
-      | _ => .none
+  let startOfStructureTkInfo : SourceInfo :=
+    match whereTk.getPos? with
+    | some pos => .synthetic pos ⟨pos.byteIdx + 1⟩ true
+    | none => .none
+  -- Position the closing `}` at the end of the trailing whitespace of `where $[$_:letDecl];*`.
+  -- We need an accurate range of the generated structure instance in the generated `TermInfo`
+  -- so that we can determine the expected type in structure field completion.
+  let structureStxTailInfo :=
+    whereStx[1].getTailInfo?
+    <|> whereStx[0].getTailInfo?
+  let endOfStructureTkInfo : SourceInfo :=
+    match structureStxTailInfo with
+    | some (SourceInfo.original _ _ trailing _) =>
+      let tokenPos := trailing.str.prev trailing.stopPos
+      let tokenEndPos := trailing.stopPos
+      .synthetic tokenPos tokenEndPos true
+    | _ => .none
 
-    let body ← `(structInst| { $structInstFields,* })
-    let body := body.raw.setInfo <|
-      match startOfStructureTkInfo.getPos?, endOfStructureTkInfo.getTailPos? with
-      | some startPos, some endPos => .synthetic startPos endPos true
-      | _, _ => .none
-    match whereDecls? with
-    | some whereDecls => expandWhereDecls whereDecls body
-    | none => return body
-  | _ => Macro.throwUnsupported
+  let body ← `(structInst| { $structInstFields,* })
+  let body := body.raw.setInfo <|
+    match startOfStructureTkInfo.getPos?, endOfStructureTkInfo.getTailPos? with
+    | some startPos, some endPos => .synthetic startPos endPos true
+    | _, _ => .none
+  match whereDecls? with
+  | some whereDecls => expandWhereDecls whereDecls body
+  | none => return body
 
 /-
 Recall that

src/Lean/Elab/PatternVar.lean

@@ -265,7 +265,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
       | `(Parser.Term.structInstField| $lval:structInstLVal := $val) => do
         let newVal ← collect val
         `(Parser.Term.structInstField| $lval:structInstLVal := $newVal)
-      | _ => throwInvalidPattern  -- `structInstFieldAbbrev` should be expanded at this point
+      | _ => throwInvalidPattern  -- `structInstField` should be expanded at this point
     `({ $[$srcs?,* with]? $fields,* $[..%$ell?]? $[: $ty?]? })
   | _ => throwInvalidPattern
 

src/Lean/Elab/StructInst.lean

@@ -31,13 +31,32 @@ open Meta
 open TSyntax.Compat
 
 /-!
-Recall that structure instances are of the form:
-```
-"{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
-    >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
+Recall that structure instances are (after removing parsing and pretty printing hints):
+
+```lean
+def structInst := leading_parser
+  "{ " >> optional (sepBy1 termParser ", " >> " with ")
+    >> structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
     >> optEllipsis
-    >> optional (" : " >> termParser)
-    >> " }"
+    >> optional (" : " >> termParser) >> " }"
+
+def structInstField := leading_parser
+  structInstLVal >> optional (many structInstFieldBinder >> optType >> structInstFieldDecl)
+
+@[builtin_structInstFieldDecl_parser]
+def structInstFieldDef := leading_parser
+  " := " >> termParser
+
+@[builtin_structInstFieldDecl_parser]
+def structInstFieldEqns := leading_parser
+  matchAlts
+
+def structInstWhereBody := leading_parser
+  structInstFields (sepByIndent structInstField "; " (allowTrailingSep := true))
+
+@[builtin_structInstFieldDecl_parser]
+def structInstFieldWhere := leading_parser
+  "where" >> structInstWhereBody
 ```
 -/
 
@@ -54,22 +73,57 @@ Structure instance notation makes use of the expected type.
     let stxNew   := stx.setArg 4 mkNullNode
     `(($stxNew : $expected))
 
+def mkStructInstField (lval : TSyntax ``Parser.Term.structInstLVal) (binders : TSyntaxArray ``Parser.Term.structInstFieldBinder)
+    (type? : Option Term) (val : Term) : MacroM (TSyntax ``Parser.Term.structInstField) := do
+  let mut val := val
+  if let some type := type? then
+    val ← `(($val : $type))
+  if !binders.isEmpty then
+    -- HACK: this produces invalid syntax, but the fun elaborator supports structInstFieldBinder as well
+    val ← `(fun $binders* => $val)
+  `(Parser.Term.structInstField| $lval := $val)
+
 /--
-Expands field abbreviation notation.
-Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }`.
+Takes an arbitrary `structInstField` and expands it to be a `structInstFieldDef` without any binders or type ascription.
 -/
-@[builtin_macro Lean.Parser.Term.structInst] def expandStructInstFieldAbbrev : Macro
-  | `({ $[$srcs,* with]? $fields,* $[..%$ell]? $[: $ty]? }) =>
-    if fields.getElems.raw.any (·.getKind == ``Lean.Parser.Term.structInstFieldAbbrev) then do
-      let fieldsNew ← fields.getElems.mapM fun
-        | `(Parser.Term.structInstFieldAbbrev| $id:ident) =>
-          `(Parser.Term.structInstField| $id:ident := $id:ident)
-        | field => return field
-      `({ $[$srcs,* with]? $fieldsNew,* $[..%$ell]? $[: $ty]? })
-    else
-      Macro.throwUnsupported
+private def expandStructInstField (stx : Syntax) : MacroM (Option Syntax) := withRef stx do
+  match stx with
+  | `(Parser.Term.structInstField| $_:structInstLVal := $_) =>
+    -- Already expanded.
+    return none
+  | `(Parser.Term.structInstField| $lval:structInstLVal $[$binders]* $[: $ty?]? $decl:structInstFieldDecl) =>
+    match decl with
+    | `(Parser.Term.structInstFieldDef| := $val) =>
+      mkStructInstField lval binders ty? val
+    | `(Parser.Term.structInstFieldEqns| $alts:matchAlts) =>
+      let val ← expandMatchAltsIntoMatch stx alts (useExplicit := false)
+      mkStructInstField lval binders ty? val
+    | _ => Macro.throwUnsupported
+  | `(Parser.Term.structInstField| $lval:structInstLVal) =>
+    -- Abbreviation
+    match lval with
+    | `(Parser.Term.structInstLVal| $id:ident) =>
+      mkStructInstField lval #[] none id
+    | _ =>
+      Macro.throwErrorAt lval "unsupported structure instance field abbreviation, expecting identifier"
   | _ => Macro.throwUnsupported
 
+/--
+Expands fields.
+* Abbrevations. Example: `{ x }` expands to `{ x := x }`.
+* Equations. Example: `{ f | 0 => 0 | n + 1 => n }` expands to `{ f := fun x => match x with | 0 => 0 | n + 1 => n }`.
+* Binders and types. Example: `{ f n : Nat := n + 1 }` expands to `{ f := fun n => (n + 1 : Nat) }`.
+-/
+@[builtin_macro Lean.Parser.Term.structInst] def expandStructInstFields : Macro | stx => do
+  let structInstFields := stx[2]
+  let fields := structInstFields[0].getSepArgs
+  let fields? ← fields.mapM expandStructInstField
+  if fields?.all (·.isNone) then
+    Macro.throwUnsupported
+  let fields := fields?.zipWith fields Option.getD
+  let structInstFields := structInstFields.setArg 0 <| Syntax.mkSep fields (mkAtomFrom stx ", ")
+  return stx.setArg 2 structInstFields
+
 /--
 If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable,
 expands into `let __src := sᵢ; { ..., __src, ... with ... }`.
@@ -187,12 +241,13 @@ def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 -/
 private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
   let s? ← stx[2][0].getSepArgs.foldlM (init := none) fun s? arg => do
-    /- arg is of the form `structInstFieldAbbrev <|> structInstField` -/
-    if arg.getKind == ``Lean.Parser.Term.structInstField then
-      /- Remark: the syntax for `structInstField` is
+    /- arg is of the form `structInstField`. It should be macro expanded at this point, but we make sure it's the case. -/
+    if arg[1][2].getKind == ``Lean.Parser.Term.structInstFieldDef then
+      /- Remark: the syntax for `structInstField` after macro expansion is
          ```
          def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
-         def structInstField  := leading_parser structInstLVal >> " := " >> termParser
+         def structInstFieldDef := leading_parser
+           structInstLVal >> group (null >> null >> group (" := " >> termParser))
          ```
       -/
       let lval := arg[0]
@@ -235,7 +290,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
     withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   let rest := modifyOp[0][1]
   if rest.isNone then
-    cont modifyOp[2]
+    cont modifyOp[1][2][1]
   else
     let s ← `(s)
     let valFirst  := rest[0]
@@ -388,7 +443,7 @@ Converts a `FieldLHS` back into syntax. This assumes the `ref` fields have the c
 
 Recall that `structInstField` elements have the form
 ```lean
-def structInstField  := leading_parser structInstLVal >> " := " >> termParser
+def structInstField  := leading_parser structInstLVal >> group (null >> null >> group (" := " >> termParser))
 def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
 def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 ```
@@ -412,9 +467,9 @@ Converts a `Field StructInstView` back into syntax. Used to construct synthetic
 private def Field.toSyntax : Field → Syntax
   | field =>
     let stx := field.ref
-    let stx := stx.setArg 2 field.val.toSyntax
+    let stx := stx.setArg 1 <| stx[1].setArg 2 <| stx[1][2].setArg 1 field.val.toSyntax
     match field.lhs with
-    | first::rest => stx.setArg 0 <| mkNullNode #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
+    | first::rest => stx.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
     | _ => unreachable!
 
 /-- Creates a view of a field left-hand side. -/
@@ -428,7 +483,7 @@ private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
       return FieldLHS.fieldName stx stx.getId.eraseMacroScopes
     else match stx.isFieldIdx? with
       | some idx => return FieldLHS.fieldIndex stx idx
-      | none     => Macro.throwError "unexpected structure syntax"
+      | none     => Macro.throwErrorAt stx "unexpected structure syntax"
 
 /--
 Creates a structure instance view from structure instance notation
@@ -436,21 +491,21 @@ and the computed structure name (from `Lean.Elab.Term.StructInst.getStructName`)
 and structure source view (from `Lean.Elab.Term.StructInst.getStructSources`).
 -/
 private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesView) : MacroM StructInstView := do
-  /- Recall that `stx` is of the form
-     ```
-     leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
-                 >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ...)
-                 >> optional ".."
-                 >> optional (" : " >> termParser)
-                 >> " }"
-     ```
-
-     This method assumes that `structInstFieldAbbrev` had already been expanded.
+  /-
+  Recall that `stx` is of the form
+  ```
+  leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
+              >> structInstFields (sepByIndent structInstField ...)
+              >> optional ".."
+              >> optional (" : " >> termParser)
+              >> " }"
+  ```
+  This method assumes that `structInstField` had already been expanded by the macro `expandStructInstFields`.
   -/
   let fields ← stx[2][0].getSepArgs.toList.mapM fun fieldStx => do
-    let val      := fieldStx[2]
-    let first    ← toFieldLHS fieldStx[0][0]
-    let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
+    let `(Parser.Term.structInstField| $lval:structInstLVal := $val) := fieldStx | Macro.throwUnsupported
+    let first ← toFieldLHS lval.raw[0]
+    let rest  ← lval.raw[1].getArgs.toList.mapM toFieldLHS
     return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field }
   return { ref := stx, structName, params := #[], fields, sources }
 
@@ -596,7 +651,7 @@ mutual
             let updateSource (structStx : Syntax) : TermElabM Syntax := do
               let sourcesNew ← s.sources.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
               let explicitSourceStx := if sourcesNew.isEmpty then mkNullNode else mkSourcesWithSyntax sourcesNew
-              let implicitSourceStx := s.sources.implicit.getD mkNullNode
+              let implicitSourceStx := s.sources.implicit.getD (mkNode ``Parser.Term.optEllipsis #[mkNullNode])
               return (structStx.setArg 1 explicitSourceStx).setArg 3 implicitSourceStx
             let valStx := s.ref -- construct substructure syntax using s.ref as template
             let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type

src/Lean/Environment.lean

@@ -900,7 +900,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
        `markPersistent` multiple times like this.
 
        Safety: There are no concurrent accesses to `env` at this point. -/
-    env := unsafe Runtime.markPersistent env
+    env ← unsafe Runtime.markPersistent env
   env ← finalizePersistentExtensions env s.moduleData opts
   if leakEnv then
     /- Ensure the final environment including environment extension states is
@@ -908,7 +908,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
 
        Safety: There are no concurrent accesses to `env` at this point, assuming
        extensions' `addImportFn`s did not spawn any unbound tasks. -/
-    env := unsafe Runtime.markPersistent env
+    env ← unsafe Runtime.markPersistent env
   pure env
 
 @[export lean_import_modules]

src/Lean/Expr.lean

@@ -1366,7 +1366,11 @@ See also `Lean.Expr.instantiateRange`, which instantiates with the "backwards" i
 @[extern "lean_expr_instantiate_rev_range"]
 opaque instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (subst : @& Array Expr) : Expr
 
-/-- Replace free (or meta) variables `xs` with loose bound variables. -/
+/-- Replace free (or meta) variables `xs` with loose bound variables,
+with `xs` ordered from outermost to innermost de Bruijn index.
+
+For example, `e := f x y` with `xs := #[x, y]` goes to `f #1 #0`,
+whereas `e := f x y` with `xs := #[y, x]` goes to `f #0 #1`. -/
 @[extern "lean_expr_abstract"]
 opaque abstract (e : @& Expr) (xs : @& Array Expr) : Expr
 

src/Lean/Language/Lean.lean

@@ -247,7 +247,7 @@ structure SetupImportsResult where
 /-- Performance option used by cmdline driver. -/
 register_builtin_option internal.cmdlineSnapshots : Bool := {
   defValue := false
-  descr    := "mark persistent and reduce information stored in snapshots to the minimum necessary \
+  descr    := "reduce information stored in snapshots to the minimum necessary \
     for the cmdline driver: diagnostics per command and final full snapshot"
 }
 
@@ -639,30 +639,21 @@ where
         pos      := ctx.fileMap.toPosition beginPos
         data     := output
       }
-    let cmdState := { cmdState with messages }
+    let cmdState : Command.State := { cmdState with messages }
+    let mut reportedCmdState := cmdState
     -- definitely resolve eventually
     snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
 
-    let mut infoTree : InfoTree := cmdState.infoState.trees[0]!
+    let infoTree : InfoTree := cmdState.infoState.trees[0]!
     let cmdline := internal.cmdlineSnapshots.get scope.opts && !Parser.isTerminalCommand stx
-    if cmdline && !Elab.async.get scope.opts then
-      /-
-      Safety: `infoTree` was created by `elabCommandTopLevel`. Thus it
-      should not have any concurrent accesses if we are on the cmdline and
-      async elaboration is disabled.
-      -/
-      -- TODO: we should likely remove this call when `Elab.async` is turned on
-      -- by default
-      infoTree := unsafe Runtime.markPersistent infoTree
+    if cmdline then
+      -- discard all metadata apart from the environment; see `internal.cmdlineSnapshots`
+      reportedCmdState := { env := reportedCmdState.env, maxRecDepth := 0 }
     finishedPromise.resolve {
       diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
       infoTree? := infoTree
       traces := cmdState.traceState
-      cmdState := if cmdline then {
-        /- Safety: as above -/
-        env := unsafe Runtime.markPersistent cmdState.env
-        maxRecDepth := 0
-      } else cmdState
+      cmdState := reportedCmdState
     }
     -- The reported `cmdState` in the snapshot may be minimized as seen above, so we return the full
     -- state here for further processing on the same thread

src/Lean/Linter/UnusedVariables.lean

@@ -248,7 +248,7 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesFunArgs opts &&
   stack.matches [`null, none, `null, ``Lean.Parser.Term.letIdDecl, none] &&
   (stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
-  (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Command.whereStructField))
+  (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Term.structInstField))
 
 /--
 Function argument in declaration signature (when `linter.unusedVariables.funArgs` is false)

src/Lean/Meta/Basic.lean

@@ -229,7 +229,7 @@ structure ParamInfo where
   hasFwdDeps     : Bool       := false
   /-- `backDeps` contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on. -/
   backDeps       : Array Nat  := #[]
-  /-- `isProp` is true if the parameter is always a proposition. -/
+  /-- `isProp` is true if the parameter type is always a proposition. -/
   isProp         : Bool       := false
   /--
     `isDecInst` is true if the parameter's type is of the form `Decidable ...`.

src/Lean/Meta/LitValues.lean

@@ -68,7 +68,7 @@ def getFinValue? (e : Expr) : MetaM (Option ((n : Nat) × Fin n)) := OptionT.run
   let n ← getNatValue? (← whnfD type.appArg!)
   match n with
   | 0 => failure
-  | m+1 => return ⟨m+1, Fin.ofNat v⟩
+  | m+1 => return ⟨m+1, Fin.ofNat' _ v⟩
 
 /--
 Return `some ⟨n, v⟩` if `e` is:

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -84,8 +84,22 @@ declare_uint_simprocs UInt8
 declare_uint_simprocs UInt16
 declare_uint_simprocs UInt32
 declare_uint_simprocs UInt64
+
 /-
-We disabled the simprocs for USize since the result of most operations depend on an opaque value: `System.Platform.numBits`.
-We could reduce some cases using the fact that this opaque value is `32` or `64`, but it is unclear whether it would be useful in practice.
+We do not use the normal simprocs for `USize` since the result of most operations depend on an opaque value: `System.Platform.numBits`.
+However, we do reduce natural literals using the fact this opaque value is at least `32`.
 -/
--- declare_uint_simprocs USize
+namespace USize
+
+def fromExpr (e : Expr) : SimpM (Option USize) := do
+  let some (n, _) ← getOfNatValue? e ``USize | return none
+  return USize.ofNat n
+
+builtin_simproc [simp, seval] reduceToNat (USize.toNat _) := fun e => do
+  let_expr USize.toNat e ← e | return .continue
+  let some (n, _) ← getOfNatValue? e ``USize | return .continue
+  unless n < UInt32.size do return .continue
+  let e := toExpr n
+  let p ← mkDecideProof (← mkLT e (mkNatLit UInt32.size))
+  let p := mkApp2 (mkConst ``USize.toNat_ofNat_of_lt_32) e p
+  return .done { expr := e, proof? := p }

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

@@ -108,13 +108,19 @@ where
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"
       return false
 
+private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
+  if thm.rfl then
+    return (← getConfig).implicitDefEqProofs
+  else
+    return false
+
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do
         return none
-      let proof? ← if thm.rfl then
+      let proof? ← if (← useImplicitDefEqProof thm) then
         pure none
       else
         let proof ← instantiateMVars (mkAppN val xs)

src/Lean/Meta/Tactic/Split.lean

@@ -269,7 +269,7 @@ def mkDiscrGenErrorMsg (e : Expr) : MessageData :=
 def throwDiscrGenError (e : Expr) : MetaM α :=
   throwError (mkDiscrGenErrorMsg e)
 
-def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
+def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withContext do
   let some app ← matchMatcherApp? e | throwError "internal error in `split` tactic: match application expected{indentExpr e}\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program"
   let matchEqns ← Match.getEquationsFor app.matcherName
   let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs
@@ -278,43 +278,14 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
     return (i+1, mvarId::mvarIds)
   return mvarIds.reverse
 
-/-- Return an `if-then-else` or `match-expr` to split. -/
-partial def findSplit? (env : Environment) (e : Expr) (splitIte := true) (exceptionSet : ExprSet := {}) : Option Expr :=
-  go e
-where
-  go (e : Expr) : Option Expr :=
-    if let some target := e.find? isCandidate then
-      if e.isIte || e.isDIte then
-        let cond := target.getArg! 1 5
-        -- Try to find a nested `if` in `cond`
-        go cond |>.getD target
-      else
-        some target
-    else
-      none
-
-  isCandidate (e : Expr) : Bool := Id.run do
-    if exceptionSet.contains e then
-      false
-    else if splitIte && (e.isIte || e.isDIte) then
-      !(e.getArg! 1 5).hasLooseBVars
-    else if let some info := isMatcherAppCore? env e then
-      let args := e.getAppArgs
-      for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
-        if args[i]!.hasLooseBVars then
-          return false
-      return true
-    else
-      false
-
 end Split
 
 open Split
 
-partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do
+partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)
   let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
-    if let some e := findSplit? (← getEnv) target splitIte badCases then
+    if let some e ← findSplit? target (if splitIte then .both else .match) badCases then
       if e.isIte || e.isDIte then
         return (← splitIfTarget? mvarId).map fun (s₁, s₂) => [s₁.mvarId, s₂.mvarId]
       else
@@ -333,7 +304,7 @@ partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (L
 
 def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId)) := commitWhenSome? do
   mvarId.withContext do
-    if let some e := findSplit? (← getEnv) (← instantiateMVars (← inferType (mkFVar fvarId))) then
+    if let some e ← findSplit? (← instantiateMVars (← inferType (mkFVar fvarId))) then
       if e.isIte || e.isDIte then
         return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂]
       else

src/Lean/Meta/Tactic/SplitIf.lean

@@ -8,6 +8,124 @@ import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
+
+inductive SplitKind where
+  | ite | match | both
+
+def SplitKind.considerIte : SplitKind → Bool
+  | .ite | .both => true
+  | _ => false
+
+def SplitKind.considerMatch : SplitKind → Bool
+  | .match | .both => true
+  | _ => false
+
+namespace FindSplitImpl
+
+structure Context where
+  exceptionSet : ExprSet := {}
+  kind : SplitKind := .both
+
+unsafe abbrev FindM := ReaderT Context $ StateT (PtrSet Expr) MetaM
+
+/--
+Checks whether `e` is a candidate for `split`.
+Returns `some e'` if a prefix is a candidate.
+Example: suppose `e` is `(if b then f else g) x`, then
+the result is `some e'` where `e'` is the subterm `(if b then f else g)`
+-/
+private def isCandidate? (env : Environment) (ctx : Context) (e : Expr) : Option Expr := Id.run do
+  let ret (e : Expr) : Option Expr :=
+    if ctx.exceptionSet.contains e then none else some e
+  if ctx.kind.considerIte then
+    if e.isAppOf ``ite || e.isAppOf ``dite then
+      let numArgs := e.getAppNumArgs
+      if numArgs >= 5 && !(e.getArg! 1 5).hasLooseBVars then
+        return ret (e.getBoundedAppFn (numArgs - 5))
+  if ctx.kind.considerMatch then
+    if let some info := isMatcherAppCore? env e then
+      let args := e.getAppArgs
+      for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
+        if args[i]!.hasLooseBVars then
+          return none
+      return ret (e.getBoundedAppFn (args.size - info.arity))
+  return none
+
+@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+  if (← get).contains e then
+    failure
+  modify fun s => s.insert e
+
+unsafe def visit (e : Expr) : OptionT FindM Expr := do
+  checkVisited e
+  if let some e := isCandidate? (← getEnv) (← read) e then
+    return e
+  else
+    -- We do not look for split candidates in proofs.
+    unless e.hasLooseBVars do
+      if (← isProof e) then
+        failure
+    match e with
+    | .lam _ _ b _ | .proj _ _ b -- We do not look for split candidates in the binder of lambdas.
+    | .mdata _ b       => visit b
+    | .forallE _ d b _ => visit d <|> visit b -- We want to look for candidates at `A → B`
+    | .letE _ _ v b _  => visit v <|> visit b
+    | .app ..          => visitApp? e
+    | _                => failure
+where
+  visitApp? (e : Expr) : FindM (Option Expr) :=
+    e.withApp fun f args => do
+    -- See comment at `Canonicalizer.lean` regarding the case where
+    -- `f` has loose bound variables.
+    let info ← if f.hasLooseBVars then
+      pure {}
+    else
+      getFunInfo f
+    for u : i in [0:args.size] do
+      let arg := args[i]
+      if h : i < info.paramInfo.size then
+        let info := info.paramInfo[i]
+        unless info.isProp do
+          if info.isExplicit then
+            let some found ← visit arg | pure ()
+            return found
+      else
+        let some found ← visit arg | pure ()
+        return found
+    visit f
+
+end FindSplitImpl
+
+/-- Return an `if-then-else` or `match-expr` to split. -/
+partial def findSplit? (e : Expr) (kind : SplitKind := .both) (exceptionSet : ExprSet := {}) : MetaM (Option Expr) := do
+  go (← instantiateMVars e)
+where
+  go (e : Expr) : MetaM (Option Expr) := do
+    if let some target ← find? e then
+      if target.isIte || target.isDIte then
+        let cond := target.getArg! 1 5
+        -- Try to find a nested `if` in `cond`
+        return (← go cond).getD target
+      else
+        return some target
+    else
+      return none
+
+  find? (e : Expr) : MetaM (Option Expr) := do
+    let some candidate ← unsafe FindSplitImpl.visit e { kind, exceptionSet } |>.run' mkPtrSet
+      | return none
+    trace[split.debug] "candidate:{indentExpr candidate}"
+    return some candidate
+
+/-- Return the condition and decidable instance of an `if` expression to case split. -/
+private partial def findIfToSplit? (e : Expr) : MetaM (Option (Expr × Expr)) := do
+  if let some iteApp ← findSplit? e .ite then
+    let cond := iteApp.getArg! 1 5
+    let dec := iteApp.getArg! 2 5
+    return (cond, dec)
+  else
+    return none
+
 namespace SplitIf
 
 /--
@@ -62,19 +180,9 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge :=
 def mkDischarge? (useDecide := false) : MetaM Simp.Discharge :=
   return discharge? (← getLCtx).numIndices useDecide
 
-/-- Return the condition and decidable instance of an `if` expression to case split. -/
-private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) :=
-  if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then
-    let cond := iteApp.getArg! 1 5
-    let dec := iteApp.getArg! 2 5
-    -- Try to find a nested `if` in `cond`
-    findIfToSplit? cond |>.getD (cond, dec)
-  else
-    none
-
-def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do
+def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := mvarId.withContext do
   let e ← instantiateMVars e
-  if let some (cond, decInst) := findIfToSplit? e then
+  if let some (cond, decInst) ← findIfToSplit? e then
     let hName ← match hName? with
       | none       => mkFreshUserName `h
       | some hName => pure hName
@@ -106,6 +214,7 @@ def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Opt
     let mvarId₁ ← simpIfTarget s₁.mvarId
     let mvarId₂ ← simpIfTarget s₂.mvarId
     if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then
+      trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}"
       return none
     else
       return some ({ s₁ with mvarId := mvarId₁ }, { s₂ with mvarId := mvarId₂ })
@@ -118,6 +227,7 @@ def splitIfLocalDecl? (mvarId : MVarId) (fvarId : FVarId) (hName? : Option Name
       let mvarId₁ ← simpIfLocalDecl s₁.mvarId fvarId
       let mvarId₂ ← simpIfLocalDecl s₂.mvarId fvarId
       if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then
+        trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}"
         return none
       else
         return some (mvarId₁, mvarId₂)

src/Lean/Parser/Command.lean

@@ -134,10 +134,8 @@ def declValSimple    := leading_parser
   " :=" >> ppHardLineUnlessUngrouped >> declBody >> Termination.suffix >> optional Term.whereDecls
 def declValEqns      := leading_parser
   Term.matchAltsWhereDecls
-def whereStructField := leading_parser
-  Term.letDecl
 def whereStructInst  := leading_parser
-  ppIndent ppSpace >> "where" >> Term.structInstFields (sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true)) >>
+  ppIndent ppSpace >> "where" >> Term.structInstFields (sepByIndent Term.structInstField "; " (allowTrailingSep := true)) >>
   optional Term.whereDecls
 /-- `declVal` matches the right-hand side of a declaration, one of:
 * `:= expr` (a "simple declaration")

src/Lean/Parser/Term.lean

@@ -269,38 +269,6 @@ an optional `x :`, then a term `ty`, then `from val` or `by tac`. -/
 @[builtin_term_parser] def «suffices» := leading_parser:leadPrec
   withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
 @[builtin_term_parser] def «show»     := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs
-def structInstArrayRef := leading_parser
-  "[" >> withoutPosition termParser >> "]"
-def structInstLVal   := leading_parser
-  (ident <|> fieldIdx <|> structInstArrayRef) >>
-  many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
-def structInstField  := ppGroup $ leading_parser
-  structInstLVal >> " := " >> termParser
-def structInstFieldAbbrev := leading_parser
-  -- `x` is an abbreviation for `x := x`
-  atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation")
-def optEllipsis      := leading_parser
-  optional " .."
-/-
-Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
-This node is used to enable structure instance field completion in the whitespace
-of a structure instance notation.
--/
-def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p
-/--
-Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
-inherited. If `e` is itself a variable called `x`, it can be elided:
-`fun y => { x := 1, y }`.
-A *structure update* of an existing value can be given via `with`:
-`{ point with x := 1 }`.
-The structure type can be specified if not inferable:
-`{ x := 1, y := 2 : Point }`.
--/
-@[builtin_term_parser] def structInst := leading_parser
-  "{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with "))
-    >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true))
-    >> optEllipsis
-    >> optional (" : " >> termParser)) >> " }"
 def typeSpec := leading_parser " : " >> termParser
 def optType : Parser := optional typeSpec
 /--
@@ -488,6 +456,56 @@ e.g. because it has no constructors.
 
 @[builtin_term_parser] def «nofun» := leading_parser "nofun"
 
+/-
+Syntax category for structure instance notation fields.
+Does not initialize `registerBuiltinDynamicParserAttribute` since this category is not meant to be user-extensible.
+-/
+builtin_initialize
+  registerBuiltinParserAttribute `builtin_structInstFieldDecl_parser ``Category.structInstFieldDecl
+@[inline] def structInstFieldDeclParser (rbp : Nat := 0) : Parser :=
+  categoryParser `structInstFieldDecl rbp
+def optEllipsis := leading_parser
+  optional " .."
+def structInstArrayRef := leading_parser
+  "[" >> withoutPosition termParser >> "]"
+def structInstLVal := leading_parser
+  (ident <|> fieldIdx <|> structInstArrayRef) >>
+  many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
+def structInstFieldBinder :=
+  withAntiquot (mkAntiquot "structInstFieldBinder" decl_name% (isPseudoKind := true)) <|
+    binderIdent <|> bracketedBinder
+def optTypeForStructInst : Parser := optional (atomic (typeSpec >> notFollowedBy "}" "}"))
+/- `x` is an abbreviation for `x := x` -/
+def structInstField := ppGroup <| leading_parser
+  structInstLVal >> optional (many (checkColGt >> structInstFieldBinder) >> optTypeForStructInst >> ppDedent structInstFieldDeclParser)
+/-
+Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
+This node is used to enable structure instance field completion in the whitespace
+of a structure instance notation.
+-/
+def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p
+/--
+Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
+inherited. If `e` is itself a variable called `x`, it can be elided:
+`fun y => { x := 1, y }`.
+A *structure update* of an existing value can be given via `with`:
+`{ point with x := 1 }`.
+The structure type can be specified if not inferable:
+`{ x := 1, y := 2 : Point }`.
+-/
+@[builtin_term_parser] def structInst := leading_parser
+  "{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with "))
+    >> structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
+    >> optEllipsis
+    >> optional (" : " >> termParser)) >> " }"
+
+@[builtin_structInstFieldDecl_parser]
+def structInstFieldDef := leading_parser
+  " := " >> termParser
+@[builtin_structInstFieldDecl_parser]
+def structInstFieldEqns := leading_parser
+  matchAlts
+
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
 def funStrictImplicitBinder :=

src/Lean/Server/Watchdog.lean

@@ -811,33 +811,35 @@ section NotificationHandling
     terminateFileWorker p.textDocument.uri
 
   def handleDidChangeWatchedFiles (p : DidChangeWatchedFilesParams) : ServerM Unit := do
-    let importData ← (← read).importData.get
-    let references := (← read).references
-    let oleanSearchPath ← Lean.searchPathRef.get
-    let ileans ← oleanSearchPath.findAllWithExt "ilean"
-    for change in p.changes do
-      let some path := fileUriToPath? change.uri
-        | continue
-      match path.extension with
-      | "lean" =>
-        let dependents := importData.importedBy.findD change.uri ∅
+    let changes := p.changes.filterMap fun c => do return (c, ← fileUriToPath? c.uri)
+    let leanChanges := changes.filter fun (_, path) => path.extension == "lean"
+    let ileanChanges := changes.filter fun (_, path) => path.extension == "ilean"
+    if ! leanChanges.isEmpty then
+      let importData ← (← read).importData.get
+      for (c, _) in leanChanges do
+        let dependents := importData.importedBy.findD c.uri ∅
         for dependent in dependents do
-          notifyAboutStaleDependency dependent change.uri
-      | "ilean" =>
-        if let FileChangeType.Deleted := change.type then
+          notifyAboutStaleDependency dependent c.uri
+    if ! ileanChanges.isEmpty then
+      let references := (← read).references
+      let oleanSearchPath ← Lean.searchPathRef.get
+      for (c, path) in ileanChanges do
+        if let FileChangeType.Deleted := c.type then
           references.modify (fun r => r.removeIlean path)
-        else if ileans.contains path then
-          try
-            let ilean ← Ilean.load path
-            if let FileChangeType.Changed := change.type then
-              references.modify (fun r => r.removeIlean path |>.addIlean path ilean)
-            else
-              references.modify (fun r => r.addIlean path ilean)
-          catch
-            -- ilean vanished, ignore error
-            | .noFileOrDirectory .. => references.modify (·.removeIlean path)
-            | e => throw e
-      | _ => continue
+          continue
+        let isIleanInSearchPath := (← searchModuleNameOfFileName path oleanSearchPath).isSome
+        if ! isIleanInSearchPath then
+          continue
+        try
+          let ilean ← Ilean.load path
+          if let FileChangeType.Changed := c.type then
+            references.modify (fun r => r.removeIlean path |>.addIlean path ilean)
+          else
+            references.modify (fun r => r.addIlean path ilean)
+        catch
+          -- ilean vanished, ignore error
+          | .noFileOrDirectory .. => references.modify (·.removeIlean path)
+          | e => throw e
 
   def handleCancelRequest (p : CancelParams) : ServerM Unit := do
     let fileWorkers ← (←read).fileWorkersRef.get

src/Lean/Util/Trace.lean

@@ -260,7 +260,7 @@ def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls :
   let ref ← getRef
   let mut m ← try msg res catch _ => pure m!"<exception thrown while producing trace node message>"
   let mut data := { cls, collapsed, tag }
-  if profiler.get opts || aboveThresh then
+  if trace.profiler.get opts then
     data := { data with startTime := start, stopTime := stop }
   addTraceNode oldTraces data ref m
   MonadExcept.ofExcept res
@@ -356,7 +356,7 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
     return (← MonadExcept.ofExcept res)
   let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
   let mut data := { cls, collapsed, tag }
-  if profiler.get opts || aboveThresh then
+  if trace.profiler.get opts then
     data := { data with startTime := start, stopTime := stop }
   addTraceNode oldTraces data ref msg
   MonadExcept.ofExcept res

src/Std/Time/DateTime/PlainDateTime.lean

@@ -106,7 +106,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do
       break
     remDays := remDays - monLen
 
-  let mday : Fin 31 := Fin.ofNat (Int.toNat remDays)
+  let mday : Fin 31 := Fin.ofNat' _ (Int.toNat remDays)
 
   let hmon ←
     if h₁ : mon.val > 10

src/Std/Time/Time/Unit/Nanosecond.lean

@@ -22,7 +22,7 @@ def Ordinal := Bounded.LE 0 999999999
   deriving Repr, BEq, LE, LT
 
 instance : OfNat Ordinal n where
-  ofNat := Bounded.LE.ofFin (Fin.ofNat n)
+  ofNat := Bounded.LE.ofFin (Fin.ofNat' _ n)
 
 instance : Inhabited Ordinal where
   default := 0

src/include/lean/lean.h

@@ -1692,6 +1692,7 @@ static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a
 static inline uint16_t lean_uint8_to_uint16(uint8_t a) { return ((uint16_t)a); }
 static inline uint32_t lean_uint8_to_uint32(uint8_t a) { return ((uint32_t)a); }
 static inline uint64_t lean_uint8_to_uint64(uint8_t a) { return ((uint64_t)a); }
+static inline size_t lean_uint8_to_usize(uint8_t a) { return ((size_t)a); }
 
 /* UInt16 */
 
@@ -1727,6 +1728,7 @@ static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <
 static inline uint8_t lean_uint16_to_uint8(uint16_t a) { return ((uint8_t)a); }
 static inline uint32_t lean_uint16_to_uint32(uint16_t a) { return ((uint32_t)a); }
 static inline uint64_t lean_uint16_to_uint64(uint16_t a) { return ((uint64_t)a); }
+static inline size_t lean_uint16_to_usize(uint16_t a) { return ((size_t)a); }
 
 /* UInt32 */
 
@@ -1762,7 +1764,7 @@ static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <
 static inline uint8_t lean_uint32_to_uint8(uint32_t a) { return ((uint8_t)a); }
 static inline uint16_t lean_uint32_to_uint16(uint32_t a) { return ((uint16_t)a); }
 static inline uint64_t lean_uint32_to_uint64(uint32_t a) { return ((uint64_t)a); }
-static inline size_t lean_uint32_to_usize(uint32_t a) { return a; }
+static inline size_t lean_uint32_to_usize(uint32_t a) { return ((size_t)a); }
 
 
 /* UInt64 */
@@ -1834,6 +1836,8 @@ static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2;
 
 
 /* usize -> other */
+static inline uint8_t lean_usize_to_uint8(size_t a) { return ((uint8_t)a); }
+static inline uint16_t lean_usize_to_uint16(size_t a) { return ((uint16_t)a); }
 static inline uint32_t lean_usize_to_uint32(size_t a) { return ((uint32_t)a); }
 static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
 
@@ -2801,16 +2805,6 @@ static inline lean_obj_res lean_nat_pred(b_lean_obj_arg n) {
     return lean_nat_sub(n, lean_box(1));
 }
 
-static inline lean_obj_res lean_runtime_mark_multi_threaded(lean_obj_arg a) {
-    lean_mark_mt(a);
-    return a;
-}
-
-static inline lean_obj_res lean_runtime_mark_persistent(lean_obj_arg a) {
-    lean_mark_persistent(a);
-    return a;
-}
-
 #ifdef __cplusplus
 }
 #endif

src/lake/Lake/Load/Materialize.lean

@@ -148,7 +148,7 @@ def Dependency.materialize
       if ver.startsWith "git#" then
         return ver.drop 4
       else
-        error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#>rev>\")"
+        error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#<rev>\")"
     let depName := dep.name.toString (escape := false)
     let pkg ←
       match (← Reservoir.fetchPkg? lakeEnv dep.scope depName |>.toLogT) with

src/runtime/io.cpp

@@ -692,7 +692,7 @@ extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezo
 
         tm = (int64_t)(nextTransition / 1000.0);
     }
-    
+
     int32_t dst_offset = ucal_get(cal, UCAL_DST_OFFSET, &status);
 
     if (U_FAILURE(status)) {
@@ -1450,6 +1450,16 @@ extern "C" LEAN_EXPORT obj_res lean_io_exit(uint8_t code, obj_arg /* w */) {
     exit(code);
 }
 
+extern "C" LEAN_EXPORT obj_res lean_runtime_mark_multi_threaded(obj_arg a, obj_arg /* w */) {
+    lean_mark_mt(a);
+    return io_result_mk_ok(a);
+}
+
+extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a, obj_arg /* w */) {
+    lean_mark_persistent(a);
+    return io_result_mk_ok(a);
+}
+
 void initialize_io() {
     g_io_error_nullptr_read = lean_mk_io_user_error(mk_ascii_string_unchecked("null reference read"));
     mark_persistent(g_io_error_nullptr_read);