benchmark

src/Init/Data/Array.lean

@@ -20,4 +20,3 @@ 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/InsertionSort.lean

@@ -5,24 +5,91 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
+import Init.Data.Nat.Fold
+import Init.Data.Vector.Lemmas
 
-@[inline] def Array.insertionSort (a : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α :=
-  traverse a 0 a.size
-where
-  @[specialize] traverse (a : Array α) (i : Nat) (fuel : Nat) : Array α :=
-    match fuel with
-    | 0      => a
-    | fuel+1 =>
-      if h : i < a.size then
-        traverse (swapLoop a i h) (i+1) fuel
-      else
-        a
-  @[specialize] swapLoop (a : Array α) (j : Nat) (h : j < a.size) : Array α :=
-    match (generalizing := false) he:j with -- using `generalizing` because we don't want to refine the type of `h`
-    | 0    => a
-    | j'+1 =>
-      have h' : j' < a.size := by subst j; exact Nat.lt_trans (Nat.lt_succ_self _) h
-      if lt a[j] a[j'] then
-        swapLoop (a.swap j j') j' (by rw [size_swap]; assumption; done)
-      else
-        a
+namespace Vector
+
+/-- Swap the `i`-th element repeatedly to the left, while the element to its left is not `lt` it. -/
+@[specialize, inline] def swapLeftWhileLT {n} (a : Vector α n) (i : Nat) (h : i < n)
+    (lt : α → α → Bool := by exact (· < ·)) : Vector α n :=
+  match h' : i with
+  | 0 => a
+  | i'+1 =>
+    if lt a[i] a[i'] then
+      swapLeftWhileLT (a.swap i' i) i' (by omega) lt
+    else
+      a
+
+end Vector
+
+open Vector
+namespace Array
+
+/-- Sort an array in place using insertion sort. -/
+@[inline] def insertionSort (a : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α :=
+  a.size.fold (init := ⟨a, rfl⟩) (fun i h acc => swapLeftWhileLT acc i h lt) |>.toArray
+
+/-- Insert an element into an array, after the last element which is not `lt` the inserted element. -/
+def orderedInsert (a : Array α) (x : α) (lt : α → α → Bool := by exact (· < ·)) : Array α :=
+ swapLeftWhileLT ⟨a.push x, rfl⟩ a.size (by simp) lt |>.toArray
+
+end Array
+
+/-! ### Verification -/
+
+namespace Vector
+
+theorem swapLeftWhileLT_push {n} (a : Vector α n) (x : α) (j : Nat) (h : j < n) :
+    swapLeftWhileLT (a.push x) j (by omega) lt = (swapLeftWhileLT a j h lt).push x := by
+  induction j generalizing a with
+  | zero => simp [swapLeftWhileLT]
+  | succ j ih =>
+    simp [swapLeftWhileLT]
+    split <;> rename_i h
+    · rw [Vector.getElem_push_lt (by omega), Vector.getElem_push_lt (by omega)] at h
+      rw [← Vector.push_swap, ih, if_pos h]
+    · rw [Vector.getElem_push_lt (by omega), Vector.getElem_push_lt (by omega)] at h
+      rw [if_neg h]
+
+theorem swapLeftWhileLT_cast {n m} (a : Vector α n) (j : Nat) (h : j < n) (h' : n = m) :
+    swapLeftWhileLT (a.cast h') j (by omega) lt = (swapLeftWhileLT a j h lt).cast h' := by
+  subst h'
+  simp
+
+end Vector
+
+namespace Array
+
+@[simp] theorem size_insertionSort (a : Array α) : (a.insertionSort lt).size = a.size := by
+  simp [insertionSort]
+
+private theorem insertionSort_push' (a : Array α) (x : α) :
+    (a.push x).insertionSort lt =
+      (swapLeftWhileLT ⟨(a.insertionSort lt).push x, rfl⟩ a.size (by simp) lt).toArray := by
+  rw [insertionSort, Nat.fold_congr (size_push a x), Nat.fold]
+  have : (a.size.fold (fun i h acc => swapLeftWhileLT acc i (by simp; omega) lt) ⟨a.push x, rfl⟩) =
+      ((a.size.fold (fun i h acc => swapLeftWhileLT acc i h lt) ⟨a, rfl⟩).push x).cast (by simp) := by
+    rw [Vector.eq_cast_iff]
+    simp only [Nat.fold_eq_finRange_foldl]
+    rw [← List.foldl_hom (fun a => (Vector.push x a)) _ (fun v ⟨i, h⟩ => swapLeftWhileLT v i (by omega) lt)]
+    rw [Vector.push_mk]
+    rw [← List.foldl_hom (Vector.cast _) _ (fun v ⟨i, h⟩ => swapLeftWhileLT v i (by omega) lt)]
+    · simp
+    · intro v i
+      simp only
+      rw [swapLeftWhileLT_cast]
+    · simp [swapLeftWhileLT_push]
+  rw [this]
+  simp only [Nat.lt_add_one, swapLeftWhileLT_cast, Vector.toArray_cast]
+  unfold insertionSort
+  simp only [Vector.push]
+  congr
+  all_goals simp
+
+theorem insertionSort_push (a : Array α) (x : α) :
+    (a.push x).insertionSort lt = (a.insertionSort lt).orderedInsert x lt := by
+  rw [insertionSort_push', orderedInsert]
+  simp
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -21,14 +21,15 @@ 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 ..
 
@@ -38,26 +39,96 @@ theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? =
   · rw [getElem?_neg a i h]
     simp_all
 
-@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[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]
 
 @[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)]
 
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [mem_def]
+theorem singleton_inj : #[a] = #[b] ↔ a = b := by
+  simp
+
+theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
 
 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
@@ -348,243 +419,10 @@ 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`.
@@ -702,6 +540,8 @@ 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
 
@@ -755,6 +595,20 @@ theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat
     (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
+theorem push_set (a : Array α) (x y : α) {i : Nat} {hi} :
+    (a.set i x).push y = (a.push y).set i x (by simp; omega):= by
+  ext j h₁ h₂
+  · simp
+  · if h' : j = a.size then
+      rw [getElem_push, getElem_set_ne, dif_neg]
+      all_goals simp_all <;> omega
+    else
+      rw [getElem_push_lt, getElem_set, getElem_set]
+      split
+      · rfl
+      · rw [getElem_push_lt]
+      simp_all; omega
+
 /-! # setIfInBounds -/
 
 @[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
@@ -1020,6 +874,11 @@ 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
@@ -1536,18 +1395,6 @@ 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 α)} :
@@ -1885,6 +1732,11 @@ theorem swap_comm (a : Array α) {i j : Nat} {hi hj} : a.swap i j hi hj = a.swap
     · split <;> simp_all
     · split <;> simp_all
 
+theorem push_swap (a : Array α) (x : α) {i j : Nat} {hi hj} :
+    (a.swap i j hi hj).push x = (a.push x).swap i j (by simp; omega) (by simp; omega) := by
+  rw [swap_def, swap_def]
+  simp [push_set, getElem_push_lt, hi, hj]
+
 /-! ### eraseIdx -/
 
 theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) :
@@ -1984,6 +1836,11 @@ 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'
@@ -2047,6 +1904,10 @@ 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
@@ -2092,6 +1953,38 @@ 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

@@ -1,65 +0,0 @@
-/-
-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.Vector.Basic
+import Init.Data.Array.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
 
-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 :=
+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
   let mid := (lo + hi) / 2
-  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) :=
+  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) :=
     if h : j < hi then
-      if lt as[j] pivot then
-        loop (as.swap i j) (i+1) (j+1)
+      if lt (as.get! j) pivot then
+        let as := as.swapIfInBounds i j
+        loop as (i+1) (j+1)
       else
         loop as i (j+1)
     else
-      (⟨i, ilo⟩, as.swap i hi)
+      let as := as.swapIfInBounds i hi
+      (i, as)
+    termination_by hi - j
+    decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
   loop as lo lo
 
-@[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
+@[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
       else
-        sort (sort as lo mid) (mid+1) hi
+        let as := sort as low mid
+        sort as (mid+1) high
     else as
-  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
+  sort as low high
 
 set_option linter.unusedVariables.funArgs false in
 /--

src/Init/Data/Fin/Basic.lean

@@ -36,6 +36,12 @@ 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`.
 
@@ -44,12 +50,9 @@ 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)⟩
 
-/--
-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 _)⟩
+-- 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
 
 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,12 +83,44 @@ 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 = [] :=
@@ -124,36 +156,6 @@ 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?`.
@@ -161,29 +163,57 @@ theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
 We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`.
 -/
 
-@[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
+theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl
 
-theorem get?_eq_none : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
+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
   | [], _, _ => rfl
-  | _ :: l, _+1, h => get?_eq_none (l := l) <| Nat.le_of_succ_le_succ h
+  | _ :: l, _+1, h => get?_len_le (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_iff : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
+theorem get?_eq_some : 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?_eq_none hn ▸ e
+    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e
     ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
   fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩
 
-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⟩
+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⟩
 
 @[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
-  simp only [getElem?_def]; split
+  simp only [getElem?, decidableGetElem?]; split
   · exact (get?_eq_get ‹_›)
-  · exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›)
+  · 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
 
 /-! ### getD
 
@@ -194,29 +224,42 @@ 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! -/
 
-We simplify `l[n]!` to `(l[n]?).getD default`.
--/
+@[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
-@[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
+@[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]
 
 /-! ### getElem? and getElem -/
 
@@ -224,19 +267,23 @@ We simplify `l[n]!` to `(l[n]?).getD default`.
   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_iff, get_eq_getElem]
+  simp only [← get?_eq_getElem?, get?_eq_some, 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_iff]
+  simp only [← get?_eq_getElem?, get?_eq_none]
 
 @[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]
@@ -253,6 +300,9 @@ 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
@@ -264,6 +314,11 @@ 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
@@ -277,10 +332,20 @@ 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
 
@@ -291,7 +356,11 @@ 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?_eq_none h₁, getElem?_eq_none]; rwa [← hl]
+      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)
 
 @[simp] theorem getElem_concat_length : ∀ (l : List α) (a : α) (i) (_ : i = l.length) (w), (l ++ [a])[i]'w = a
   | [], a, _, h, _ => by subst h; simp
@@ -300,11 +369,19 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
 theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a := by
   simp
 
-theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := 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 isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
-  simp
+@[simp] theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
+  by_cases h : n < l.length
+  · simp_all
+  · simp [h]
+    simp_all
+
+@[simp] theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
+  by_cases h : n < l.length
+  · simp_all
+  · simp [h]
 
 /-! ### mem -/
 
@@ -416,18 +493,42 @@ 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
@@ -478,6 +579,18 @@ 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 [*]
@@ -502,18 +615,6 @@ 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.
@@ -531,10 +632,19 @@ theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a)
   | _ :: _, 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 : α} :
@@ -556,6 +666,12 @@ 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
@@ -570,6 +686,11 @@ 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
@@ -589,14 +710,6 @@ 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
@@ -611,6 +724,8 @@ 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
@@ -3330,137 +3445,17 @@ 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
@@ -3474,9 +3469,16 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) :
 @[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
@@ -3511,18 +3513,4 @@ 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_iff] at m; exact m.1⟩ x := by
-  simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx]
+    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some] at m; exact m.1⟩ x := by
+  simp only [getElem?_eq, length_mapFinIdx, getElem_mapFinIdx]
   split <;> simp
 
 @[simp]
@@ -126,8 +126,7 @@ 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_iff] at m; exact m.1⟩ x := by
+      fun ⟨⟨i, x⟩, m⟩ => f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some] at m; exact m.1⟩ x := by
   apply ext_getElem <;> simp
 
 @[simp]
