chore: reduce use of deprecated lemmas in Array

Trivial to add and works nicely.

src/Init/Data/Array/Basic.lean

@@ -810,11 +810,27 @@ 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 =>
@@ -832,6 +848,8 @@ 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

src/Init/Data/Array/Lemmas.lean

@@ -424,12 +424,18 @@ 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]
 
-@[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (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? ..
 
@@ -443,7 +449,7 @@ theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD
   simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_get?]
+  simp [back?, getElem?_eq_toList_getElem?]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
@@ -602,12 +608,11 @@ abbrev data_range := @toList_range
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
   simp [getElem_eq_getElem_toList]
 
-set_option linter.deprecated false in
 @[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.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
+      (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
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
     · match j with | j+1 => ?_
       simp only [Nat.add_sub_cancel]
@@ -615,34 +620,34 @@ set_option linter.deprecated false in
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
       · intro k
-        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?]
+        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?]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_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.get?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_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.get?_reverse' _ _ h).symm
+        exact (List.getElem?_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_get? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    refine List.ext_getElem? <| 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.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.toList.length_reverse ▸ ‹_›)]
+      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
 
 /-! ### foldl / foldr -/
 

src/Init/Data/Array/QSort.lean

@@ -5,6 +5,7 @@ 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
@@ -44,4 +45,11 @@ 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

src/Init/Data/BitVec/Bitblast.lean

@@ -799,7 +799,6 @@ 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

src/Init/Data/Float.lean

