chore: rename List.maximum? to max?

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`.

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/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/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/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 -/