remove deprecation

src/Init/Data/Array/BasicAux.lean

@@ -9,7 +9,7 @@ import Init.Data.Nat.Linear
 import Init.NotationExtra
 
 theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
-  simp [push] at h
+  simp only [push, mk.injEq] at h
   have ⟨h₁, h₂⟩ := List.of_concat_eq_concat h
   cases as; cases bs
   simp_all

src/Init/Data/Array/Lemmas.lean

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

src/Init/Data/Fin/Basic.lean

@@ -210,4 +210,7 @@ theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1
 
 theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := h
 
+theorem exists_iff {p : Fin n → Prop} : (Exists fun i => p i) ↔ Exists fun i => Exists fun h => p ⟨i, h⟩ :=
+  ⟨fun ⟨⟨i, hi⟩, hpi⟩ => ⟨i, hi, hpi⟩, fun ⟨i, hi, hpi⟩ => ⟨⟨i, hi⟩, hpi⟩⟩
+
 end Fin

src/Init/Data/Fin/Lemmas.lean

@@ -43,9 +43,6 @@ theorem ext_iff {a b : Fin n} : a = b ↔ a.1 = b.1 := val_inj.symm
 
 theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
 
-theorem exists_iff {p : Fin n → Prop} : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ :=
-  ⟨fun ⟨⟨i, hi⟩, hpi⟩ => ⟨i, hi, hpi⟩, fun ⟨i, hi, hpi⟩ => ⟨⟨i, hi⟩, hpi⟩⟩
-
 theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩ :=
   ⟨fun h i hi => h ⟨i, hi⟩, fun h ⟨i, hi⟩ => h i hi⟩
 

src/Init/Data/List.lean

@@ -10,3 +10,4 @@ import Init.Data.List.Control
 import Init.Data.List.Lemmas
 import Init.Data.List.Impl
 import Init.Data.List.TakeDrop
+import Init.Data.List.Notation

src/Init/Data/List/BasicAux.lean

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Linear
-import Init.Ext
 
 universe u
 
@@ -13,6 +12,10 @@ namespace List
 /-! The following functions can't be defined at `Init.Data.List.Basic`, because they depend on `Init.Util`,
    and `Init.Util` depends on `Init.Data.List.Basic`. -/
 
+/-! ## Alternative getters -/
+
+/-! ### get! -/
+
 /--
 Returns the `i`-th element in the list (zero-based).
 
@@ -24,110 +27,12 @@ def get! [Inhabited α] : (as : List α) → (i : Nat) → α
   | _::as, n+1 => get! as n
   | _,     _   => panic! "invalid index"
 
-/--
-Returns the `i`-th element in the list (zero-based).
+theorem get!_nil [Inhabited α] (n : Nat) : [].get! n = (default : α) := rfl
+theorem get!_cons_succ [Inhabited α] (l : List α) (a : α) (n : Nat) :
+    (a::l).get! (n+1) = get! l n := rfl
+theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
 
-If the index is out of bounds (`i ≥ as.length`), this function returns `none`.
-Also see `get`, `getD` and `get!`.
--/
-def get? : (as : List α) → (i : Nat) → Option α
-  | a::_,  0   => some a
-  | _::as, n+1 => get? as n
-  | _,     _   => none
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function returns `fallback`.
-See also `get?` and `get!`.
--/
-def getD (as : List α) (i : Nat) (fallback : α) : α :=
-  (as.get? i).getD fallback
-
-theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
-  | [], [], _ => rfl
-  | a :: l₁, [], h => nomatch h 0
-  | [], a' :: l₂, h => nomatch h 0
-  | a :: l₁, a' :: l₂, h => by
-    have h0 : some a = some a' := h 0
-    injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
-
-@[deprecated (since := "2024-06-07")] abbrev ext := @ext_get?
-
-/--
-Returns the first element in the list.
-
-If the list is empty, this function panics when executed, and returns `default`.
-See `head` and `headD` for safer alternatives.
--/
-def head! [Inhabited α] : List α → α
-  | []   => panic! "empty list"
-  | a::_ => a
-
-/--
-Returns the first element in the list.
-
-If the list is empty, this function returns `none`.
-Also see `headD` and `head!`.
--/
-def head? : List α → Option α
-  | []   => none
-  | a::_ => some a
-
-/--
-Returns the first element in the list.
-
-If the list is empty, this function returns `fallback`.
-Also see `head?` and `head!`.
--/
-def headD : (as : List α) → (fallback : α) → α
-  | [],   fallback => fallback
-  | a::_, _  => a
-
-/--
-Returns the first element of a non-empty list.
--/
-def head : (as : List α) → as ≠ [] → α
-  | a::_, _ => a
-
-/--
-Drops the first element of the list.
-
-If the list is empty, this function panics when executed, and returns the empty list.
-See `tail` and `tailD` for safer alternatives.
--/
-def tail! : List α → List α
-  | []    => panic! "empty list"
-  | _::as => as
-
-/--
-Drops the first element of the list.
-
-If the list is empty, this function returns `none`.
-Also see `tailD` and `tail!`.
--/
-def tail? : List α → Option (List α)
-  | []    => none
-  | _::as => some as
-
-/--
-Drops the first element of the list.
-
-If the list is empty, this function returns `fallback`.
-Also see `head?` and `head!`.
--/
-def tailD (list fallback : List α) : List α :=
-  match list with
-  | [] => fallback
-  | _ :: tl => tl
-
-/--
-Returns the last element of a non-empty list.
--/
-def getLast : ∀ (as : List α), as ≠ [] → α
-  | [],       h => absurd rfl h
-  | [a],      _ => a
-  | _::b::as, _ => getLast (b::as) (fun h => List.noConfusion h)
+/-! ### getLast! -/
 
 /--
 Returns the last element in the list.
@@ -139,59 +44,116 @@ def getLast! [Inhabited α] : List α → α
   | []    => panic! "empty list"
   | a::as => getLast (a::as) (fun h => List.noConfusion h)
 
-/--
-Returns the last element in the list.
+/-! ## Head and tail -/
 
