restore newly-confluence #check_simp

src/Init/Data/List/Basic.lean

@@ -567,10 +567,12 @@ def replicate : (n : Nat) → (a : α) → List α
   | n+1, a => a :: replicate n a
 
 @[simp] theorem replicate_zero : replicate 0 a = [] := rfl
-@[simp] theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
+theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
 
 @[simp] theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
-  induction n <;> simp_all
+  induction n with
+  | zero => simp
+  | succ n ih => simp only [ih, replicate_succ, length_cons, Nat.succ_eq_add_one]
 
 /-! ## List membership
 
@@ -609,13 +611,13 @@ def isEmpty : List α → Bool
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
-  | b::bs => match b == a with
+  | b::bs => match a == b with
     | true  => true
     | false => elem a bs
 
 @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
 theorem elem_cons [BEq α] {a : α} :
-    (a::as).elem b = match a == b with | true => true | false => as.elem b := rfl
+    (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
 
 /-- `notElem a l` is `!(elem a l)`. -/
 @[deprecated (since := "2024-06-15")]
@@ -850,6 +852,9 @@ That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
 def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
+@[simp] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
+  simp [isSuffixOf]
+
 /-! ### isSuffixOf? -/
 
 /-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
@@ -906,13 +911,13 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
 -/
 def replace [BEq α] : List α → α → α → List α
   | [],    _, _ => []
-  | a::as, b, c => match a == b with
+  | a::as, b, c => match b == a with
     | true  => c::as
     | false => a :: replace as b c
 
 @[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
 theorem replace_cons [BEq α] {a : α} :
-    (a::as).replace b c = match a == b with | true => c::as | false => a :: replace as b c :=
+    (a::as).replace b c = match b == a with | true => c::as | false => a :: replace as b c :=
   rfl
 
 /-! ### insert -/

src/Init/Data/List/Impl.lean

@@ -258,7 +258,7 @@ theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++
   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)
+  | a::as, acc => bif b == a 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]

src/Init/Data/List/Lemmas.lean

@@ -38,6 +38,8 @@ namespace List
 
 open Nat
 
+/-! ## Preliminaries -/
+
 -- We may want to replace these `simp` attributes with explicit equational lemmas,
 -- as we already have for all the non-monadic functions.
 attribute [simp] mapA forA filterAuxM firstM anyM allM findM? findSomeM?
@@ -162,9 +164,11 @@ theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some
 theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
   simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
 