@@ -236,7 +235,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?_def, Array.length_toList,
+    simp only [mapIdx.go, Array.toListImpl_eq, getElem?_eq, 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,4 +15,3 @@ 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

@@ -1,54 +0,0 @@
-/-
-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,9 +39,6 @@ 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₂ :=
@@ -105,7 +102,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 α) :
-    (l₁ ++ (l₂ ++ l₃)) ~ (l₂ ++ (l₁ ++ l₃)) := by
+    Perm (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
@@ -136,7 +133,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 : α} : ¬((a::l) ~ []) :=
+theorem not_perm_cons_nil {l : List α} {a : α} : ¬(Perm (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
@@ -481,15 +478,6 @@ 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,24 +192,6 @@ 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,7 +36,3 @@ 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,16 +278,6 @@ 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, François G. Dorais, Mario Carneiro, Mac Malone
+Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.UInt.Basic
@@ -9,202 +9,129 @@ 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 bits:term:arg : command => do
-  let mut cmds ← Syntax.getArgs <$> `(
-  namespace $typeName
+macro "declare_uint_theorems" typeName:ident : command =>
+`(
+namespace $typeName
 
-  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
+instance : Inhabited $typeName where
+  default := 0
 
-  @[simp] theorem toNat_mk : (mk a).toNat = a.toNat := 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_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
+@[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
+  | ⟨_, _⟩ => rfl
 
-  @[simp] theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatCore n h).toNat = n := BitVec.toNat_ofNatLt ..
+theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
+  Nat.mod_eq_of_lt
 
-  @[simp] theorem val_val_eq_toNat (x : $typeName) : x.val.val = x.toNat := rfl
+theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
+  rw [toNat, toBitVec_eq_of_lt h]
 
-  theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
+theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
 
-  @[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
-    | ⟨_, _⟩ => rfl
+theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
 
-  theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
-    Nat.mod_eq_of_lt
+@[simp] protected theorem not_le {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 not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := by simp [le_def, lt_def]
 
-  theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
+@[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
 
-  theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
+@[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
 
-  theorem le_iff_toNat_le {a b : $typeName} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
+protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
 
-  theorem lt_iff_toNat_lt {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
 
-  @[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := by simp [le_def, lt_def]
+protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
 
-  @[simp] protected theorem not_lt {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 le_refl (a : $typeName) : a ≤ a := by simp [le_def]
+protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
 
-  @[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
+protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
+  cases a; cases b; simp_all
 
-  protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
+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 lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_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 le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
+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 lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
+@[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
 
-  protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
+@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
 
-  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_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv  ..
 
-  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
+@[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) 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 toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
 
-  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 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 (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
+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 (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 mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
+  simp only [lt_def, mod_def]
+  apply BitVec.umod_lt
 
-  @[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
+protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
-  @[simp] protected theorem toNat_add (a b : $typeName) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ $bits := BitVec.toNat_add ..
+@[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
 
-  protected theorem toNat_sub (a b : $typeName) : (a - b).toNat = (2 ^ $bits - b.toNat + a.toNat) % 2 ^ $bits := BitVec.toNat_sub  ..
+@[simp]
+theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.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 toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
 
-  @[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
+@[simp]
+theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
 
-  @[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv  ..
+end $typeName
+)
 
-  @[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
+declare_uint_theorems UInt8
+declare_uint_theorems UInt16
+declare_uint_theorems UInt32
+declare_uint_theorems UInt64
+declare_uint_theorems USize
 
 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,9 +21,6 @@ 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,6 +13,8 @@ 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
 
@@ -21,6 +23,9 @@ namespace Vector
   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]
@@ -59,6 +64,9 @@ protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i
 @[simp] theorem pop_mk {data : Array α} {size : data.size = n} :
     (Vector.mk data size).pop = Vector.mk data.pop (by simp [size]) := rfl
 
+@[simp] theorem swap_mk {data : Array α} {size : data.size = n} {i j : Nat} {hi hj} :
+    (Vector.mk data size).swap i j hi hj = Vector.mk (data.swap i j) (by simp_all) := rfl
+
 @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
   rcases v with ⟨data, rfl⟩
   simp
@@ -88,156 +96,40 @@ defeq issues in the implicit size argument.
     subst h
     simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero]
 
+theorem push_swap (a : Vector α n) (x : α) {i j : Nat} {hi hj} :
+    (a.swap i j hi hj).push x = (a.push x).swap i j := by
+  cases a
+  simp [Array.push_swap]
 
-/-! ### mk lemmas -/
+/-! ### cast -/
 
-theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
+@[simp] theorem cast_mk {n m} (a : Array α) (w : a.size = n) (h : n = m) :
+    (Vector.mk a w).cast h = ⟨a, h ▸ w⟩ := by
+  simp [Vector.cast]
 
-@[simp] theorem allDiff_mk [BEq α] (a : Array α) (h : a.size = n) :
-    (Vector.mk a h).allDiff = a.allDiff := rfl
+@[simp] theorem cast_refl {n} (a : Vector α n) : a.cast rfl = a := by
+  cases a
+  simp
 
-@[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 toArray_cast {n m} (a : Vector α n) (h : n = m) :
+    (a.cast h).toArray = a.toArray := by
+  subst h
+  simp
 
-@[simp] theorem back!_mk [Inhabited α] (a : Array α) (h : a.size = n) :
-    (Vector.mk a h).back! = a.back! := rfl
+theorem cast_inj {n m} (a : Vector α n) (b : Vector α n) (h : n = m) :
+    a.cast h = b.cast h ↔ a = b := by
+  cases h
+  simp
 
-@[simp] theorem back?_mk (a : Array α) (h : a.size = n) :
-    (Vector.mk a h).back? = a.back? := rfl
+theorem cast_eq_iff {n m} (a : Vector α n) (b : Vector α m) (h : n = m) :
+    a.cast h = b ↔ a = b.cast h.symm := by
+  cases h
+  simp
 
-@[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
+theorem eq_cast_iff {n m} (a : Vector α n) (b : Vector α m) (h : m = n) :
+    a = b.cast h ↔ a.cast h.symm = b := by
+  cases h
+  simp
 
 /-! ### Decidable quantifiers. -/
 

src/Init/GetElem.lean

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

src/Init/Notation.lean

@@ -48,10 +48,6 @@ 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,9 +32,13 @@ 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_iff.mpr h]
+  rw [get, List.get?_eq_none.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,25 +959,3 @@ 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,14 +23,5 @@ 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,3 +79,25 @@ 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,36 +282,52 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
       k fvars
   loop 0 #[]
 
-private def expandWhereStructInst : Macro := fun whereStx => do
-  let `(Parser.Command.whereStructInst| where%$whereTk $[$structInstFields];* $[$whereDecls?:whereDecls]?) := whereStx
-    | Macro.throwUnsupported
+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
 
-  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
+    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
 
 /-
 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  -- `structInstField` should be expanded at this point
+      | _ => throwInvalidPattern  -- `structInstFieldAbbrev` should be expanded at this point
     `({ $[$srcs?,* with]? $fields,* $[..%$ell?]? $[: $ty?]? })
   | _ => throwInvalidPattern
 

src/Lean/Elab/StructInst.lean

@@ -31,32 +31,13 @@ open Meta
 open TSyntax.Compat
 
 /-!
-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))
+Recall that structure instances are of the form:
+```
+"{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
+    >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
     >> optEllipsis
-    >> 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
+    >> optional (" : " >> termParser)
+    >> " }"
 ```
 -/
 
@@ -73,57 +54,22 @@ 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)
-
 /--
-Takes an arbitrary `structInstField` and expands it to be a `structInstFieldDef` without any binders or type ascription.
+Expands field abbreviation notation.
+Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }`.
 -/
-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"
+@[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
   | _ => 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 ... }`.
@@ -241,13 +187,12 @@ 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 `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
+    /- arg is of the form `structInstFieldAbbrev <|> structInstField` -/
+    if arg.getKind == ``Lean.Parser.Term.structInstField then
+      /- Remark: the syntax for `structInstField` is
          ```
          def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
-         def structInstFieldDef := leading_parser
-           structInstLVal >> group (null >> null >> group (" := " >> termParser))
+         def structInstField  := leading_parser structInstLVal >> " := " >> termParser
          ```
       -/
       let lval := arg[0]
@@ -290,7 +235,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[1][2][1]
+    cont modifyOp[2]
   else
     let s ← `(s)
     let valFirst  := rest[0]
@@ -443,7 +388,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 >> group (null >> null >> group (" := " >> termParser))
+def structInstField  := leading_parser structInstLVal >> " := " >> termParser
 def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
 def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 ```
@@ -467,9 +412,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 1 <| stx[1].setArg 2 <| stx[1][2].setArg 1 field.val.toSyntax
+    let stx := stx.setArg 2 field.val.toSyntax
     match field.lhs with
-    | first::rest => stx.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
+    | first::rest => stx.setArg 0 <| mkNullNode #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
     | _ => unreachable!
 
 /-- Creates a view of a field left-hand side. -/
@@ -483,7 +428,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.throwErrorAt stx "unexpected structure syntax"
+      | none     => Macro.throwError "unexpected structure syntax"
 
 /--
 Creates a structure instance view from structure instance notation
@@ -491,21 +436,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 structInstField ...)
-              >> optional ".."
-              >> optional (" : " >> termParser)
-              >> " }"
-  ```
-  This method assumes that `structInstField` had already been expanded by the macro `expandStructInstFields`.
+  /- 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.
   -/
   let fields ← stx[2][0].getSepArgs.toList.mapM fun fieldStx => do
-    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
+    let val      := fieldStx[2]
+    let first    ← toFieldLHS fieldStx[0][0]
+    let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
     return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field }
   return { ref := stx, structName, params := #[], fields, sources }
 
@@ -651,7 +596,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 (mkNode ``Parser.Term.optEllipsis #[mkNullNode])
+              let implicitSourceStx := s.sources.implicit.getD mkNullNode
               return (structStx.setArg 1 explicitSourceStx).setArg 3 implicitSourceStx
             let valStx := s.ref -- construct substructure syntax using s.ref as template
             let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type

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,11 +1366,7 @@ 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,
-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`. -/
+/-- Replace free (or meta) variables `xs` with loose bound variables. -/
 @[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    := "reduce information stored in snapshots to the minimum necessary \
+  descr    := "mark persistent and reduce information stored in snapshots to the minimum necessary \
     for the cmdline driver: diagnostics per command and final full snapshot"
 }
 
@@ -639,21 +639,30 @@ where
         pos      := ctx.fileMap.toPosition beginPos
         data     := output
       }
-    let cmdState : Command.State := { cmdState with messages }
-    let mut reportedCmdState := cmdState
+    let cmdState := { cmdState with messages }
     -- definitely resolve eventually
     snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
 
-    let infoTree : InfoTree := cmdState.infoState.trees[0]!
+    let mut infoTree : InfoTree := cmdState.infoState.trees[0]!
     let cmdline := internal.cmdlineSnapshots.get scope.opts && !Parser.isTerminalCommand stx
-    if cmdline then
-      -- discard all metadata apart from the environment; see `internal.cmdlineSnapshots`
-      reportedCmdState := { env := reportedCmdState.env, maxRecDepth := 0 }
+    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
     finishedPromise.resolve {
       diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
       infoTree? := infoTree
       traces := cmdState.traceState
-      cmdState := reportedCmdState
+      cmdState := if cmdline then {
+        /- Safety: as above -/
+        env := unsafe Runtime.markPersistent cmdState.env
+        maxRecDepth := 0
+      } else cmdState
     }
     -- 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.Term.structInstField))
+  (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Command.whereStructField))
 
 /--
 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 type is always a proposition. -/
+  /-- `isProp` is true if the parameter 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,22 +84,8 @@ declare_uint_simprocs UInt8
 declare_uint_simprocs UInt16
 declare_uint_simprocs UInt32
 declare_uint_simprocs UInt64
-
 /-
-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`.
+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.
 -/
-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 }
+-- declare_uint_simprocs USize

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

@@ -108,19 +108,13 @@ 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 (← useImplicitDefEqProof thm) then
+      let proof? ← if thm.rfl 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) := mvarId.withContext do
+def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := 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,14 +278,43 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.with
     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 mvarId.withContext do
+partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do
   let target ← instantiateMVars (← mvarId.getType)
   let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
-    if let some e ← findSplit? target (if splitIte then .both else .match) badCases then
+    if let some e := findSplit? (← getEnv) target splitIte badCases then
       if e.isIte || e.isDIte then
         return (← splitIfTarget? mvarId).map fun (s₁, s₂) => [s₁.mvarId, s₂.mvarId]
       else
@@ -304,7 +333,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? (← instantiateMVars (← inferType (mkFVar fvarId))) then
+    if let some e := findSplit? (← getEnv) (← 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,124 +8,6 @@ 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
 
 /--
@@ -180,9 +62,19 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge :=
 def mkDischarge? (useDecide := false) : MetaM Simp.Discharge :=
   return discharge? (← getLCtx).numIndices useDecide
 
-def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := mvarId.withContext do
+/-- 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
   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
@@ -214,7 +106,6 @@ 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₂ })
@@ -227,7 +118,6 @@ 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,8 +134,10 @@ 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 Term.structInstField "; " (allowTrailingSep := true)) >>
+  ppIndent ppSpace >> "where" >> Term.structInstFields (sepByIndent (ppGroup whereStructField) "; " (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,6 +269,38 @@ 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
 /--
@@ -456,56 +488,6 @@ 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,35 +811,33 @@ section NotificationHandling
     terminateFileWorker p.textDocument.uri
 
   def handleDidChangeWatchedFiles (p : DidChangeWatchedFilesParams) : ServerM Unit := do
-    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 ∅
+    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 ∅
         for dependent in dependents do
-          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
+          notifyAboutStaleDependency dependent change.uri
+      | "ilean" =>
+        if let FileChangeType.Deleted := change.type then
           references.modify (fun r => r.removeIlean path)
-          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
+        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
 
   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 trace.profiler.get opts then
+  if profiler.get opts || aboveThresh 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 trace.profiler.get opts then
+  if profiler.get opts || aboveThresh 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,7 +1692,6 @@ 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 */
 
@@ -1728,7 +1727,6 @@ 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 */
 
@@ -1764,7 +1762,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 ((size_t)a); }
+static inline size_t lean_uint32_to_usize(uint32_t a) { return a; }
 
 
 /* UInt64 */
@@ -1836,8 +1834,6 @@ 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); }
 
@@ -2805,6 +2801,16 @@ 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,16 +1450,6 @@ 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);