@@ -72,21 +72,35 @@ 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 positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt8, returns 0. -/
+/-- 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).
+-/
 @[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8
-/-- 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. -/
+/-- 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).
+-/
 @[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16
-/-- 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. -/
+/-- 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).
+-/
 @[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32
-/-- 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. -/
+/-- 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).
+-/
 @[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64
-/-- 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. -/
+/-- 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).
+-/
 @[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize
 
 @[extern "lean_float_isnan"] opaque Float.isNaN : Float → Bool

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: `minimum?` and `maximum?`.
+* Minima and maxima: `min?` and `max?`.
 * Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
   `removeAll`
   (currently these functions are mostly only used in meta code,
@@ -1464,30 +1464,34 @@ def enum : List α → List (Nat × α) := enumFrom 0
 
 /-! ## Minima and maxima -/
 
-/-! ### minimum? -/
+/-! ### min? -/
 
 /--
 Returns the smallest element of the list, if it is not empty.
-* `[].minimum? = none`
-* `[4].minimum? = some 4`
-* `[1, 4, 2, 10, 6].minimum? = some 1`
+* `[].min? = none`
+* `[4].min? = some 4`
+* `[1, 4, 2, 10, 6].min? = some 1`
 -/
-def minimum? [Min α] : List α → Option α
+def min? [Min α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 
-/-! ### maximum? -/
+@[inherit_doc min?, deprecated min? (since := "2024-09-29")] abbrev minimum? := @min?
+
+/-! ### max? -/
 
 /--
 Returns the largest element of the list, if it is not empty.
-* `[].maximum? = none`
-* `[4].maximum? = some 4`
-* `[1, 4, 2, 10, 6].maximum? = some 10`
+* `[].max? = none`
+* `[4].max? = some 4`
+* `[1, 4, 2, 10, 6].max? = some 10`
 -/
-def maximum? [Max α] : List α → Option α
+def max? [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,

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`,
-`minimum?`, `maximum?`, and `removeAll`.
+`min?`, `max?`, 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`.

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.minimum?` and `List.maximum?`.
+* `Init.Data.List.MinMax` for lemmas about `List.min?` and `List.max?`.
 * `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,6 +203,9 @@ 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
@@ -489,7 +492,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 _⟩
 
-theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
+@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
@@ -878,6 +881,20 @@ 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]
@@ -1004,7 +1021,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]
 
-theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
+@[simp] 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)
@@ -1102,7 +1119,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
 
-theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
+@[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
   | [], h => absurd rfl h
   | _::_, _ => .head ..
 
@@ -2392,6 +2409,10 @@ 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 :=

src/Init/Data/List/MinMax.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.List.Lemmas
 
 /-!
-# Lemmas about `List.minimum?` and `List.maximum?.
+# Lemmas about `List.min?` and `List.max?.
 -/
 
 namespace List
@@ -16,24 +16,24 @@ open Nat
 
 /-! ## Minima and maxima -/
 
-/-! ### minimum? -/
+/-! ### min? -/
 
-@[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl
+@[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
 
--- We don't put `@[simp]` on `minimum?_cons`,
+-- We don't put `@[simp]` on `min?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem minimum?_cons [Min α] {xs : List α} : (x :: xs).minimum? = foldl min x xs := rfl
+theorem min?_cons [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
 
-@[simp] theorem minimum?_eq_none_iff {xs : List α} [Min α] : xs.minimum? = none ↔ xs = [] := by
-  cases xs <;> simp [minimum?]
+@[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = [] := by
+  cases xs <;> simp [min?]
 
-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
+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
   intro xs
   match xs with
   | nil => simp
   | x :: xs =>
-    simp only [minimum?_cons, Option.some.injEq, List.mem_cons]
+    simp only [min?_cons, Option.some.injEq, List.mem_cons]
     intro eq
     induction xs generalizing x with
     | nil =>
@@ -49,12 +49,12 @@ theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b
 
 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
 
-theorem le_minimum?_iff [Min α] [LE α]
+theorem le_min?_iff [Min α] [LE α]
     (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
-    {xs : List α} → xs.minimum? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
+    {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
   | nil => by simp
   | cons x xs => by
-    rw [minimum?]
+    rw [min?]
     intro eq y
     simp only [Option.some.injEq] at eq
     induction xs generalizing x with
@@ -67,46 +67,46 @@ theorem le_minimum?_iff [Min α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem min?_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.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 _)⟩, ?_⟩
+    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 _)⟩, ?_⟩
   intro ⟨h₁, h₂⟩
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
     exact congrArg some <| anti.1
-      ((le_minimum?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
-      (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
+      ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))
 
-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
+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
   induction n with
   | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, minimum?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons]
 
-@[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]
+@[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]
 
-/-! ### maximum? -/
+/-! ### max? -/
 
-@[simp] theorem maximum?_nil [Max α] : ([] : List α).maximum? = none := rfl
+@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
 
--- We don't put `@[simp]` on `maximum?_cons`,
+-- We don't put `@[simp]` on `max?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem maximum?_cons [Max α] {xs : List α} : (x :: xs).maximum? = foldl max x xs := rfl
+theorem max?_cons [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
 
-@[simp] theorem maximum?_eq_none_iff {xs : List α} [Max α] : xs.maximum? = none ↔ xs = [] := by
-  cases xs <;> simp [maximum?]
+@[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = [] := by
+  cases xs <;> simp [max?]
 
-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
+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
   | nil => by simp
   | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩
+    rw [max?]; rintro ⟨⟩
     induction xs generalizing x with simp at *
     | cons y xs ih =>
       rcases ih (max x y) with h | h <;> simp [h]
@@ -114,40 +114,57 @@ theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b
 
 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
 
-theorem maximum?_le_iff [Max α] [LE α]
+theorem max?_le_iff [Max α] [LE α]
     (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
-    {xs : List α} → xs.maximum? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
+    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
   | nil => by simp
   | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩ y
+    rw [max?]; 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 maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem max?_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.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 _)⟩, ?_⟩
+    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 _)⟩, ?_⟩
   intro ⟨h₁, h₂⟩
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
     exact congrArg some <| anti.1
-      (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl))
-      ((maximum?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
+      ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
 
-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
+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
   induction n with
   | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, maximum?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons]
 
-@[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]
+@[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
 
 end List

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⟩
 
-/-! ### minimum? -/
+/-! ### min? -/
 
--- 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
+-- 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
     (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => by omega)
-    (le_min_iff := fun _ _ _ => by omega)
+    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
+    (le_min_iff := fun _ _ _ => Nat.le_min)
 
 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem minimum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).minimum? = some (match l.minimum? with
+theorem min?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).min? = some (match l.min? with
     | none => a
     | some m => min a m) := by
-  rw [minimum?_eq_some_iff']
+  rw [min?_eq_some_iff']
   split <;> rename_i h m
   · simp_all
-  · rw [minimum?_eq_some_iff'] at m
+  · rw [min?_eq_some_iff'] at m
     obtain ⟨m, le⟩ := m
     rw [Nat.min_def]
     constructor
@@ -122,11 +122,11 @@ theorem minimum?_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.minimum?.getD a) := by
+    l.foldl (init := a) min = min a (l.min?.getD a) := by
   cases l with
   | nil => simp [Std.IdempotentOp.idempotent]
   | cons b l =>
-    simp only [minimum?]
+    simp only [min?]
     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).minimum?.getD b) := by
+    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).min?.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 minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    l.minimum?.getD k ≤ a := by
+theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.min?.getD k ≤ a := by
   cases l with
   | nil => simp at h
   | cons b l =>
-    simp [minimum?_cons]
+    simp [min?_cons]
     simp at h
     rcases h with (rfl | h)
     · exact foldl_min_le
@@ -166,26 +166,26 @@ theorem minimum?_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
 
-/-! ### maximum? -/
+/-! ### max? -/
 
--- 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
+-- 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
     (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => by omega)
-    (max_le_iff := fun _ _ _ => by omega)
+    (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp)
+    (max_le_iff := fun _ _ _ => Nat.max_le)
 
 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem maximum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).maximum? = some (match l.maximum? with
+theorem max?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).max? = some (match l.max? with
     | none => a
     | some m => max a m) := by
-  rw [maximum?_eq_some_iff']
+  rw [max?_eq_some_iff']
   split <;> rename_i h m
   · simp_all
-  · rw [maximum?_eq_some_iff'] at m
+  · rw [max?_eq_some_iff'] at m
     obtain ⟨m, le⟩ := m
     rw [Nat.max_def]
     constructor
@@ -202,11 +202,11 @@ theorem maximum?_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.maximum?.getD a) := by
+    l.foldl (init := a) max = max a (l.max?.getD a) := by
   cases l with
   | nil => simp [Std.IdempotentOp.idempotent]
   | cons b l =>
-    simp only [maximum?]
+    simp only [max?]
     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).maximum?.getD b) := by
+    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).max?.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_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    a ≤ l.maximum?.getD k := by
+theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.max?.getD k := by
   cases l with
   | nil => simp at h
   | cons b l =>
-    simp [maximum?_cons]
+    simp [max?_cons]
     simp at h
     rcases h with (rfl | h)
     · exact le_foldl_max
@@ -246,4 +246,11 @@ theorem le_maximum?_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

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. -/
-theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
+@[simp] 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 [getElem_take' _ hi hj]
+  simp
 
 /-- 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. -/

src/Init/Data/List/Perm.lean

@@ -248,6 +248,10 @@ 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
@@ -264,6 +268,28 @@ 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))) :

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

@@ -277,6 +277,7 @@ 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]) =>

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

@@ -29,12 +29,14 @@ 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) |>.minimum? |>.getD 0
+def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.min? |>.getD 0
 
 -- 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
+-- 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
     (le_refl := Nat.le_refl)
     (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
     (le_min_iff := fun _ _ _ => Nat.le_min)
@@ -42,27 +44,27 @@ theorem minimum?_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, minimum?_eq_none_iff, minimum?_eq_some_iff',
+  simp [nonzeroMinimum, Option.getD_eq_iff, min?_eq_none_iff, min?_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) |>.minimum?) = m at *
+  generalize h : (xs.filter (· ≠ 0) |>.min?) = m at *
   match m, w with
-  | some (m+1), _ => simp_all [minimum?_eq_some_iff', mem_filter]
+  | some (m+1), _ => simp_all [min?_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) |>.minimum?) = some xs.nonzeroMinimum := by
+  have : (xs.filter (· ≠ 0) |>.min?) = some xs.nonzeroMinimum := by
     have w := nonzeroMinimum_pos m h
     dsimp [nonzeroMinimum] at *
-    generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m? at *
+    generalize h : (xs.filter (· ≠ 0) |>.min?) = m? at *
     match m?, w with
     | some m?, _ => rfl
-  rw [minimum?_eq_some_iff'] at this
+  rw [min?_eq_some_iff''] at this
   apply this.2
   simp [List.mem_filter]
   exact ⟨m, h⟩
@@ -142,4 +144,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 |>.maximum? |>.getD 0
+def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.max? |>.getD 0

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

@@ -573,15 +573,33 @@ 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 r.expr.isTrue then
+  if let some p ← dischargeRfl r.expr then
+    return some (← mkEqMPR (← r.getProof) p)
+  else if r.expr.isTrue then
     return some (← mkOfEqTrue (← r.getProof))
   else
     return none

src/Lean/PrettyPrinter/Formatter.lean

@@ -360,7 +360,8 @@ 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
-      push $ tk ++ " "
+      pushLine
+      push tk
       modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
   else
     -- already separated => use `tk` as is

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) |>.maximum?
+    results.map (·.1) |>.max?
   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) |>.maximum?
+  let maxPrio? := gs.map (·.priority) |>.max?
   gs.filter (some ·.priority == maxPrio?)
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool

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)) |>.maximum?
+def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.max?
 
 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.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