-If the list is empty, this function returns `none`.
-Also see `getLastD` and `getLast!`.
--/
-def getLast? : List α → Option α
-  | []    => none
-  | a::as => some (getLast (a::as) (fun h => List.noConfusion h))
+/-! ### head! -/
 
 /--
-Returns the last element in the list.
+Returns the first element in the list.
 
-If the list is empty, this function returns `fallback`.
-Also see `getLast?` and `getLast!`.
+If the list is empty, this function panics when executed, and returns `default`.
+See `head` and `headD` for safer alternatives.
 -/
-def getLastD : (as : List α) → (fallback : α) → α
-  | [],   a₀ => a₀
-  | a::as, _ => getLast (a::as) (fun h => List.noConfusion h)
+def head! [Inhabited α] : List α → α
+  | []   => panic! "empty list"
+  | a::_ => a
+
+/-! ### tail! -/
 
 /--
-`O(n)`. Rotates the elements of `xs` to the left such that the element at
-`xs[i]` rotates to `xs[(i - n) % l.length]`.
-* `rotateLeft [1, 2, 3, 4, 5] 3 = [4, 5, 1, 2, 3]`
-* `rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
-* `rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]`
+Drops the first element of the list.
+
+If the list is empty, this function panics when executed, and returns the empty list.
+See `tail` and `tailD` for safer alternatives.
 -/
-def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
-  let len := xs.length
-  if len ≤ 1 then
-    xs
-  else
-    let n := n % len
-    let b := xs.take n
-    let e := xs.drop n
-    e ++ b
+def tail! : List α → List α
+  | []    => panic! "empty list"
+  | _::as => as
+
+@[simp] theorem tail!_cons : @tail! α (a::l) = l := rfl
+
+/-! ### partitionM -/
 
 /--
-`O(n)`. Rotates the elements of `xs` to the right such that the element at
-`xs[i]` rotates to `xs[(i + n) % l.length]`.
-* `rotateRight [1, 2, 3, 4, 5] 3 = [3, 4, 5, 1, 2]`
-* `rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
-* `rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]`
+Monadic generalization of `List.partition`.
+
+This uses `Array.toList` and which isn't imported by `Init.Data.List.Basic` or `Init.Data.List.Control`.
+```
+def posOrNeg (x : Int) : Except String Bool :=
+  if x > 0 then pure true
+  else if x < 0 then pure false
+  else throw "Zero is not positive or negative"
+
+partitionM posOrNeg [-1, 2, 3] = Except.ok ([2, 3], [-1])
+partitionM posOrNeg [0, 2, 3] = Except.error "Zero is not positive or negative"
+```
 -/
-def rotateRight (xs : List α) (n : Nat := 1) : List α :=
-  let len := xs.length
-  if len ≤ 1 then
-    xs
-  else
-    let n := len - n % len
-    let b := xs.take n
-    let e := xs.drop n
-    e ++ b
+@[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α) :=
+  go l #[] #[]
+where
+  /-- Auxiliary for `partitionM`:
+  `partitionM.go p l acc₁ acc₂` returns `(acc₁.toList ++ left, acc₂.toList ++ right)`
+  if `partitionM p l` returns `(left, right)`. -/
+  @[specialize] go : List α → Array α → Array α → m (List α × List α)
+  | [], acc₁, acc₂ => pure (acc₁.toList, acc₂.toList)
+  | x :: xs, acc₁, acc₂ => do
+    if ← p x then
+      go xs (acc₁.push x) acc₂
+    else
+      go xs acc₁ (acc₂.push x)
+
+/-! ### partitionMap -/
+
+/--
+Given a function `f : α → β ⊕ γ`, `partitionMap f l` maps the list by `f`
+whilst partitioning the result into a pair of lists, `List β × List γ`,
+partitioning the `.inl _` into the left list, and the `.inr _` into the right List.
+```
+partitionMap (id : Nat ⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
+```
+-/
+@[inline] def partitionMap (f : α → β ⊕ γ) (l : List α) : List β × List γ := go l #[] #[] where
+  /-- Auxiliary for `partitionMap`:
+  `partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)`
+  if `partitionMap f l = (left, right)`. -/
+  @[specialize] go : List α → Array β → Array γ → List β × List γ
+  | [], acc₁, acc₂ => (acc₁.toList, acc₂.toList)
+  | x :: xs, acc₁, acc₂ =>
+    match f x with
+    | .inl a => go xs (acc₁.push a) acc₂
+    | .inr b => go xs acc₁ (acc₂.push b)
+
+/-! ### mapMono
+
+This is a performance optimization for `List.mapM` that avoids allocating a new list when the result of each `f a` is a pointer equal value `a`.
+
+For verification purposes, `List.mapMono = List.map`.
+-/
+
+@[specialize] private unsafe def mapMonoMImp [Monad m] (as : List α) (f : α → m α) : m (List α) := do
+  match as with
+  | [] => return as
+  | b :: bs =>
+    let b'  ← f b
+    let bs' ← mapMonoMImp bs f
+    if ptrEq b' b && ptrEq bs' bs then
+      return as
+    else
+      return b' :: bs'
+
+/--
+Monomorphic `List.mapM`. The internal implementation uses pointer equality, and does not allocate a new list
+if the result of each `f a` is a pointer equal value `a`.
+-/
+@[implemented_by mapMonoMImp] def mapMonoM [Monad m] (as : List α) (f : α → m α) : m (List α) :=
+  match as with
+  | [] => return []
+  | a :: as => return (← f a) :: (← mapMonoM as f)
+
+def mapMono (as : List α) (f : α → α) : List α :=
+  Id.run <| as.mapMonoM f
+
+/-! ## Additional lemmas required for bootstrapping `Array`. -/
 
 theorem getElem_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs)[i] = as[i] := by
   induction as generalizing i with