-@[simp] theorem getElem?_eq_none : l[n]? = none ↔ length l ≤ n := by
+@[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
   simp only [← get?_eq_getElem?, get?_eq_none]
 
+theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
+
 @[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 @[simp] theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
@@ -364,6 +368,20 @@ theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = so
 theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
   simp [getElem?_eq_some, Fin.exists_iff, mem_iff_get]
 
+@[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
+    decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
+  cases h : y == a <;> simp_all
+
+/-! ### any / all -/
+
+theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by induction l <;> simp [*]
+
+theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l →  p x) := by induction l <;> simp [*]
+
+@[simp] theorem any_eq_true {l : List α} : l.any p ↔ ∃ x, x ∈ l ∧ p x := by simp [any_eq]
+
+@[simp] theorem all_eq_true {l : List α} : l.all p ↔ ∀ x, x ∈ l →  p x := by simp [all_eq]
+
 /-! ### set -/
 
 -- As `List.set` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
@@ -414,7 +432,7 @@ theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
   by_cases hj : j < (l.set i a).length
   · rw [getElem?_eq_getElem hj, getElem?_eq_getElem (by simp_all)]
     simp_all
-  · rw [getElem?_eq_none.mpr (by simp_all), getElem?_eq_none.mpr (by simp_all)]
+  · rw [getElem?_eq_none (by simp_all), getElem?_eq_none (by simp_all)]
 
 theorem getElem_set {l : List α} {m n} {a} (h) :
     (set l m a)[n]'h = if m = n then a else l[n]'(length_set .. ▸ h) := by
@@ -479,6 +497,49 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
 
 -- See also `set_eq_take_append_cons_drop` in `Init.Data.List.TakeDrop`.
 
+/-! ### Lexicographic ordering -/
+
+theorem lt_irrefl' [LT α] (lt_irrefl : ∀ x : α, ¬x < x) (l : List α) : ¬l < l := by
+  induction l with
+  | nil => nofun
+  | cons a l ih => intro
+    | .head _ _ h => exact lt_irrefl _ h
+    | .tail _ _ h => exact ih h
+
+theorem lt_trans' [LT α] [DecidableRel (@LT.lt α _)]
+    (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
+    (le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z)
+    {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
+  induction h₁ generalizing l₃ with
+  | nil => let _::_ := l₃; exact List.lt.nil ..
+  | @head a l₁ b l₂ ab =>
+    match h₂ with
+    | .head l₂ l₃ bc => exact List.lt.head _ _ (lt_trans ab bc)
+    | .tail _ cb ih =>
+      exact List.lt.head _ _ <| Decidable.by_contra (le_trans · cb ab)
+  | @tail a l₁ b l₂ ab ba h₁ ih2 =>
+    match h₂ with
+    | .head l₂ l₃ bc =>
+      exact List.lt.head _ _ <| Decidable.by_contra (le_trans ba · bc)
+    | .tail bc cb ih =>
+      exact List.lt.tail (le_trans ab bc) (le_trans cb ba) (ih2 ih)
+
+theorem lt_antisymm' [LT α]
+    (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y)
+    {l₁ l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) : l₁ = l₂ := by
+  induction l₁ generalizing l₂ with
+  | nil =>
+    cases l₂ with
+    | nil => rfl
+    | cons b l₂ => cases h₁ (.nil ..)
+  | cons a l₁ ih =>
+    cases l₂ with
+    | nil => cases h₂ (.nil ..)
+    | cons b l₂ =>
+      have ab : ¬a < b := fun ab => h₁ (.head _ _ ab)
+      cases lt_antisymm ab (fun ba => h₂ (.head _ _ ba))
+      rw [ih (fun ll => h₁ (.tail ab ab ll)) (fun ll => h₂ (.tail ab ab ll))]
+
 /-! ### foldlM and foldrM -/
 
 @[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β → α → m β) (b) :
@@ -526,50 +587,6 @@ theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α
     (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
   induction l generalizing init <;> simp [*]
 
-/-! ### lt -/
-
-theorem lt_irrefl' [LT α] (lt_irrefl : ∀ x : α, ¬x < x) (l : List α) : ¬l < l := by
-  induction l with
-  | nil => nofun
-  | cons a l ih => intro
-    | .head _ _ h => exact lt_irrefl _ h
-    | .tail _ _ h => exact ih h
-
-theorem lt_trans' [LT α] [DecidableRel (@LT.lt α _)]
-    (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
-    (le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z)
-    {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
-  induction h₁ generalizing l₃ with
-  | nil => let _::_ := l₃; exact List.lt.nil ..
-  | @head a l₁ b l₂ ab =>
-    match h₂ with
-    | .head l₂ l₃ bc => exact List.lt.head _ _ (lt_trans ab bc)
-    | .tail _ cb ih =>
-      exact List.lt.head _ _ <| Decidable.by_contra (le_trans · cb ab)
-  | @tail a l₁ b l₂ ab ba h₁ ih2 =>
-    match h₂ with
-    | .head l₂ l₃ bc =>
-      exact List.lt.head _ _ <| Decidable.by_contra (le_trans ba · bc)
-    | .tail bc cb ih =>
-      exact List.lt.tail (le_trans ab bc) (le_trans cb ba) (ih2 ih)
-
-theorem lt_antisymm' [LT α]
-    (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y)
-    {l₁ l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) : l₁ = l₂ := by
-  induction l₁ generalizing l₂ with
-  | nil =>
-    cases l₂ with
-    | nil => rfl
-    | cons b l₂ => cases h₁ (.nil ..)
-  | cons a l₁ ih =>
-    cases l₂ with
-    | nil => cases h₂ (.nil ..)
-    | cons b l₂ =>
-      have ab : ¬a < b := fun ab => h₁ (.head _ _ ab)
-      cases lt_antisymm ab (fun ba => h₂ (.head _ _ ba))
-      rw [ih (fun ll => h₁ (.tail ab ab ll)) (fun ll => h₂ (.tail ab ab ll))]
-
-
 /-! ### getD -/
 
 @[simp] theorem getD_eq_getElem? (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by
@@ -643,6 +660,8 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1)
 @[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
   rw [getLastD_eq_getLast?, getLast?_concat]; rfl
 
+/-! ## Head and tail -/
+
 /-! ### head -/
 
 theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a → head! l = a
@@ -656,6 +675,8 @@ theorem head?_eq_head : ∀ l h, @head? α l = some (head l h)
 @[simp] theorem tailD_eq_tail? (l l' : List α) : tailD l l' = (tail? l).getD l' := by
   cases l <;> rfl
 
+/-! ## Basic operations -/
+
 /-! ### map -/
 
 @[simp] theorem length_map (as : List α) (f : α → β) : (as.map f).length = as.length := by
@@ -1113,12 +1134,30 @@ theorem bind_map (f : β → γ) (g : α → List β) :
 
 /-! ### replicate -/
 
+@[simp] theorem replicate_one : replicate 1 a = [a] := rfl
+
+@[simp] theorem contains_replicate [BEq α] {n : Nat} {a b : α} :
+    (replicate n b).contains a = (a == b && !n == 0) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, elem_cons]
+    split <;> simp_all
+
+@[simp] theorem decide_mem_replicate [BEq α] [LawfulBEq α] {a b : α} :
+    ∀ {n}, decide (b ∈ replicate n a) = ((¬ n == 0) && b == a)
+  | 0 => by simp
+  | n+1 => by simp [replicate_succ, decide_mem_replicate, Nat.succ_ne_zero]
+
 @[simp] theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
   | 0 => by simp
-  | n+1 => by simp [mem_replicate, Nat.succ_ne_zero]
+  | n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]
 
 theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
+@[simp] theorem replicate_succ_ne_nil (n : Nat) (a : α) : replicate (n+1) a ≠ [] := by
+  simp [replicate_succ]
+
 @[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) :
     (replicate n a)[m] = a :=
   eq_of_mem_replicate (get_mem _ _ _)
@@ -1127,6 +1166,27 @@ theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a :=
 theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by
   simp
 
+theorem getElem?_replicate : (replicate n a)[m]? = if m < n then some a else none := by
+  by_cases h : m < n
+  · rw [getElem?_eq_getElem (by simpa), getElem_replicate, if_pos h]
+  · rw [getElem?_eq_none (by simpa using h), if_neg h]
+
+@[simp] theorem getElem?_replicate_of_lt {n : Nat} {m : Nat} (h : m < n) : (replicate n a)[m]? = some a := by
+  simp [getElem?_replicate, h]
+
+@[simp] theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) :=
+  ⟨fun h => have eq : n = m := by simpa using congrArg length h
+    ⟨eq, by
+    subst eq
+    by_cases w : n = 0
+    · simp_all
+    · right
+      have p := congrArg (·[0]?) h
+      replace w : 0 < n := by exact zero_lt_of_ne_zero w
+      simp only [getElem?_replicate, if_pos w] at p
+      simp_all⟩,
+    by rintro ⟨rfl, rfl | rfl⟩ <;> rfl⟩
+
 theorem eq_replicate_of_mem {a : α} :
     ∀ {l : List α}, (∀ (b) (_ : b ∈ l), b = a) → l = replicate l.length a
   | [], _ => rfl
@@ -1139,6 +1199,76 @@ theorem eq_replicate {a : α} {n} {l : List α} :
   ⟨fun h => h ▸ ⟨length_replicate .., fun _ => eq_of_mem_replicate⟩,
    fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩
 
+@[simp] theorem append_replicate_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
+  rw [eq_replicate]
+  constructor
+  · simp
+  · intro b
+    simp only [mem_append, mem_replicate, ne_eq]
+    rintro (⟨-, rfl⟩ | ⟨_, rfl⟩) <;> rfl
+
+@[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
+  ext1 n
+  simp only [getElem?_map, getElem?_replicate]
+  split <;> simp
+
+theorem filter_replicate : (replicate n a).filter p = if p a then replicate n a else [] := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, filter_cons]
+    split <;> simp_all
+
+@[simp] theorem filter_replicate_of_pos (h : p a) : (replicate n a).filter p = replicate n a := by
+  simp [filter_replicate, h]
+
+@[simp] theorem filter_replicate_of_neg (h : ¬ p a) : (replicate n a).filter p = [] := by
+  simp [filter_replicate, h]
+
+theorem filterMap_replicate {f : α → Option β} :
+    (replicate n a).filterMap f = match f a with | none => [] | .some b => replicate n b := by
+  induction n with
+  | zero => split <;> simp
+  | succ n ih =>
+    simp only [replicate_succ, filterMap_cons]
+    split <;> simp_all
+
+-- This is not a useful `simp` lemma because `b` is unknown.
+theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
+    (replicate n a).filterMap f = replicate n b := by
+  simp [filterMap_replicate, h]
+
+@[simp] theorem filterMap_replicate_of_isSome {f : α → Option β} (h : (f a).isSome) :
+    (replicate n a).filterMap f = replicate n (Option.get _ h) := by
+  rw [Option.isSome_iff_exists] at h
+  obtain ⟨b, h⟩ := h
+  simp [filterMap_replicate, h]
+
+@[simp] theorem filterMap_replicate_of_none {f : α → Option β} (h : f a = none) :
+    (replicate n a).filterMap f = [] := by
+  simp [filterMap_replicate, h]
+
+@[simp] theorem join_replicate_nil : (replicate n ([] : List α)).join = [] := by
+  induction n <;> simp_all [replicate_succ]
+
+@[simp] theorem join_replicate_singleton : (replicate n [a]).join = replicate n a := by
+  induction n <;> simp_all [replicate_succ]
+
+@[simp] theorem join_replicate_replicate : (replicate n (replicate m a)).join = replicate (n * m) a := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, join_cons, ih, append_replicate_replicate, replicate_inj, or_true,
+      and_true, add_one_mul, Nat.add_comm]
+
+theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (replicate n (f a)).join := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp only [replicate_succ, bind_cons, ih, join_cons]
+
+@[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
+  cases n <;> simp [replicate_succ]
+
 /-! ### reverse -/
 
 @[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by
@@ -1214,6 +1344,13 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
     l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
   (foldl_reverse ..).symm.trans <| by simp
 
+@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
+  eq_replicate.2
+    ⟨by rw [length_reverse, length_replicate],
+     fun b h => eq_of_mem_replicate (mem_reverse.1 h)⟩
+
+/-! ## List membership -/
+
 /-! ### elem -/
 
 @[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by
@@ -1222,13 +1359,15 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
 /-! ### contains -/
 
 @[simp] theorem contains_cons [BEq α] :
-    (a :: as : List α).contains x = (a == x || as.contains x) := by
+    (a :: as : List α).contains x = (x == a || as.contains x) := by
   simp only [contains, elem]
   split <;> simp_all
 
-theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (· == a) := by
+theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 
+/-! ## Sublists -/
+
 /-! ### take and drop
 
 Further results on `List.take` and `List.drop`, which rely on stronger automation in `Nat`,
@@ -1413,6 +1552,11 @@ theorem drop_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : drop n (l
 
 /-! ### takeWhile and dropWhile -/
 
+theorem takeWhile_cons (p : α → Bool) (a : α) (l : List α) :
+    (a :: l).takeWhile p = if p a then a :: l.takeWhile p else [] := by
+  simp only [takeWhile]
+  by_cases h: p a <;> simp [h]
+
 theorem dropWhile_cons :
     (x :: xs : List α).dropWhile p = if p x then xs.dropWhile p else x :: xs := by
   split <;> simp_all [dropWhile]
@@ -1431,6 +1575,31 @@ theorem dropWhile_append {xs ys : List α} :
     simp only [cons_append, dropWhile_cons]
     split <;> simp_all
 
+@[simp] theorem takeWhile_replicate_eq_filter (p : α → Bool) :
+    (replicate n a).takeWhile p = (replicate n a).filter p := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, takeWhile_cons]
+    split <;> simp_all
+
+theorem takeWhile_replicate (p : α → Bool) :
+    (replicate n a).takeWhile p = if p a then replicate n a else [] := by
+  rw [takeWhile_replicate_eq_filter, filter_replicate]
+
+@[simp] theorem dropWhile_replicate_eq_filter_not (p : α → Bool) :
+    (replicate n a).dropWhile p = (replicate n a).filter (fun a => !p a) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, dropWhile_cons]
+    split <;> simp_all
+
+theorem dropWhile_replicate (p : α → Bool) :
+    (replicate n a).dropWhile p = if p a then [] else replicate n a := by
+  simp only [dropWhile_replicate_eq_filter_not, filter_replicate]
+  split <;> simp_all
+
 /-! ### partition -/
 
 @[simp] theorem partition_eq_filter_filter (p : α → Bool) (l : List α) :
@@ -1476,21 +1645,94 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b:
 
 @[simp 1100] theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by simp
 
-/-! ### isPrefixOf -/
+@[simp] theorem dropLast_replicate (n) (a : α) : dropLast (replicate n a) = replicate (n - 1) a := by
+  match n with
+  | 0 => simp
+  | 1 => simp [replicate_succ]
+  | n+2 =>
+    rw [replicate_succ, dropLast_cons_of_ne_nil, dropLast_replicate]
+    · simp [replicate_succ]
+    · simp
 
-@[simp] theorem isPrefixOf_cons₂_self [BEq α] [LawfulBEq α] {a : α} :
+@[simp] theorem dropLast_cons_self_replicate (n) (a : α) :
+    dropLast (a :: replicate n a) = replicate n a := by
+  rw [← replicate_succ, dropLast_replicate, Nat.add_sub_cancel]
+
+/-! ### isPrefixOf -/
+section isPrefixOf
+variable [BEq α]
+
+@[simp] theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} :
     isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons₂]
 
-/-! ### replace -/
+@[simp] theorem isPrefixOf_length_pos_nil {L : List α} (h : 0 < L.length) : isPrefixOf L [] = false := by
+  cases L <;> simp_all [isPrefixOf]
 
-@[simp] theorem replace_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
+@[simp] theorem isPrefixOf_replicate {a : α} :
+    isPrefixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a)) := by
+  induction l generalizing n with
+  | nil => simp
+  | cons h t ih =>
+    cases n
+    · simp
+    · simp [replicate_succ, isPrefixOf_cons₂, ih, Nat.succ_le_succ_iff, Bool.and_left_comm]
+
+end isPrefixOf
+
+/-! ### isSuffixOf -/
+section isSuffixOf
+variable [BEq α]
+
+@[simp] theorem isSuffixOf_cons_nil : isSuffixOf (a::as) ([] : List α) = false := by
+  simp [isSuffixOf]
+
+@[simp] theorem isSuffixOf_replicate {a : α} :
+    isSuffixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a)) := by
+  simp [isSuffixOf, all_eq]
+
+end isSuffixOf
+
+/-! ### rotateLeft -/
+
+@[simp] theorem rotateLeft_zero (l : List α) : rotateLeft l 0 = l := by
+  simp [rotateLeft]
+
+/-! ### rotateRight -/
+
+@[simp] theorem rotateRight_zero (l : List α) : rotateRight l 0 = l := by
+  simp [rotateRight]
+
+/-! ## Manipulating elements -/
+
+/-! ### replace -/
+section replace
+variable [BEq α]
+
+@[simp] theorem replace_cons_self [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
   simp [replace_cons]
 
+@[simp] theorem replace_of_not_mem {l : List α} (h : !l.elem a) : l.replace a b = l := by
+  induction l <;> simp_all [replace_cons]
+
+@[simp] theorem replace_replicate_self [LawfulBEq α] {a : α} (h : 0 < n) :
+    (replicate n a).replace a b = b :: replicate (n - 1) a := by
+  cases n <;> simp_all [replicate_succ, replace_cons]
+
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+    (replicate n a).replace b c = replicate n a := by
+  rw [replace_of_not_mem]
+  simp_all
+
+end replace
+
 /-! ### insert -/
 
 section insert
 variable [BEq α] [LawfulBEq α]
 
+@[simp] theorem insert_nil (a : α) : [].insert a = [a] := by
+  simp [List.insert]
+
 @[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by
   simp [List.insert, h]
 
@@ -1521,6 +1763,14 @@ theorem eq_or_mem_of_mem_insert {l : List α} (h : a ∈ l.insert b) : a = b ∨
 @[simp] theorem length_insert_of_not_mem {l : List α} (h : a ∉ l) :
     length (l.insert a) = length l + 1 := by rw [insert_of_not_mem h]; rfl
 
+@[simp] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
+  cases n <;> simp_all
+
+@[simp] theorem insert_replicate_ne {a b : α} (h : !b == a) :
+    (replicate n a).insert b = b :: replicate n a := by
+  rw [insert_of_not_mem]
+  simp_all
+
 end insert
 
 /-! ### erase -/
@@ -1540,15 +1790,24 @@ theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l
     rw [mem_cons, not_or] at h
     simp only [erase_cons, if_neg, erase_of_not_mem h.2, beq_iff_eq, Ne.symm h.1, not_false_eq_true]
 
+@[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} :
+    (replicate n a).erase a = replicate (n - 1) a := by
+  cases n <;> simp [replicate_succ]
+
+@[simp] theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
+    (replicate n a).erase b = replicate n a := by
+  rw [erase_of_not_mem]
+  simp_all
+
 end erase
 
 /-! ### find? -/
 
-@[simp] theorem find?_cons_of_pos (l) (h : p a) : find? p (a :: l) = some a :=
-  by simp [find?, h]
+@[simp] theorem find?_cons_of_pos (l) (h : p a) : find? p (a :: l) = some a := by
+  simp [find?, h]
 
-@[simp] theorem find?_cons_of_neg (l) (h : ¬p a) : find? p (a :: l) = find? p l :=
-  by simp [find?, h]
+@[simp] theorem find?_cons_of_neg (l) (h : ¬p a) : find? p (a :: l) = find? p l := by
+  simp [find?, h]
 
 @[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
   induction l <;> simp [find?_cons]; split <;> simp [*]
@@ -1565,8 +1824,30 @@ theorem find?_some : ∀ {l}, find? p l = some a → p a
     · exact H ▸ .head _
     · exact .tail _ (mem_of_find?_eq_some H)
 
+theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
+  cases n
+  · simp
+  · by_cases p a <;> simp_all [replicate_succ]
+
+@[simp] theorem find?_replicate_of_length_pos (h : 0 < n) : find? p (replicate n a) = if p a then some a else none := by
+  simp [find?_replicate, Nat.ne_of_gt h]
+
+@[simp] theorem find?_replicate_of_pos (h : p a) : find? p (replicate n a) = if n = 0 then none else some a := by
+  simp [find?_replicate, h]
+
+@[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
+  simp [find?_replicate, h]
+
 /-! ### findSome? -/
 
+@[simp] theorem findSome?_cons_of_isSome (l) (h : (f a).isSome) : findSome? f (a :: l) = f a := by
+  simp only [findSome?]
+  split <;> simp_all
+
+@[simp] theorem findSome?_cons_of_isNone (l) (h : (f a).isNone) : findSome? f (a :: l) = findSome? f l := by
+  simp only [findSome?]
+  split <;> simp_all
+
 theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.findSome? f = some b) :
     ∃ a, a ∈ l ∧ f a = b := by
   induction l with
@@ -1575,17 +1856,60 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
     split at w <;> simp_all
 
-/-! ### lookup -/
+theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, findSome?_cons]
+    split <;> simp_all
 
-@[simp] theorem lookup_cons_self [BEq α] [LawfulBEq α] {k : α} : ((k,b)::es).lookup k = some b := by
+@[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
+  simp [findSome?_replicate, Nat.ne_of_gt h]
+
+@[simp] theorem find?_replicate_of_isSome (h : (f a).isSome) : findSome? f (replicate n a) = if n = 0 then none else f a := by
+  simp [findSome?_replicate, h]
+
+@[simp] theorem find?_replicate_of_isNone (h : (f a).isNone) : findSome? f (replicate n a) = none := by
+  rw [Option.isNone_iff_eq_none] at h
+  simp [findSome?_replicate, h]
+
+/-! ### lookup -/
+section lookup
+variable [BEq α] [LawfulBEq α]
+
+@[simp] theorem lookup_cons_self  {k : α} : ((k,b)::es).lookup k = some b := by
   simp [lookup_cons]
 
+theorem lookup_replicate {k : α} :
+    (replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, lookup_cons]
+    split <;> simp_all
+
+theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
+    (replicate n (a,b)).lookup k = if k == a then some b else none := by
+  simp [lookup_replicate, Nat.ne_of_gt h]
+
+theorem lookup_replicate_self {a : α} :
+    (replicate n (a, b)).lookup a = if n = 0 then none else some b := by
+  simp [lookup_replicate]
+
+@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
+    (replicate n (a, b)).lookup a = some b := by
+  simp [lookup_replicate_self, Nat.ne_of_gt h]
+
+@[simp] theorem lookup_replicate_ne {k : α} (h : !k == a) :
+    (replicate n (a,b)).lookup k = none := by
+  simp_all [lookup_replicate]
+
+end lookup
+
+/-! ## Logic -/
+
 /-! ### any / all -/
 
-@[simp] theorem any_eq_true {l : List α} : l.any p ↔ ∃ x, x ∈ l ∧ p x := by induction l <;> simp [*]
-
-@[simp] theorem all_eq_true {l : List α} : l.all p ↔ ∀ x, x ∈ l →  p x := by induction l <;> simp [*]
-
 theorem not_any_eq_all_not (l : List α) (p : α → Bool) : (!l.any p) = l.all fun a => !p a := by
   induction l with simp | cons _ _ ih => rw [ih]
 
@@ -1614,6 +1938,8 @@ theorem any_eq_not_all_not (l : List α) (p : α → Bool) : l.any p = !l.all (!
 theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!p .) := by
   simp only [not_any_eq_all_not, Bool.not_not]
 
+/-! ## Zippers -/
+
 /-! ### zip -/
 
 theorem zip_map (f : α → γ) (g : β → δ) :
@@ -1670,6 +1996,13 @@ theorem map_snd_zip :
     show _ :: map Prod.snd (zip as bs) = _ :: bs
     rw [map_snd_zip as bs h]
 
+/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
+@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
+    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [replicate_succ, ih]
+
 /-! ### zipWith -/
 
 theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
@@ -1760,9 +2093,16 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
       simp only [length_cons, Nat.succ.injEq] at h
       simp [ih _ h]
 
+/-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
+@[simp] theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
+    zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [replicate_succ, ih]
+
 /-! ### zipWithAll -/
 
-theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat } :
+theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
     (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with
       | none, none => .none | a?, b? => some (f a? b?) := by
   induction as generalizing bs i with
@@ -1784,6 +2124,22 @@ theorem get?_zipWithAll {f : Option α → Option β → γ} :
 set_option linter.deprecated false in
 @[deprecated getElem?_zipWithAll (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll
 
+@[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
+    zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [replicate_succ, ih]
+
+/-! ### unzip -/
+
+@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
+    unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [replicate_succ, ih]
+
+/-! ## Ranges and enumeration -/
+
 /-! ### enumFrom -/
 
 @[simp] theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
@@ -1797,6 +2153,8 @@ set_option linter.deprecated false in
 
 theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
 
+/-! ## Minima and maxima -/
+
 /-! ### minimum? -/
 
 @[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl
@@ -1860,6 +2218,16 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
       ((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
       (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
 
+theorem minimum?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
+    (replicate n a).minimum? = if n = 0 then none else some a := by
+  induction n with
+  | zero => rfl
+  | succ n ih => cases n <;> simp_all [replicate_succ, minimum?_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]
+
 /-! ### maximum? -/
 
 @[simp] theorem maximum?_nil [Max α] : ([] : List α).maximum? = none := rfl
@@ -1907,6 +2275,18 @@ theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·
       (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl))
       ((maximum?_le_iff max_le_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
 
+theorem maximum?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
+    (replicate n a).maximum? = if n = 0 then none else some a := by
+  induction n with
+  | zero => rfl
+  | succ n ih => cases n <;> simp_all [replicate_succ, maximum?_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]
+
+/-! ## Monadic operations -/
+
 /-! ### mapM -/
 
 /-- Alternate (non-tail-recursive) form of mapM for proofs. -/

src/Init/Data/List/TakeDrop.lean

@@ -39,10 +39,15 @@ theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m)
   | succ n, succ m, a :: l => by
     simp only [take, succ_min_succ, take_take n m l]
 
-theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
+@[simp] theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
-  | succ n, succ m => by simp [succ_min_succ, take_replicate]
+  | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
+
+@[simp] theorem drop_replicate (a : α) : ∀ n m : Nat, drop n (replicate m a) = replicate (m - n) a
+  | n, 0 => by simp
+  | 0, m => by simp
+  | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]
 
 /-- 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₂`. -/
@@ -97,7 +102,7 @@ theorem get_take' (L : List α) {j i} :
 
 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
+  getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
 @[deprecated getElem?_take_eq_none (since := "2024-06-12")]
 theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
@@ -298,6 +303,32 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
 
 @[deprecated (since := "2024-06-15")] abbrev reverse_take := @take_reverse
 
+/-! ### rotateLeft -/
+
+@[simp] theorem rotateLeft_replicate (n) (a : α) : rotateLeft (replicate m a) n = replicate m a := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    suffices 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m by
+      simpa [rotateLeft]
+    intro h
+    rw [Nat.min_eq_left (Nat.le_of_lt (Nat.mod_lt _ (by omega)))]
+    have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
+    omega
+
+/-! ### rotateLeft -/
+
+@[simp] theorem rotateRight_replicate (n) (a : α) : rotateRight (replicate m a) n = replicate m a := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    suffices 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m by
+      simpa [rotateRight]
+    intro h
+    have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
+    rw [Nat.min_eq_left (by omega)]
+    omega
+
 /-! ### zipWith -/
 
 @[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
@@ -305,10 +336,32 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
   induction l₁ generalizing l₂ <;> cases l₂ <;>
     simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
 
+theorem zipWith_eq_zipWith_take_min : ∀ (l₁ : List α) (l₂ : List β),
+    zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
+  | [], _ => by simp
+  | _, [] => by simp
+  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zipWith_eq_zipWith_take_min l₁ l₂]
+
+@[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
+    zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
+  rw [zipWith_eq_zipWith_take_min]
+  simp
+
 /-! ### zip -/
 
 @[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
     length (zip l₁ l₂) = min (length l₁) (length l₂) := by
   simp [zip]
 
+theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
+    zip l₁ l₂ = zip (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
+  | [], _ => by simp
+  | _, [] => by simp
+  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zip_eq_zip_take_min l₁ l₂]
+
+@[simp] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
+    zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
+  rw [zip_eq_zip_take_min]
+  simp
+
 end List

src/Init/Data/Nat/Lemmas.lean

@@ -212,13 +212,19 @@ instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem min_zero (a) : min a 0 = 0 := Nat.min_eq_right (Nat.zero_le _)
 
-protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
+@[simp] protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
   | 0, _, _ => by rw [Nat.zero_min, Nat.zero_min, Nat.zero_min]
   | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
   | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..
 instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 
+@[simp] protected theorem min_self_assoc {m n : Nat} : min m (min m n) = min m n := by
+  rw [← Nat.min_assoc, Nat.min_self]
+
+@[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
+  rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
+
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
   | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]

src/Init/Data/Option/Instances.lean

@@ -26,7 +26,7 @@ instance : Membership α (Option α) := ⟨fun a b => b = some a⟩
 instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
   inferInstanceAs <| Decidable (o = some j)
 
-theorem isNone_iff_eq_none {o : Option α} : o.isNone ↔ o = none :=
+@[simp] theorem isNone_iff_eq_none {o : Option α} : o.isNone ↔ o = none :=
   ⟨Option.eq_none_of_isNone, fun e => e.symm ▸ rfl⟩
 
 theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp; rfl

src/Lean/Elab/CheckTactic.lean

@@ -17,6 +17,7 @@ namespace Lean.Elab.CheckTactic
 
 open Lean.Meta CheckTactic
 open Lean.Elab.Tactic
+open Lean.Elab.Term
 open Lean.Elab.Command
 
 @[builtin_command_elab Lean.Parser.checkTactic]
@@ -24,7 +25,7 @@ def elabCheckTactic : CommandElab := fun stx => do
   let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
   withoutModifyingEnv $ do
     runTermElabM $ fun _vars => do
-      let u ← Lean.Elab.Term.elabTerm t none
+      let u ← withSynthesize (postpone := .no) <| Lean.Elab.Term.elabTerm t none
       let type ← inferType u
       let checkGoalType ← mkCheckGoalType u type
       let mvar ← mkFreshExprMVar (.some checkGoalType)

tests/lean/run/list_simp.lean

@@ -0,0 +1,346 @@
+open List
+
+variable {α : Type _}
+variable {x y z : α}
+variable (l l₁ l₂ l₃ : List α)
+
+variable (m n : Nat)
+
+/-! ## Preliminaries -/
+
+/-! ### cons -/
+
+/-! ### length -/
+
+/-! ### L[i] and L[i]? -/
+
+/-! ### mem -/
+
+/-! ### set -/
+
+/-! ### foldlM and foldrM -/
+
+/-! ### foldl and foldr -/
+
+/-! ### Equality -/
+
+/-! ### Lexicographic order -/
+
+/-! ## Getters -/
+
+#check_simp [x, y, x, y][0] ~> x
+#check_simp [x, y, x, y][1] ~> y
+#check_simp [x, y, x, y][2] ~> x
+#check_simp [x, y, x, y][3] ~> y
+
+#check_simp [x, y, x, y][0]? ~> some x
+#check_simp [x, y, x, y][1]? ~> some y
+#check_simp [x, y, x, y][2]? ~> some x
+#check_simp [x, y, x, y][3]? ~> some y
+
+/-! ### get, get!, get?, getD -/
+
+/-! ### getLast, getLast!, getLast?, getLastD -/
+
+/-! ## Head and tail -/
+
+/-! ### head, head!, head?, headD -/
+
+/-! ### tail!, tail?, tailD -/
+
+/-! ## Basic operations -/
+
+/-! ### map -/
+
+/-! ### filter -/
+
+/-! ### filterMap -/
+
+/-! ### append -/
+
+/-! ### concat -/
+
+/-! ### join -/
+
+/-! ### bind -/
+
+/-! ### replicate -/
+
+#check_simp replicate 0 x ~> []
+#check_simp replicate 1 x ~> [x]
+
+-- `∈` and `contains
+
+#check_simp y ∈ replicate 0 x ~> False
+
+variable [BEq α] in
+#check_simp (replicate 0 x).contains y ~> false
+
+variable [BEq α] [LawfulBEq α] in
+#check_simp (replicate 0 x).contains y ~> false
+
+#check_simp y ∈ replicate 7 x ~> y = x
+
+variable [BEq α] in
+#check_simp (replicate 7 x).contains y ~> y == x
+
+variable [BEq α] [LawfulBEq α] in
+#check_simp (replicate 7 x).contains y ~> y == x
+
+-- `getElem` and `getElem?`
+
+variable (h : n < m) (w) in
+#check_tactic (replicate m x)[n]'w ~> x by simp [h]
+
+variable (h : n < m) in
+#check_tactic (replicate m x)[n]? ~> some x by simp [h]
+
+#check_simp (replicate 7 x)[5] ~> x
+
+#check_simp (replicate 7 x)[5]? ~> some x
+
+-- injectivity
+
+#check_simp replicate 3 x = replicate 7 x ~> False
+#check_simp replicate 3 x = replicate 3 y ~> x = y
+#check_simp replicate 3 "1" = replicate 3 "1" ~> True
+#check_simp replicate n x = replicate m y ~> n = m ∧ (n = 0 ∨ x = y)
+
+-- append
+
+#check_simp replicate n x ++ replicate m x ~> replicate (n + m) x
+
+-- map
+
+#check_simp (replicate n "x").map (fun s => s ++ s) ~> replicate n "xx"
+
+-- filter
+
+#check_simp (replicate n [1]).filter (fun s => s.length = 1) ~> replicate n [1]
+#check_simp (replicate n [1]).filter (fun s => s.length = 2) ~> []
+
+-- filterMap
+
+#check_simp (replicate n [1]).filterMap (fun s => if s.length = 1 then some s else none) ~> replicate n [1]
+#check_simp (replicate n [1]).filterMap (fun s => if s.length = 2 then some s else none) ~> []
+
+-- join
+
+#check_simp (replicate n (replicate m x)).join ~> replicate (n * m) x
+#check_simp (replicate 1 (replicate m x)).join ~> replicate m x
+#check_simp (replicate n (replicate 1 x)).join ~> replicate n x
+#check_simp (replicate n (replicate 0 x)).join ~> []
+#check_simp (replicate 0 (replicate m x)).join ~> []
+#check_simp (replicate 0 (replicate 0 x)).join ~> []
+
+-- isEmpty
+
+#check_simp (replicate (n + 1) x).isEmpty ~> false
+#check_simp (replicate 0 x).isEmpty ~> true
+variable (h : ¬ n = 0) in -- It would be nice if this also worked with `h : 0 < n`
+#check_tactic (replicate n x).isEmpty ~> false by simp [h]
+
+-- reverse
+
+#check_simp (replicate n x).reverse ~> replicate n x
+
+-- dropLast
+
+#check_simp (replicate 0 x).dropLast ~> []
+#check_simp (replicate n x).dropLast ~> replicate (n-1) x
+#check_simp (replicate (n+1) x).dropLast ~> replicate n x
+
+-- isPrefixOf
+
+variable [BEq α] [LawfulBEq α] in
+#check_simp isPrefixOf [x, y, x] (replicate n x) ~> decide (3 ≤ n) && y == x
+
+attribute [local simp] isPrefixOf_cons₂ in
+variable [BEq α] [LawfulBEq α] in
+#check_simp isPrefixOf [x, y, x] (replicate (n+3) x) ~> y == x
+
+-- isSuffixOf
+
+variable [BEq α] [LawfulBEq α] in
+#check_simp isSuffixOf [x, y, x] (replicate n x) ~> decide (3 ≤ n) && y == x
+
+-- rotateLeft
+
+#check_simp (replicate n x).rotateLeft m ~> replicate n x
+
+-- rotateRight
+
+#check_simp (replicate n x).rotateRight m ~> replicate n x
+
+-- replace
+
+variable [BEq α] [LawfulBEq α] in
+#check_simp (replicate (n+1) x).replace x y ~> y :: replicate n x
+
+#check_simp (replicate n "1").replace "2" "3" ~> (replicate n "1")
+
+-- insert
+
+variable [BEq α] [LawfulBEq α] (h : 0 < n) in
+#check_tactic (replicate n x).insert x ~> replicate n x by simp [h]
+
+#check_simp (replicate n "1").insert "2" ~> "2" :: replicate n "1"
+
+-- erase
+
+variable [BEq α] [LawfulBEq α] in
+#check_simp (replicate (n+1) x).erase x ~> replicate n x
+
+#check_simp (replicate n "1").erase "2" ~> replicate n "1"
+
+-- find?
+
+#check_simp (replicate (n+1) x).find? (fun _ => true) ~> some x
+#check_simp (replicate (n+1) x).find? (fun _ => false) ~> none
+
+variable {p : α → Bool} (w : p x) in
+#check_tactic (replicate (n+1) x).find? p ~> some x by simp [w]
+variable {p : α → Bool} (w : ¬ p x) in
+#check_tactic (replicate (n+1) x).find? p ~> none by simp [w]
+
+variable (h : 0 < n) in
+#check_tactic (replicate n x).find? (fun _ => true) ~> some x by simp [h]
+variable (h : 0 < n) in
+#check_tactic (replicate n x).find? (fun _ => false) ~> none by simp [h]
+
+variable {p : α → Bool} (w : p x) (h : 0 < n) in
+#check_tactic (replicate n x).find? p ~> some x by simp [w, h]
+variable {p : α → Bool} (w : ¬ p x) (h : 0 < n) in
+#check_tactic (replicate n x).find? p ~> none by simp [w, h]
+
+-- findSome?
+
+#check_simp (replicate (n+1) x).findSome? (fun x => some x) ~> some x
+#check_simp (replicate (n+1) x).findSome? (fun _ => none) ~> none
+
+variable {f : α → Option β} (w : (f x).isSome) in
+#check_tactic (replicate (n+1) x).findSome? f ~> f x by simp [w]
+variable {f : α → Option β} (w : (f x).isNone) in
+#check_tactic (replicate (n+1) x).findSome? f ~> none by simp_all [w]
+
+variable (h : 0 < n) in
+#check_tactic (replicate n x).findSome? (fun x => some x) ~> some x by simp [h]
+variable (h : 0 < n) in
+#check_tactic (replicate n x).findSome? (fun _ => none) ~> none by simp [h]
+
+variable {f : α → Option β} (w : (f x).isSome) (h : 0 < n) in
+#check_tactic (replicate n x).findSome? f ~> f x by simp [w, h]
+variable {f : α → Option β} (w : (f x).isNone) (h : 0 < n) in
+#check_tactic (replicate n x).findSome? f ~> none by simp_all [w, h]
+
+-- lookup
+
+variable [BEq α] [LawfulBEq α] in
+#check_simp (replicate (n+1) (x, y)).lookup x ~> some y
+
+variable [BEq α] [LawfulBEq α] (h : 0 < n) in
+#check_tactic (replicate n (x, y)).lookup x ~> some y by simp [h]
+
+#check_simp (replicate n ("1", "2")).lookup "3" ~> none
+
+-- zip
+
+#check_simp (replicate n x).zip (replicate n y) ~> replicate n (x, y)
+#check_simp (replicate n x).zip (replicate m y) ~> replicate (min n m) (x, y)
+variable (h : n ≤ m) in
+#check_tactic (replicate n x).zip (replicate m y) ~> replicate n (x, y) by simp [h, Nat.min_eq_left]
+
+-- zipWith
+section
+variable (f : α → α → α)
+
+#check_simp zipWith f (replicate n x) (replicate n y) ~> replicate n (f x y)
+#check_simp zipWith f (replicate n x) (replicate m y) ~> replicate (min n m) (f x y)
+variable (h : n ≤ m) in
+#check_tactic zipWith f (replicate n x) (replicate m y) ~> replicate n (f x y) by simp [h, Nat.min_eq_left]
+
+-- unzip
+#check_simp unzip (replicate n (x, y)) ~> (replicate n x, replicate n y)
+
+-- minimum?
+
+#check_simp (replicate (n+1) 7).minimum? ~> some 7
+
+variable (h : 0 < n) in
+#check_tactic (replicate n 7).minimum? ~> some 7 by simp [h]
+
+-- maximum?
+
+#check_simp (replicate (n+1) 7).maximum? ~> some 7
+
+variable (h : 0 < n) in
+#check_tactic (replicate n 7).maximum? ~> some 7 by simp [h]
+
+end
+
+/-! ### reverse -/
+
+/-! ## List membership -/
+
+/-! ### elem / contains -/
+
+/-! ## Sublists -/
+
+/-! ### take and drop -/
+
+/-! ### takeWhile and dropWhile -/
+
+/-! ### partition -/
+
+/-! ### dropLast  -/
+
+/-! ### isPrefixOf -/
+
+/-! ### isSuffixOf -/
+
+variable [BEq α] in
+#check_simp ([] : List α).isSuffixOf l ~> true
+
+/-! ### rotateLeft -/
+
+/-! ### rotateRight -/
+
+/-! ## Manipulating elements -/
+
+/-! ### replace -/
+
+/-! ### insert -/
+
+/-! ### erase -/
+
+/-! ### find? -/
+
+/-! ### findSome? -/
+
+/-! ### lookup -/
+
+/-! ## Logic -/
+
+/-! ### any / all -/
+
+/-! ## Zippers -/
+
+/-! ### zip -/
+
+/-! ### zipWith -/
+
+/-! ### zipWithAll -/
+
+/-! ## Ranges and enumeration -/
+
+/-! ### enumFrom -/
+
+/-! ### minimum? -/
+
+/-! ### maximum? -/
+
+/-! ## Monadic operations -/
+
+/-! ### mapM -/
+
+/-! ### forM -/