+  simp only [maxLiteral, List.max?_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.maximum?_eq_none_iff _ (c.map (·.1)) _
+    have h2 := not_congr <| @List.max?_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.maximum?_eq_none_iff, List.map_eq_nil_iff] at h
+  simp only [maxLiteral, List.max?_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 |>.maximum?
+  List.filterMap Clause.maxLiteral f |>.max?
 
 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.maximum?_eq_some_iff'] at h
+  simp [maxLiteral, List.max?_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.maximum?_eq_none_iff] at h
+  simp only [maxLiteral, List.max?_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

tests/compiler/float.lean

@@ -19,12 +19,29 @@ 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))

tests/compiler/float.lean.expected.out

@@ -18,11 +18,21 @@ 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)))))

tests/lean/run/5424.lean

@@ -0,0 +1,21 @@
+/-!
+# 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

tests/lean/run/eraseReps.lean

@@ -0,0 +1,2 @@
+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

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)
 
--- minimum?
+-- min?
 
 -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma
-#check_simp (replicate (n+1) 7).minimum? ~> some 7
+#check_simp (replicate (n+1) 7).min? ~> some 7
 
 variable (h : 0 < n) in
-#check_tactic (replicate n 7).minimum? ~> some 7 by simp [h]
+#check_tactic (replicate n 7).min? ~> some 7 by simp [h]
 
--- maximum?
+-- max?
 
 -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma
-#check_simp (replicate (n+1) 7).maximum? ~> some 7
+#check_simp (replicate (n+1) 7).max? ~> some 7
 
 variable (h : 0 < n) in
-#check_tactic (replicate n 7).maximum? ~> some 7 by simp [h]
+#check_tactic (replicate n 7).max? ~> some 7 by simp [h]
 
 end
 
@@ -456,9 +456,9 @@ end Pairwise
 
 /-! ### enumFrom -/
 
-/-! ### minimum? -/
+/-! ### min? -/
 
-/-! ### maximum? -/
+/-! ### max? -/
 
 /-! ## Monadic operations -/
 

tests/lean/run/omega.lean

@@ -458,6 +458,14 @@ 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
 

tests/lean/run/simpHigherOrder.lean

@@ -0,0 +1,69 @@
+/-!
+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]