@@ -287,74 +249,4 @@ theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as
 instance [LT α] [Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm h₁ h₂ := le_antisymm h₁ h₂
 
-@[specialize] private unsafe def mapMonoMImp [Monad m] (as : List α) (f : α → m α) : m (List α) := do
-  match as with
-  | [] => return as
-  | b :: bs =>
-    let b'  ← f b
-    let bs' ← mapMonoMImp bs f
-    if ptrEq b' b && ptrEq bs' bs then
-      return as
-    else
-      return b' :: bs'
-
-/--
-Monomorphic `List.mapM`. The internal implementation uses pointer equality, and does not allocate a new list
-if the result of each `f a` is a pointer equal value `a`.
--/
-@[implemented_by mapMonoMImp] def mapMonoM [Monad m] (as : List α) (f : α → m α) : m (List α) :=
-  match as with
-  | [] => return []
-  | a :: as => return (← f a) :: (← mapMonoM as f)
-
-def mapMono (as : List α) (f : α → α) : List α :=
-  Id.run <| as.mapMonoM f
-
-/--
-Monadic generalization of `List.partition`.
-
-This uses `Array.toList` and which isn't imported by `Init.Data.List.Basic`.
-```
-def posOrNeg (x : Int) : Except String Bool :=
-  if x > 0 then pure true
-  else if x < 0 then pure false
-  else throw "Zero is not positive or negative"
-
-partitionM posOrNeg [-1, 2, 3] = Except.ok ([2, 3], [-1])
-partitionM posOrNeg [0, 2, 3] = Except.error "Zero is not positive or negative"
-```
--/
-@[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α) :=
-  go l #[] #[]
-where
-  /-- Auxiliary for `partitionM`:
-  `partitionM.go p l acc₁ acc₂` returns `(acc₁.toList ++ left, acc₂.toList ++ right)`
-  if `partitionM p l` returns `(left, right)`. -/
-  @[specialize] go : List α → Array α → Array α → m (List α × List α)
-  | [], acc₁, acc₂ => pure (acc₁.toList, acc₂.toList)
-  | x :: xs, acc₁, acc₂ => do
-    if ← p x then
-      go xs (acc₁.push x) acc₂
-    else
-      go xs acc₁ (acc₂.push x)
-
-/--
-Given a function `f : α → β ⊕ γ`, `partitionMap f l` maps the list by `f`
-whilst partitioning the result it into a pair of lists, `List β × List γ`,
-partitioning the `.inl _` into the left list, and the `.inr _` into the right List.
-```
-partitionMap (id : Nat ⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
-```
--/
-@[inline] def partitionMap (f : α → β ⊕ γ) (l : List α) : List β × List γ := go l #[] #[] where
-  /-- Auxiliary for `partitionMap`:
-  `partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)`
-  if `partitionMap f l = (left, right)`. -/
-  @[specialize] go : List α → Array β → Array γ → List β × List γ
-  | [], acc₁, acc₂ => (acc₁.toList, acc₂.toList)
-  | x :: xs, acc₁, acc₂ =>
-    match f x with
-    | .inl a => go xs (acc₁.push a) acc₂
-    | .inr b => go xs acc₁ (acc₂.push b)
-
 end List

src/Init/Data/List/Control.lean

@@ -151,6 +151,11 @@ protected def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w
     let s' ← f s a
     List.foldlM f s' as
 
+@[simp] theorem foldlM_nil [Monad m] (f : β → α → m β) (b) : [].foldlM f b = pure b := rfl
+@[simp] theorem foldlM_cons [Monad m] (f : β → α → m β) (b) (a) (l : List α) :
+    (a :: l).foldlM f b = f b a >>= l.foldlM f := by
+  simp [List.foldlM]
+
 /--
 Folds a monadic function over a list from right to left:
 ```
@@ -165,6 +170,8 @@ foldrM f x₀ [a, b, c] = do
 def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m s :=
   l.reverse.foldlM (fun s a => f a s) init
 
+@[simp] theorem foldrM_nil [Monad m] (f : α → β → m β) (b) : [].foldrM f b = pure b := rfl
+
 /--
 Maps `f` over the list and collects the results with `<|>`.
 ```

src/Init/Data/List/Impl.lean

@@ -16,7 +16,44 @@ so these are in a separate file to minimize imports.
 
 namespace List
 
-/-- Tail recursive version of `erase`. -/
+/-! ## Basic `List` operations.
+
+The following operations are already tail-recursive, and do not need `@[csimp]` replacements:
+`get`, `foldl`, `beq`, `isEqv`, `reverse`, `elem` (and hence `contains`), `drop`, `dropWhile`,
+`partition`, `isPrefixOf`, `isPrefixOf?`, `find?`, `findSome?`, `lookup`, `any` (and hence `or`),
+`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `groupBy`.
+
+The following operations are still missing `@[csimp]` replacements:
+`concat`, `zipWithAll`.
+
+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`.
+
+The following operations are given `@[csimp]` replacements below:
+`length`, `set`, `map`, `filter`, `filterMap`, `foldr`, `append`, `bind`, `join`, `replicate`,
+`take`, `takeWhile`, `dropLast`, `replace`, `erase`, `eraseIdx`, `zipWith`, `unzip`, `iota`,
+`enumFrom`, `intersperse`, and `intercalate`.
+
+-/
+
+/-! ### length -/
+
+theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n := by
+  induction as generalizing n with
+  | nil  => simp [length, lengthTRAux]
+  | cons a as ih =>
+    simp [length, lengthTRAux, ← ih, Nat.succ_add]
+    rfl
+
+@[csimp] theorem length_eq_lengthTR : @List.length = @List.lengthTR := by
+  apply funext; intro α; apply funext; intro as
+  simp [lengthTR, ← length_add_eq_lengthTRAux]
+
+/-! ### set -/
+
+/-- Tail recursive version of `List.set`. -/
 @[inline] def setTR (l : List α) (n : Nat) (a : α) : List α := go l n #[] where
   /-- Auxiliary for `setTR`: `setTR.go l a xs n acc = acc.toList ++ set xs a`,
   unless `n ≥ l.length` in which case it returns `l` -/
@@ -31,10 +68,214 @@ namespace List
     setTR.go l a xs n acc = acc.data ++ xs.set n a
   | [], _ => fun h => by simp [setTR.go, set, h]
   | x::xs, 0 => by simp [setTR.go, set]
-  | x::xs, n+1 => fun h => by simp [setTR.go, set]; rw [go _ xs]; {simp}; simp [h]
+  | x::xs, n+1 => fun h => by simp only [setTR.go, set]; rw [go _ xs] <;> simp [h]
   exact (go #[] _ _ rfl).symm
 
-/-- Tail recursive version of `erase`. -/
+/-! ### map -/
+
+/-- Tail-recursive version of `List.map`. -/
+@[inline] def mapTR (f : α → β) (as : List α) : List β :=
+  loop as []
+where
+  @[specialize] loop : List α → List β → List β
+  | [],    bs => bs.reverse
+  | a::as, bs => loop as (f a :: bs)
+
+theorem mapTR_loop_eq (f : α → β) (as : List α) (bs : List β) :
+    mapTR.loop f as bs = bs.reverse ++ map f as := by
+  induction as generalizing bs with
+  | nil => simp [mapTR.loop, map]
+  | cons a as ih =>
+    simp only [mapTR.loop, map]
+    rw [ih (f a :: bs), reverse_cons, append_assoc]
+    rfl
+
+@[csimp] theorem map_eq_mapTR : @map = @mapTR :=
+  funext fun α => funext fun β => funext fun f => funext fun as => by
+    simp [mapTR, mapTR_loop_eq]
+
+/-! ### filter -/
+
+/-- Tail-recursive version of `List.filter`. -/
+@[inline] def filterTR (p : α → Bool) (as : List α) : List α :=
+  loop as []
+where
+  @[specialize] loop : List α → List α → List α
+  | [],    rs => rs.reverse
+  | a::as, rs => match p a with
+     | true  => loop as (a::rs)
+     | false => loop as rs
+
+theorem filterTR_loop_eq (p : α → Bool) (as bs : List α) :
+    filterTR.loop p as bs = bs.reverse ++ filter p as := by
+  induction as generalizing bs with
+  | nil => simp [filterTR.loop, filter]
+  | cons a as ih =>
+    simp only [filterTR.loop, filter]
+    split <;> simp_all
+
+@[csimp] theorem filter_eq_filterTR : @filter = @filterTR := by
+  apply funext; intro α; apply funext; intro p; apply funext; intro as
+  simp [filterTR, filterTR_loop_eq]
+
+/-! ### filterMap -/
+
+/-- Tail recursive version of `filterMap`. -/
+@[inline] def filterMapTR (f : α → Option β) (l : List α) : List β := go l #[] where
+  /-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | a::as, acc => match f a with
+    | none => go as acc
+    | some b => go as (acc.push b)
+
+@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
+  funext α β f l
+  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
+    | [], acc => by simp [filterMapTR.go, filterMap]
+    | a::as, acc => by
+      simp only [filterMapTR.go, go as, Array.push_data, append_assoc, singleton_append, filterMap]
+      split <;> simp [*]
+  exact (go l #[]).symm
+
+/-! ### foldr -/
+
+/-- Tail recursive version of `List.foldr`. -/
+@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
+
+@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
+  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
+
+/-! ### bind  -/
+
+/-- Tail recursive version of `List.bind`. -/
+@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
+  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | x::xs, acc => go xs (acc ++ f x)
+
+@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
+  funext α β as f
+  let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
+    | [], acc => by simp [bindTR.go, bind]
+    | x::xs, acc => by simp [bindTR.go, bind, go xs]
+  exact (go as #[]).symm
+
+/-! ### join -/
+
+/-- Tail recursive version of `List.join`. -/
+@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
+
+@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
+  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
+
+/-! ### replicate -/
+
+/-- Tail-recursive version of `List.replicate`. -/
+def replicateTR {α : Type u} (n : Nat) (a : α) : List α :=
+  let rec loop : Nat → List α → List α
+    | 0, as => as
+    | n+1, as => loop n (a::as)
+  loop n []
+
+theorem replicateTR_loop_replicate_eq (a : α) (m n : Nat) :
+  replicateTR.loop a n (replicate m a) = replicate (n + m) a := by
+  induction n generalizing m with simp [replicateTR.loop]
+  | succ n ih => simp [Nat.succ_add]; exact ih (m+1)
+
+theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc
+  | 0 => rfl
+  | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
+    replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl
+
+@[csimp] theorem replicate_eq_replicateTR : @List.replicate = @List.replicateTR := by
+  apply funext; intro α; apply funext; intro n; apply funext; intro a
+  exact (replicateTR_loop_replicate_eq _ 0 n).symm
+
+/-! ## Sublists -/
+
+/-! ### take -/
+
+/-- Tail recursive version of `List.take`. -/
+@[inline] def takeTR (n : Nat) (l : List α) : List α := go l n #[] where
+  /-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`,
+  unless `n ≥ xs.length` in which case it returns `l`. -/
+  @[specialize] go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::_, 0, acc => acc.toList
+  | a::as, n+1, acc => go as n (acc.push a)
+
+@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
+  funext α n l; simp [takeTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs generalizing n with intro acc
+  | nil => cases n <;> simp [take, takeTR.go]
+  | cons x xs IH =>
+    cases n with simp only [take, takeTR.go]
+    | zero => simp
+    | succ n => intro h; rw [IH] <;> simp_all
+
+/-! ### takeWhile -/
+
+/-- Tail recursive version of `List.takeWhile`. -/
+@[inline] def takeWhileTR (p : α → Bool) (l : List α) : List α := go l #[] where
+  /-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`,
+  unless no element satisfying `p` is found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif p a then go as (acc.push a) else acc.toList
+
+@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
+  funext α p l; simp [takeWhileTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [takeWhile, takeWhileTR.go]
+  | cons x xs IH =>
+    simp only [takeWhileTR.go, Array.toList_eq, takeWhile]
+    split
+    · intro h; rw [IH] <;> simp_all
+    · simp [*]
+
+/-! ### dropLast -/
+
+/-- Tail recursive version of `dropLast`. -/
+@[inline] def dropLastTR (l : List α) : List α := l.toArray.pop.toList
+
+@[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by
+  funext α l; simp [dropLastTR]
+
+/-! ## Manipulating elements -/
+
+/-! ### replace -/
+
+/-- Tail recursive version of `List.replace`. -/
+@[inline] def replaceTR [BEq α] (l : List α) (b c : α) : List α := go l #[] where
+  /-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`,
+  unless `b` is not found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
+
+@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
+  funext α _ l b c; simp [replaceTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [replace, replaceTR.go]
+  | cons x xs IH =>
+    simp only [replaceTR.go, Array.toListAppend_eq, replace]
+    split
+    · simp [*]
+    · intro h; rw [IH] <;> simp_all
+
+/-! ### erase -/
+
+/-- Tail recursive version of `List.erase`. -/
 @[inline] def eraseTR [BEq α] (l : List α) (a : α) : List α := go l #[] where
   /-- Auxiliary for `eraseTR`: `eraseTR.go l a xs acc = acc.toList ++ erase xs a`,
   unless `a` is not present in which case it returns `l` -/
@@ -49,11 +290,14 @@ namespace List
   intro xs; induction xs with intro acc h
   | nil => simp [List.erase, eraseTR.go, h]
   | cons x xs IH =>
-    simp [List.erase, eraseTR.go]
-    cases x == a <;> simp
-    · rw [IH]; simp; simp; exact h
+    simp only [eraseTR.go, Array.toListAppend_eq, List.erase]
+    cases x == a
+    · rw [IH] <;> simp_all
+    · simp
 
-/-- Tail recursive version of `eraseIdx`. -/
+/-! ### eraseIdx -/
+
+/-- Tail recursive version of `List.eraseIdx`. -/
 @[inline] def eraseIdxTR (l : List α) (n : Nat) : List α := go l n #[] where
   /-- Auxiliary for `eraseIdxTR`: `eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a`,
   unless `a` is not present in which case it returns `l` -/
@@ -72,109 +316,14 @@ namespace List
     match n with
     | 0 => simp [eraseIdx, eraseIdxTR.go]
     | n+1 =>
-      simp [eraseIdx, eraseIdxTR.go]
+      simp only [eraseIdxTR.go, eraseIdx]
       rw [IH]; simp; simp; exact h
 
-/-- Tail recursive version of `bind`. -/
-@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
-  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
-  @[specialize] go : List α → Array β → List β
-  | [], acc => acc.toList
-  | x::xs, acc => go xs (acc ++ f x)
+/-! ## Zippers -/
 
-@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
-  funext α β as f
-  let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
-    | [], acc => by simp [bindTR.go, bind]
-    | x::xs, acc => by simp [bindTR.go, bind, go xs]
-  exact (go as #[]).symm
+/-! ### zipWith -/
 
-/-- Tail recursive version of `join`. -/
-@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
-
-@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
-  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
-
-/-- Tail recursive version of `filterMap`. -/
-@[inline] def filterMapTR (f : α → Option β) (l : List α) : List β := go l #[] where
-  /-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l` -/
-  @[specialize] go : List α → Array β → List β
-  | [], acc => acc.toList
-  | a::as, acc => match f a with
-    | none => go as acc
-    | some b => go as (acc.push b)
-
-@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
-  funext α β f l
-  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
-    | [], acc => by simp [filterMapTR.go, filterMap]
-    | a::as, acc => by simp [filterMapTR.go, filterMap, go as]; split <;> simp [*]
-  exact (go l #[]).symm
-
-/-- Tail recursive version of `replace`. -/
-@[inline] def replaceTR [BEq α] (l : List α) (b c : α) : List α := go l #[] where
-  /-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`,
-  unless `b` is not found in `xs` in which case it returns `l`. -/
-  @[specialize] go : List α → Array α → List α
-  | [], _ => l
-  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
-
-@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
-  funext α _ l b c; simp [replaceTR]
-  suffices ∀ xs acc, l = acc.data ++ xs →
-      replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs with intro acc
-  | nil => simp [replace, replaceTR.go]
-  | cons x xs IH =>
-    simp [replace, replaceTR.go]; split <;> simp [*]
-    · intro h; rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `take`. -/
-@[inline] def takeTR (n : Nat) (l : List α) : List α := go l n #[] where
-  /-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`,
-  unless `n ≥ xs.length` in which case it returns `l`. -/
-  @[specialize] go : List α → Nat → Array α → List α
-  | [], _, _ => l
-  | _::_, 0, acc => acc.toList
-  | a::as, n+1, acc => go as n (acc.push a)
-
-@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
-  funext α n l; simp [takeTR]
-  suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs generalizing n with intro acc
-  | nil => cases n <;> simp [take, takeTR.go]
-  | cons x xs IH =>
-    cases n with simp [take, takeTR.go]
-    | succ n => intro h; rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `takeWhile`. -/
-@[inline] def takeWhileTR (p : α → Bool) (l : List α) : List α := go l #[] where
-  /-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`,
-  unless no element satisfying `p` is found in `xs` in which case it returns `l`. -/
-  @[specialize] go : List α → Array α → List α
-  | [], _ => l
-  | a::as, acc => bif p a then go as (acc.push a) else acc.toList
-
-@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
-  funext α p l; simp [takeWhileTR]
-  suffices ∀ xs acc, l = acc.data ++ xs →
-      takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs with intro acc
-  | nil => simp [takeWhile, takeWhileTR.go]
-  | cons x xs IH =>
-    simp [takeWhile, takeWhileTR.go]; split <;> simp [*]
-    · intro h; rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `foldr`. -/
-@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
-
-@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
-
-/-- Tail recursive version of `zipWith`. -/
+/-- Tail recursive version of `List.zipWith`. -/
 @[inline] def zipWithTR (f : α → β → γ) (as : List α) (bs : List β) : List γ := go as bs #[] where
   /-- Auxiliary for `zipWith`: `zipWith.go f as bs acc = acc.toList ++ zipWith f as bs` -/
   go : List α → List β → Array γ → List γ
@@ -188,14 +337,37 @@ namespace List
     | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
   exact (go as bs #[]).symm
 
-/-- Tail recursive version of `unzip`. -/
+/-! ### unzip -/
+
+/-- Tail recursive version of `List.unzip`. -/
 def unzipTR (l : List (α × β)) : List α × List β :=
   l.foldr (fun (a, b) (al, bl) => (a::al, b::bl)) ([], [])
 
 @[csimp] theorem unzip_eq_unzipTR : @unzip = @unzipTR := by
   funext α β l; simp [unzipTR]; induction l <;> simp [*]
 
-/-- Tail recursive version of `enumFrom`. -/
+/-! ## Ranges and enumeration -/
+
+/-! ### iota -/
+
+/-- Tail-recursive version of `List.iota`. -/
+def iotaTR (n : Nat) : List Nat :=
+  let rec go : Nat → List Nat → List Nat
+    | 0, r => r.reverse
+    | m@(n+1), r => go n (m::r)
+  go n []
+
+@[csimp]
+theorem iota_eq_iotaTR : @iota = @iotaTR :=
+  have aux (n : Nat) (r : List Nat) : iotaTR.go n r = r.reverse ++ iota n := by
+    induction n generalizing r with
+    | zero => simp [iota, iotaTR.go]
+    | succ n ih => simp [iota, iotaTR.go, ih, append_assoc]
+  funext fun n => by simp [iotaTR, aux]
+
+/-! ### enumFrom -/
+
+/-- Tail recursive version of `List.enumFrom`. -/
 def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
   let arr := l.toArray
   (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
@@ -211,18 +383,11 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
   rw [Array.foldr_eq_foldr_data]
   simp [go]
 
-theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc
-  | 0 => rfl
-  | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
-    replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl
+/-! ## Other list operations -/
 
-/-- Tail recursive version of `dropLast`. -/
-@[inline] def dropLastTR (l : List α) : List α := l.toArray.pop.toList
+/-! ### intersperse -/
 
-@[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by
-  funext α l; simp [dropLastTR]
-
-/-- Tail recursive version of `intersperse`. -/
+/-- Tail recursive version of `List.intersperse`. -/
 def intersperseTR (sep : α) : List α → List α
   | [] => []
   | [x] => [x]
@@ -234,7 +399,9 @@ def intersperseTR (sep : α) : List α → List α
   | [] | [_] => rfl
   | x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*]
 
-/-- Tail recursive version of `intercalate`. -/
+/-! ### intercalate -/
+
+/-- Tail recursive version of `List.intercalate`. -/
 def intercalateTR (sep : List α) : List (List α) → List α
   | [] => []
   | [x] => x

src/Init/Data/List/Notation.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import Init.Data.Nat.Div
+
+/-!
+# Notation for `List` literals.
+-/
+
+set_option linter.missingDocs true -- keep it documented
+open Decidable List
+
+/--
+The syntax `[a, b, c]` is shorthand for `a :: b :: c :: []`, or
+`List.cons a (List.cons b (List.cons c List.nil))`. It allows conveniently constructing
+list literals.
+
+For lists of length at least 64, an alternative desugaring strategy is used
+which uses let bindings as intermediates as in
+`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
+Note that this changes the order of evaluation, although it should not be observable
+unless you use side effecting operations like `dbg_trace`.
+-/
+syntax "[" withoutPosition(term,*,?) "]"  : term
+
+/--
+Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
+The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
+It uses binary partitioning to construct a tree of intermediate let bindings as in
+`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
+-/
+syntax "%[" withoutPosition(term,*,? " | " term) "]" : term
+
+namespace Lean
+
+macro_rules
+  | `([ $elems,* ]) => do
+    -- NOTE: we do not have `TSepArray.getElems` yet at this point
+    let rec expandListLit (i : Nat) (skip : Bool) (result : TSyntax `term) : MacroM Syntax := do
+      match i, skip with
+      | 0,   _     => pure result
+      | i+1, true  => expandListLit i false result
+      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
+    let size := elems.elemsAndSeps.size
+    if size < 64 then
+      expandListLit size (size % 2 == 0) (← ``(List.nil))
+    else
+      `(%[ $elems,* | List.nil ])
+
+end Lean

src/Init/Data/List/TakeDrop.lean

@@ -8,10 +8,10 @@ import Init.Data.List.Lemmas
 import Init.Data.Nat.Lemmas
 
 /-!
-# Lemmas about `List.take`, `List.drop`, `List.zip` and `List.zipWith`.
+# Further lemmas about `List.take`, `List.drop`, `List.zip` and `List.zipWith`.
 
 These are in a separate file from most of the list lemmas
-as they required importing more lemmas about natural numbers.
+as they required importing more lemmas about natural numbers, and use `omega`.
 -/
 
 namespace List
@@ -20,8 +20,6 @@ open Nat
 
 /-! ### take -/
 
-abbrev take_succ_cons := @take_cons_succ
-
 @[simp] theorem length_take : ∀ (i : Nat) (l : List α), length (take i l) = min i (length l)
   | 0, l => by simp [Nat.zero_min]
   | succ n, [] => by simp [Nat.min_zero]
@@ -34,17 +32,6 @@ theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
 
 theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
 
-theorem take_all_of_le {n} {l : List α} (h : length l ≤ n) : take n l = l :=
-  take_length_le h
-
-@[simp]
-theorem take_left : ∀ l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
-  | [], _ => rfl
-  | a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
-
-theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
-  rw [← h]; apply take_left
-
 theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m) l
   | n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
   | 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
@@ -57,12 +44,6 @@ theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replic
   | 0, m => by simp [Nat.zero_min]
   | succ n, succ m => by simp [succ_min_succ, take_replicate]
 
-theorem map_take (f : α → β) :
-    ∀ (L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
-  | [], i => by simp
-  | _, 0 => by simp
-  | h :: t, n + 1 => by dsimp; rw [map_take f t n]
-
 /-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
 of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
 theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
@@ -114,22 +95,6 @@ theorem get_take' (L : List α) {j i} :
     get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
   simp [getElem_take']
 
-theorem getElem?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]? := by
-  induction n generalizing l m with
-  | zero =>
-    exact absurd h (Nat.not_lt_of_le m.zero_le)
-  | succ _ hn =>
-    cases l with
-    | nil => simp only [take_nil]
-    | cons hd tl =>
-      cases m
-      · simp
-      · simpa using hn (Nat.lt_of_succ_lt_succ h)
-
-@[deprecated getElem?_take (since := "2024-06-12")]
-theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
-  simp [getElem?_take, h]
-
 theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
     (l.take n)[m]? = none :=
   getElem?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
@@ -150,23 +115,6 @@ theorem get?_take_eq_if {l : List α} {n m : Nat} :
     (l.take n).get? m = if m < n then l.get? m else none := by
   simp [getElem?_take_eq_if]
 
-@[simp]
-theorem get?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? :=
-  getElem?_take (Nat.lt_succ_self n)
-
-theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ l[n]?.toList := by
-  induction l generalizing n with
-  | nil =>
-    simp only [take_nil, Option.toList, getElem?_nil, append_nil]
-  | cons hd tl hl =>
-    cases n
-    · simp only [take, Option.toList, getElem?_cons_zero, nil_append]
-    · simp only [take, hl, getElem?_cons_succ, cons_append]
-
-@[simp]
-theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ l = [] ∨ k = 0 := by
-  cases l <;> cases k <;> simp [Nat.succ_ne_zero]
-
 @[simp]
 theorem take_eq_take :
     ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
@@ -187,20 +135,6 @@ theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.dro
   · apply length_take_le
   · apply Nat.le_add_right
 
-theorem take_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.take i = []
-  | _, _, rfl => take_nil
-
-theorem ne_nil_of_take_ne_nil {as : List α} {i : Nat} (h: as.take i ≠ []) : as ≠ [] :=
-  mt take_eq_nil_of_eq_nil h
-
-theorem dropLast_eq_take (l : List α) : l.dropLast = l.take l.length.pred := by
-  cases l with
-  | nil => simp [dropLast]
-  | cons x l =>
-    induction l generalizing x with
-    | nil => simp [dropLast]
-    | cons hd tl hl => simp [dropLast, hl]
-
 theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
     (l.take n).dropLast = l.take n.pred := by
   simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, take_take, pred_le, Nat.min_eq_left]
@@ -217,19 +151,6 @@ theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
 
 /-! ### drop -/
 
-@[simp]
-theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by
-  refine' ⟨fun h => _, drop_eq_nil_of_le⟩
-  induction k generalizing l with
-  | zero =>
-    simp only [drop] at h
-    simp [h]
-  | succ k hk =>
-    cases l
-    · simp
-    · simp only [drop] at h
-      simpa [Nat.succ_le_succ_iff] using hk h
-
 theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
     (a :: l).drop l.length = [l.getLast h] := by
   induction l generalizing a with
@@ -266,15 +187,6 @@ theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l
   rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
     simp [Nat.add_sub_cancel_left, Nat.le_add_right]
 
-theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) ≤ sizeOf l := by
-  induction l generalizing n with
-  | nil => rw [drop_nil]; apply Nat.le_refl
-  | cons _ _ lih =>
-    induction n with
-    | zero => apply Nat.le_refl
-    | succ n =>
-      exact Trans.trans (lih _) (Nat.le_add_left _ _)
-
 theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by
   have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
   rw [(take_append_drop i L).symm] at h
@@ -328,20 +240,6 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? :=
 theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
   simp
 
-@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
-  | m, [] => by simp
-  | 0, l => by simp
-  | m + 1, a :: l =>
-    calc
-      drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
-      _ = drop (n + m) l := drop_drop n m l
-      _ = drop (n + (m + 1)) (a :: l) := rfl
-
-theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
-  | 0, _, _ => by simp
-  | _, _, [] => by simp
-  | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
-
 theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
   | 0, _, _ => by simp
   | _, 0, _ => by simp
@@ -351,14 +249,6 @@ theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m -
     congr 1
     omega
 
-theorem map_drop (f : α → β) :
-    ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
-  | [], i => by simp
-  | L, 0 => by simp
-  | h :: t, n + 1 => by
-    dsimp
-    rw [map_drop f t]
-
 theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
     xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
   induction xs generalizing n <;>
@@ -379,29 +269,6 @@ theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
     rw [length_append, length_reverse]
     rfl
 
-@[simp]
-theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length),
-    l[i] :: drop (i + 1) l = drop i l
-  | _::_, 0, _ => rfl
-  | _::_, i+1, _ => getElem_cons_drop _ i _
-
-@[deprecated getElem_cons_drop (since := "2024-06-12")]
-theorem get_cons_drop (l : List α) (i) : get l i :: drop (i + 1) l = drop i l := by
-  simp
-
-theorem drop_eq_getElem_cons {n} {l : List α} (h) : drop n l = l[n] :: drop (n + 1) l :=
-  (getElem_cons_drop _ n h).symm
-
-@[deprecated drop_eq_getElem_cons (since := "2024-06-12")]
-theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l := by
-  simp [drop_eq_getElem_cons]
-
-theorem drop_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.drop i = []
-  | _, _, rfl => drop_nil
-
-theorem ne_nil_of_drop_ne_nil {as : List α} {i : Nat} (h: as.drop i ≠ []) : as ≠ [] :=
-  mt drop_eq_nil_of_eq_nil h
-
 /-! ### zipWith -/
 
 @[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :

src/Init/Prelude.lean

@@ -2302,24 +2302,6 @@ protected def List.hasDecEq {α : Type u} [DecidableEq α] : (a b : List α) →
 
 instance {α : Type u} [DecidableEq α] : DecidableEq (List α) := List.hasDecEq
 
-/--
-Folds a function over a list from the left:
-`foldl f z [a, b, c] = f (f (f z a) b) c`
--/
-@[specialize]
-def List.foldl {α : Type u} {β : Type v} (f : α → β → α) : (init : α) → List β → α
-  | a, nil      => a
-  | a, cons b l => foldl f (f a b) l
-
-/--
-`l.set n a` sets the value of list `l` at (zero-based) index `n` to `a`:
-`[a, b, c, d].set 1 b' = [a, b', c, d]`
--/
-def List.set : List α → Nat → α → List α
-  | cons _ as, 0,          b => cons b as
-  | cons a as, Nat.succ n, b => cons a (set as n b)
-  | nil,       _,          _ => nil
-
 /--
 The length of a list: `[].length = 0` and `(a :: l).length = l.length + 1`.
 
@@ -2346,11 +2328,6 @@ def List.lengthTR (as : List α) : Nat :=
 @[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=
   rfl
 
-/-- `l.concat a` appends `a` at the *end* of `l`, that is, `l ++ [a]`. -/
-def List.concat {α : Type u} : List α → α → List α
-  | nil,       b => cons b nil
-  | cons a as, b => cons a (concat as b)
-
 /--
 `as.get i` returns the `i`'th element of the list `as`.
 This version of the function uses `i : Fin as.length` to ensure that it will
@@ -2360,6 +2337,29 @@ def List.get {α : Type u} : (as : List α) → Fin as.length → α
   | cons a _,  ⟨0, _⟩ => a
   | cons _ as, ⟨Nat.succ i, h⟩ => get as ⟨i, Nat.le_of_succ_le_succ h⟩
 
+/--
+`l.set n a` sets the value of list `l` at (zero-based) index `n` to `a`:
+`[a, b, c, d].set 1 b' = [a, b', c, d]`
+-/
+def List.set : List α → Nat → α → List α
+  | cons _ as, 0,          b => cons b as
+  | cons a as, Nat.succ n, b => cons a (set as n b)
+  | nil,       _,          _ => nil
+
+/--
+Folds a function over a list from the left:
+`foldl f z [a, b, c] = f (f (f z a) b) c`
+-/
+@[specialize]
+def List.foldl {α : Type u} {β : Type v} (f : α → β → α) : (init : α) → List β → α
+  | a, nil      => a
+  | a, cons b l => foldl f (f a b) l
+
+/-- `l.concat a` appends `a` at the *end* of `l`, that is, `l ++ [a]`. -/
+def List.concat {α : Type u} : List α → α → List α
+  | nil,       b => cons b nil
+  | cons a as, b => cons a (concat as b)
+
 /--
 `String` is the type of (UTF-8 encoded) strings.
 

tests/lean/run/delabMatch.lean

@@ -17,7 +17,7 @@ fun x =>
 #guard_msgs in
 #print Nat.pred
 /--
-info: def List.head?.{u_1} : {α : Type u_1} → List α → Option α :=
+info: def List.head?.{u} : {α : Type u} → List α → Option α :=
 fun {α} x =>
   match x with
   | [] => none

tests/lean/run/maze.lean

@@ -181,19 +181,19 @@ inductive Move where
 @[simp]
 def make_move : GameState → Move → GameState
 | ⟨s, ⟨x,y⟩, w⟩, Move.east =>
-             if w.notElem ⟨x+1, y⟩ ∧ x + 1 ≤ s.x
+             if !w.elem ⟨x+1, y⟩ ∧ x + 1 ≤ s.x
              then ⟨s, ⟨x+1, y⟩, w⟩
              else ⟨s, ⟨x,y⟩, w⟩
 | ⟨s, ⟨x,y⟩, w⟩, Move.west =>
-             if w.notElem ⟨x-1, y⟩
+             if !w.elem ⟨x-1, y⟩
              then ⟨s, ⟨x-1, y⟩, w⟩
              else ⟨s, ⟨x,y⟩, w⟩
 | ⟨s, ⟨x,y⟩, w⟩, Move.north =>
-             if w.notElem ⟨x, y-1⟩
+             if !w.elem ⟨x, y-1⟩
              then ⟨s, ⟨x, y-1⟩, w⟩
              else ⟨s, ⟨x,y⟩, w⟩
 | ⟨s, ⟨x,y⟩, w⟩, Move.south =>
-             if w.notElem ⟨x, y + 1⟩ ∧ y + 1 ≤ s.y
+             if !w.elem ⟨x, y + 1⟩ ∧ y + 1 ≤ s.y
              then ⟨s, ⟨x, y+1⟩, w⟩
              else ⟨s, ⟨x,y⟩, w⟩
 
@@ -211,7 +211,7 @@ theorem step_west
   {s: Coords}
   {x y : Nat}
   {w: List Coords}
-  (hclear' : w.notElem ⟨x,y⟩)
+  (hclear' : !w.elem ⟨x,y⟩)
   (W : can_escape ⟨s,⟨x,y⟩,w⟩) :
   can_escape ⟨s,⟨x+1,y⟩,w⟩ :=
    by have hmm : GameState.mk s ⟨x,y⟩ w = make_move ⟨s,⟨x+1, y⟩,w⟩ Move.west :=
@@ -224,7 +224,7 @@ theorem step_east
   {s: Coords}
   {x y : Nat}
   {w: List Coords}
-  (hclear' : w.notElem ⟨x+1,y⟩)
+  (hclear' : !w.elem ⟨x+1,y⟩)
   (hinbounds : x + 1 ≤ s.x)
   (E : can_escape ⟨s,⟨x+1,y⟩,w⟩) :
   can_escape ⟨s,⟨x, y⟩,w⟩ :=
@@ -237,7 +237,7 @@ theorem step_north
   {s: Coords}
   {x y : Nat}
   {w: List Coords}
-  (hclear' : w.notElem ⟨x,y⟩)
+  (hclear' : !w.elem ⟨x,y⟩)
   (N : can_escape ⟨s,⟨x,y⟩,w⟩) :
   can_escape ⟨s,⟨x, y+1⟩,w⟩ :=
     by have hmm : GameState.mk s ⟨x,y⟩ w = make_move ⟨s,⟨x, y+1⟩,w⟩ Move.north :=
@@ -250,7 +250,7 @@ theorem step_south
   {s: Coords}
   {x y : Nat}
   {w: List Coords}
-  (hclear' : w.notElem ⟨x,y+1⟩)
+  (hclear' : !w.elem ⟨x,y+1⟩)
   (hinbounds : y + 1 ≤ s.y)
   (S : can_escape ⟨s,⟨x,y+1⟩,w⟩) :
   can_escape ⟨s,⟨x, y⟩,w⟩ :=