chore: upstream Subarray.empty

2026-03-20 20:04:23 +00:00 · 2024-09-29 15:33:54 +10:00
36 changed files with 245 additions and 815 deletions
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -810,27 +810,11 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
  as.foldl (init := (#[], #[])) fun (as, bs) a =>
    if p a then (as.push a, bs) else (as, bs.push a)

-/-! ## Auxiliary functions used in metaprogramming.
+/-! ### Auxiliary functions used in metaprogramming.

 We do not intend to provide verification theorems for these functions.
 -/

-/-! ### eraseReps -/
-
-/--
-`O(|l|)`. Erase repeated adjacent elements. Keeps the first occurrence of each run.
-* `eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5]`
-/
-def eraseReps {α} [BEq α] (as : Array α) : Array α :=
-  if h : 0 < as.size then
-    let ⟨last, r⟩ := as.foldl (init := (as[0], #[])) fun ⟨last, r⟩ a =>
-      if a == last then ⟨last, r⟩ else ⟨a, r.push last⟩
-    r.push last
-  else
-    #[]
-
-/-! ### allDiff -/
-
 private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
  | 0,   _ => true
  | i+1, h =>
@@ -848,8 +832,6 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def allDiff [BEq α] (as : Array α) : Bool :=
  allDiffAux as 0

-/-! ### getEvenElems -/
-
@[inline] def getEvenElems (as : Array α) : Array α :=
  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
    if even then
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -73,7 +73,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α

@[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl

-@[simp] theorem toList_append (arr arr' : Array α) :
+@[simp] theorem append_toList (arr arr' : Array α) :
    (arr ++ arr').toList = arr.toList ++ arr'.toList := by
  rw [← append_eq_append]; unfold Array.append
  rw [foldl_eq_foldl_toList]
@@ -111,8 +111,8 @@ abbrev toList_eq := @toListImpl_eq
@[deprecated pop_toList (since := "2024-09-09")]
 abbrev pop_data := @pop_toList

-@[deprecated toList_append (since := "2024-09-09")]
-abbrev append_data := @toList_append
+@[deprecated append_toList (since := "2024-09-09")]
+abbrev append_data := @append_toList

@[deprecated appendList_toList (since := "2024-09-09")]
 abbrev appendList_data := @appendList_toList
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -91,8 +91,6 @@ abbrev toArray_data := @toArray_toList
@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
    a.toArray[i] = a[i]'(by simpa using h) := rfl

-@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
-
@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
 theorem toArray_concat {as : List α} {x : α} :
    (as ++ [x]).toArray = as.toArray.push x := by
@@ -100,7 +98,7 @@ theorem toArray_concat {as : List α} {x : α} :
  simp

@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
-  apply ext'
+  apply Array.ext'
  simp

 /-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
@@ -125,11 +123,6 @@ theorem toArray_concat {as : List α} {x : α} :
    l.toArray.foldl f init = l.foldl f init := by
  rw [foldl_eq_foldl_toList]

-@[simp] theorem append_toArray (l₁ l₂ : List α) :
-    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
-  apply ext'
-  simp
-
 end List

 namespace Array
@@ -143,10 +136,10 @@ attribute [simp] uset
@[deprecated toArray_toList (since := "2024-09-09")]
 abbrev toArray_data := @toArray_toList

-@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
+@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl

-@[deprecated length_toList (since := "2024-09-09")]
-abbrev data_length := @length_toList
+@[deprecated toList_length (since := "2024-09-09")]
+abbrev data_length := @toList_length

@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl

@@ -182,25 +175,25 @@ where
      mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
    unfold mapM.map; split
    · rw [← List.get_drop_eq_drop _ i ‹_›]
-      simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
+      simp only [aux (i + 1), map_eq_pure_bind, toList_length, List.foldlM_cons, bind_assoc,
        pure_bind]
      rfl
    · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
  termination_by arr.size - i
  decreasing_by decreasing_trivial_pre_omega

-@[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
+@[simp] theorem map_toList (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
  rw [map, mapM_eq_foldlM]
  apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
  have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
    induction l generalizing arr <;> simp [*]
  simp [H]

-@[deprecated toList_map (since := "2024-09-09")]
-abbrev map_data := @toList_map
+@[deprecated map_toList (since := "2024-09-09")]
+abbrev map_data := @map_toList

@[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
-  simp only [← length_toList]
+  simp only [← toList_length]
  simp

@[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@@ -208,11 +201,6 @@ abbrev map_data := @toList_map
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
    arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)

-@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
-    (arr ++ l).toList = arr.toList ++ l := by
-  cases arr
-  simp
-
 theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
    (F : Array β → α → Array β) (G : α → List β)
    (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
@@ -304,14 +292,14 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
@[simp] theorem set!_is_setD : @set! = @setD := rfl

@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
-    (Array.setD a index val).size = a.size := by
+  (Array.setD a index val).size = a.size := by
  if h : index < a.size  then
    simp [setD, h]
  else
    simp [setD, h]

@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-    (setD a i v)[i]'h = v := by
+  (setD a i v)[i]'h = v := by
  simp at h
  simp only [setD, h, dite_true, getElem_set, ite_true]

@@ -321,7 +309,7 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a

 /-- Simplifies a normal form from `get!` -/
@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
-    Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
+  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
  by_cases h : i < a.size <;>
    simp [setD, Nat.not_lt_of_le, h,  getD_get?]

@@ -436,18 +424,12 @@ theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList :
@[deprecated getElem_mem_toList (since := "2024-09-09")]
 abbrev getElem_mem_data := @getElem_mem_toList

-theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
-
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
 theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]

-set_option linter.deprecated false in
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
+@[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?

-set_option linter.deprecated false in
 theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
  getElem?_eq_toList_get? ..

@@ -457,15 +439,11 @@ abbrev get?_eq_data_get? := @get?_eq_toList_get?
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
  simp [get!_eq_getD]

-theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
-  cases as
-  simp [List.getElem?_eq_some_iff]
-
@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
  simp [back, back?]

@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_getElem?]
+  simp [back?, getElem?_eq_toList_get?]

 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp

@@ -523,7 +501,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
  simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]

 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
-    (setD a i v)[i] = v := by
+  (setD a i v)[i] = v := by
  simp at h
  simp only [setD, h, dite_true, get_set, ite_true]

@@ -625,11 +603,11 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
  simp [getElem_eq_getElem_toList]

 set_option linter.deprecated false in
-@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
+@[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
  let rec go (as : Array α) (i j hj)
      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
-      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
+      (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
+      (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
    rw [reverse.loop]; dsimp; split <;> rename_i h₁
    · match j with | j+1 => ?_
      simp only [Nat.add_sub_cancel]
@@ -637,37 +615,34 @@ set_option linter.deprecated false in
      · rwa [Nat.add_right_comm i]
      · simp [size_swap, h₂]
      · intro k
-        rw [← getElem?_eq_toList_getElem?, get?_swap]
-        simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          getElem?_eq_toList_getElem?]
+        rw [← getElem?_eq_toList_get?, get?_swap]
+        simp only [H, getElem_eq_toList_get, ← List.get?_eq_get, Nat.le_of_lt h₁,
+          getElem?_eq_toList_get?]
        split <;> rename_i h₂
        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+          exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
        split <;> rename_i h₃
        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+          exact (List.get?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
    · rw [H]; split <;> rename_i h₂
      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
        cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.getElem?_reverse' _ _ h).symm
+        exact (List.get?_reverse' _ _ h).symm
      · rfl
    termination_by j - i
  simp only [reverse]
  split
  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    refine List.ext_get? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
    split
    · rfl
    · rename_i h
      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
        true_and, Nat.not_lt] at h
-      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
-
-@[deprecated toList_reverse (since := "2024-09-30")]
-abbrev reverse_toList := @toList_reverse
+      rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.toList.length_reverse ▸ ‹_›)]

 /-! ### foldl / foldr -/

@@ -733,20 +708,16 @@ theorem foldr_induction
 /-! ### map -/

@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
-  simp only [mem_def, toList_map, List.mem_map]
+  simp only [mem_def, map_toList, List.mem_map]

 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
+    arr.mapM f = return mk (← arr.toList.mapM f) := by
  rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
  conv => rhs; rw [← List.reverse_reverse arr.toList]
  induction arr.toList.reverse with
  | nil => simp
  | cons a l ih => simp [ih]

-@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    toList <$> arr.mapM f = arr.toList.mapM f := by
-  simp [mapM_eq_mapM_toList]
-
@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList

@@ -803,20 +774,16 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
  simpa using map_induction as f (fun _ => True) trivial p (by simp_all)

@[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
-    (as.map f)[i] = f (as[i]'(size_map .. ▸ h)) := by
+    ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
  have := map_spec as f (fun i b => b = f (as[i]))
  simp only [implies_true, true_implies] at this
  obtain ⟨eq, w⟩ := this
  apply w
  simp_all

-@[simp] theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) :
-    (as.map f)[i]? = as[i]?.map f := by
-  simp [getElem?_def]
-
 /-! ### mapIdx -/

-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
+-- This could also be prove from `SatisfiesM_mapIdxM`.
 theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
    (motive : Nat → Prop) (h0 : motive 0)
    (p : Fin as.size → β → Prop)
@@ -856,15 +823,10 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)

@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
    (h : i < (mapIdx a f).size) :
-    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
+    haveI : i < a.size := by simp_all
+    (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _

-@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
-    (a.mapIdx f)[i]? =
-      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
-  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
-  split <;> simp_all
-
 /-! ### modify -/

@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
@@ -956,45 +918,34 @@ abbrev empty_data := @toList_empty
 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl

@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  simp only [mem_def, toList_append, List.mem_append]
+  simp only [mem_def, append_toList, List.mem_append]

-@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, toList_append, List.length_append]
+theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, append_toList, List.length_append]

-theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
-    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
-  cases as; cases bs
-  simp [List.getElem_append]
-
-theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
+theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
    (as ++ bs)[i] = as[i] := by
  simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
-  apply List.get_of_eq; rw [toList_append]
+  apply List.get_of_eq; rw [append_toList]

-@[deprecated getElem_append_left (since := "2024-09-30")]
-abbrev get_append_left := @getElem_append_left
-
-theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
+theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
    (as ++ bs)[i] = bs[i - as.size] := by
  simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
-  apply List.get_of_eq; rw [toList_append]
-
-@[deprecated getElem_append_right (since := "2024-09-30")]
-abbrev get_append_right := @getElem_append_right
+  apply List.get_of_eq; rw [append_toList]

@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
-  apply ext'; simp only [toList_append, toList_empty, List.append_nil]
+  apply ext'; simp only [append_toList, toList_empty, List.append_nil]

@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
-  apply ext'; simp only [toList_append, toList_empty, List.nil_append]
+  apply ext'; simp only [append_toList, toList_empty, List.nil_append]

 theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
-  apply ext'; simp only [toList_append, List.append_assoc]
+  apply ext'; simp only [append_toList, List.append_assoc]

 /-! ### extract -/

@@ -1044,20 +995,20 @@ theorem size_extract_loop (as bs : Array α) (size start : Nat) :
  simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
    Nat.min_assoc, Nat.min_self]

-theorem getElem_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
+theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
    i < (extract.loop as size start bs).size := by
  rw [size_extract_loop]
  apply Nat.lt_of_lt_of_le hlt
  exact Nat.le_add_right ..

-theorem getElem_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
-    (h := getElem_extract_loop_lt_aux as bs size start hlt) :
+theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
+    (h := get_extract_loop_lt_aux as bs size start hlt) :
    (extract.loop as size start bs)[i] = bs[i] := by
-  apply Eq.trans _ (getElem_append_left (bs:=extract.loop as size start #[]) hlt)
+  apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
  · rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
  · congr; rw [extract_loop_eq_aux]

-theorem getElem_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
    (h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
  have h : i < bs.size + (as.size - start) := by
      apply Nat.lt_of_lt_of_le h
@@ -1068,9 +1019,9 @@ theorem getElem_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge :
  apply Nat.add_lt_of_lt_sub'
  exact Nat.sub_lt_left_of_lt_add hge h

-theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
    (h : i < (extract.loop as size start bs).size)
-    (h' := getElem_extract_loop_ge_aux as bs size start hge h) :
+    (h' := get_extract_loop_ge_aux as bs size start hge h) :
    (extract.loop as size start bs)[i] = as[start + i - bs.size] := by
  induction size using Nat.recAux generalizing start bs with
  | zero =>
@@ -1092,37 +1043,28 @@ theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i
      have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
        rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
      have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
+        rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
      rw [h]; congr; rw [Nat.add_sub_cancel]
    else
      have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
      rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
      congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]

-theorem getElem_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
+theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
    start + i < as.size := by
  rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
  apply Nat.sub_le_sub_right; apply Nat.min_le_right

-@[simp] theorem getElem_extract {as : Array α} {start stop : Nat}
+@[simp] theorem get_extract {as : Array α} {start stop : Nat}
    (h : i < (as.extract start stop).size) :
-    (as.extract start stop)[i] = as[start + i]'(getElem_extract_aux h) :=
+    (as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
  show (extract.loop as (min stop as.size - start) start #[])[i]
-    = as[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
-
-theorem getElem?_extract {as : Array α} {start stop : Nat} :
-    (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none := by
-  simp only [getElem?_def, size_extract, getElem_extract]
-  split
-  · split
-    · rfl
-    · omega
-  · rfl
+    = as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _

@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
  apply ext
  · rw [size_extract, Nat.min_self, Nat.sub_zero]
-  · intros; rw [getElem_extract]; congr; rw [Nat.zero_add]
+  · intros; rw [get_extract]; congr; rw [Nat.zero_add]

 theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
    as.extract start stop = #[] := by
@@ -1204,12 +1146,9 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
 theorem any_eq_true {p : α → Bool} {as : Array α} :
    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]

-theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
+theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.any p := by
  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
-  exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
-
-@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
-abbrev any_def := @any_toList
+  exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩

 /-! ### all -/

@@ -1241,25 +1180,22 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
 theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
  simp [all_iff_forall, Fin.isLt]

-theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
+theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p := by
  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
  constructor
-  · intro w i
-    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
  · rintro w x ⟨r, h, rfl⟩
    rw [← getElem_eq_getElem_toList]
    exact w ⟨r, h⟩
-
-@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
-abbrev all_def := @all_toList
+  · intro w i
+    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩

 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
-  simp only [← all_toList, List.all_eq_true, mem_def]
+  simp only [all_def, List.all_eq_true, mem_def]

 /-! ### contains -/

 theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
-  rw [mem_def, contains, ← any_toList, List.any_eq_true]; simp [and_comm]
+  rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]

 instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
  decidable_of_iff _ contains_def
@@ -1268,12 +1204,12 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=

 open Fin

-@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
+@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]

-@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
+@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
-    simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
+    simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
  else by
    apply Eq.trans
    · apply Array.get_set_ne
@@ -1281,7 +1217,7 @@ open Fin
      · assumption
    · simp [get_set_ne]

-@[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
+@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
    (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
  apply Eq.trans
  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
@@ -1293,22 +1229,22 @@ open Fin
    · apply Ne.symm
      · assumption

-theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
+theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
  split
-  · simp_all only [getElem_swap_left]
+  · simp_all only [get_swap_left]
  · split <;> simp_all

-theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.swap i j).size) :
+theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
    (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
-  apply getElem_swap'
+  apply get_swap

@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
  apply ext
  · simp only [size_swap]
  · intros
-    simp only [getElem_swap]
+    simp only [get_swap']
    split
    · simp_all
    · split <;> simp_all
@@ -1317,35 +1253,11 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
  apply ext
  · simp only [size_swap]
  · intros
-    simp only [getElem_swap]
+    simp only [get_swap']
    split
    · split <;> simp_all
    · split <;> simp_all

-@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
-abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
-@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
-abbrev get_extract_loop_lt := @getElem_extract_loop_lt
-@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
-abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
-@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
-abbrev get_extract_loop_ge := @getElem_extract_loop_ge
-@[deprecated getElem_extract_aux (since := "2024-09-30")]
-abbrev get_extract_aux := @getElem_extract_aux
-@[deprecated getElem_extract (since := "2024-09-30")]
-abbrev get_extract := @getElem_extract
-
-@[deprecated getElem_swap_right (since := "2024-09-30")]
-abbrev get_swap_right := @getElem_swap_right
-@[deprecated getElem_swap_left (since := "2024-09-30")]
-abbrev get_swap_left := @getElem_swap_left
-@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
-abbrev get_swap_of_ne := @getElem_swap_of_ne
-@[deprecated getElem_swap (since := "2024-09-30")]
-abbrev get_swap := @getElem_swap
-@[deprecated getElem_swap' (since := "2024-09-30")]
-abbrev get_swap' := @getElem_swap'
-
 end Array


@@ -1362,6 +1274,9 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
  simp [mem_def]

+@[simp] theorem getElem?_toArray (l : List α) (i : Nat) : l.toArray[i]? = l[i]? := by
+  simp [getElem?_eq_getElem?_toList]
+
@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
  simp

@@ -1416,14 +1331,14 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
  rw [← anyM_toList]

@[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [any_toList]
+  rw [Array.any_def]

@[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
    l.toArray.allM p = l.allM p := by
  rw [← allM_toList]

@[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [all_toList]
+  rw [Array.all_def]

@[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
    l.toArray.swap i j = ((l.set i l[j]).set j l[i]).toArray := by
@@ -1448,6 +1363,11 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
  apply ext'
  erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.

+@[simp] theorem append_toArray (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
@[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
  apply ext'
  simp
--- a/src/Init/Data/Array/QSort.lean
+++ b/src/Init/Data/Array/QSort.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 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
@@ -45,11 +44,4 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
    else as
  sort as low high

-set_option linter.unusedVariables.funArgs false in
-/--
-Sort an array using `compare` to compare elements.
-/
-def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
-  xs.qsort fun x y => compare x y |>.isLT
-
 end Array
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -799,6 +799,7 @@ theorem umod_eq_divRec (hd : 0#w < d) :
  have := lawful_divRec this
  apply DivModState.umod_eq_of_lawful this (wn_divRec ..)

+@[simp]
 theorem divRec_succ' (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
    divRec (m+1) args qr =
    let wn := qr.wn - 1
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -72,35 +72,21 @@ instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
 instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b

@[extern "lean_float_to_string"] opaque Float.toString : Float → String
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns 0.
-If larger than the maximum value for UInt8 (including Inf), returns maximum value of UInt8
-(i.e. UInt8.size - 1).
-/
+
+/-- If the given float is positive, truncates the value to the nearest positive integer.
+If negative or larger than the maximum value for UInt8, returns 0. -/
@[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns 0.
-If larger than the maximum value for UInt16 (including Inf), returns maximum value of UInt16
-(i.e. UInt16.size - 1).
-/
+/-- If the given float is positive, truncates the value to the nearest positive integer.
+If negative or larger than the maximum value for UInt16, returns 0. -/
@[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns 0.
-If larger than the maximum value for UInt32 (including Inf), returns maximum value of UInt32
-(i.e. UInt32.size - 1).
-/
+/-- If the given float is positive, truncates the value to the nearest positive integer.
+If negative or larger than the maximum value for UInt32, returns 0. -/
@[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns 0.
-If larger than the maximum value for UInt64 (including Inf), returns maximum value of UInt64
-(i.e. UInt64.size - 1).
-/
+/-- If the given float is positive, truncates the value to the nearest positive integer.
+If negative or larger than the maximum value for UInt64, returns 0. -/
@[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns 0.
-If larger than the maximum value for USize (including Inf), returns maximum value of USize
-(i.e. USize.size - 1;  Note that this value is platform dependent).
-/
+/-- If the given float is positive, truncates the value to the nearest positive integer.
+If negative or larger than the maximum value for USize, returns 0. -/
@[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize

@[extern "lean_float_isnan"] opaque Float.isNaN : Float → Bool
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -43,7 +43,7 @@ The operations are organized as follow:
 * Logic: `any`, `all`, `or`, and `and`.
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
 * Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
-* Minima and maxima: `min?` and `max?`.
+* Minima and maxima: `minimum?` and `maximum?`.
 * Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
  `removeAll`
  (currently these functions are mostly only used in meta code,
@@ -1464,34 +1464,30 @@ def enum : List α → List (Nat × α) := enumFrom 0

 /-! ## Minima and maxima -/

-/-! ### min? -/
+/-! ### minimum? -/

 /--
 Returns the smallest element of the list, if it is not empty.
-* `[].min? = none`
-* `[4].min? = some 4`
-* `[1, 4, 2, 10, 6].min? = some 1`
+* `[].minimum? = none`
+* `[4].minimum? = some 4`
+* `[1, 4, 2, 10, 6].minimum? = some 1`
 -/
-def min? [Min α] : List α → Option α
+def minimum? [Min α] : List α → Option α
  | []    => none
  | a::as => some <| as.foldl min a

-@[inherit_doc min?, deprecated min? (since := "2024-09-29")] abbrev minimum? := @min?
-
-/-! ### max? -/
+/-! ### maximum? -/

 /--
 Returns the largest element of the list, if it is not empty.
-* `[].max? = none`
-* `[4].max? = some 4`
-* `[1, 4, 2, 10, 6].max? = some 10`
+* `[].maximum? = none`
+* `[4].maximum? = some 4`
+* `[1, 4, 2, 10, 6].maximum? = some 10`
 -/
-def max? [Max α] : List α → Option α
+def maximum? [Max α] : List α → Option α
  | []    => none
  | a::as => some <| as.foldl max a

-@[inherit_doc max?, deprecated max? (since := "2024-09-29")] abbrev maximum? := @max?
-
 /-! ## Other list operations

 The functions are currently mostly used in meta code,
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -31,7 +31,7 @@ The following operations are still missing `@[csimp]` replacements:
 The following operations are not recursive to begin with
 (or are defined in terms of recursive primitives):
 `isEmpty`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft`, `rotateRight`, `insert`, `zip`, `enum`,
-`min?`, `max?`, and `removeAll`.
+`minimum?`, `maximum?`, and `removeAll`.

 The following operations were already given `@[csimp]` replacements in `Init/Data/List/Basic.lean`:
 `length`, `map`, `filter`, `replicate`, `leftPad`, `unzip`, `range'`, `iota`, `intersperse`.
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -55,7 +55,7 @@ See also
 * `Init.Data.List.Erase` for lemmas about `List.eraseP` and `List.erase`.
 * `Init.Data.List.Find` for lemmas about `List.find?`, `List.findSome?`, `List.findIdx`,
  `List.findIdx?`, and `List.indexOf`
-* `Init.Data.List.MinMax` for lemmas about `List.min?` and `List.max?`.
+* `Init.Data.List.MinMax` for lemmas about `List.minimum?` and `List.maximum?`.
 * `Init.Data.List.Pairwise` for lemmas about `List.Pairwise` and `List.Nodup`.
 * `Init.Data.List.Sublist` for lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`,
  `List.IsSuffix`, and `List.IsInfix`.
@@ -203,9 +203,6 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=

@[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
@@ -492,7 +489,7 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 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 _⟩

-@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
+theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
  | _ :: _, 0, _ => .head ..
  | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)

@@ -881,20 +878,6 @@ theorem foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' :
  · simp
  · simp [*, h]

-theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] :
-    ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
-  | [], a₁, a₂ => rfl
-  | a :: l, a₁, a₂ => by
-    simp only [foldl_cons, ha.assoc]
-    rw [foldl_assoc]
-
-theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] :
-    ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
-  | [], a₁, a₂ => rfl
-  | a :: l, a₁, a₂ => by
-    simp only [foldr_cons, ha.assoc]
-    rw [foldr_assoc]
-
 theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
  induction l generalizing init <;> simp [*, H]
@@ -1021,7 +1004,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
 theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
  simp [getLast!, getLast_eq_getLastD]

-@[simp] theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
+theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
  | [], h => absurd rfl h
  | [_], _ => .head ..
  | _::a::l, _ => .tail _ <| getLast_mem (cons_ne_nil a l)
@@ -1119,7 +1102,7 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys
@[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
  cases l <;> simp

-@[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
+theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
  | [], h => absurd rfl h
  | _::_, _ => .head ..

@@ -2409,10 +2392,6 @@ theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
@[simp] theorem map_const (l : List α) (b : β) : map (Function.const α b) l = replicate l.length b :=
  map_eq_replicate_iff.mpr fun _ _ => rfl

-@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.length x) := by
-  funext l
-  simp
-
 /-- Variant of `map_const` using a lambda rather than `Function.const`. -/
 -- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
 theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.length b :=
--- a/src/Init/Data/List/MinMax.lean
+++ b/src/Init/Data/List/MinMax.lean
@@ -7,7 +7,7 @@ prelude
 import Init.Data.List.Lemmas

 /-!
-# Lemmas about `List.min?` and `List.max?.
+# Lemmas about `List.minimum?` and `List.maximum?.
 -/

 namespace List
@@ -16,24 +16,24 @@ open Nat

 /-! ## Minima and maxima -/

-/-! ### min? -/
+/-! ### minimum? -/

-@[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
+@[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl

-- We don't put `@[simp]` on `min?_cons`,
+-- We don't put `@[simp]` on `minimum?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem min?_cons [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
+theorem minimum?_cons [Min α] {xs : List α} : (x :: xs).minimum? = foldl min x xs := rfl

-@[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = [] := by
-  cases xs <;> simp [min?]
+@[simp] theorem minimum?_eq_none_iff {xs : List α} [Min α] : xs.minimum? = none ↔ xs = [] := by
+  cases xs <;> simp [minimum?]

-theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
-    {xs : List α} → xs.min? = some a → a ∈ xs := by
+theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
+    {xs : List α} → xs.minimum? = some a → a ∈ xs := by
  intro xs
  match xs with
  | nil => simp
  | x :: xs =>
-    simp only [min?_cons, Option.some.injEq, List.mem_cons]
+    simp only [minimum?_cons, Option.some.injEq, List.mem_cons]
    intro eq
    induction xs generalizing x with
    | nil =>
@@ -49,12 +49,12 @@ theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b

 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.

-theorem le_min?_iff [Min α] [LE α]
+theorem le_minimum?_iff [Min α] [LE α]
    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
-    {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
+    {xs : List α} → xs.minimum? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
  | nil => by simp
  | cons x xs => by
-    rw [min?]
+    rw [minimum?]
    intro eq y
    simp only [Option.some.injEq] at eq
    induction xs generalizing x with
@@ -67,46 +67,46 @@ theorem le_min?_iff [Min α] [LE α]

 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
    (le_refl : ∀ a : α, a ≤ a)
    (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
-    xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
-  refine ⟨fun h => ⟨min?_mem min_eq_or h, (le_min?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
+    xs.minimum? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
+  refine ⟨fun h => ⟨minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
  intro ⟨h₁, h₂⟩
  cases xs with
  | nil => simp at h₁
  | cons x xs =>
    exact congrArg some <| anti.1
-      ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
-      (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))
+      ((le_minimum?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))

-theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
-    (replicate n a).min? = if n = 0 then none else some a := by
+theorem minimum?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
+    (replicate n a).minimum? = if n = 0 then none else some a := by
  induction n with
  | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, minimum?_cons]

-@[simp] theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
-    (replicate n a).min? = some a := by
-  simp [min?_replicate, Nat.ne_of_gt h, w]
+@[simp] theorem minimum?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
+    (replicate n a).minimum? = some a := by
+  simp [minimum?_replicate, Nat.ne_of_gt h, w]

-/-! ### max? -/
+/-! ### maximum? -/

-@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
+@[simp] theorem maximum?_nil [Max α] : ([] : List α).maximum? = none := rfl

-- We don't put `@[simp]` on `max?_cons`,
+-- We don't put `@[simp]` on `maximum?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem max?_cons [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
+theorem maximum?_cons [Max α] {xs : List α} : (x :: xs).maximum? = foldl max x xs := rfl

-@[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = [] := by
-  cases xs <;> simp [max?]
+@[simp] theorem maximum?_eq_none_iff {xs : List α} [Max α] : xs.maximum? = none ↔ xs = [] := by
+  cases xs <;> simp [maximum?]

-theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
-    {xs : List α} → xs.max? = some a → a ∈ xs
+theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
+    {xs : List α} → xs.maximum? = some a → a ∈ xs
  | nil => by simp
  | cons x xs => by
-    rw [max?]; rintro ⟨⟩
+    rw [maximum?]; rintro ⟨⟩
    induction xs generalizing x with simp at *
    | cons y xs ih =>
      rcases ih (max x y) with h | h <;> simp [h]
@@ -114,57 +114,40 @@ theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b

 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.

-theorem max?_le_iff [Max α] [LE α]
+theorem maximum?_le_iff [Max α] [LE α]
    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
-    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
+    {xs : List α} → xs.maximum? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
  | nil => by simp
  | cons x xs => by
-    rw [max?]; rintro ⟨⟩ y
+    rw [maximum?]; rintro ⟨⟩ y
    induction xs generalizing x with
    | nil => simp
    | cons y xs ih => simp [ih, max_le_iff, and_assoc]

 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
 -- and `le_min_iff`.
-theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
    (le_refl : ∀ a : α, a ≤ a)
    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
-    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
-  refine ⟨fun h => ⟨max?_mem max_eq_or h, (max?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
+    xs.maximum? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
+  refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
  intro ⟨h₁, h₂⟩
  cases xs with
  | nil => simp at h₁
  | cons x xs =>
    exact congrArg some <| anti.1
-      (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
-      ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl))
+      ((maximum?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)

-theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
-    (replicate n a).max? = if n = 0 then none else some a := by
+theorem maximum?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
+    (replicate n a).maximum? = if n = 0 then none else some a := by
  induction n with
  | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, maximum?_cons]

-@[simp] theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
-    (replicate n a).max? = some a := by
-  simp [max?_replicate, Nat.ne_of_gt h, w]
-
-@[deprecated min?_nil (since := "2024-09-29")] abbrev minimum?_nil := @min?_nil
-@[deprecated min?_cons (since := "2024-09-29")] abbrev minimum?_cons := @min?_cons
-@[deprecated min?_eq_none_iff (since := "2024-09-29")] abbrev mininmum?_eq_none_iff := @min?_eq_none_iff
-@[deprecated min?_mem (since := "2024-09-29")] abbrev minimum?_mem := @min?_mem
-@[deprecated le_min?_iff (since := "2024-09-29")] abbrev le_minimum?_iff := @le_min?_iff
-@[deprecated min?_eq_some_iff (since := "2024-09-29")] abbrev minimum?_eq_some_iff := @min?_eq_some_iff
-@[deprecated min?_replicate (since := "2024-09-29")] abbrev minimum?_replicate := @min?_replicate
-@[deprecated min?_replicate_of_pos (since := "2024-09-29")] abbrev minimum?_replicate_of_pos := @min?_replicate_of_pos
-@[deprecated max?_nil (since := "2024-09-29")] abbrev maximum?_nil := @max?_nil
-@[deprecated max?_cons (since := "2024-09-29")] abbrev maximum?_cons := @max?_cons
-@[deprecated max?_eq_none_iff (since := "2024-09-29")] abbrev maximum?_eq_none_iff := @max?_eq_none_iff
-@[deprecated max?_mem (since := "2024-09-29")] abbrev maximum?_mem := @max?_mem
-@[deprecated max?_le_iff (since := "2024-09-29")] abbrev maximum?_le_iff := @max?_le_iff
-@[deprecated max?_eq_some_iff (since := "2024-09-29")] abbrev maximum?_eq_some_iff := @max?_eq_some_iff
-@[deprecated max?_replicate (since := "2024-09-29")] abbrev maximum?_replicate := @max?_replicate
-@[deprecated max?_replicate_of_pos (since := "2024-09-29")] abbrev maximum?_replicate_of_pos := @max?_replicate_of_pos
+@[simp] theorem maximum?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
+    (replicate n a).maximum? = some a := by
+  simp [maximum?_replicate, Nat.ne_of_gt h, w]

 end List
--- a/src/Init/Data/List/Nat/Basic.lean
+++ b/src/Init/Data/List/Nat/Basic.lean
@@ -86,26 +86,26 @@ theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃
    obtain ⟨h', -⟩ := getElem?_eq_some_iff.1 h
    exact ⟨h', h⟩

-/-! ### min? -/
+/-! ### minimum? -/

-- A specialization of `min?_eq_some_iff` to Nat.
-theorem min?_eq_some_iff' {xs : List Nat} :
-    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  min?_eq_some_iff
+-- A specialization of `minimum?_eq_some_iff` to Nat.
+theorem minimum?_eq_some_iff' {xs : List Nat} :
+    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  minimum?_eq_some_iff
    (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
-    (le_min_iff := fun _ _ _ => Nat.le_min)
+    (min_eq_or := fun _ _ => by omega)
+    (le_min_iff := fun _ _ _ => by omega)

 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem min?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).min? = some (match l.min? with
+theorem minimum?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).minimum? = some (match l.minimum? with
    | none => a
    | some m => min a m) := by
-  rw [min?_eq_some_iff']
+  rw [minimum?_eq_some_iff']
  split <;> rename_i h m
  · simp_all
-  · rw [min?_eq_some_iff'] at m
+  · rw [minimum?_eq_some_iff'] at m
    obtain ⟨m, le⟩ := m
    rw [Nat.min_def]
    constructor
@@ -122,11 +122,11 @@ theorem min?_cons' {a : Nat} {l : List Nat} :
 theorem foldl_min
    {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
    {l : List α} {a : α} :
-    l.foldl (init := a) min = min a (l.min?.getD a) := by
+    l.foldl (init := a) min = min a (l.minimum?.getD a) := by
  cases l with
  | nil => simp [Std.IdempotentOp.idempotent]
  | cons b l =>
-    simp only [min?]
+    simp only [minimum?]
    induction l generalizing a b with
    | nil => simp
    | cons c l ih => simp [ih, Std.Associative.assoc]
@@ -134,7 +134,7 @@ theorem foldl_min
 theorem foldl_min_right {α β : Type _}
    [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)]
    {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).min?.getD b) := by
+    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
  rw [← foldl_map, foldl_min]

 theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by
@@ -148,12 +148,12 @@ theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
    l.foldl (init := a) min ≤ b :=
  Nat.le_trans (foldl_min_le) h

-theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    l.min?.getD k ≤ a := by
+theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.minimum?.getD k ≤ a := by
  cases l with
  | nil => simp at h
  | cons b l =>
-    simp [min?_cons]
+    simp [minimum?_cons]
    simp at h
    rcases h with (rfl | h)
    · exact foldl_min_le
@@ -166,26 +166,26 @@ theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
        · exact foldl_min_min_of_le (Nat.min_le_right _ _)
        · exact ih _ h

-/-! ### max? -/
+/-! ### maximum? -/

-- A specialization of `max?_eq_some_iff` to Nat.
-theorem max?_eq_some_iff' {xs : List Nat} :
-    xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
-  max?_eq_some_iff
+-- A specialization of `maximum?_eq_some_iff` to Nat.
+theorem maximum?_eq_some_iff' {xs : List Nat} :
+    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
+  maximum?_eq_some_iff
    (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp)
-    (max_le_iff := fun _ _ _ => Nat.max_le)
+    (max_eq_or := fun _ _ => by omega)
+    (max_le_iff := fun _ _ _ => by omega)

 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem max?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).max? = some (match l.max? with
+theorem maximum?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).maximum? = some (match l.maximum? with
    | none => a
    | some m => max a m) := by
-  rw [max?_eq_some_iff']
+  rw [maximum?_eq_some_iff']
  split <;> rename_i h m
  · simp_all
-  · rw [max?_eq_some_iff'] at m
+  · rw [maximum?_eq_some_iff'] at m
    obtain ⟨m, le⟩ := m
    rw [Nat.max_def]
    constructor
@@ -202,11 +202,11 @@ theorem max?_cons' {a : Nat} {l : List Nat} :
 theorem foldl_max
    {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
    {l : List α} {a : α} :
-    l.foldl (init := a) max = max a (l.max?.getD a) := by
+    l.foldl (init := a) max = max a (l.maximum?.getD a) := by
  cases l with
  | nil => simp [Std.IdempotentOp.idempotent]
  | cons b l =>
-    simp only [max?]
+    simp only [maximum?]
    induction l generalizing a b with
    | nil => simp
    | cons c l ih => simp [ih, Std.Associative.assoc]
@@ -214,7 +214,7 @@ theorem foldl_max
 theorem foldl_max_right {α β : Type _}
    [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)]
    {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).max?.getD b) := by
+    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
  rw [← foldl_map, foldl_max]

 theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by
@@ -228,12 +228,12 @@ theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
    a ≤ l.foldl (init := b) max :=
  Nat.le_trans h (le_foldl_max)

-theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    a ≤ l.max?.getD k := by
+theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.maximum?.getD k := by
  cases l with
  | nil => simp at h
  | cons b l =>
-    simp [max?_cons]
+    simp [maximum?_cons]
    simp at h
    rcases h with (rfl | h)
    · exact le_foldl_max
@@ -246,11 +246,4 @@ theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
        · exact le_foldl_max_of_le (Nat.le_max_right b a)
        · exact ih _ h

-@[deprecated min?_eq_some_iff' (since := "2024-09-29")] abbrev minimum?_eq_some_iff' := @min?_eq_some_iff'
-@[deprecated min?_cons' (since := "2024-09-29")] abbrev minimum?_cons' := @min?_cons'
-@[deprecated min?_getD_le_of_mem (since := "2024-09-29")] abbrev minimum?_getD_le_of_mem := @min?_getD_le_of_mem
-@[deprecated max?_eq_some_iff' (since := "2024-09-29")] abbrev maximum?_eq_some_iff' := @max?_eq_some_iff'
-@[deprecated max?_cons' (since := "2024-09-29")] abbrev maximum?_cons' := @max?_cons'
-@[deprecated le_max?_getD_of_mem (since := "2024-09-29")] abbrev le_maximum?_getD_of_mem := @le_max?_getD_of_mem
-
 end List
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -42,7 +42,7 @@ theorem getElem_take' (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j)

 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
-@[simp] theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
+theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
    (L.take j)[i] =
    L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
  rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1]
@@ -52,7 +52,7 @@ length `> i`. Version designed to rewrite from the big list to the small list. -
@[deprecated getElem_take' (since := "2024-06-12")]
 theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
-  simp
+  simp [getElem_take' _ hi hj]

 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -248,10 +248,6 @@ theorem countP_eq_countP_filter_add (l : List α) (p q : α → Bool) :
 theorem Perm.count_eq [DecidableEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) :
    count a l₁ = count a l₂ := p.countP_eq _

-/-
-This theorem is a variant of `Perm.foldl_eq` defined in Mathlib which uses typeclasses rather
-than the explicit `comm` argument.
-/
 theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f (f z x) y = f (f z y) x)
    (init) : foldl f init l₁ = foldl f init l₂ := by
@@ -268,28 +264,6 @@ theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~
    refine (IH₁ comm init).trans (IH₂ ?_ _)
    intros; apply comm <;> apply p₁.symm.subset <;> assumption

-/-
-This theorem is a variant of `Perm.foldr_eq` defined in Mathlib which uses typeclasses rather
-than the explicit `comm` argument.
-/
-theorem Perm.foldr_eq' {f : α → β → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
-    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f y (f x z) = f x (f y z))
-    (init) : foldr f init l₁ = foldr f init l₂ := by
-  induction p using recOnSwap' generalizing init with
-  | nil => simp
-  | cons x _p IH =>
-    simp only [foldr]
-    congr 1
-    apply IH; intros; apply comm <;> exact .tail _ ‹_›
-  | swap' x y _p IH =>
-    simp only [foldr]
-    rw [comm x (.tail _ <| .head _) y (.head _)]
-    congr 2
-    apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›)
-  | trans p₁ _p₂ IH₁ IH₂ =>
-    refine (IH₁ comm init).trans (IH₂ ?_ _)
-    intros; apply comm <;> apply p₁.symm.subset <;> assumption
-
 theorem Perm.rec_heq {β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α}
    (hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b'))
    (f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :
--- a/src/Init/Data/Option.lean
+++ b/src/Init/Data/Option.lean
@@ -8,5 +8,3 @@ import Init.Data.Option.Basic
 import Init.Data.Option.BasicAux
 import Init.Data.Option.Instances
 import Init.Data.Option.Lemmas
-import Init.Data.Option.Attach
-import Init.Data.Option.List
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -1,178 +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.Option.Basic
-import Init.Data.Option.List
-import Init.Data.List.Attach
-import Init.BinderPredicates
-
-namespace Option
-
-/--
-Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
-`Option {x // P x}` is the same as the input `Option α`.
-/
-@[inline] private unsafe def attachWithImpl
-    (o : Option α) (P : α → Prop) (_ : ∀ x ∈ o, P x) : Option {x // P x} := unsafeCast o
-
-/-- "Attach" a proof `P x` that holds for the element of `o`, if present,
-to produce a new option with the same element but in the type `{x // P x}`. -/
-@[implemented_by attachWithImpl] def attachWith
-    (xs : Option α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Option {x // P x} :=
-  match xs with
-  | none => none
-  | some x => some ⟨x, H x (mem_some_self x)⟩
-
-/-- "Attach" the proof that the element of `xs`, if present, is in `xs`
-to produce a new option with the same elements but in the type `{x // x ∈ xs}`. -/
-@[inline] def attach (xs : Option α) : Option {x // x ∈ xs} := xs.attachWith _ fun _ => id
-
-@[simp] theorem attach_none : (none : Option α).attach = none := rfl
-@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
-
-@[simp] theorem attach_some {x : α} :
-    (some x).attach = some ⟨x, rfl⟩ := rfl
-@[simp] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) :
-    (some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl
-
-theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
-    o₁.attach = o₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
-  subst h
-  simp
-
-theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
-    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
-  subst w
-  simp
-
-theorem attach_map_coe (o : Option α) (f : α → β) :
-    (o.attach.map fun (i : {i // i ∈ o}) => f i) = o.map f := by
-  cases o <;> simp
-
-theorem attach_map_val (o : Option α) (f : α → β) :
-    (o.attach.map fun i => f i.val) = o.map f :=
-  attach_map_coe _ _
-
-@[simp]
-theorem attach_map_subtype_val (o : Option α) :
-    o.attach.map Subtype.val = o :=
-  (attach_map_coe _ _).trans (congrFun Option.map_id _)
-
-theorem attachWith_map_coe {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
-    ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
-  cases o <;> simp [H]
-
-theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
-    ((o.attachWith p H).map fun i => f i.val) = o.map f :=
-  attachWith_map_coe _ _ _
-
-@[simp]
-theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
-    (o.attachWith p H).map Subtype.val = o :=
-  (attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
-
-@[simp] theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
-  | none, ⟨x, h⟩ => by simp at h
-  | some a, ⟨x, h⟩ => by simpa using h
-
-@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
-  cases o <;> simp
-
-@[simp] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
-    (o.attachWith p H).isNone = o.isNone := by
-  cases o <;> simp
-
-@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
-  cases o <;> simp
-
-@[simp] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
-    (o.attachWith p H).isSome = o.isSome := by
-  cases o <;> simp
-
-@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none ↔ o = none := by
-  cases o <;> simp
-
-@[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} :
-    o.attach = some x ↔ o = some x.val := by
-  cases o <;> cases x <;> simp
-
-@[simp] theorem attachWith_eq_none_iff {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
-    o.attachWith p H = none ↔ o = none := by
-  cases o <;> simp
-
-@[simp] theorem attachWith_eq_some_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) {x : {x // p x}} :
-    o.attachWith p H = some x ↔ o = some x.val := by
-  cases o <;> cases x <;> simp
-
-@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
-    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ := by
-  cases o
-  · simp at h
-  · simp [get_some]
-
-@[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) (h : (o.attachWith p H).isSome) :
-    (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
-  cases o
-  · simp at h
-  · simp [get_some]
-
-@[simp] theorem toList_attach (o : Option α) :
-    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
-  cases o <;> simp
-
-theorem attach_map {o : Option α} (f : α → β) :
-    (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
-  cases o <;> simp
-
-theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
-    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
-      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
-  cases o <;> simp
-
-theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
-    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
-  cases o <;> simp
-
-theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
-    (f : { x // P x } → β) :
-    (o.attachWith P H).map f =
-      o.pmap (fun a (h : a ∈ o ∧ P a) => f ⟨a, h.2⟩) (fun a h => ⟨h, H a h⟩) := by
-  cases o <;> simp
-
-theorem attach_bind {o : Option α} {f : α → Option β} :
-    (o.bind f).attach =
-      o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, mem_bind_iff.mpr ⟨x, h, h'⟩⟩ := by
-  cases o <;> simp
-
-theorem bind_attach {o : Option α} {f : {x // x ∈ o} → Option β} :
-    o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
-  cases o <;> simp
-
-theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → a ∈ o → Option β} :
-    o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
-  cases o <;> simp
-
-theorem attach_filter {o : Option α} {p : α → Bool} :
-    (o.filter p).attach =
-      o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [filter_some, attach_some]
-    ext
-    simp only [mem_def, attach_eq_some_iff, ite_none_right_eq_some, some.injEq, some_bind,
-      dite_none_right_eq_some]
-    constructor
-    · rintro ⟨h, w⟩
-      refine ⟨h, by ext; simpa using w⟩
-    · rintro ⟨h, rfl⟩
-      simp [h]
-
-theorem filter_attach {o : Option α} {p : {x // x ∈ o} → Bool} :
-    o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
-  cases o <;> simp [filter_some]
-
-end Option
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -138,10 +138,6 @@ theorem bind_eq_none' {o : Option α} {f : α → Option β} :
    o.bind f = none ↔ ∀ b a, a ∈ o → b ∉ f a := by
  simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]

-theorem mem_bind_iff {o : Option α} {f : α → Option β} :
-    b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
-  cases o <;> simp
-
 theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β) :
    (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
  cases a <;> cases b <;> rfl
@@ -236,27 +232,9 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
  cases o <;> simp at h ⊢

@[simp] theorem filter_eq_none {p : α → Bool} :
-    o.filter p = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
+    Option.filter p o = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
  cases o <;> simp [filter_some]

-@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} :
-    o.filter p = some a ↔ a ∈ o ∧ p a := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp [filter_some]
-    split <;> rename_i h
-    · simp only [some.injEq, iff_self_and]
-      rintro rfl
-      exact h
-    · simp only [reduceCtorEq, false_iff, not_and, Bool.not_eq_true]
-      rintro rfl
-      simpa using h
-
-theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
-    a ∈ o.filter p ↔ a ∈ o ∧ p a := by
-  simp
-
@[simp] theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
    Option.all q (guard p a) = (!p a || q a) := by
  simp only [guard]
@@ -372,8 +350,6 @@ end choice

@[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl

-- See `Init.Data.Option.List` for lemmas about `toList`.
-
@[simp] theorem or_some : (some a).or o = some a := rfl
@[simp] theorem none_or : none.or o = o := rfl

--- a/src/Init/Data/Option/List.lean
+++ b/src/Init/Data/Option/List.lean
@@ -1,14 +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.Lemmas
-
-namespace Option
-
-@[simp] theorem mem_toList (a : α) (o : Option α) : a ∈ o.toList ↔ a ∈ o := by
-  cases o <;> simp [eq_comm]
-
-end Option
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -733,8 +733,7 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
        throwError "invalid default value for field, it contains metavariables{indentExpr value}"
      /- The identity function is used as "marker". -/
      let value ← mkId value
-      -- No need to compile the definition, since it is only used during elaboration.
-      discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
+      discard <| mkAuxDefinition declName type value (zetaDelta := true)
      setReducibleAttribute declName

 /--
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -277,7 +277,6 @@ where
      | _ => mkAtomLinearCombo e
    | (``Min.min, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_min []) a b)
    | (``Max.max, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_max []) a b)
-    | (``Int.toNat, #[n]) => rewrite e (mkApp (.const ``Int.toNat_eq_max []) n)
    | (``HShiftLeft.hShiftLeft, #[_, _, _, _, a, b]) =>
      rewrite e (mkApp2 (.const ``Int.ofNat_shiftLeft_eq []) a b)
    | (``HShiftRight.hShiftRight, #[_, _, _, _, a, b]) =>
--- a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
+++ b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
@@ -29,14 +29,12 @@ The minimum non-zero entry in a list of natural numbers, or zero if all entries
 We completely characterize the function via
 `nonzeroMinimum_eq_zero_iff` and `nonzeroMinimum_eq_nonzero_iff` below.
 -/
-def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.min? |>.getD 0
+def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.minimum? |>.getD 0

 -- A specialization of `minimum?_eq_some_iff` to Nat.
-- This is a duplicate `min?_eq_some_iff'` proved in `Init.Data.List.Nat.Basic`,
-- and could be deduplicated but the import hierarchy is awkward.
-theorem min?_eq_some_iff'' {xs : List Nat} :
-    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  min?_eq_some_iff
+theorem minimum?_eq_some_iff' {xs : List Nat} :
+    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  minimum?_eq_some_iff
    (le_refl := Nat.le_refl)
    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
    (le_min_iff := fun _ _ _ => Nat.le_min)
@@ -44,27 +42,27 @@ theorem min?_eq_some_iff'' {xs : List Nat} :
 open Classical in
@[simp] theorem nonzeroMinimum_eq_zero_iff {xs : List Nat} :
    xs.nonzeroMinimum = 0 ↔ ∀ x ∈ xs, x = 0 := by
-  simp [nonzeroMinimum, Option.getD_eq_iff, min?_eq_none_iff, min?_eq_some_iff'',
+  simp [nonzeroMinimum, Option.getD_eq_iff, minimum?_eq_none_iff, minimum?_eq_some_iff',
    filter_eq_nil_iff, mem_filter]

 theorem nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum ≠ 0) :
    xs.nonzeroMinimum ∈ xs := by
  dsimp [nonzeroMinimum] at *
-  generalize h : (xs.filter (· ≠ 0) |>.min?) = m at *
+  generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m at *
  match m, w with
-  | some (m+1), _ => simp_all [min?_eq_some_iff'', mem_filter]
+  | some (m+1), _ => simp_all [minimum?_eq_some_iff', mem_filter]

 theorem nonzeroMinimum_pos {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : 0 < xs.nonzeroMinimum :=
  Nat.pos_iff_ne_zero.mpr fun w => h (nonzeroMinimum_eq_zero_iff.mp w _ m)

 theorem nonzeroMinimum_le {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : xs.nonzeroMinimum ≤ a := by
-  have : (xs.filter (· ≠ 0) |>.min?) = some xs.nonzeroMinimum := by
+  have : (xs.filter (· ≠ 0) |>.minimum?) = some xs.nonzeroMinimum := by
    have w := nonzeroMinimum_pos m h
    dsimp [nonzeroMinimum] at *
-    generalize h : (xs.filter (· ≠ 0) |>.min?) = m? at *
+    generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m? at *
    match m?, w with
    | some m?, _ => rfl
-  rw [min?_eq_some_iff''] at this
+  rw [minimum?_eq_some_iff'] at this
  apply this.2
  simp [List.mem_filter]
  exact ⟨m, h⟩
@@ -144,4 +142,4 @@ theorem minNatAbs_eq_nonzero_iff (xs : List Int) (w : z ≠ 0) :
@[simp] theorem minNatAbs_nil : ([] : List Int).minNatAbs = 0 := rfl

 /-- The maximum absolute value in a list of integers. -/
-def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.max? |>.getD 0
+def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.maximum? |>.getD 0
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -573,33 +573,15 @@ where
    catch _  =>
      return some mvarId

-/--
-Discharges assumptions of the form `∀ …, a = b` using `rfl`. This is particularly useful for higher
-order assumptions of the form `∀ …, e = ?g x y` to instaniate  a paramter `g` even if that does not
-appear on the lhs of the rule.
-/
-def dischargeRfl (e : Expr) : SimpM (Option Expr) := do
-  forallTelescope e fun xs e => do
-    let some (t, a, b) := e.eq? | return .none
-    unless a.getAppFn.isMVar || b.getAppFn.isMVar do return .none
-    if (← withReducible <| isDefEq a b) then
-      trace[Meta.Tactic.simp.discharge] "Discharging with rfl: {e}"
-      let u ← getLevel t
-      let proof := mkApp2 (.const ``rfl [u]) t a
-      let proof ← mkLambdaFVars xs proof
-      return .some proof
-    return .none
-
-
 def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
  let e := e.cleanupAnnotations
  if isEqnThmHypothesis e then
-    if let some r ← dischargeUsingAssumption? e then return some r
-    if let some r ← dischargeEqnThmHypothesis? e then return some r
+    if let some r ← dischargeUsingAssumption? e then
+      return some r
+    if let some r ← dischargeEqnThmHypothesis? e then
+      return some r
  let r ← simp e
-  if let some p ← dischargeRfl r.expr then
-    return some (← mkEqMPR (← r.getProof) p)
-  else if r.expr.isTrue then
+  if r.expr.isTrue then
    return some (← mkOfEqTrue (← r.getProof))
  else
    return none
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -360,8 +360,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
    else
      -- stopped after `tk` => add space
-      pushLine
-      push tk
+      push $ tk ++ " "
      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
  else
    -- already separated => use `tk` as is
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -237,7 +237,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
    let _ := @lexOrd
    let _ := @leOfOrd.{0}
    let _ := @maxOfLe
-    results.map (·.1) |>.max?
+    results.map (·.1) |>.maximum?
  let res? := results.find? (·.1 == maxPrio?) |>.map (·.2)
  if let some i := res? then
    if let .ofTermInfo ti := i.info then
@@ -380,7 +380,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
              priority := if hoverPos.byteIdx == tailPos.byteIdx + trailSize then 0 else 1
            }]
    return gs
-  let maxPrio? := gs.map (·.priority) |>.max?
+  let maxPrio? := gs.map (·.priority) |>.maximum?
  gs.filter (some ·.priority == maxPrio?)
 where
  hasNestedTactic (pos tailPos) : InfoTree → Bool
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -186,7 +186,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
    have := (hg (l := []) (l' := [])).length_eq
    rw [List.length_append, List.append_nil] at this
    omega
-  rw [updateAllBuckets, toListModel, Array.toList_map, List.bind_eq_foldl, List.foldl_map,
+  rw [updateAllBuckets, toListModel, Array.map_toList, List.bind_eq_foldl, List.foldl_map,
    toListModel, List.bind_eq_foldl]
  suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
      Perm (g l'') l' →
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -104,10 +104,10 @@ def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) :=
    by
      intro i h
      by_cases hsplit : i < lrefs.size
-      · rw [Array.getElem_append_left]
+      · rw [Array.get_append_left]
        apply hl2
        omega
-      · rw [Array.getElem_append_right]
+      · rw [Array.get_append_right]
        · apply hr2
          omega
        · omega
@@ -124,9 +124,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
  simp only [get, append]
  split
  · simp [Ref.mk.injEq]
-    rw [Array.getElem_append_left]
+    rw [Array.get_append_left]
  · simp only [Ref.mk.injEq]
-    rw [Array.getElem_append_right]
+    rw [Array.get_append_right]
    · simp [lhs.hlen]
    · rw [lhs.hlen]
      omega
--- a/src/Std/Sat/CNF/RelabelFin.lean
+++ b/src/Std/Sat/CNF/RelabelFin.lean
@@ -15,12 +15,12 @@ namespace CNF
 /--
 Obtain the literal with the largest identifier in `c`.
 -/
-def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.max?
+def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.maximum?

 theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) :
    ∀ lit, Mem lit c → lit ≤ maxLit := by
  intro lit hlit
-  simp only [maxLiteral, List.max?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
+  simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at h
  simp only [Mem] at hlit
  rcases h with ⟨_, hbar⟩
@@ -35,25 +35,25 @@ theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) :
  cases h <;> rename_i h
  all_goals
    have h1 := List.ne_nil_of_mem h
-    have h2 := not_congr <| @List.max?_eq_none_iff _ (c.map (·.1)) _
+    have h2 := not_congr <| @List.maximum?_eq_none_iff _ (c.map (·.1)) _
    simp [← Option.ne_none_iff_exists', h1, h2, maxLiteral]

 theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) :
    ∀ lit, ¬Mem lit c := by
  intro lit hlit
-  simp only [maxLiteral, List.max?_eq_none_iff, List.map_eq_nil_iff] at h
+  simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil_iff] at h
  simp only [h, not_mem_nil] at hlit

 /--
 Obtain the literal with the largest identifier in `f`.
 -/
 def maxLiteral (f : CNF Nat) : Option Nat :=
-  List.filterMap Clause.maxLiteral f |>.max?
+  List.filterMap Clause.maxLiteral f |>.maximum?

 theorem of_maxLiteral_eq_some' (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
    ∀ clause, clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit := by
  intro clause hclause1 hclause2
-  simp [maxLiteral, List.max?_eq_some_iff'] at h
+  simp [maxLiteral, List.maximum?_eq_some_iff'] at h
  rcases h with ⟨_, hclause3⟩
  apply hclause3 localMax clause hclause1 hclause2

@@ -70,7 +70,7 @@ theorem of_maxLiteral_eq_some (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
 theorem of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) :
    ∀ lit, ¬Mem lit f := by
  intro lit hlit
-  simp only [maxLiteral, List.max?_eq_none_iff] at h
+  simp only [maxLiteral, List.maximum?_eq_none_iff] at h
  dsimp [Mem] at hlit
  rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩
  have := Clause.of_maxLiteral_eq_none clause (List.forall_none_of_filterMap_eq_nil h clause hclause1) lit
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -502,7 +502,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
              have idx_in_bounds2 : idx < f.clauses.size := by
                conv => rhs; rw [Array.size_mk]
                exact hbound
-              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
              rw [hidx, hl] at heq
              simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
@@ -535,7 +535,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
              have idx_in_bounds2 : idx < f.clauses.size := by
                conv => rhs; rw [Array.size_mk]
                exact hbound
-              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
              rw [hidx, hl] at heq
              simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
@@ -595,7 +595,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
              have idx_in_bounds2 : idx < f.clauses.size := by
                conv => rhs; rw [Array.size_mk]
                exact hbound
-              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
              rw [hidx] at heq
              simp only [Option.some.injEq] at heq
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -468,10 +468,10 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
  rcases List.get_of_mem h with ⟨j, h'⟩
  have j_in_bounds : j < ratHints.size := by
    have j_property := j.2
-    simp only [Array.toList_map, List.length_map] at j_property
+    simp only [Array.map_toList, List.length_map] at j_property
    dsimp at *
    omega
-  simp only [List.get_eq_getElem, Array.toList_map, Array.length_toList, List.getElem_map] at h'
+  simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
  rw [← Array.getElem_eq_getElem_toList] at h'
  rw [← Array.getElem_eq_getElem_toList] at c'_in_f
  exists ⟨j.1, j_in_bounds⟩
--- a/tests/compiler/float.lean
+++ b/tests/compiler/float.lean
@@ -19,29 +19,12 @@ def tst1 : IO Unit := do
  IO.println (0 / 0 : Float).toUInt16
  IO.println (0 / 0 : Float).toUInt32
  IO.println (0 / 0 : Float).toUInt64
-  IO.println (0 / 0 : Float).toUSize
-
  IO.println (-1 : Float).toUInt8
  IO.println (256 : Float).toUInt8
  IO.println (1 / 0 : Float).toUInt8
-
-  IO.println (-1 : Float).toUInt16
-  IO.println (2^16 : Float).toUInt16
-  IO.println (1 / 0 : Float).toUInt16
-
-  IO.println (-1 : Float).toUInt32
-  IO.println (2^32 : Float).toUInt32
-  IO.println (1 / 0 : Float).toUInt32
-
  IO.println (-1 : Float).toUInt64
  IO.println (2^64 : Float).toUInt64
  IO.println (1 / 0 : Float).toUInt64
-
-  let platBits := USize.size.log2.toFloat
-  IO.println (-1 : Float).toUSize
-  IO.println ((2^platBits).toUSize.toNat == (USize.size - 1))
-  IO.println ((1 / 0 : Float).toUSize.toNat == (USize.size - 1))
-
  IO.println (let x : Float := 1.4; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
  IO.println (let x : Float := 0 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
  IO.println (let x : Float := -0 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
--- a/tests/compiler/float.lean.expected.out
+++ b/tests/compiler/float.lean.expected.out
@@ -18,21 +18,11 @@ true
 0
 0
 0
-0
 255
 255
 0
-65535
-65535
-0
-4294967295
-4294967295
-0
 18446744073709551615
 18446744073709551615
-0
-true
-true
 (1.400000, (false, (false, (true, (0.700000, 1)))))
 (NaN, (true, (false, (false, (NaN, 0)))))
 (NaN, (true, (false, (false, (NaN, 0)))))
--- a/tests/lean/run/2710.lean
+++ b/tests/lean/run/2710.lean
@@ -1,8 +0,0 @@
-/-!
-# Structure field default values can be noncomputable
-/
-
-noncomputable def ohno := 1
-
-structure OhNo where
-  x := ohno
--- a/tests/lean/run/5424.lean
+++ b/tests/lean/run/5424.lean
@@ -1,21 +0,0 @@
-/-!
-# Long runs of identifiers should include line breaks
-/
-
-set_option linter.unusedVariables false
-
-def foo (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20
-         a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 a32 a33 a34 a35 a36 a37 a38 a39 a40
-         a41 a42 a43 a44 a45 a46 a47 a48 a49 a50 a51 a52 a53 a54 a55 a56 a57 a58 a59 a60
-         a61 a62 a63 a64 a65 a66 a67 a68 a69 a70 a71 a72 a73 a74 a75 a76 a77 a78 a79 a80
-         a81 a82 a83 a84 a85 a86 a87 a88 a89 a90 a91 a92 a93 a94 a95 a96 a97 a98 a99 : Nat) : Nat := 0
-
-/--
-info: foo
-  (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31
-    a32 a33 a34 a35 a36 a37 a38 a39 a40 a41 a42 a43 a44 a45 a46 a47 a48 a49 a50 a51 a52 a53 a54 a55 a56 a57 a58 a59 a60
-    a61 a62 a63 a64 a65 a66 a67 a68 a69 a70 a71 a72 a73 a74 a75 a76 a77 a78 a79 a80 a81 a82 a83 a84 a85 a86 a87 a88 a89
-    a90 a91 a92 a93 a94 a95 a96 a97 a98 a99 : Nat) :
-  Nat
-/
-#guard_msgs(whitespace := exact) in #check foo
--- a/tests/lean/run/eraseReps.lean
+++ b/tests/lean/run/eraseReps.lean
@@ -1,2 +0,0 @@
-example : Array.eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5] := rfl
-example : List.eraseReps   [1, 3, 2, 2, 2, 3, 5] =  [1, 3, 2, 3, 5] := rfl
--- a/tests/lean/run/list_simp.lean
+++ b/tests/lean/run/list_simp.lean
@@ -336,21 +336,21 @@ variable (h : n ≤ m) in
 -- unzip
 #check_simp unzip (replicate n (x, y)) ~> (replicate n x, replicate n y)

-- min?
+-- minimum?

 -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma
-#check_simp (replicate (n+1) 7).min? ~> some 7
+#check_simp (replicate (n+1) 7).minimum? ~> some 7

 variable (h : 0 < n) in
-#check_tactic (replicate n 7).min? ~> some 7 by simp [h]
+#check_tactic (replicate n 7).minimum? ~> some 7 by simp [h]

-- max?
+-- maximum?

 -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma
-#check_simp (replicate (n+1) 7).max? ~> some 7
+#check_simp (replicate (n+1) 7).maximum? ~> some 7

 variable (h : 0 < n) in
-#check_tactic (replicate n 7).max? ~> some 7 by simp [h]
+#check_tactic (replicate n 7).maximum? ~> some 7 by simp [h]

 end

@@ -456,9 +456,9 @@ end Pairwise

 /-! ### enumFrom -/

-/-! ### min? -/
+/-! ### minimum? -/

-/-! ### max? -/
+/-! ### maximum? -/

 /-! ## Monadic operations -/

--- a/tests/lean/run/omega.lean
+++ b/tests/lean/run/omega.lean
@@ -458,14 +458,6 @@ example (a : Nat) :
    (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by
  omega

-/-! ### Int.toNat -/
-
-example (z : Int) : z.toNat = 0 ↔ z ≤ 0 := by
-  omega
-
-example (z : Int) (a : Fin z.toNat) (h : 0 ≤ z) : ↑↑a ≤ z := by
-  omega
-
 /-! ### BitVec -/
 open BitVec

--- a/tests/lean/run/simpHigherOrder.lean
+++ b/tests/lean/run/simpHigherOrder.lean
@@ -1,69 +0,0 @@
-/-!
-This test checks that simp is able to instantiate the parameter `g` below. It does not
-appear on the lhs of the rule, but solving `hf` fully determines it.
-/
-
-theorem List.foldl_subtype (p : α → Prop) (l : List (Subtype p)) (f : β → Subtype p → β)
-  (g : β → α → β) (b : β)
-  (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
-    l.foldl f b = (l.map (·.val)).foldl g b := by
-  induction l generalizing b with
-  | nil => simp
-  | cons a l ih => simp [hf, ih]
-
-example (l : List Nat)  :
-  l.attach.foldl (fun acc t => max acc (t.val)) 0 = l.foldl (fun acc t => max acc t) 0 := by
-  simp [List.foldl_subtype]
-
-example (l : List Nat)  :
-  l.attach.foldl (fun acc ⟨t, _⟩ => max acc t) 0 = l.foldl (fun acc t => max acc t) 0 := by
-  simp [List.foldl_subtype]
-
-
-theorem foldr_to_sum (l : List Nat) (f : Nat → Nat → Nat) (g : Nat → Nat)
-  (h : ∀ acc x, f x acc = g x + acc) :
-  l.foldr f 0 = Nat.sum (l.map g) := by
-  rw [Nat.sum, List.foldr_map]
-  congr
-  funext x acc
-  apply h
-
-- this works:
-example (l : List Nat) :
-  l.foldr (fun x a => x*x + a) 0 = Nat.sum (l.map (fun x => x * x)) := by
-  simp [foldr_to_sum]
-
-- this does not, so such a pattern is still quite fragile
-
-/-- error: simp made no progress -/
-#guard_msgs in
-example (l : List Nat) :
-  l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
-  simp [foldr_to_sum]
-
-- but with stronger simp normal forms, it would work:
-
-@[simp]
-theorem add_eq_add_cancel (a x y : Nat) : (a + x = y + a) ↔  (x = y) := by omega
-
-example (l : List Nat) :
-  l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
-  simp [foldr_to_sum]
-
-
-- An example with zipWith
-
-theorem zipWith_ignores_right
-  (l₁ : List α) (l₂ : List β) (f : α → β → γ) (g : α → γ)
-  (h : ∀ a b, f a b = g a) :
-  List.zipWith f l₁ l₂ = List.map g (l₁.take l₂.length) := by
-  induction l₁ generalizing l₂ with
-  | nil => simp
-  | cons x xs ih =>
-    cases l₂
-    · simp
-    · simp [List.zipWith, h, ih]
-
-example (l₁ l₂ : List Nat) (hlen: l₁.length = l₂.length):
-  List.zipWith (fun x y => x*x) l₁ l₂ = l₁.map (fun x => x * x) := by
-  simp only [zipWith_ignores_right, hlen.symm, List.take_length]