Merge remote-tracking branch 'origin/master' into array_swap_docstring

It addresses a performance issue at
https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym20.lean

src/Init/ByCases.lean

@@ -67,12 +67,8 @@ theorem ite_some_none_eq_none [Decidable P] :
 -- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
 theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
     (if h : P then some (x h) else none) = none ↔ ¬P := by
-  simp only [dite_eq_right_iff]
-  rfl
+  simp
 
 @[simp] theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
     (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
-  by_cases h : P <;> simp only [h, dite_cond_eq_true, dite_cond_eq_false, Option.some.injEq,
-    false_iff, not_exists]
-  case pos => exact ⟨fun h_eq ↦ Exists.intro h h_eq, fun h_exists => h_exists.2⟩
-  case neg => exact fun h_false _ ↦ h_false
+  by_cases h : P <;> simp [h]

src/Init/Core.lean

@@ -1204,7 +1204,7 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 /-! # Dependent products -/
 
-theorem PSigma.exists {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
+theorem PSigma.exists {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
   | ⟨x, hx⟩ => ⟨x, hx⟩
 
 @[deprecated PSigma.exists (since := "2024-07-27")]

src/Init/Data/Array/Basic.lean

@@ -108,7 +108,7 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   a'.set (size_set a i v₂ ▸ j) v₁
 
 /--
-Swaps two entries in an array, or panics if either index is out of bounds.
+Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
 
 This will perform the update destructively provided that `a` has a reference
 count of 1 when called.

src/Init/Data/Array/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro
 prelude
 import Init.Data.Nat.MinMax
 import Init.Data.Nat.Lemmas
-import Init.Data.List.Lemmas
+import Init.Data.List.Monadic
 import Init.Data.Fin.Basic
 import Init.Data.Array.Mem
 import Init.TacticsExtra

src/Init/Data/Array/TakeDrop.lean

@@ -5,7 +5,7 @@ Authors: Markus Himmel
 -/
 prelude
 import Init.Data.Array.Lemmas
-import Init.Data.List.TakeDrop
+import Init.Data.List.Nat.TakeDrop
 
 namespace Array
 

src/Init/Data/List.lean

@@ -4,13 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Data.List.Attach
 import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
-import Init.Data.List.Lemmas
-import Init.Data.List.Attach
+import Init.Data.List.Count
+import Init.Data.List.Erase
+import Init.Data.List.Find
 import Init.Data.List.Impl
-import Init.Data.List.TakeDrop
-import Init.Data.List.Notation
-import Init.Data.List.Range
+import Init.Data.List.Lemmas
+import Init.Data.List.MinMax
+import Init.Data.List.Monadic
 import Init.Data.List.Nat
+import Init.Data.List.Notation
+import Init.Data.List.Pairwise
+import Init.Data.List.Sublist
+import Init.Data.List.TakeDrop
+import Init.Data.List.Zip

src/Init/Data/List/Attach.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 prelude
-import Init.Data.List.Lemmas
+import Init.Data.List.Count
 import Init.Data.Subtype
 
 namespace List

src/Init/Data/List/Count.lean

@@ -0,0 +1,242 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Sublist
+
+/-!
+# Lemmas about `List.countP` and `List.count`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ### countP -/
+section countP
+
+variable (p q : α → Bool)
+
+@[simp] theorem countP_nil : countP p [] = 0 := rfl
+
+protected theorem countP_go_eq_add (l) : countP.go p l n = n + countP.go p l 0 := by
+  induction l generalizing n with
+  | nil => rfl
+  | cons head tail ih =>
+    unfold countP.go
+    rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
+    if h : p head then simp [h, Nat.add_assoc] else simp [h]
+
+@[simp] theorem countP_cons_of_pos (l) (pa : p a) : countP p (a :: l) = countP p l + 1 := by
+  have : countP.go p (a :: l) 0 = countP.go p l 1 := show cond .. = _ by rw [pa]; rfl
+  unfold countP
+  rw [this, Nat.add_comm, List.countP_go_eq_add]
+
+@[simp] theorem countP_cons_of_neg (l) (pa : ¬p a) : countP p (a :: l) = countP p l := by
+  simp [countP, countP.go, pa]
+
+theorem countP_cons (a : α) (l) : countP p (a :: l) = countP p l + if p a then 1 else 0 := by
+  by_cases h : p a <;> simp [h]
+
+theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a => ¬p a) l := by
+  induction l with
+  | nil => rfl
+  | cons x h ih =>
+    if h : p x then
+      rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
+      · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
+      · simp only [h, not_true_eq_false, decide_False, not_false_eq_true]
+    else
+      rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
+      · rfl
+      · simp only [h, not_false_eq_true, decide_True]
+
+theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
+  induction l with
+  | nil => rfl
+  | cons x l ih =>
+    if h : p x
+    then rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos h, length]
+    else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg h]
+
+theorem countP_le_length : countP p l ≤ l.length := by
+  simp only [countP_eq_length_filter]
+  apply length_filter_le
+
+@[simp] theorem countP_append (l₁ l₂) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
+  simp only [countP_eq_length_filter, filter_append, length_append]
+
+theorem countP_pos : 0 < countP p l ↔ ∃ a ∈ l, p a := by
+  simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
+
+theorem countP_eq_zero : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
+  simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil]
+
+theorem countP_eq_length : countP p l = l.length ↔ ∀ a ∈ l, p a := by
+  rw [countP_eq_length_filter, filter_length_eq_length]
+
+theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ := by
+  simp only [countP_eq_length_filter]
+  apply s.filter _ |>.length_le
+
+theorem countP_filter (l : List α) :
+    countP p (filter q l) = countP (fun a => p a ∧ q a) l := by
+  simp only [countP_eq_length_filter, filter_filter]
+
+@[simp] theorem countP_true {l : List α} : (l.countP fun _ => true) = l.length := by
+  rw [countP_eq_length]
+  simp
+
+@[simp] theorem countP_false {l : List α} : (l.countP fun _ => false) = 0 := by
+  rw [countP_eq_zero]
+  simp
+
+@[simp] theorem countP_map (p : β → Bool) (f : α → β) :
+    ∀ l, countP p (map f l) = countP (p ∘ f) l
+  | [] => rfl
+  | a :: l => by rw [map_cons, countP_cons, countP_cons, countP_map p f l]; rfl
+
+variable {p q}
+
+theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
+  induction l with
+  | nil => apply Nat.le_refl
+  | cons a l ihl =>
+    rw [forall_mem_cons] at h
+    have ⟨ha, hl⟩ := h
+    simp [countP_cons]
+    cases h : p a
+    · simp only [Bool.false_eq_true, ↓reduceIte, Nat.add_zero]
+      apply Nat.le_trans ?_ (Nat.le_add_right _ _)
+      apply ihl hl
+    · simp only [↓reduceIte, ha h, succ_le_succ_iff]
+      apply ihl hl
+
+theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l :=
+  Nat.le_antisymm
+    (countP_mono_left fun x hx => (h x hx).1)
+    (countP_mono_left fun x hx => (h x hx).2)
+
+end countP
+
+/-! ### count -/
+section count
+
+variable [BEq α]
+
+@[simp] theorem count_nil (a : α) : count a [] = 0 := rfl
+
+theorem count_cons (a b : α) (l : List α) :
+    count a (b :: l) = count a l + if b == a then 1 else 0 := by
+  simp [count, countP_cons]
+
+theorem count_tail : ∀ (l : List α) (a : α) (h : l ≠ []),
+      l.tail.count a = l.count a - if l.head h == a then 1 else 0
+  | head :: tail, a, _ => by simp [count_cons]
+
+theorem count_le_length (a : α) (l : List α) : count a l ≤ l.length := countP_le_length _
+
+theorem Sublist.count_le (h : l₁ <+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.countP_le _
+
+theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) :=
+  (sublist_cons_self _ _).count_le _
+
+theorem count_singleton (a b : α) : count a [b] = if b == a then 1 else 0 := by
+  simp [count_cons]
+
+@[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
+  countP_append _
+
+variable [LawfulBEq α]
+
+@[simp] theorem count_cons_self (a : α) (l : List α) : count a (a :: l) = count a l + 1 := by
+  simp [count_cons]
+
+@[simp] theorem count_cons_of_ne (h : a ≠ b) (l : List α) : count a (b :: l) = count a l := by
+  simp only [count_cons, cond_eq_if, beq_iff_eq]
+  split <;> simp_all
+
+theorem count_singleton_self (a : α) : count a [a] = 1 := by simp
+
+theorem count_concat_self (a : α) (l : List α) :
+    count a (concat l a) = (count a l) + 1 := by simp
+
+@[simp]
+theorem count_pos_iff_mem {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by
+  simp only [count, countP_pos, beq_iff_eq, exists_eq_right]
+
+theorem count_eq_zero_of_not_mem {a : α} {l : List α} (h : a ∉ l) : count a l = 0 :=
+  Decidable.byContradiction fun h' => h <| count_pos_iff_mem.1 (Nat.pos_of_ne_zero h')
+
+theorem not_mem_of_count_eq_zero {a : α} {l : List α} (h : count a l = 0) : a ∉ l :=
+  fun h' => Nat.ne_of_lt (count_pos_iff_mem.2 h') h.symm
+
+theorem count_eq_zero {l : List α} : count a l = 0 ↔ a ∉ l :=
+  ⟨not_mem_of_count_eq_zero, count_eq_zero_of_not_mem⟩
+
+theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b := by
+  rw [count, countP_eq_length]
+  refine ⟨fun h b hb => Eq.symm ?_, fun h b hb => ?_⟩
+  · simpa using h b hb
+  · rw [h b hb, beq_self_eq_true]
+
+@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n :=
+  (count_eq_length.2 <| fun _ h => (eq_of_mem_replicate h).symm).trans (length_replicate ..)
+
+theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if b == a then n else 0 := by
+  split <;> (rename_i h; simp only [beq_iff_eq] at h)
+  · exact ‹b = a› ▸ count_replicate_self ..
+  · exact count_eq_zero.2 <| mt eq_of_mem_replicate (Ne.symm h)
+
+theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a := by
+  simp only [count, countP_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
+  exact ⟨trivial, fun _ h => h.2⟩
+
+theorem filter_eq {α} [DecidableEq α] (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
+  filter_beq l a
+
+theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · exact ((replicate_sublist_replicate a).2 h).trans <| filter_beq l a ▸ filter_sublist _
+  · simpa only [count_replicate_self] using h.count_le a
+
+theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = length l) :
+    replicate (count a l) a = l :=
+  (le_count_iff_replicate_sublist.mp (Nat.le_refl _)).eq_of_length <|
+    (length_replicate (count a l) a).trans h
+
+@[simp] theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l := by
+  rw [count, countP_filter]; congr; funext b
+  simp; rintro rfl; exact h
+
+theorem count_le_count_map [DecidableEq β] (l : List α) (f : α → β) (x : α) :
+    count x l ≤ count (f x) (map f l) := by
+  rw [count, count, countP_map]
+  apply countP_mono_left; simp (config := { contextual := true })
+
+theorem count_erase (a b : α) :
+    ∀ l : List α, count a (l.erase b) = count a l - if b == a then 1 else 0
+  | [] => by simp
+  | c :: l => by
+    rw [erase_cons]
+    if hc : c = b then
+      have hc_beq := (beq_iff_eq _ _).mpr hc
+      rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
+    else
+      have hc_beq := beq_false_of_ne hc
+      simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
+      if ha : b = a then
+        rw [ha, eq_comm] at hc
+        rw [if_pos ((beq_iff_eq _ _).2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]
+      else
+        rw [if_neg (by simpa using ha), Nat.sub_zero, Nat.sub_zero]
+
+@[simp] theorem count_erase_self (a : α) (l : List α) :
+    count a (List.erase l a) = count a l - 1 := by rw [count_erase, if_pos (by simp)]
+
+@[simp] theorem count_erase_of_ne (ab : a ≠ b) (l : List α) : count a (l.erase b) = count a l := by
+  rw [count_erase, if_neg (by simpa using ab.symm), Nat.sub_zero]
+
+end count

src/Init/Data/List/Erase.lean

@@ -0,0 +1,445 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
+  Yury Kudryashov
+-/
+prelude
+import Init.Data.List.Pairwise
+
+/-!
+# Lemmas about `List.eraseP` and `List.erase`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ### eraseP -/
+
+@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl
+
+theorem eraseP_cons (a : α) (l : List α) :
+    (a :: l).eraseP p = bif p a then l else a :: l.eraseP p := rfl
+
+@[simp] theorem eraseP_cons_of_pos {l : List α} {p} (h : p a) : (a :: l).eraseP p = l := by
+  simp [eraseP_cons, h]
+
+@[simp] theorem eraseP_cons_of_neg {l : List α} {p} (h : ¬p a) :
+    (a :: l).eraseP p = a :: l.eraseP p := by simp [eraseP_cons, h]
+
+theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l := by
+  induction l with
+  | nil => rfl
+  | cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]
+
+theorem exists_of_eraseP : ∀ {l : List α} {a} (al : a ∈ l) (pa : p a),
+    ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂
+  | b :: l, a, al, pa =>
+    if pb : p b then
+      ⟨b, [], l, forall_mem_nil _, pb, by simp [pb]⟩
+    else
+      match al with
+      | .head .. => nomatch pb pa
+      | .tail _ al =>
+        let ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ := exists_of_eraseP al pa
+        ⟨c, b::l₁, l₂, (forall_mem_cons ..).2 ⟨pb, h₁⟩,
+          h₂, by rw [h₃, cons_append], by simp [pb, h₄]⟩
+
+theorem exists_or_eq_self_of_eraseP (p) (l : List α) :
+    l.eraseP p = l ∨
+    ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂ :=
+  if h : ∃ a ∈ l, p a then
+    let ⟨_, ha, pa⟩ := h
+    .inr (exists_of_eraseP ha pa)
+  else
+    .inl (eraseP_of_forall_not (h ⟨·, ·, ·⟩))
+
+@[simp] theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) :
+    length (l.eraseP p) = length l - 1 := by
+  let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
+  rw [e₂]; simp [length_append, e₁]; rfl
+
+theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length := by
+  split <;> rename_i h
+  · simp only [any_eq_true] at h
+    obtain ⟨x, m, h⟩ := h
+    simp [length_eraseP_of_mem m h]
+  · simp only [any_eq_true] at h
+    rw [eraseP_of_forall_not]
+    simp_all
+
+theorem eraseP_sublist (l : List α) : l.eraseP p <+ l := by
+  match exists_or_eq_self_of_eraseP p l with
+  | .inl h => rw [h]; apply Sublist.refl
+  | .inr ⟨c, l₁, l₂, _, _, h₃, h₄⟩ => rw [h₄, h₃]; simp
+
+theorem eraseP_subset (l : List α) : l.eraseP p ⊆ l := (eraseP_sublist l).subset
+
+protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p
+  | .slnil => Sublist.refl _
+  | .cons a s => by
+    by_cases h : p a
+    · simpa [h] using s.eraseP.trans (eraseP_sublist _)
+    · simpa [h] using s.eraseP.cons _
+  | .cons₂ a s => by
+    by_cases h : p a
+    · simpa [h] using s
+    · simpa [h] using s.eraseP
+
+theorem length_eraseP_le (l : List α) : (l.eraseP p).length ≤ l.length :=
+  l.eraseP_sublist.length_le
+
+theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset _ ·)
+
+@[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
+  refine ⟨mem_of_mem_eraseP, fun al => ?_⟩
+  match exists_or_eq_self_of_eraseP p l with
+  | .inl h => rw [h]; assumption
+  | .inr ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ =>
+    rw [h₄]; rw [h₃] at al
+    have : a ≠ c := fun h => (h ▸ pa).elim h₂
+    simp [this] at al; simp [al]
+
+@[simp] theorem eraseP_eq_self_iff {p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a := by
+  rw [← Sublist.length_eq (eraseP_sublist l), length_eraseP]
+  split <;> rename_i h
+  · simp only [any_eq_true, length_eq_zero] at h
+    constructor
+    · intro; simp_all [Nat.sub_one_eq_self]
+    · intro; obtain ⟨x, m, h⟩ := h; simp_all
+  · simp_all
+
+theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map f (l.eraseP (p ∘ f))
+  | [] => rfl
+  | b::l => by by_cases h : p (f b) <;> simp [h, eraseP_map f l, eraseP_cons_of_pos]
+
+theorem eraseP_filterMap (f : α → Option β) : ∀ (l : List α),
+    (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false))
+  | [] => rfl
+  | a::l => by
+    rw [filterMap_cons, eraseP_cons]
+    split <;> rename_i h
+    · simp [h, eraseP_filterMap]
+    · rename_i b
+      rw [h, eraseP_cons]
+      by_cases w : p b
+      · simp [w]
+      · simp only [w, cond_false]
+        rw [filterMap_cons_some h, eraseP_filterMap]
+
+theorem eraseP_filter (f : α → Bool) (l : List α) :
+    (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x)) := by
+  rw [← filterMap_eq_filter, eraseP_filterMap]
+  congr
+  ext x
+  simp only [Option.guard]
+  split <;> split at * <;> simp_all
+
+theorem eraseP_append_left {a : α} (pa : p a) :
+    ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂
+  | x :: xs, l₂, h => by
+    by_cases h' : p x <;> simp [h']
+    rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]
+    intro | rfl => exact pa
+
+theorem eraseP_append_right :
+    ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
+  | [],      l₂, _ => rfl
+  | x :: xs, l₂, h => by
+    simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]
+
+theorem eraseP_append (l₁ l₂ : List α) :
+    (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p := by
+  split <;> rename_i h
+  · simp only [any_eq_true] at h
+    obtain ⟨x, m, h⟩ := h
+    rw [eraseP_append_left h _ m]
+  · simp only [any_eq_true] at h
+    rw [eraseP_append_right _]
+    simp_all
+
+theorem eraseP_eq_iff {p} {l : List α} :
+    l.eraseP p = l' ↔
+      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
+        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by
+  cases exists_or_eq_self_of_eraseP p l with
+  | inl h =>
+    constructor
+    · intro h'
+      left
+      exact ⟨eraseP_eq_self_iff.1 h, by simp_all⟩
+    · rintro (⟨-, rfl⟩ | ⟨a, l₁, l₂, h₁, h₂, rfl, rfl⟩)
+      · assumption
+      · rw [eraseP_append_right _ h₁, eraseP_cons_of_pos h₂]
+  | inr h =>
+    obtain ⟨a, l₁, l₂, h₁, h₂, w₁, w₂⟩ := h
+    rw [w₂]
+    subst w₁
+    constructor
+    · rintro rfl
+      right
+      refine ⟨a, l₁, l₂, ?_⟩
+      simp_all
+    · rintro (h | h)
+      · simp_all
+      · obtain ⟨a', l₁', l₂', h₁', h₂', h, rfl⟩ := h
+        have p : l₁ = l₁' := by
+          have q : l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂) := by
+            rw [takeWhile_append_of_pos (by simp_all),
+              takeWhile_cons_of_neg (by simp [h₂]), append_nil]
+          have q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂') := by
+            rw [takeWhile_append_of_pos (by simpa using h₁'),
+              takeWhile_cons_of_neg (by simp [h₂']), append_nil]
+          simp [h] at q
+          rw [q', q]
+        subst p
+        simp_all
+
+@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
+    (replicate n a).eraseP p = replicate (n - 1) a := by
+  cases n <;> simp [replicate_succ, h]
+
+@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
+    (replicate n a).eraseP p = replicate n a := by
+  rw [eraseP_of_forall_not (by simp_all)]
+
+theorem Nodup.eraseP (p) : Nodup l → Nodup (l.eraseP p) :=
+  Nodup.sublist <| eraseP_sublist _
+
+theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
+    (l.eraseP p).eraseP q = (l.eraseP q).eraseP p := by
+  induction l with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [eraseP_cons]
+    by_cases h₁ : p a
+    · by_cases h₂ : q a
+      · simp_all
+      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
+    · by_cases h₂ : q a
+      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
+      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
+
+/-! ### erase -/
+section erase
+variable [BEq α]
+
+@[simp] theorem erase_cons_head [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l := by
+  simp [erase_cons]
+
+@[simp] theorem erase_cons_tail {a b : α} {l : List α} (h : ¬(b == a)) :
+    (b :: l).erase a = b :: l.erase a := by simp only [erase_cons, if_neg h]
+
+theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l
+  | [], _ => rfl
+  | b :: l, h => by
+    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]
+
+theorem erase_eq_eraseP' (a : α) (l : List α) : l.erase a = l.eraseP (· == a) := by
+  induction l
+  · simp
+  · next b t ih =>
+    rw [erase_cons, eraseP_cons, ih]
+    if h : b == a then simp [h] else simp [h]
+
+theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ l : List α,  l.erase a = l.eraseP (a == ·)
+  | [] => rfl
+  | b :: l => by
+    if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l]
+
+theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
+    ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂ := by
+  let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _)
+  rw [erase_eq_eraseP]; exact ⟨l₁, l₂, fun h => h₁ _ h (beq_self_eq_true _), eq_of_beq e ▸ h₂, h₃⟩
+
+@[simp] theorem length_erase_of_mem [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
+    length (l.erase a) = length l - 1 := by
+  rw [erase_eq_eraseP]; exact length_eraseP_of_mem h (beq_self_eq_true a)
+
+theorem length_erase [LawfulBEq α] (a : α) (l : List α) :
+    length (l.erase a) = if a ∈ l then length l - 1 else length l := by
+  rw [erase_eq_eraseP, length_eraseP]
+  split <;> split <;> simp_all
+
+theorem erase_sublist (a : α) (l : List α) : l.erase a <+ l :=
+  erase_eq_eraseP' a l ▸ eraseP_sublist ..
+
+theorem erase_subset (a : α) (l : List α) : l.erase a ⊆ l := (erase_sublist a l).subset
+
+theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a := by
+  simp only [erase_eq_eraseP']; exact h.eraseP
+
+theorem length_erase_le (a : α) (l : List α) : (l.erase a).length ≤ l.length :=
+  (erase_sublist a l).length_le
+
+theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset _ _ h
+
+@[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
+    a ∈ l.erase b ↔ a ∈ l :=
+  erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
+
+@[simp] theorem erase_eq_self_iff [LawfulBEq α] {l : List α} : l.erase a = l ↔ a ∉ l := by
+  rw [erase_eq_eraseP', eraseP_eq_self_iff]
+  simp
+
+theorem erase_filter [LawfulBEq α] (f : α → Bool) (l : List α) :
+    (filter f l).erase a = filter f (l.erase a) := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    by_cases h : a = x
+    · rw [erase_cons]
+      simp only [h, beq_self_eq_true, ↓reduceIte]
+      rw [filter_cons]
+      split
+      · rw [erase_cons_head]
+      · rw [erase_of_not_mem]
+        simp_all [mem_filter]
+    · rw [erase_cons_tail (by simpa using Ne.symm h), filter_cons, filter_cons]
+      split
+      · rw [erase_cons_tail (by simpa using Ne.symm h), ih]
+      · rw [ih]
+
+theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁) :
+    (l₁ ++ l₂).erase a = l₁.erase a ++ l₂ := by
+  simp [erase_eq_eraseP]; exact eraseP_append_left (beq_self_eq_true a) l₂ h
+
+theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a ∉ l₁) :
+    (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a) := by
+  rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right]
+  intros b h' h''; rw [eq_of_beq h''] at h; exact h h'
+
+theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
+    (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a := by
+  simp [erase_eq_eraseP, eraseP_append]
+
+theorem erase_comm [LawfulBEq α] (a b : α) (l : List α) :
+    (l.erase a).erase b = (l.erase b).erase a := by
+  if ab : a == b then rw [eq_of_beq ab] else ?_
+  if ha : a ∈ l then ?_ else
+    simp only [erase_of_not_mem ha, erase_of_not_mem (mt mem_of_mem_erase ha)]
+  if hb : b ∈ l then ?_ else
+    simp only [erase_of_not_mem hb, erase_of_not_mem (mt mem_of_mem_erase hb)]
+  match l, l.erase a, exists_erase_eq ha with
+  | _, _, ⟨l₁, l₂, ha', rfl, rfl⟩ =>
+    if h₁ : b ∈ l₁ then
+      rw [erase_append_left _ h₁, erase_append_left _ h₁,
+          erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head]
+    else
+      rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha',
+          erase_cons_tail ab, erase_cons_head]
+
+theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
+    l.erase a = l' ↔
+      (a ∉ l ∧ l = l') ∨
+        ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by
+  rw [erase_eq_eraseP', eraseP_eq_iff]
+  simp only [beq_iff_eq, forall_mem_ne', exists_and_left]
+  constructor
+  · rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, x, rfl, rfl⟩)
+    · left; simp_all
+    · right; refine ⟨l', h, x, by simp⟩
+  · rintro (⟨h, rfl⟩ | ⟨l₁, h, x, rfl, rfl⟩)
+    · left; simp_all
+    · right; refine ⟨a, l₁, h, by simp⟩
+
+@[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
+
+theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a) := by
+  induction d with
+  | nil => rfl
+  | cons m _n ih =>
+    rename_i b l
+    by_cases h : b = a
+    · subst h
+      rw [erase_cons_head, filter_cons_of_neg (by simp)]
+      apply Eq.symm
+      rw [filter_eq_self]
+      simpa [@eq_comm α] using m
+    · simp [beq_false_of_ne h, ih, h]
+
+theorem Nodup.mem_erase_iff [BEq α] [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
+  rw [Nodup.erase_eq_filter d, mem_filter, and_comm, bne_iff_ne]
+
+theorem Nodup.not_mem_erase [BEq α] [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
+  simpa using ((Nodup.mem_erase_iff h).mp H).left
+
+theorem Nodup.erase [BEq α] [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
+  Nodup.sublist <| erase_sublist _ _
+
+end erase
+
+/-! ### eraseIdx -/
+
+theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i) = length l - 1
+  | [], _, _ => rfl
+  | _::_, 0, _ => by simp [eraseIdx]
+  | x::xs, i+1, h => by
+    have : i < length xs := Nat.lt_of_succ_lt_succ h
+    simp [eraseIdx, ← Nat.add_one]
+    rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
+
+@[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl
+
+theorem eraseIdx_eq_take_drop_succ :
+    ∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1)
+  | nil, _ => by simp
+  | a::l, 0 => by simp
+  | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]
+
+theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
+  | [], _ => by simp
+  | a::l, 0 => by simp
+  | a::l, k + 1 => by simp [eraseIdx_sublist l k]
+
+theorem eraseIdx_subset (l : List α) (k : Nat) : eraseIdx l k ⊆ l := (eraseIdx_sublist l k).subset
+
+@[simp]
+theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ length l ≤ k
+  | [], _ => by simp
+  | a::l, 0 => by simp [(cons_ne_self _ _).symm]
+  | a::l, k + 1 => by simp [eraseIdx_eq_self]
+
+theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l := by
+  rw [eraseIdx_eq_self.2 h]
+
+theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
+    eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
+  induction l generalizing k with
+  | nil => simp_all
+  | cons x l ih =>
+    cases k with
+    | zero => rfl
+    | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_lt_succ_iff]
+
+theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤ k) (l' : List α) :
+    eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l) := by
+  induction l generalizing k with
+  | nil => simp_all
+  | cons x l ih =>
+    cases k with
+    | zero => simp_all
+    | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_sub_succ]
+
+protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
+    eraseIdx l k <+: eraseIdx l' k := by
+  rcases h with ⟨t, rfl⟩
+  if hkl : k < length l then
+    simp [eraseIdx_append_of_lt_length hkl]
+  else
+    rw [Nat.not_lt] at hkl
+    simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl]
+
+-- See also `mem_eraseIdx_iff_getElem` and `mem_eraseIdx_iff_getElem?` in
+-- `Init/Data/List/Nat/Basic.lean`.
+
+end List

src/Init/Data/List/Find.lean

@@ -0,0 +1,229 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Lemmas
+
+/-!
+# Lemmas about `List.find?`, `List.findSome?`, `List.findIdx`, `List.findIdx?`, and `List.indexOf`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ### 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_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 [*]
+
+theorem find?_some : ∀ {l}, find? p l = some a → p a
+  | b :: l, H => by
+    by_cases h : p b <;> simp [find?, h] at H
+    · exact H ▸ h
+    · exact find?_some H
+
+@[simp] theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
+  | b :: l, H => by
+    by_cases h : p b <;> simp [find?, h] at H
+    · exact H ▸ .head _
+    · exact .tail _ (mem_of_find?_eq_some H)
+
+@[simp] theorem find?_map (f : β → α) (l : List β) : find? p (l.map f) = (l.find? (p ∘ f)).map f := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [map_cons, find?]
+    by_cases h : p (f x) <;> simp [h, ih]
+
+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]
+
+theorem find?_isSome_of_sublist {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁.find? p).isSome → (l₂.find? p).isSome := by
+  induction h with
+  | slnil => simp
+  | cons a h ih
+  | cons₂ a h ih =>
+    simp only [find?]
+    split <;> simp_all
+
+/-! ### 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
+  | nil => simp_all
+  | cons h l ih =>
+    simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
+    split at w <;> simp_all
+
+@[simp] theorem findSome?_map (f : β → γ) (l : List β) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [map_cons, findSome?]
+    split <;> simp_all
+
+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 findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
+  simp [findSome?_replicate, Nat.ne_of_gt h]
+
+-- Argument is unused, but used to decide whether `simp` should unfold.
+@[simp] theorem find?_replicate_of_isSome (_ : (f a).isSome) : findSome? f (replicate n a) = if n = 0 then none else f a := by
+  simp [findSome?_replicate]
+
+@[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]
+
+theorem findSome?_isSome_of_sublist {l₁ l₂ : List α} (h : l₁ <+ l₂) :
+    (l₁.findSome? f).isSome → (l₂.findSome? f).isSome := by
+  induction h with
+  | slnil => simp
+  | cons a h ih
+  | cons₂ a h ih =>
+    simp only [findSome?]
+    split <;> simp_all
+
+/-! ### findIdx -/
+
+theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) :
+    (b :: l).findIdx p = bif p b then 0 else (l.findIdx p) + 1 := by
+  cases H : p b with
+  | true => simp [H, findIdx, findIdx.go]
+  | false => simp [H, findIdx, findIdx.go, findIdx_go_succ]
+where
+  findIdx_go_succ (p : α → Bool) (l : List α) (n : Nat) :
+      List.findIdx.go p l (n + 1) = (findIdx.go p l n) + 1 := by
+    cases l with
+    | nil => unfold findIdx.go; exact Nat.succ_eq_add_one n
+    | cons head tail =>
+      unfold findIdx.go
+      cases p head <;> simp only [cond_false, cond_true]
+      exact findIdx_go_succ p tail (n + 1)
+
+theorem findIdx_of_get?_eq_some {xs : List α} (w : xs.get? (xs.findIdx p) = some y) : p y := by
+  induction xs with
+  | nil => simp_all
+  | cons x xs ih => by_cases h : p x <;> simp_all [findIdx_cons]
+
+theorem findIdx_get {xs : List α} {w : xs.findIdx p < xs.length} :
+    p (xs.get ⟨xs.findIdx p, w⟩) :=
+  xs.findIdx_of_get?_eq_some (get?_eq_get w)
+
+theorem findIdx_lt_length_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
+    xs.findIdx p < xs.length := by
+  induction xs with
+  | nil => simp_all
+  | cons x xs ih =>
+    by_cases p x
+    · simp_all only [forall_exists_index, and_imp, mem_cons, exists_eq_or_imp, true_or,
+        findIdx_cons, cond_true, length_cons]
+      apply Nat.succ_pos
+    · simp_all [findIdx_cons]
+      refine Nat.succ_lt_succ ?_
+      obtain ⟨x', m', h'⟩ := h
+      exact ih x' m' h'
+
+theorem findIdx_get?_eq_get_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
+    xs.get? (xs.findIdx p) = some (xs.get ⟨xs.findIdx p, xs.findIdx_lt_length_of_exists h⟩) :=
+  get?_eq_get (findIdx_lt_length_of_exists h)
+
+  /-! ### findIdx? -/
+
+@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
+
+@[simp] theorem findIdx?_cons :
+    (x :: xs).findIdx? p i = if p x then some i else findIdx? p xs (i + 1) := rfl
+
+@[simp] theorem findIdx?_succ :
+    (xs : List α).findIdx? p (i+1) = (xs.findIdx? p i).map fun i => i + 1 := by
+  induction xs generalizing i with simp
+  | cons _ _ _ => split <;> simp_all
+
+theorem findIdx?_eq_some_iff (xs : List α) (p : α → Bool) :
+    xs.findIdx? p = some i ↔ (xs.take (i + 1)).map p = replicate i false ++ [true] := by
+  induction xs generalizing i with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, take_succ_cons, map_cons]
+    split <;> cases i <;> simp_all [replicate_succ, succ_inj']
+
+theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p = some i) :
+    match xs.get? i with | some a => p a | none => false := by
+  induction xs generalizing i with
+  | nil => simp_all
+  | cons x xs ih =>
+    simp_all only [findIdx?_cons, Nat.zero_add, findIdx?_succ]
+    split at w <;> cases i <;> simp_all [succ_inj']
+
+theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
+    ∀ i, match xs.get? i with | some a => ¬ p a | none => true := by
+  intro i
+  induction xs generalizing i with
+  | nil => simp_all
+  | cons x xs ih =>
+    simp_all only [Bool.not_eq_true, findIdx?_cons, Nat.zero_add, findIdx?_succ]
+    cases i with
+    | zero =>
+      split at w <;> simp_all
+    | succ i =>
+      simp only [get?_cons_succ]
+      apply ih
+      split at w <;> simp_all
+
+@[simp] theorem findIdx?_append :
+    (xs ++ ys : List α).findIdx? p =
+      (xs.findIdx? p <|> (ys.findIdx? p).map fun i => i + xs.length) := by
+  induction xs with simp
+  | cons _ _ _ => split <;> simp_all [Option.map_orElse, Option.map_map]; rfl
+
+@[simp] theorem findIdx?_replicate :
+    (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, Nat.zero_lt_succ, true_and]
+    split <;> simp_all
+
+/-! ### indexOf -/
+
+theorem indexOf_cons [BEq α] :
+    (x :: xs : List α).indexOf y = bif x == y then 0 else xs.indexOf y + 1 := by
+  dsimp [indexOf]
+  simp [findIdx_cons]
+
+end List

src/Init/Data/List/MinMax.lean

@@ -0,0 +1,153 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Lemmas
+
+/-!
+# Lemmas about `List.minimum?` and `List.maximum?.
+-/
+
+namespace List
+
+open Nat
+
+/-! ## Minima and maxima -/
+
+/-! ### minimum? -/
+
+@[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl
+
+-- We don't put `@[simp]` on `minimum?_cons`,
+-- because the definition in terms of `foldl` is not useful for proofs.
+theorem minimum?_cons [Min α] {xs : List α} : (x :: xs).minimum? = foldl min x xs := rfl
+
+@[simp] theorem minimum?_eq_none_iff {xs : List α} [Min α] : xs.minimum? = none ↔ xs = [] := by
+  cases xs <;> simp [minimum?]
+
+theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
+    {xs : List α} → xs.minimum? = some a → a ∈ xs := by
+  intro xs
+  match xs with
+  | nil => simp
+  | x :: xs =>
+    simp only [minimum?_cons, Option.some.injEq, List.mem_cons]
+    intro eq
+    induction xs generalizing x with
+    | nil =>
+      simp at eq
+      simp [eq]
+    | cons y xs ind =>
+      simp at eq
+      have p := ind _ eq
+      cases p with
+      | inl p =>
+        cases min_eq_or x y with | _ q => simp [p, q]
+      | inr p => simp [p, mem_cons]
+
+-- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
+
+theorem le_minimum?_iff [Min α] [LE α]
+    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
+    {xs : List α} → xs.minimum? = some a → ∀ x, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
+  | nil => by simp
+  | cons x xs => by
+    rw [minimum?]
+    intro eq y
+    simp only [Option.some.injEq] at eq
+    induction xs generalizing x with
+    | nil =>
+      simp at eq
+      simp [eq]
+    | cons z xs ih =>
+      simp at eq
+      simp [ih _ eq, le_min_iff, and_assoc]
+
+-- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
+-- and `le_min_iff`.
+theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+    (le_refl : ∀ a : α, a ≤ a)
+    (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
+    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
+    xs.minimum? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
+  refine ⟨fun h => ⟨minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h _).1 (le_refl _)⟩, ?_⟩
+  intro ⟨h₁, h₂⟩
+  cases xs with
+  | nil => simp at h₁
+  | cons x xs =>
+    exact congrArg some <| anti.1
+      ((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
+      (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
+
+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
+
+-- We don't put `@[simp]` on `maximum?_cons`,
+-- because the definition in terms of `foldl` is not useful for proofs.
+theorem maximum?_cons [Max α] {xs : List α} : (x :: xs).maximum? = foldl max x xs := rfl
+
+@[simp] theorem maximum?_eq_none_iff {xs : List α} [Max α] : xs.maximum? = none ↔ xs = [] := by
+  cases xs <;> simp [maximum?]
+
+theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
+    {xs : List α} → xs.maximum? = some a → a ∈ xs
+  | nil => by simp
+  | cons x xs => by
+    rw [maximum?]; rintro ⟨⟩
+    induction xs generalizing x with simp at *
+    | cons y xs ih =>
+      rcases ih (max x y) with h | h <;> simp [h]
+      simp [← or_assoc, min_eq_or x y]
+
+-- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
+
+theorem maximum?_le_iff [Max α] [LE α]
+    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
+    {xs : List α} → xs.maximum? = some a → ∀ x, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
+  | nil => by simp
+  | cons x xs => by
+    rw [maximum?]; rintro ⟨⟩ y
+    induction xs generalizing x with
+    | nil => simp
+    | cons y xs ih => simp [ih, max_le_iff, and_assoc]
+
+-- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
+-- and `le_min_iff`.
+theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+    (le_refl : ∀ a : α, a ≤ a)
+    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
+    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
+    xs.maximum? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
+  refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h _).1 (le_refl _)⟩, ?_⟩
+  intro ⟨h₁, h₂⟩
+  cases xs with
+  | nil => simp at h₁
+  | cons x xs =>
+    exact congrArg some <| anti.1
+      (h₂ _ (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]
+
+end List

src/Init/Data/List/Monadic.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.TakeDrop
+
+/-!
+# Lemmas about `List.mapM` and `List.forM`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ## Monadic operations -/
+
+-- 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?
+
+-- Previously `mapM.loop`, `filterMapM.loop`, `forIn.loop`, `forIn'.loop`
+-- had attribute `@[simp]`.
+-- We don't currently provide simp lemmas,
+-- as this is an internal implementation and they don't seem to be needed.
+
+/-! ### mapM -/
+
+/-- Alternate (non-tail-recursive) form of mapM for proofs. -/
+def mapM' [Monad m] (f : α → m β) : List α → m (List β)
+  | [] => pure []
+  | a :: l => return (← f a) :: (← l.mapM' f)
+
+@[simp] theorem mapM'_nil [Monad m] {f : α → m β} : mapM' f [] = pure [] := rfl
+@[simp] theorem mapM'_cons [Monad m] {f : α → m β} :
+    mapM' f (a :: l) = return ((← f a) :: (← l.mapM' f)) :=
+  rfl
+
+theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
+    mapM' f l = mapM f l := by simp [go, mapM] where
+  go : ∀ l acc, mapM.loop f l acc = return acc.reverse ++ (← mapM' f l)
+    | [], acc => by simp [mapM.loop, mapM']
+    | a::l, acc => by simp [go l, mapM.loop, mapM']
+
+@[simp] theorem mapM_nil [Monad m] (f : α → m β) : [].mapM f = pure [] := rfl
+
+@[simp] theorem mapM_cons [Monad m] [LawfulMonad m] (f : α → m β) :
+    (a :: l).mapM f = (return (← f a) :: (← l.mapM f)) := by simp [← mapM'_eq_mapM, mapM']
+
+@[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} :
+    (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
+
+/-! ### forM -/
+
+-- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
+-- As such we need to replace `List.forM_nil` and `List.forM_cons`:
+
+@[simp] theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl
+
+@[simp] theorem forM_cons' [Monad m] :
+    (a::as).forM f = (f a >>= fun _ => as.forM f : m PUnit) :=
+  List.forM_cons _ _ _
+
+@[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : List α) (f : α → m PUnit) :
+    (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
+  induction l₁ <;> simp [*]
+
+end List

src/Init/Data/List/Nat.lean

@@ -1,93 +1,10 @@
 /-
-Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+Authors: Kim Morrison
 -/
 prelude
-import Init.Data.List.Lemmas
-import Init.Data.Nat.Lemmas
-
-/-!
-# Miscellaneous `List` lemmas, that require more `Nat` lemmas than are available in `Init.Data.List.Lemmas`.
-
-In particular, `omega` is available here.
--/
-
-open Nat
-
-namespace List
-
-/-! ### filter -/
-
-theorem length_filter_lt_length_iff_exists (l) :
-    length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x := by
-  simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using
-  countP_pos (fun x => ¬p x) (l := l)
-
-/-! ### minimum? -/
-
--- A specialization of `minimum?_eq_some_iff` to Nat.
-theorem minimum?_eq_some_iff' {xs : List Nat} :
-    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  minimum?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => by omega)
-    (le_min_iff := fun _ _ _ => by omega)
-
--- This could be generalized,
--- but will first require further work on order typeclasses in the core repository.
-theorem minimum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).minimum? = some (match l.minimum? with
-    | none => a
-    | some m => min a m) := by
-  rw [minimum?_eq_some_iff']
-  split <;> rename_i h m
-  · simp_all
-  · rw [minimum?_eq_some_iff'] at m
-    obtain ⟨m, le⟩ := m
-    rw [Nat.min_def]
-    constructor
-    · split
-      · exact mem_cons_self a l
-      · exact mem_cons_of_mem a m
-    · intro b m
-      cases List.mem_cons.1 m with
-      | inl => split <;> omega
-      | inr h =>
-        specialize le b h
-        split <;> omega
-
-/-! ### maximum? -/
-
--- A specialization of `maximum?_eq_some_iff` to Nat.
-theorem maximum?_eq_some_iff' {xs : List Nat} :
-    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
-  maximum?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => by omega)
-    (max_le_iff := fun _ _ _ => by omega)
-
--- This could be generalized,
--- but will first require further work on order typeclasses in the core repository.
-theorem maximum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).maximum? = some (match l.maximum? with
-    | none => a
-    | some m => max a m) := by
-  rw [maximum?_eq_some_iff']
-  split <;> rename_i h m
-  · simp_all
-  · rw [maximum?_eq_some_iff'] at m
-    obtain ⟨m, le⟩ := m
-    rw [Nat.max_def]
-    constructor
-    · split
-      · exact mem_cons_of_mem a m
-      · exact mem_cons_self a l
-    · intro b m
-      cases List.mem_cons.1 m with
-      | inl => split <;> omega
-      | inr h =>
-        specialize le b h
-        split <;> omega
-
-end List
+import Init.Data.List.Nat.Basic
+import Init.Data.List.Nat.Pairwise
+import Init.Data.List.Nat.Range
+import Init.Data.List.Nat.TakeDrop

src/Init/Data/List/Nat/Basic.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Count
+import Init.Data.List.MinMax
+import Init.Data.Nat.Lemmas
+
+/-!
+# Miscellaneous `List` lemmas, that require more `Nat` lemmas than are available in `Init.Data.List.Lemmas`.
+
+In particular, `omega` is available here.
+-/
+
+open Nat
+
+namespace List
+
+/-! ### filter -/
+
+theorem length_filter_lt_length_iff_exists (l) :
+    length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x := by
+  simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using
+  countP_pos (fun x => ¬p x) (l := l)
+
+/-! ### leftpad -/
+
+/-- The length of the List returned by `List.leftpad n a l` is equal
+  to the larger of `n` and `l.length` -/
+@[simp]
+theorem leftpad_length (n : Nat) (a : α) (l : List α) :
+    (leftpad n a l).length = max n l.length := by
+  simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
+
+/-! ### eraseIdx -/
+
+theorem mem_eraseIdx_iff_getElem {x : α} :
+    ∀ {l} {k}, x ∈ eraseIdx l k ↔ ∃ i h, i ≠ k ∧ l[i]'h = x
+  | [], _ => by
+    simp only [eraseIdx, not_mem_nil, false_iff]
+    rintro ⟨i, h, -⟩
+    exact Nat.not_lt_zero _ h
+  | a::l, 0 => by simp [mem_iff_getElem, Nat.succ_lt_succ_iff]
+  | a::l, k+1 => by
+    rw [← Nat.or_exists_add_one]
+    simp [mem_eraseIdx_iff_getElem, @eq_comm _ a, succ_inj', Nat.succ_lt_succ_iff]
+
+theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x := by
+  simp only [mem_eraseIdx_iff_getElem, getElem_eq_iff, exists_and_left]
+  refine exists_congr fun i => and_congr_right' ?_
+  constructor
+  · rintro ⟨_, h⟩; exact h
+  · rintro h;
+    obtain ⟨h', -⟩ := getElem?_eq_some.1 h
+    exact ⟨h', h⟩
+
+/-! ### minimum? -/
+
+-- A specialization of `minimum?_eq_some_iff` to Nat.
+theorem minimum?_eq_some_iff' {xs : List Nat} :
+    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  minimum?_eq_some_iff
+    (le_refl := Nat.le_refl)
+    (min_eq_or := fun _ _ => by omega)
+    (le_min_iff := fun _ _ _ => by omega)
+
+-- This could be generalized,
+-- but will first require further work on order typeclasses in the core repository.
+theorem minimum?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).minimum? = some (match l.minimum? with
+    | none => a
+    | some m => min a m) := by
+  rw [minimum?_eq_some_iff']
+  split <;> rename_i h m
+  · simp_all
+  · rw [minimum?_eq_some_iff'] at m
+    obtain ⟨m, le⟩ := m
+    rw [Nat.min_def]
+    constructor
+    · split
+      · exact mem_cons_self a l
+      · exact mem_cons_of_mem a m
+    · intro b m
+      cases List.mem_cons.1 m with
+      | inl => split <;> omega
+      | inr h =>
+        specialize le b h
+        split <;> omega
+
+/-! ### maximum? -/
+
+-- A specialization of `maximum?_eq_some_iff` to Nat.
+theorem maximum?_eq_some_iff' {xs : List Nat} :
+    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
+  maximum?_eq_some_iff
+    (le_refl := Nat.le_refl)
+    (max_eq_or := fun _ _ => by omega)
+    (max_le_iff := fun _ _ _ => by omega)
+
+-- This could be generalized,
+-- but will first require further work on order typeclasses in the core repository.
+theorem maximum?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).maximum? = some (match l.maximum? with
+    | none => a
+    | some m => max a m) := by
+  rw [maximum?_eq_some_iff']
+  split <;> rename_i h m
+  · simp_all
+  · rw [maximum?_eq_some_iff'] at m
+    obtain ⟨m, le⟩ := m
+    rw [Nat.max_def]
+    constructor
+    · split
+      · exact mem_cons_of_mem a m
+      · exact mem_cons_self a l
+    · intro b m
+      cases List.mem_cons.1 m with
+      | inl => split <;> omega
+      | inr h =>
+        specialize le b h
+        split <;> omega
+
+end List

src/Init/Data/List/Nat/Pairwise.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, James Gallicchio
+-/
+prelude
+import Init.Data.Fin.Lemmas
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Pairwise
+
+/-!
+# Lemmas about `List.Pairwise`
+-/
+
+namespace List
+
+/-- Given a list `is` of monotonically increasing indices into `l`, getting each index
+  produces a sublist of `l`.  -/
+theorem map_getElem_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (· < ·)) :
+    is.map (l[·]) <+ l := by
+  suffices ∀ n l', l' = l.drop n → (∀ i ∈ is, n ≤ i) → map (l[·]) is <+ l'
+    from this 0 l (by simp) (by simp)
+  rintro n l' rfl his
+  induction is generalizing n with
+  | nil => simp
+  | cons hd tl IH =>
+    simp only [Fin.getElem_fin, map_cons]
+    have := IH h.of_cons (hd+1) (pairwise_cons.mp h).1
+    specialize his hd (.head _)
+    have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd)
+    have := Sublist.append (nil_sublist (take hd l |>.drop n)) this
+    rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this
+    simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his]
+
+@[deprecated map_getElem_sublist (since := "2024-07-30")]
+theorem map_get_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (·.val < ·.val)) :
+    is.map (get l) <+ l := by
+  simpa using map_getElem_sublist h
+
+/-- Given a sublist `l' <+ l`, there exists an increasing list of indices `is` such that
+  `l' = is.map fun i => l[i]`. -/
+theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (Fin l.length),
+    l' = is.map (l[·]) ∧ is.Pairwise (· < ·) := by
+  induction h with
+  | slnil => exact ⟨[], by simp⟩
+  | cons _ _ IH =>
+    let ⟨is, IH⟩ := IH
+    refine ⟨is.map (·.succ), ?_⟩
+    simpa [Function.comp_def, pairwise_map]
+  | cons₂ _ _ IH =>
+    rcases IH with ⟨is,IH⟩
+    refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
+    simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem]
+
+@[deprecated sublist_eq_map_getElem (since := "2024-07-30")]
+theorem sublist_eq_map_get (h : l' <+ l) : ∃ is : List (Fin l.length),
+    l' = map (get l) is ∧ is.Pairwise (· < ·) := by
+  simpa using sublist_eq_map_getElem h
+
+theorem pairwise_iff_getElem : Pairwise R l ↔
+    ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
+  rw [pairwise_iff_forall_sublist]
+  constructor <;> intro h
+  · intros i j hi hj h'
+    apply h
+    simpa [h'] using map_getElem_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩])
+  · intros a b h'
+    have ⟨is, h', hij⟩ := sublist_eq_map_getElem h'
+    rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h'
+    rcases h' with ⟨rfl, rfl⟩
+    apply h; simpa using hij
+
+end List

src/Init/Data/List/Nat/Range.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
 prelude
-import Init.Data.List.TakeDrop
-import Init.Data.Nat.Lemmas
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Pairwise
 
 /-!
 # Lemmas about `List.range` and `List.enum`

src/Init/Data/List/Nat/TakeDrop.lean

@@ -0,0 +1,503 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Zip
+import Init.Data.Nat.Lemmas
+
+/-!
+# 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, and use `omega`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ### take -/
+
+@[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]
+  | succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
+
+theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [Nat.min_le_left]
+
+theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
+  by simp [Nat.min_le_right]
+
+theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the big list to the small list. -/
+theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+    L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) :=
+  getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append ..
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the small list to the big list. -/
+theorem getElem_take' (L : List α) {j i : Nat} {h : i < (L.take j).length} :
+    (L.take j)[i] =
+    L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
+  rw [length_take, Nat.lt_min] at h; rw [getElem_take L _ h.1]
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the big list to the small list. -/
+@[deprecated getElem_take (since := "2024-06-12")]
+theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
+  simp [getElem_take _ hi hj]
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the small list to the big list. -/
+@[deprecated getElem_take (since := "2024-06-12")]
+theorem get_take' (L : List α) {j i} :
+    get (L.take j) i =
+    get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
+  simp [getElem_take']
+
+theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
+    (l.take n)[m]? = none :=
+  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) :
+    (l.take n).get? m = none := by
+  simp [getElem?_take_eq_none h]
+
+theorem getElem?_take_eq_if {l : List α} {n m : Nat} :
+    (l.take n)[m]? = if m < n then l[m]? else none := by
+  split
+  · next h => exact getElem?_take h
+  · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)
+
+@[deprecated getElem?_take_eq_if (since := "2024-06-12")]
+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]
+
+theorem head?_take {l : List α} {n : Nat} :
+    (l.take n).head? = if n = 0 then none else l.head? := by
+  simp [head?_eq_getElem?, getElem?_take_eq_if]
+  split
+  · rw [if_neg (by omega)]
+  · rw [if_pos (by omega)]
+
+theorem head_take {l : List α} {n : Nat} (h : l.take n ≠ []) :
+    (l.take n).head h = l.head (by simp_all) := by
+  apply Option.some_inj.1
+  rw [← head?_eq_head, ← head?_eq_head, head?_take, if_neg]
+  simp_all
+
+theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast? := by
+  rw [getLast?_eq_getElem?, getElem?_take_eq_if, length_take]
+  split
+  · rw [if_neg (by omega)]
+    rw [Nat.min_def]
+    split
+    · rw [getElem?_eq_getElem (by omega)]
+      simp
+    · rw [← getLast?_eq_getElem?, getElem?_eq_none (by omega)]
+      simp
+  · rw [if_pos]
+    omega
+
+theorem getLast_take {l : List α} (h : l.take n ≠ []) :
+    (l.take n).getLast h = l[n - 1]?.getD (l.getLast (by simp_all)) := by
+  rw [getLast_eq_getElem, getElem_take']
+  simp [length_take, Nat.min_def]
+  simp at h
+  split
+  · rw [getElem?_eq_getElem (by omega)]
+    simp
+  · rw [getElem?_eq_none (by omega), getLast_eq_getElem]
+    simp
+
+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]
+  | succ n, succ m, nil => by simp only [take_nil]
+  | succ n, succ m, a :: l => by
+    simp only [take, succ_min_succ, take_take n m l]
+
+theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) :
+    (l.set n a).take m = l.take m :=
+  List.ext_getElem? fun i => by
+    rw [getElem?_take_eq_if, getElem?_take_eq_if]
+    split
+    · next h' => rw [getElem?_set_ne (by omega)]
+    · rfl
+
+@[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 [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₂`. -/
+theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
+    take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
+  induction l₁ generalizing n
+  · simp
+  · cases n
+    · simp [*]
+    · simp only [cons_append, take_succ_cons, length_cons, succ_eq_add_one, cons.injEq,
+        append_cancel_left_eq, true_and, *]
+      congr 1
+      omega
+
+theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
+    (l₁ ++ l₂).take n = l₁.take n := by
+  simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
+
+/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
+`i` elements of `l₂` to `l₁`. -/
+theorem take_append {l₁ l₂ : List α} (i : Nat) :
+    take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
+  rw [take_append_eq_append_take, take_of_length_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
+
+@[simp]
+theorem take_eq_take :
+    ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
+  | [], m, n => by simp [Nat.min_zero]
+  | _ :: xs, 0, 0 => by simp
+  | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]
+
+theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
+  suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
+    rw [take_append_drop] at this
+    assumption
+  rw [take_append_eq_append_take, take_of_length_le, append_right_inj]
+  · simp only [take_eq_take, length_take, length_drop]
+    omega
+  apply Nat.le_trans (m := m)
+  · apply length_take_le
+  · apply Nat.le_add_right
+
+theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
+    (l.take n).dropLast = l.take (n - 1) := by
+  simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
+
+theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
+    (h : map f l = s₁ ++ s₂) : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂ := by
+  have := h
+  rw [← take_append_drop (length s₁) l] at this ⊢
+  rw [map_append] at this
+  refine ⟨_, _, rfl, append_inj this ?_⟩
+  rw [length_map, length_take, Nat.min_eq_left]
+  rw [← length_map l f, h, length_append]
+  apply Nat.le_add_right
+
+/-! ### drop -/
+
+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
+  simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
+    length_append] using h
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
+theorem getElem_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
+    L[i + j] = (L.drop i)[j]'(lt_length_drop L h) := by
+  have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
+  rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right'] <;>
+    simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
+@[deprecated getElem_drop (since := "2024-06-12")]
+theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
+    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
+  simp [getElem_drop]
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
+theorem getElem_drop' (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} :
+    (L.drop i)[j] = L[i + j]'(by
+      rw [Nat.add_comm]
+      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)) := by
+  rw [getElem_drop]
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
+@[deprecated getElem_drop' (since := "2024-06-12")]
+theorem get_drop' (L : List α) {i j} :
+    get (L.drop i) j = get L ⟨i + j, by
+      rw [Nat.add_comm]
+      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
+  simp [getElem_drop']
+
+@[simp]
+theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by
+  ext
+  simp only [getElem?_eq_some, getElem_drop', Option.mem_def]
+  constructor <;> intro ⟨h, ha⟩
+  · exact ⟨_, ha⟩
+  · refine ⟨?_, ha⟩
+    rw [length_drop]
+    rw [Nat.add_comm] at h
+    apply Nat.lt_sub_of_add_lt h
+
+@[deprecated getElem?_drop (since := "2024-06-12")]
+theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
+  simp
+
+theorem head?_drop (l : List α) (n : Nat) :
+    (l.drop n).head? = l[n]? := by
+  rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
+
+theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
+    (l.drop n).head h = l[n]'(by simp_all) := by
+  have w : n < l.length := length_lt_of_drop_ne_nil h
+  simpa [head?_eq_head, getElem?_eq_getElem, h, w] using head?_drop l n
+
+theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n then none else l.getLast? := by
+  rw [getLast?_eq_getElem?, getElem?_drop]
+  rw [length_drop]
+  split
+  · rw [getElem?_eq_none (by omega)]
+  · rw [getLast?_eq_getElem?]
+    congr
+    omega
+
+theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
+    (l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
+  simp only [ne_eq, drop_eq_nil_iff_le] at h
+  apply Option.some_inj.1
+  simp only [← getLast?_eq_getLast, getLast?_drop, ite_eq_right_iff]
+  omega
+
+theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
+    (a :: l).drop l.length = [l.getLast h] := by
+  induction l generalizing a with
+  | nil =>
+    cases h rfl
+  | cons y l ih =>
+    simp only [drop, length]
+    by_cases h₁ : l = []
+    · simp [h₁]
+    rw [getLast_cons h₁]
+    exact ih h₁ y
+
+/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
+in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
+theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
+    drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
+  induction l₁ generalizing n
+  · simp
+  · cases n
+    · simp [*]
+    · simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]
+      congr 1
+      omega
+
+theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
+    (l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
+  simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
+
+/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
+up to `i` in `l₂`. -/
+@[simp]
+theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
+  rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
+    simp [Nat.add_sub_cancel_left, Nat.le_add_right]
+
+theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
+    l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l := by
+  split <;> rename_i h
+  · ext1 m
+    by_cases h' : m < n
+    · rw [getElem?_append (by simp [length_take]; omega), getElem?_set_ne (by omega),
+        getElem?_take h']
+    · by_cases h'' : m = n
+      · subst h''
+        rw [getElem?_set_eq ‹_›, getElem?_append_right, length_take,
+          Nat.min_eq_left (by omega), Nat.sub_self, getElem?_cons_zero]
+        rw [length_take]
+        exact Nat.min_le_left m l.length
+      · have h''' : n < m := by omega
+        rw [getElem?_set_ne (by omega), getElem?_append_right, length_take,
+          Nat.min_eq_left (by omega)]
+        · obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h'''
+          have p : n + k + 1 - n = k + 1 := by omega
+          rw [p]
+          rw [getElem?_cons_succ, getElem?_drop]
+          congr 1
+          omega
+        · rw [length_take]
+          exact Nat.le_trans (Nat.min_le_left _ _) (by omega)
+  · rw [set_eq_of_length_le]
+    omega
+
+theorem exists_of_set {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by
+  refine ⟨l.take n, l.drop (n + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩
+  simp [set_eq_take_append_cons_drop, h]
+
+theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α)
+    (hnm : n < m) : drop m (l.set n a) = l.drop m :=
+  ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)
+
+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
+  | _, _, [] => by simp
+  | m+1, n+1, h :: t => by
+    simp [take_succ_cons, drop_succ_cons, drop_take m n t]
+    congr 1
+    omega
+
+theorem take_reverse {α} {xs : List α} {n : Nat} (h : n ≤ xs.length) :
+    xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
+  induction xs generalizing n <;>
+    simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
+  next xs_hd xs_tl xs_ih =>
+  cases Nat.lt_or_eq_of_le h with
+  | inl h' =>
+    have h' := Nat.le_of_succ_le_succ h'
+    rw [take_append_of_le_length, xs_ih h']
+    rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
+    · rwa [succ_eq_add_one, Nat.sub_add_comm]
+    · rwa [length_reverse]
+  | inr h' =>
+    subst h'
+    rw [length, Nat.sub_self, drop]
+    suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
+      rw [this, take_length, reverse_cons]
+    rw [length_append, length_reverse]
+    rfl
+
+@[deprecated (since := "2024-06-15")] abbrev reverse_take := @take_reverse
+
+theorem drop_reverse {α} {xs : List α} {n : Nat} (h : n ≤ xs.length) :
+    xs.reverse.drop n = (xs.take (xs.length - n)).reverse := by
+  conv =>
+    rhs
+    rw [← reverse_reverse xs]
+  rw [← reverse_reverse xs] at h
+  generalize xs.reverse = xs' at h ⊢
+  rw [take_reverse]
+  · simp only [length_reverse, reverse_reverse] at *
+    congr
+    omega
+  · simp only [length_reverse, sub_le]
+
+/-! ### 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
+
+/-! ### rotateRight -/
+
+@[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₂) :
+    length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;>
+    simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
+
+theorem lt_length_left_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
+    (h : i < (zipWith f l l').length) : i < l.length := by rw [length_zipWith] at h; omega
+
+theorem lt_length_right_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
+    (h : i < (zipWith f l l').length) : i < l'.length := by rw [length_zipWith] at h; omega
+
+@[simp]
+theorem getElem_zipWith {f : α → β → γ} {l : List α} {l' : List β}
+    {i : Nat} {h : i < (zipWith f l l').length} :
+    (zipWith f l l')[i] =
+      f (l[i]'(lt_length_left_of_zipWith h))
+        (l'[i]'(lt_length_right_of_zipWith h)) := by
+  rw [← Option.some_inj, ← getElem?_eq_getElem, getElem?_zipWith_eq_some]
+  exact
+    ⟨l[i]'(lt_length_left_of_zipWith h), l'[i]'(lt_length_right_of_zipWith h),
+      by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem]; exact ⟨rfl, rfl⟩⟩
+
+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₂]
+
+theorem reverse_zipWith (h : l.length = l'.length) :
+    (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by
+  induction l generalizing l' with
+  | nil => simp
+  | cons hd tl hl =>
+    cases l' with
+    | nil => simp
+    | cons hd' tl' =>
+      simp only [Nat.add_right_cancel_iff, length] at h
+      have : tl.reverse.length = tl'.reverse.length := by simp [h]
+      simp [hl h, zipWith_append _ _ _ _ _ this]
+
+@[deprecated reverse_zipWith (since := "2024-07-28")] abbrev zipWith_distrib_reverse := @reverse_zipWith
+
+@[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 lt_length_left_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) :
+    i < l.length :=
+  lt_length_left_of_zipWith h
+
+theorem lt_length_right_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) :
+    i < l'.length :=
+  lt_length_right_of_zipWith h
+
+@[simp]
+theorem getElem_zip {l : List α} {l' : List β} {i : Nat} {h : i < (zip l l').length} :
+    (zip l l')[i] =
+      (l[i]'(lt_length_left_of_zip h), l'[i]'(lt_length_right_of_zip h)) :=
+  getElem_zipWith (h := h)
+
+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/List/Pairwise.lean

@@ -0,0 +1,269 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Sublist
+
+/-!
+# Lemmas about `List.Pairwise` and `List.Nodup`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ## Pairwise and Nodup -/
+
+/-! ### Pairwise -/
+
+theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
+  | .slnil, h => h
+  | .cons _ s, .cons _ h₂ => h₂.sublist s
+  | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h)
+
+theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) :
+    ∀ {l : List α}, l.Pairwise R → l.Pairwise S
+  | _, .nil => .nil
+  | _, .cons h₁ h₂ => .cons (H ∘ h₁ ·) (h₂.imp H)
+
+theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : ∀ {a'}, a' ∈ l → R a a' :=
+  (pairwise_cons.1 p).1 _
+
+theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
+  (pairwise_cons.1 p).2
+
+theorem Pairwise.tail : ∀ {l : List α} (_p : Pairwise R l), Pairwise R l.tail
+  | [], h => h
+  | _ :: _, h => h.of_cons
+
+theorem Pairwise.imp_of_mem {S : α → α → Prop}
+    (H : ∀ {a b}, a ∈ l → b ∈ l → R a b → S a b) (p : Pairwise R l) : Pairwise S l := by
+  induction p with
+  | nil => constructor
+  | @cons a l r _ ih =>
+    constructor
+    · exact fun x h => H (mem_cons_self ..) (mem_cons_of_mem _ h) <| r x h
+    · exact ih fun m m' => H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')
+
+theorem Pairwise.and (hR : Pairwise R l) (hS : Pairwise S l) :
+    l.Pairwise fun a b => R a b ∧ S a b := by
+  induction hR with
+  | nil => simp only [Pairwise.nil]
+  | cons R1 _ IH =>
+    simp only [Pairwise.nil, pairwise_cons] at hS ⊢
+    exact ⟨fun b bl => ⟨R1 b bl, hS.1 b bl⟩, IH hS.2⟩
+
+theorem pairwise_and_iff : l.Pairwise (fun a b => R a b ∧ S a b) ↔ Pairwise R l ∧ Pairwise S l :=
+  ⟨fun h => ⟨h.imp fun h => h.1, h.imp fun h => h.2⟩, fun ⟨hR, hS⟩ => hR.and hS⟩
+
+theorem Pairwise.imp₂ (H : ∀ a b, R a b → S a b → T a b)
+    (hR : Pairwise R l) (hS : l.Pairwise S) : l.Pairwise T :=
+  (hR.and hS).imp fun ⟨h₁, h₂⟩ => H _ _ h₁ h₂
+
+theorem Pairwise.iff_of_mem {S : α → α → Prop} {l : List α}
+    (H : ∀ {a b}, a ∈ l → b ∈ l → (R a b ↔ S a b)) : Pairwise R l ↔ Pairwise S l :=
+  ⟨Pairwise.imp_of_mem fun m m' => (H m m').1, Pairwise.imp_of_mem fun m m' => (H m m').2⟩
+
+theorem Pairwise.iff {S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {l : List α} :
+    Pairwise R l ↔ Pairwise S l :=
+  Pairwise.iff_of_mem fun _ _ => H ..
+
+theorem pairwise_of_forall {l : List α} (H : ∀ x y, R x y) : Pairwise R l := by
+  induction l <;> simp [*]
+
+theorem Pairwise.and_mem {l : List α} :
+    Pairwise R l ↔ Pairwise (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l :=
+  Pairwise.iff_of_mem <| by simp (config := { contextual := true })
+
+theorem Pairwise.imp_mem {l : List α} :
+    Pairwise R l ↔ Pairwise (fun x y => x ∈ l → y ∈ l → R x y) l :=
+  Pairwise.iff_of_mem <| by simp (config := { contextual := true })
+
+theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pairwise R l)
+    (h₃ : l.Pairwise (flip R)) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y := by
+  induction l with
+  | nil => exact forall_mem_nil _
+  | cons a l ih =>
+    rw [pairwise_cons] at h₂ h₃
+    simp only [mem_cons]
+    rintro x (rfl | hx) y (rfl | hy)
+    · exact h₁ _ (l.mem_cons_self _)
+    · exact h₂.1 _ hy
+    · exact h₃.1 _ hx
+    · exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
+
+theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
+
+theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
+
+theorem pairwise_map {l : List α} :
+    (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b) := by
+  induction l
+  · simp
+  · simp only [map, pairwise_cons, forall_mem_map, *]
+
+theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b)
+    (p : Pairwise S (map f l)) : Pairwise R l :=
+  (pairwise_map.1 p).imp (H _ _)
+
+theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
+    (p : Pairwise R l) : Pairwise S (map f l) :=
+  pairwise_map.2 <| p.imp (H _ _)
+
+theorem pairwise_filterMap (f : β → Option α) {l : List β} :
+    Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b ∈ f a, ∀ b' ∈ f a', R b b') l := by
+  let _S (a a' : β) := ∀ b ∈ f a, ∀ b' ∈ f a', R b b'
+  simp only [Option.mem_def]
+  induction l with
+  | nil => simp only [filterMap, Pairwise.nil]
+  | cons a l IH => ?_
+  match e : f a with
+  | none =>
+    rw [filterMap_cons_none e, pairwise_cons]
+    simp only [e, false_implies, implies_true, true_and, IH]
+  | some b =>
+    rw [filterMap_cons_some e]
+    simpa [IH, e] using fun _ =>
+      ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
+
+theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
+    (H : ∀ a a' : α, R a a' → ∀ b ∈ f a, ∀ b' ∈ f a', S b b') {l : List α} (p : Pairwise R l) :
+    Pairwise S (filterMap f l) :=
+  (pairwise_filterMap _).2 <| p.imp (H _ _)
+
+@[deprecated Pairwise.filterMap (since := "2024-07-29")] abbrev Pairwise.filter_map := @Pairwise.filterMap
+
+theorem pairwise_filter (p : α → Prop) [DecidablePred p] {l : List α} :
+    Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l := by
+  rw [← filterMap_eq_filter, pairwise_filterMap]
+  simp
+
+theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
+  Pairwise.sublist (filter_sublist _)
+
+theorem pairwise_append {l₁ l₂ : List α} :
+    (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b := by
+  induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]
+
+theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {l₁ l₂ : List α} :
+    Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁) := by
+  have (l₁ l₂ : List α) (H : ∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y)
+    (x : α) (xm : x ∈ l₂) (y : α) (ym : y ∈ l₁) : R x y := s (H y ym x xm)
+  simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
+
+theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
+    Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) := by
+  show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
+  rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
+  simp only [mem_append, or_comm]
+
+theorem pairwise_join {L : List (List α)} :
+    Pairwise R (join L) ↔
+      (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L := by
+  induction L with
+  | nil => simp
+  | cons l L IH =>
+    simp only [join, pairwise_append, IH, mem_join, exists_imp, and_imp, forall_mem_cons,
+      pairwise_cons, and_assoc, and_congr_right_iff]
+    rw [and_comm, and_congr_left_iff]
+    intros; exact ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩
+
+theorem pairwise_bind {R : β → β → Prop} {l : List α} {f : α → List β} :
+    List.Pairwise R (l.bind f) ↔
+      (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
+  simp [List.bind, pairwise_join, pairwise_map]
+
+theorem pairwise_reverse {l : List α} :
+    l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by
+  induction l <;> simp [*, pairwise_append, and_comm]
+
+@[simp] theorem pairwise_replicate {n : Nat} {a : α} :
+    (replicate n a).Pairwise R ↔ n ≤ 1 ∨ R a a := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, pairwise_cons, mem_replicate, ne_eq, and_imp,
+      forall_eq_apply_imp_iff, ih]
+    constructor
+    · rintro ⟨h, h' | h'⟩
+      · by_cases w : n = 0
+        · left
+          subst w
+          simp
+        · right
+          exact h w
+      · right
+        exact h'
+    · rintro (h | h)
+      · obtain rfl := eq_zero_of_le_zero (le_of_lt_succ h)
+        simp
+      · exact ⟨fun _ => h, Or.inr h⟩
+
+theorem Pairwise.drop {l : List α} {n : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop n) :=
+  h.sublist (drop_sublist _ _)
+
+theorem Pairwise.take {l : List α} {n : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take n) :=
+  h.sublist (take_sublist _ _)
+
+theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by
+  induction l with
+  | nil => simp
+  | cons hd tl IH =>
+    rw [List.pairwise_cons]
+    constructor <;> intro h
+    · intro
+      | a, b, .cons _ hab => exact IH.mp h.2 hab
+      | _, b, .cons₂ _ hab => refine h.1 _ (hab.subset ?_); simp
+    · constructor
+      · intro x hx
+        apply h
+        rw [List.cons_sublist_cons, List.singleton_sublist]
+        exact hx
+      · apply IH.mpr
+        intro a b hab
+        apply h; exact hab.cons _
+
+/-! ### Nodup -/
+
+@[simp]
+theorem nodup_nil : @Nodup α [] :=
+  Pairwise.nil
+
+@[simp]
+theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
+  simp only [Nodup, pairwise_cons, forall_mem_ne]
+
+theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+  Pairwise.sublist
+
+theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+  Nodup.sublist
+
+theorem getElem?_inj {xs : List α}
+    (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs[i]? = xs[j]?) : i = j := by
+  induction xs generalizing i j with
+  | nil => cases h₀
+  | cons x xs ih =>
+    match i, j with
+    | 0, 0 => rfl
+    | i+1, j+1 =>
+      cases h₁ with
+      | cons ha h₁ =>
+        simp only [getElem?_cons_succ] at h₂
+        exact congrArg (· + 1) (ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂)
+    | i+1, 0 => ?_
+    | 0, j+1 => ?_
+    all_goals
+      simp only [get?_eq_getElem?, getElem?_cons_zero, getElem?_cons_succ] at h₂
+      cases h₁; rename_i h' h
+      have := h x ?_ rfl; cases this
+      rw [mem_iff_get?]
+      simp only [get?_eq_getElem?]
+    exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
+
+@[simp] theorem nodup_replicate {n : Nat} {a : α} :
+    (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
+
+end List

src/Init/Data/List/Sublist.lean

@@ -0,0 +1,754 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.TakeDrop
+
+/-!
+# Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ### isPrefixOf -/
+section isPrefixOf
+variable [BEq α]
+
+@[simp] theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} :
+    isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons₂]
+
+@[simp] theorem isPrefixOf_length_pos_nil {L : List α} (h : 0 < L.length) : isPrefixOf L [] = false := by
+  cases L <;> simp_all [isPrefixOf]
+
+@[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
+
+/-! ### Subset -/
+
+/-! ### List subset -/
+
+theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂ := .rfl
+
+@[simp] theorem nil_subset (l : List α) : [] ⊆ l := nofun
+
+@[simp] theorem Subset.refl (l : List α) : l ⊆ l := fun _ i => i
+
+theorem Subset.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ :=
+  fun _ i => h₂ (h₁ i)
+
+instance : Trans (Membership.mem : α → List α → Prop) Subset Membership.mem :=
+  ⟨fun h₁ h₂ => h₂ h₁⟩
+
+instance : Trans (Subset : List α → List α → Prop) Subset Subset :=
+  ⟨Subset.trans⟩
+
+@[simp] theorem subset_cons_self (a : α) (l : List α) : l ⊆ a :: l := fun _ => Mem.tail _
+
+theorem subset_of_cons_subset {a : α} {l₁ l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
+  fun s _ i => s (mem_cons_of_mem _ i)
+
+theorem subset_cons_of_subset (a : α) {l₁ l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂ :=
+  fun s _ i => .tail _ (s i)
+
+theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂ :=
+  fun _ => by simp only [mem_cons]; exact Or.imp_right (@s _)
+
+@[simp] theorem cons_subset : a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m := by
+  simp only [subset_def, mem_cons, or_imp, forall_and, forall_eq]
+
+@[simp] theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] :=
+  ⟨fun h => match l with | [] => rfl | _::_ => (nomatch h (.head ..)), fun | rfl => Subset.refl _⟩
+
+theorem map_subset {l₁ l₂ : List α} {f : α → β} (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
+  fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
+
+theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=
+  fun x => by simp_all [mem_filter, subset_def.1 H]
+
+theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
+    filterMap f l₁ ⊆ filterMap f l₂ := by
+  intro x
+  simp only [mem_filterMap]
+  rintro ⟨a, h, w⟩
+  exact ⟨a, H h, w⟩
+
+@[simp] theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
+
+@[simp] theorem subset_append_right (l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂ := fun _ => mem_append_right _
+
+theorem subset_append_of_subset_left (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂ :=
+fun s => Subset.trans s <| subset_append_left _ _
+
+theorem subset_append_of_subset_right (l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ :=
+fun s => Subset.trans s <| subset_append_right _ _
+
+@[simp] theorem append_subset {l₁ l₂ l : List α} :
+    l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l := by simp [subset_def, or_imp, forall_and]
+
+theorem replicate_subset {n : Nat} {a : α} {l : List α} : replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp (config := {contextual := true}) [replicate_succ, ih, cons_subset]
+
+theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆ replicate n a ↔ ∀ x ∈ l, x = a := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [cons_subset, mem_replicate, ne_eq, ih, mem_cons, forall_eq_or_imp,
+      and_congr_left_iff, and_iff_right_iff_imp]
+    solve_by_elim
+
+@[simp] theorem reverse_subset {l₁ l₂ : List α} : reverse l₁ ⊆ l₂ ↔ l₁ ⊆ l₂ := by
+  simp [subset_def]
+
+@[simp] theorem subset_reverse {l₁ l₂ : List α} : l₁ ⊆ reverse l₂ ↔ l₁ ⊆ l₂ := by
+  simp [subset_def]
+
+/-! ### Sublist and isSublist -/
+
+@[simp] theorem nil_sublist : ∀ l : List α, [] <+ l
+  | [] => .slnil
+  | a :: l => (nil_sublist l).cons a
+
+@[simp] theorem Sublist.refl : ∀ l : List α, l <+ l
+  | [] => .slnil
+  | a :: l => (Sublist.refl l).cons₂ a
+
+theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) : l₁ <+ l₃ := by
+  induction h₂ generalizing l₁ with
+  | slnil => exact h₁
+  | cons _ _ IH => exact (IH h₁).cons _
+  | @cons₂ l₂ _ a _ IH =>
+    generalize e : a :: l₂ = l₂'
+    match e ▸ h₁ with
+    | .slnil => apply nil_sublist
+    | .cons a' h₁' => cases e; apply (IH h₁').cons
+    | .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂
+
+instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩
+
+@[simp] theorem sublist_cons_self (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _
+
+theorem sublist_of_cons_sublist : a :: l₁ <+ l₂ → l₁ <+ l₂ :=
+  (sublist_cons_self a l₁).trans
+
+@[simp]
+theorem cons_sublist_cons : a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ :=
+  ⟨fun | .cons _ s => sublist_of_cons_sublist s | .cons₂ _ s => s, .cons₂ _⟩
+
+theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l₂ ∨ a ∈ l := by
+  induction l₁ generalizing l with
+  | nil => match h with
+    | .cons _ h => exact .inl h
+    | .cons₂ _ h => exact .inr (.head ..)
+  | cons b l₁ IH =>
+    match h with
+    | .cons _ h => exact (IH h).imp_left (Sublist.cons _)
+    | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)
+
+theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
+  | .slnil, _, h => h
+  | .cons _ s, _, h => .tail _ (s.subset h)
+  | .cons₂ .., _, .head .. => .head ..
+  | .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h)
+
+instance : Trans (@Sublist α) Subset Subset :=
+  ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
+
+instance : Trans Subset (@Sublist α) Subset :=
+  ⟨fun h₁ h₂ => trans h₁ h₂.subset⟩
+
+instance : Trans (Membership.mem : α → List α → Prop) Sublist Membership.mem :=
+  ⟨fun h₁ h₂ => h₂.subset h₁⟩
+
+theorem mem_of_cons_sublist {a : α} {l₁ l₂ : List α} (s : a :: l₁ <+ l₂) : a ∈ l₂ :=
+  (cons_subset.1 s.subset).1
+
+@[simp] theorem sublist_nil {l : List α} : l <+ [] ↔ l = [] :=
+  ⟨fun s => subset_nil.1 s.subset, fun H => H ▸ Sublist.refl _⟩
+
+theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂
+  | .slnil => Nat.le_refl 0
+  | .cons _l s => le_succ_of_le (length_le s)
+  | .cons₂ _ s => succ_le_succ (length_le s)
+
+theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l₁ = l₂
+  | .slnil, _ => rfl
+  | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
+  | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]
+
+theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=
+  s.eq_of_length <| Nat.le_antisymm s.length_le h
+
+theorem Sublist.length_eq (s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂ :=
+  ⟨s.eq_of_length, congrArg _⟩
+
+protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂ := by
+  induction s with
+  | slnil => simp
+  | cons a s ih =>
+    simpa using cons (f a) ih
+  | cons₂ a s ih =>
+    simpa using cons₂ (f a) ih
+
+protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
+    filterMap f l₁ <+ filterMap f l₂ := by
+  induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons, cons₂]
+
+protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
+  rw [← filterMap_eq_filter]; apply s.filterMap
+
+theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} :
+    l₁ <+ l₂.filterMap f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filterMap f := by
+  induction l₂ generalizing l₁ with
+  | nil => simp
+  | cons a l₂ ih =>
+    simp only [filterMap_cons]
+    split
+    · simp only [ih]
+      constructor
+      · rintro ⟨l', h, rfl⟩
+        exact ⟨l', Sublist.cons a h, rfl⟩
+      · rintro ⟨l', h, rfl⟩
+        cases h with
+        | cons _ h =>
+          exact ⟨l', h, rfl⟩
+        | cons₂ _ h =>
+          rename_i l'
+          exact ⟨l', h, by simp_all⟩
+    · constructor
+      · intro w
+        cases w with
+        | cons _ h =>
+          obtain ⟨l', s, rfl⟩ := ih.1 h
+          exact ⟨l', Sublist.cons a s, rfl⟩
+        | cons₂ _ h =>
+          rename_i l'
+          obtain ⟨l', s, rfl⟩ := ih.1 h
+          refine ⟨a :: l', Sublist.cons₂ a s, ?_⟩
+          rwa [filterMap_cons_some]
+      · rintro ⟨l', h, rfl⟩
+        replace h := h.filterMap f
+        rwa [filterMap_cons_some] at h
+        assumption
+
+theorem sublist_map_iff {l₁ : List β} {f : α → β} :
+    l₁ <+ l₂.map f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.map f := by
+  simp only [← filterMap_eq_map, sublist_filterMap_iff]
+
+theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} :
+    l₁ <+ l₂.filter p ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filter p := by
+  simp only [← filterMap_eq_filter, sublist_filterMap_iff]
+
+@[simp] theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂
+  | [], _ => nil_sublist _
+  | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons₂ _
+
+@[simp] theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
+  | [], _ => Sublist.refl _
+  | _ :: l₁, l₂ => (sublist_append_right l₁ l₂).cons _
+
+@[simp] theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l := by
+  refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩
+  obtain ⟨_, _, rfl⟩ := append_of_mem h
+  exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)
+
+theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ :=
+  s.trans <| sublist_append_left ..
+
+theorem sublist_append_of_sublist_right (s : l <+ l₂) : l <+ l₁ ++ l₂ :=
+  s.trans <| sublist_append_right ..
+
+@[simp] theorem append_sublist_append_left : ∀ l, l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂
+  | [] => Iff.rfl
+  | _ :: l => cons_sublist_cons.trans (append_sublist_append_left l)
+
+theorem Sublist.append_left : l₁ <+ l₂ → ∀ l, l ++ l₁ <+ l ++ l₂ :=
+  fun h l => (append_sublist_append_left l).mpr h
+
+theorem Sublist.append_right : l₁ <+ l₂ → ∀ l, l₁ ++ l <+ l₂ ++ l
+  | .slnil, _ => Sublist.refl _
+  | .cons _ h, _ => (h.append_right _).cons _
+  | .cons₂ _ h, _ => (h.append_right _).cons₂ _
+
+theorem Sublist.append (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ :=
+  (hl.append_right _).trans ((append_sublist_append_left _).2 hr)
+
+theorem sublist_cons_iff {a : α} {l l'} :
+    l <+ a :: l' ↔ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l' := by
+  constructor
+  · intro h
+    cases h with
+    | cons _ h => exact Or.inl h
+    | cons₂ _ h => exact Or.inr ⟨_, rfl, h⟩
+  · rintro (h | ⟨r, rfl, h⟩)
+    · exact h.cons _
+    · exact h.cons₂ _
+
+theorem cons_sublist_iff {a : α} {l l'} :
+    a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂ := by
+  induction l' with
+  | nil => simp
+  | cons a' l' ih =>
+    constructor
+    · intro w
+      cases w with
+      | cons _ w =>
+        obtain ⟨r₁, r₂, rfl, h₁, h₂⟩ := ih.1 w
+        exact ⟨a' :: r₁, r₂, by simp, mem_cons_of_mem a' h₁, h₂⟩
+      | cons₂ _ w =>
+        exact ⟨[a], l', by simp, mem_singleton_self _, w⟩
+    · rintro ⟨r₁, r₂, w, h₁, h₂⟩
+      rw [w, ← singleton_append]
+      exact Sublist.append (by simpa) h₂
+
+theorem sublist_append_iff {l : List α} :
+    l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂ := by
+  induction r₁ generalizing l with
+  | nil =>
+    constructor
+    · intro w
+      refine ⟨[], l, by simp_all⟩
+    · rintro ⟨l₁, l₂, rfl, w₁, w₂⟩
+      simp_all
+  | cons r r₁ ih =>
+    constructor
+    · intro w
+      simp only [cons_append] at w
+      cases w with
+      | cons _ w =>
+        obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
+        exact ⟨l₁, l₂, rfl, Sublist.cons r w₁, w₂⟩
+      | cons₂ _ w =>
+        rename_i l
+        obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
+        refine ⟨r :: l₁, l₂, by simp, cons_sublist_cons.mpr w₁, w₂⟩
+    · rintro ⟨l₁, l₂, rfl, w₁, w₂⟩
+      cases w₁ with
+      | cons _ w₁ =>
+        exact Sublist.cons _ (Sublist.append w₁ w₂)
+      | cons₂ _ w₁ =>
+        rename_i l
+        exact Sublist.cons₂ _ (Sublist.append w₁ w₂)
+
+theorem append_sublist_iff {l₁ l₂ : List α} :
+    l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂ := by
+  induction l₁ generalizing r with
+  | nil =>
+    constructor
+    · intro w
+      refine ⟨[], r, by simp_all⟩
+    · rintro ⟨r₁, r₂, rfl, -, w₂⟩
+      simp only [nil_append]
+      exact sublist_append_of_sublist_right w₂
+  | cons a l₁ ih =>
+    constructor
+    · rw [cons_append, cons_sublist_iff]
+      rintro ⟨r₁, r₂, rfl, h₁, h₂⟩
+      obtain ⟨s₁, s₂, rfl, t₁, t₂⟩ := ih.1 h₂
+      refine ⟨r₁ ++ s₁, s₂, by simp, ?_, t₂⟩
+      rw [← singleton_append]
+      exact Sublist.append (by simpa) t₁
+    · rintro ⟨r₁, r₂, rfl, h₁, h₂⟩
+      exact Sublist.append h₁ h₂
+
+theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
+  | .slnil => Sublist.refl _
+  | .cons _ h => by rw [reverse_cons]; exact sublist_append_of_sublist_left h.reverse
+  | .cons₂ _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _
+
+@[simp] theorem reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ :=
+  ⟨fun h => l₁.reverse_reverse ▸ l₂.reverse_reverse ▸ h.reverse, Sublist.reverse⟩
+
+theorem sublist_reverse_iff : l₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂ :=
+  by rw [← reverse_sublist, reverse_reverse]
+
+@[simp] theorem append_sublist_append_right (l) : l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂ :=
+  ⟨fun h => by
+    have := h.reverse
+    simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this
+    exact this,
+   fun h => h.append_right l⟩
+
+@[simp] theorem replicate_sublist_replicate {m n} (a : α) :
+    replicate m a <+ replicate n a ↔ m ≤ n := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · have := h.length_le; simp only [length_replicate] at this ⊢; exact this
+  · induction h with
+    | refl => apply Sublist.refl
+    | step => simp [*, replicate, Sublist.cons]
+
+theorem sublist_replicate_iff : l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a := by
+  induction l generalizing m with
+  | nil =>
+    simp only [nil_sublist, true_iff]
+    exact ⟨0, zero_le m, by simp⟩
+  | cons b l ih =>
+    constructor
+    · intro w
+      cases m with
+      | zero => simp at w
+      | succ m =>
+        simp [replicate_succ] at w
+        cases w with
+        | cons _ w =>
+          obtain ⟨n, le, rfl⟩ := ih.1 (sublist_of_cons_sublist w)
+          obtain rfl := (mem_replicate.1 (mem_of_cons_sublist w)).2
+          exact ⟨n+1, Nat.add_le_add_right le 1, rfl⟩
+        | cons₂ _ w =>
+          obtain ⟨n, le, rfl⟩ := ih.1 w
+          refine ⟨n+1, Nat.add_le_add_right le 1, by simp [replicate_succ]⟩
+    · rintro ⟨n, le, w⟩
+      rw [w]
+      exact (replicate_sublist_replicate a).2 le
+
+theorem sublist_join_of_mem {L : List (List α)} {l} (h : l ∈ L) : l <+ L.join := by
+  induction L with
+  | nil => cases h
+  | cons l' L ih =>
+    rcases mem_cons.1 h with (rfl | h)
+    · simp [h]
+    · simp [ih h, join_cons, sublist_append_of_sublist_right]
+
+theorem sublist_join_iff {L : List (List α)} {l} :
+    l <+ L.join ↔
+      ∃ L' : List (List α), l = L'.join ∧ ∀ i (_ : i < L'.length), L'[i] <+ L[i]?.getD [] := by
+  induction L generalizing l with
+  | nil =>
+    constructor
+    · intro w
+      simp only [join_nil, sublist_nil] at w
+      subst w
+      exact ⟨[], by simp, fun i x => by cases x⟩
+    · rintro ⟨L', rfl, h⟩
+      simp only [join_nil, sublist_nil, join_eq_nil_iff]
+      simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
+      exact (forall_getElem L' (· = [])).1 h
+  | cons l' L ih =>
+    simp only [join_cons, sublist_append_iff, ih]
+    constructor
+    · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
+      refine ⟨l₁ :: L', by simp, ?_⟩
+      intro i lt
+      cases i <;> simp_all
+    · rintro ⟨L', rfl, h⟩
+      cases L' with
+      | nil =>
+        exact ⟨[], [], by simp, by simp, [], by simp, fun i x => by cases x⟩
+      | cons l₁ L' =>
+        exact ⟨l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
+          fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
+
+theorem join_sublist_iff {L : List (List α)} {l} :
+    L.join <+ l ↔
+      ∃ L' : List (List α), l = L'.join ∧ ∀ i (_ : i < L.length), L[i] <+ L'[i]?.getD [] := by
+  induction L generalizing l with
+  | nil =>
+    constructor
+    · intro _
+      exact ⟨[l], by simp, fun i x => by cases x⟩
+    · rintro ⟨L', rfl, _⟩
+      simp only [join_nil, nil_sublist]
+  | cons l' L ih =>
+    simp only [join_cons, append_sublist_iff, ih]
+    constructor
+    · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
+      refine ⟨l₁ :: L', by simp, ?_⟩
+      intro i lt
+      cases i <;> simp_all
+    · rintro ⟨L', rfl, h⟩
+      cases L' with
+      | nil =>
+        exact ⟨[], [], by simp, by simpa using h 0 (by simp), [], by simp,
+          fun i x => by simpa using h (i+1) (Nat.add_lt_add_right x 1)⟩
+      | cons l₁ L' =>
+        exact ⟨l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
+          fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
+
+@[simp] theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+    l₁.isSublist l₂ ↔ l₁ <+ l₂ := by
+  cases l₁ <;> cases l₂ <;> simp [isSublist]
+  case cons.cons hd₁ tl₁ hd₂ tl₂ =>
+    if h_eq : hd₁ = hd₂ then
+      simp [h_eq, cons_sublist_cons, isSublist_iff_sublist]
+    else
+      simp only [beq_iff_eq, h_eq]
+      constructor
+      · intro h_sub
+        apply Sublist.cons
+        exact isSublist_iff_sublist.mp h_sub
+      · intro h_sub
+        cases h_sub
+        case cons h_sub =>
+          exact isSublist_iff_sublist.mpr h_sub
+        case cons₂ =>
+          contradiction
+
+instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
+  decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
+
+/-! ### IsPrefix / IsSuffix / IsInfix -/
+
+@[simp] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
+
+@[simp] theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩
+
+theorem infix_append (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃ := ⟨l₁, l₃, rfl⟩
+
+@[simp] theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by
+  rw [← List.append_assoc]; apply infix_append
+
+theorem IsPrefix.isInfix : l₁ <+: l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨[], t, h⟩
+
+theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩
+
+@[simp] theorem nil_prefix (l : List α) : [] <+: l := ⟨l, rfl⟩
+
+@[simp] theorem nil_suffix (l : List α) : [] <:+ l := ⟨l, append_nil _⟩
+
+@[simp] theorem nil_infix (l : List α) : [] <:+: l := (nil_prefix _).isInfix
+
+@[simp] theorem prefix_refl (l : List α) : l <+: l := ⟨[], append_nil _⟩
+
+@[simp] theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩
+
+@[simp] theorem infix_refl (l : List α) : l <:+: l := (prefix_refl l).isInfix
+
+@[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
+
+theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨L₁, L₂, h⟩ => ⟨a :: L₁, L₂, h ▸ rfl⟩
+
+theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨L₁, L₂, h⟩ =>
+  ⟨L₁, concat L₂ a, by simp [← h, concat_eq_append, append_assoc]⟩
+
+theorem IsPrefix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
+  | _, _, _, ⟨r₁, rfl⟩, ⟨r₂, rfl⟩ => ⟨r₁ ++ r₂, (append_assoc _ _ _).symm⟩
+
+theorem IsSuffix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
+  | _, _, _, ⟨l₁, rfl⟩, ⟨l₂, rfl⟩ => ⟨l₂ ++ l₁, append_assoc _ _ _⟩
+
+theorem IsInfix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
+  | l, _, _, ⟨l₁, r₁, rfl⟩, ⟨l₂, r₂, rfl⟩ => ⟨l₂ ++ l₁, r₁ ++ r₂, by simp only [append_assoc]⟩
+
+protected theorem IsInfix.sublist : l₁ <:+: l₂ → l₁ <+ l₂
+  | ⟨_, _, h⟩ => h ▸ (sublist_append_right ..).trans (sublist_append_left ..)
+
+protected theorem IsInfix.subset (hl : l₁ <:+: l₂) : l₁ ⊆ l₂ :=
+  hl.sublist.subset
+
+protected theorem IsPrefix.sublist (h : l₁ <+: l₂) : l₁ <+ l₂ :=
+  h.isInfix.sublist
+
+protected theorem IsPrefix.subset (hl : l₁ <+: l₂) : l₁ ⊆ l₂ :=
+  hl.sublist.subset
+
+protected theorem IsSuffix.sublist (h : l₁ <:+ l₂) : l₁ <+ l₂ :=
+  h.isInfix.sublist
+
+protected theorem IsSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ :=
+  hl.sublist.subset
+
+@[simp] theorem reverse_suffix : reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ :=
+  ⟨fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]⟩,
+   fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_append, e]⟩⟩
+
+@[simp] theorem reverse_prefix : reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂ := by
+  rw [← reverse_suffix]; simp only [reverse_reverse]
+
+@[simp] theorem reverse_infix : reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂ := by
+  refine ⟨fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩, fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩⟩
+  · rw [← reverse_reverse l₁, append_assoc, ← reverse_append, ← reverse_append, e,
+      reverse_reverse]
+  · rw [append_assoc, ← reverse_append, ← reverse_append, e]
+
+theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length :=
+  h.sublist.length_le
+
+theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length :=
+  h.sublist.length_le
+
+theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length :=
+  h.sublist.length_le
+
+@[simp] theorem infix_nil : l <:+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ infix_refl _)⟩
+
+@[simp] theorem prefix_nil : l <+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ prefix_refl _)⟩
+
+@[simp] theorem suffix_nil : l <:+ [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ suffix_refl _)⟩
+
+theorem infix_iff_prefix_suffix (l₁ l₂ : List α) : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ :=
+  ⟨fun ⟨_, t, e⟩ => ⟨l₁ ++ t, ⟨_, rfl⟩, e ▸ append_assoc .. ▸ ⟨_, rfl⟩⟩,
+    fun ⟨_, ⟨t, rfl⟩, s, e⟩ => ⟨s, t, append_assoc .. ▸ e⟩⟩
+
+theorem IsInfix.eq_of_length (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
+  h.sublist.eq_of_length
+
+theorem IsPrefix.eq_of_length (h : l₁ <+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
+  h.sublist.eq_of_length
+
+theorem IsSuffix.eq_of_length (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂ :=
+  h.sublist.eq_of_length
+
+theorem prefix_of_prefix_length_le :
+    ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
+  | [], l₂, _, _, _, _ => nil_prefix _
+  | a :: l₁, b :: l₂, _, ⟨r₁, rfl⟩, ⟨r₂, e⟩, ll => by
+    injection e with _ e'; subst b
+    rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩
+    exact ⟨r₃, rfl⟩
+
+theorem prefix_or_prefix_of_prefix (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂ ∨ l₂ <+: l₁ :=
+  (Nat.le_total (length l₁) (length l₂)).imp (prefix_of_prefix_length_le h₁ h₂)
+    (prefix_of_prefix_length_le h₂ h₁)
+
+theorem suffix_of_suffix_length_le
+    (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : length l₁ ≤ length l₂) : l₁ <:+ l₂ :=
+  reverse_prefix.1 <|
+    prefix_of_prefix_length_le (reverse_prefix.2 h₁) (reverse_prefix.2 h₂) (by simp [ll])
+
+theorem suffix_or_suffix_of_suffix (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) : l₁ <:+ l₂ ∨ l₂ <:+ l₁ :=
+  (prefix_or_prefix_of_prefix (reverse_prefix.2 h₁) (reverse_prefix.2 h₂)).imp reverse_prefix.1
+    reverse_prefix.1
+
+theorem prefix_cons_iff : l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :: t ∧ t <+: l₂ := by
+  cases l₁ with
+  | nil => simp
+  | cons a' l₁ =>
+    constructor
+    · rintro ⟨t, h⟩
+      simp at h
+      obtain ⟨rfl, rfl⟩ := h
+      exact Or.inr ⟨l₁, rfl, prefix_append l₁ t⟩
+    · rintro (h | ⟨t, w, ⟨s, h'⟩⟩)
+      · simp [h]
+      · simp only [w]
+        refine ⟨s, by simp [h']⟩
+
+@[simp] theorem cons_prefix_cons : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
+  simp only [prefix_cons_iff, cons.injEq, false_or]
+  constructor
+  · rintro ⟨t, ⟨rfl, rfl⟩, h⟩
+    exact ⟨rfl, h⟩
+  · rintro ⟨rfl, h⟩
+    exact ⟨l₁, ⟨rfl, rfl⟩, h⟩
+
+theorem suffix_cons_iff : l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂ := by
+  constructor
+  · rintro ⟨⟨hd, tl⟩, hl₃⟩
+    · exact Or.inl hl₃
+    · simp only [cons_append] at hl₃
+      injection hl₃ with _ hl₄
+      exact Or.inr ⟨_, hl₄⟩
+  · rintro (rfl | hl₁)
+    · exact (a :: l₂).suffix_refl
+    · exact hl₁.trans (l₂.suffix_cons _)
+
+theorem infix_cons_iff : l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ := by
+  constructor
+  · rintro ⟨⟨hd, tl⟩, t, hl₃⟩
+    · exact Or.inl ⟨t, hl₃⟩
+    · simp only [cons_append] at hl₃
+      injection hl₃ with _ hl₄
+      exact Or.inr ⟨_, t, hl₄⟩
+  · rintro (h | hl₁)
+    · exact h.isInfix
+    · exact infix_cons hl₁
+
+theorem infix_of_mem_join : ∀ {L : List (List α)}, l ∈ L → l <:+: join L
+  | l' :: _, h =>
+    match h with
+    | List.Mem.head .. => infix_append [] _ _
+    | List.Mem.tail _ hlMemL =>
+      IsInfix.trans (infix_of_mem_join hlMemL) <| (suffix_append _ _).isInfix
+
+theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂ :=
+  exists_congr fun r => by rw [append_assoc, append_right_inj]
+
+@[simp]
+theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
+  prefix_append_right_inj [a]
+
+theorem take_prefix (n) (l : List α) : take n l <+: l :=
+  ⟨_, take_append_drop _ _⟩
+
+theorem drop_suffix (n) (l : List α) : drop n l <:+ l :=
+  ⟨_, take_append_drop _ _⟩
+
+theorem take_sublist (n) (l : List α) : take n l <+ l :=
+  (take_prefix n l).sublist
+
+theorem drop_sublist (n) (l : List α) : drop n l <+ l :=
+  (drop_suffix n l).sublist
+
+theorem take_subset (n) (l : List α) : take n l ⊆ l :=
+  (take_sublist n l).subset
+
+theorem drop_subset (n) (l : List α) : drop n l ⊆ l :=
+  (drop_sublist n l).subset
+
+theorem mem_of_mem_take {l : List α} (h : a ∈ l.take n) : a ∈ l :=
+  take_subset n l h
+
+theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l :=
+  drop_subset _ _ h
+
+theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
+    l₁.filter p <+: l₂.filter p := by
+  obtain ⟨xs, rfl⟩ := h
+  rw [filter_append]; apply prefix_append
+
+theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
+    l₁.filter p <:+ l₂.filter p := by
+  obtain ⟨xs, rfl⟩ := h
+  rw [filter_append]; apply suffix_append
+
+theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
+    l₁.filter p <:+: l₂.filter p := by
+  obtain ⟨xs, ys, rfl⟩ := h
+  rw [filter_append, filter_append]; apply infix_append _
+
+@[simp] theorem isPrefixOf_iff_prefix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+    l₁.isPrefixOf l₂ ↔ l₁ <+: l₂ := by
+  induction l₁ generalizing l₂ with
+  | nil => simp
+  | cons a l₁ ih =>
+    cases l₂ with
+    | nil => simp
+    | cons a' l₂ => simp [isPrefixOf, ih]
+
+instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+: l₂) :=
+  decidable_of_iff (l₁.isPrefixOf l₂) isPrefixOf_iff_prefix
+
+@[simp] theorem isSuffixOf_iff_suffix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+    l₁.isSuffixOf l₂ ↔ l₁ <:+ l₂ := by
+  simp [isSuffixOf]
+
+instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+ l₂) :=
+  decidable_of_iff (l₁.isSuffixOf l₂) isSuffixOf_iff_suffix
+
+end List

src/Init/Data/List/TakeDrop.lean

@@ -5,499 +5,443 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Lemmas
-import Init.Data.Nat.Lemmas
 
 /-!
-# 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, and use `omega`.
+# Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`.
 -/
 
 namespace List
 
 open Nat
 
-/-! ### take -/
+/-! ### take and drop
 
-@[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]
-  | succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
-
-theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [Nat.min_le_left]
-
-theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
-  by simp [Nat.min_le_right]
-
-theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
-
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the big list to the small list. -/
-theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
-    L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) :=
-  getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append ..
-
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the small list to the big list. -/
-theorem getElem_take' (L : List α) {j i : Nat} {h : i < (L.take j).length} :
-    (L.take j)[i] =
-    L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
-  rw [length_take, Nat.lt_min] at h; rw [getElem_take L _ h.1]
-
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the big list to the small list. -/
-@[deprecated getElem_take (since := "2024-06-12")]
-theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
-    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
-  simp [getElem_take _ hi hj]
-
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the small list to the big list. -/
-@[deprecated getElem_take (since := "2024-06-12")]
-theorem get_take' (L : List α) {j i} :
-    get (L.take j) i =
-    get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
-  simp [getElem_take']
-
-theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
-    (l.take n)[m]? = none :=
-  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) :
-    (l.take n).get? m = none := by
-  simp [getElem?_take_eq_none h]
-
-theorem getElem?_take_eq_if {l : List α} {n m : Nat} :
-    (l.take n)[m]? = if m < n then l[m]? else none := by
-  split
-  · next h => exact getElem?_take h
-  · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)
-
-@[deprecated getElem?_take_eq_if (since := "2024-06-12")]
-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]
-
-theorem head?_take {l : List α} {n : Nat} :
-    (l.take n).head? = if n = 0 then none else l.head? := by
-  simp [head?_eq_getElem?, getElem?_take_eq_if]
-  split
-  · rw [if_neg (by omega)]
-  · rw [if_pos (by omega)]
-
-theorem head_take {l : List α} {n : Nat} (h : l.take n ≠ []) :
-    (l.take n).head h = l.head (by simp_all) := by
-  apply Option.some_inj.1
-  rw [← head?_eq_head, ← head?_eq_head, head?_take, if_neg]
-  simp_all
-
-theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast? := by
-  rw [getLast?_eq_getElem?, getElem?_take_eq_if, length_take]
-  split
-  · rw [if_neg (by omega)]
-    rw [Nat.min_def]
-    split
-    · rw [getElem?_eq_getElem (by omega)]
-      simp
-    · rw [← getLast?_eq_getElem?, getElem?_eq_none (by omega)]
-      simp
-  · rw [if_pos]
-    omega
-
-theorem getLast_take {l : List α} (h : l.take n ≠ []) :
-    (l.take n).getLast h = l[n - 1]?.getD (l.getLast (by simp_all)) := by
-  rw [getLast_eq_getElem, getElem_take']
-  simp [length_take, Nat.min_def]
-  simp at h
-  split
-  · rw [getElem?_eq_getElem (by omega)]
-    simp
-  · rw [getElem?_eq_none (by omega), getLast_eq_getElem]
-    simp
-
-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]
-  | succ n, succ m, nil => by simp only [take_nil]
-  | succ n, succ m, a :: l => by
-    simp only [take, succ_min_succ, take_take n m l]
-
-theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) :
-    (l.set n a).take m = l.take m :=
-  List.ext_getElem? fun i => by
-    rw [getElem?_take_eq_if, getElem?_take_eq_if]
-    split
-    · next h' => rw [getElem?_set_ne (by omega)]
-    · rfl
-
-@[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 [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₂`. -/
-theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
-    take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
-  induction l₁ generalizing n
-  · simp
-  · cases n
-    · simp [*]
-    · simp only [cons_append, take_succ_cons, length_cons, succ_eq_add_one, cons.injEq,
-        append_cancel_left_eq, true_and, *]
-      congr 1
-      omega
-
-theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
-    (l₁ ++ l₂).take n = l₁.take n := by
-  simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
-
-/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
-`i` elements of `l₂` to `l₁`. -/
-theorem take_append {l₁ l₂ : List α} (i : Nat) :
-    take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
-  rw [take_append_eq_append_take, take_of_length_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
+Further results on `List.take` and `List.drop`, which rely on stronger automation in `Nat`,
+are given in `Init.Data.List.TakeDrop`.
+-/
 
 @[simp]
-theorem take_eq_take :
-    ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
-  | [], m, n => by simp [Nat.min_zero]
-  | _ :: xs, 0, 0 => by simp
-  | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
-  | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
-  | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]
+theorem drop_one : ∀ l : List α, drop 1 l = tail l
+  | [] | _ :: _ => rfl
 
-theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
-  suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
-    rw [take_append_drop] at this
-    assumption
-  rw [take_append_eq_append_take, take_of_length_le, append_right_inj]
-  · simp only [take_eq_take, length_take, length_drop]
-    omega
-  apply Nat.le_trans (m := m)
-  · apply length_take_le
-  · apply Nat.le_add_right
+@[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
+  | 0, _ => rfl
+  | _+1, [] => rfl
+  | n+1, x :: xs => congrArg (cons x) <| take_append_drop n xs
 
-theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
-    (l.take n).dropLast = l.take (n - 1) := by
-  simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
+@[simp] theorem length_drop : ∀ (i : Nat) (l : List α), length (drop i l) = length l - i
+  | 0, _ => rfl
+  | succ i, [] => Eq.symm (Nat.zero_sub (succ i))
+  | succ i, x :: l => calc
+    length (drop (succ i) (x :: l)) = length l - i := length_drop i l
+    _ = succ (length l) - succ i := (Nat.succ_sub_succ_eq_sub (length l) i).symm
 
-theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
-    (h : map f l = s₁ ++ s₂) : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂ := by
-  have := h
-  rw [← take_append_drop (length s₁) l] at this ⊢
-  rw [map_append] at this
-  refine ⟨_, _, rfl, append_inj this ?_⟩
-  rw [length_map, length_take, Nat.min_eq_left]
-  rw [← length_map l f, h, length_append]
-  apply Nat.le_add_right
+theorem drop_of_length_le {l : List α} (h : l.length ≤ i) : drop i l = [] :=
+  length_eq_zero.1 (length_drop .. ▸ Nat.sub_eq_zero_of_le h)
 
-/-! ### drop -/
+theorem length_lt_of_drop_ne_nil {l : List α} {n} (h : drop n l ≠ []) : n < l.length :=
+  gt_of_not_le (mt drop_of_length_le h)
 
-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
-  simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
-    length_append] using h
+theorem take_of_length_le {l : List α} (h : l.length ≤ i) : take i l = l := by
+  have := take_append_drop i l
+  rw [drop_of_length_le h, append_nil] at this; exact this
 
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
-theorem getElem_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
-    L[i + j] = (L.drop i)[j]'(lt_length_drop L h) := by
-  have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
-  rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right'] <;>
-    simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
+theorem lt_length_of_take_ne_self {l : List α} {n} (h : l.take n ≠ l) : n < l.length :=
+  gt_of_not_le (mt take_of_length_le h)
 
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
-@[deprecated getElem_drop (since := "2024-06-12")]
-theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
-    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
-  simp [getElem_drop]
+@[deprecated drop_of_length_le (since := "2024-07-07")] abbrev drop_length_le := @drop_of_length_le
+@[deprecated take_of_length_le (since := "2024-07-07")] abbrev take_length_le := @take_of_length_le
 
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
-theorem getElem_drop' (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} :
-    (L.drop i)[j] = L[i + j]'(by
-      rw [Nat.add_comm]
-      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)) := by
-  rw [getElem_drop]
+@[simp] theorem drop_length (l : List α) : drop l.length l = [] := drop_of_length_le (Nat.le_refl _)
 
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
-@[deprecated getElem_drop' (since := "2024-06-12")]
-theorem get_drop' (L : List α) {i j} :
-    get (L.drop i) j = get L ⟨i + j, by
-      rw [Nat.add_comm]
-      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
-  simp [getElem_drop']
+@[simp] theorem take_length (l : List α) : take l.length l = l := take_of_length_le (Nat.le_refl _)
 
 @[simp]
-theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by
-  ext
-  simp only [getElem?_eq_some, getElem_drop', Option.mem_def]
-  constructor <;> intro ⟨h, ha⟩
-  · exact ⟨_, ha⟩
-  · refine ⟨?_, ha⟩
-    rw [length_drop]
-    rw [Nat.add_comm] at h
-    apply Nat.lt_sub_of_add_lt h
+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?_drop (since := "2024-06-12")]
-theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
+@[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 head?_drop (l : List α) (n : Nat) :
-    (l.drop n).head? = l[n]? := by
-  rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
+theorem drop_eq_getElem_cons {n} {l : List α} (h) : drop n l = l[n] :: drop (n + 1) l :=
+  (getElem_cons_drop _ n h).symm
 
-theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
-    (l.drop n).head h = l[n]'(by simp_all) := by
-  have w : n < l.length := length_lt_of_drop_ne_nil h
-  simpa [head?_eq_head, getElem?_eq_getElem, h, w] using head?_drop l n
+@[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 getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n then none else l.getLast? := by
-  rw [getLast?_eq_getElem?, getElem?_drop]
-  rw [length_drop]
-  split
-  · rw [getElem?_eq_none (by omega)]
-  · rw [getLast?_eq_getElem?]
-    congr
-    omega
-
-theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
-    (l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
-  simp only [ne_eq, drop_eq_nil_iff_le] at h
-  apply Option.some_inj.1
-  simp only [← getLast?_eq_getLast, getLast?_drop, ite_eq_right_iff]
-  omega
-
-theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
-    (a :: l).drop l.length = [l.getLast h] := by
-  induction l generalizing a with
-  | nil =>
-    cases h rfl
-  | cons y l ih =>
-    simp only [drop, length]
-    by_cases h₁ : l = []
-    · simp [h₁]
-    rw [getLast_cons h₁]
-    exact ih h₁ y
-
-/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
-in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
-theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
-    drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
-  induction l₁ generalizing n
-  · simp
-  · cases n
-    · simp [*]
-    · simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]
-      congr 1
-      omega
-
-theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
-    (l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
-  simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
-
-/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
-up to `i` in `l₂`. -/
 @[simp]
-theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
-  rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
-    simp [Nat.add_sub_cancel_left, Nat.le_add_right]
+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)
 
-theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
-    l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l := by
-  split <;> rename_i h
-  · ext1 m
-    by_cases h' : m < n
-    · rw [getElem?_append (by simp [length_take]; omega), getElem?_set_ne (by omega),
-        getElem?_take h']
-    · by_cases h'' : m = n
-      · subst h''
-        rw [getElem?_set_eq ‹_›, getElem?_append_right, length_take,
-          Nat.min_eq_left (by omega), Nat.sub_self, getElem?_cons_zero]
-        rw [length_take]
-        exact Nat.min_le_left m l.length
-      · have h''' : n < m := by omega
-        rw [getElem?_set_ne (by omega), getElem?_append_right, length_take,
-          Nat.min_eq_left (by omega)]
-        · obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h'''
-          have p : n + k + 1 - n = k + 1 := by omega
-          rw [p]
-          rw [getElem?_cons_succ, getElem?_drop]
-          congr 1
-          omega
-        · rw [length_take]
-          exact Nat.le_trans (Nat.min_le_left _ _) (by omega)
-  · rw [set_eq_of_length_le]
-    omega
+@[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 exists_of_set {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by
-  refine ⟨l.take n, l.drop (n + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩
-  simp [set_eq_take_append_cons_drop, h]
+@[simp]
+theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? :=
+  getElem?_take (Nat.lt_succ_self n)
 
-theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α)
-    (hnm : n < m) : drop m (l.set n a) = l.drop m :=
-  ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)
+theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by
+  induction l generalizing n with
+  | nil => simp
+  | cons hd tl hl =>
+    cases n
+    · simp
+    · simp [hl]
 
-theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
+@[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
+
+@[simp]
+theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ k = 0 ∨ l = [] := by
+  cases l <;> cases k <;> simp [Nat.succ_ne_zero]
+
+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
+
+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 set_take {l : List α} {n m : Nat} {a : α} :
+    (l.set m a).take n = (l.take n).set m a := by
+  induction n generalizing l m with
+  | zero => simp
+  | succ _ hn =>
+    cases l with
+    | nil => simp
+    | cons hd tl => cases m <;> simp_all
+
+theorem drop_set {l : List α} {n m : Nat} {a : α} :
+    (l.set m a).drop n = if m < n then l.drop n else (l.drop n).set (m - n) a := by
+  induction n generalizing l m with
+  | zero => simp
+  | succ _ hn =>
+    cases l with
+    | nil => simp
+    | cons hd tl =>
+      cases m
+      · simp_all
+      · simp only [hn, set_cons_succ, drop_succ_cons, succ_lt_succ_iff]
+        congr 2
+        exact (Nat.add_sub_add_right ..).symm
+
+theorem set_drop {l : List α} {n m : Nat} {a : α} :
+    (l.drop n).set m a = (l.set (n + m) a).drop n := by
+  rw [drop_set, if_neg, add_sub_self_left n m]
+  exact (Nat.not_lt).2 (le_add_right n m)
+
+theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
+    (l.take i).concat l[i] = l.take (i+1) :=
+  Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
+    rw [concat_eq_append, append_assoc, singleton_append, get_drop_eq_drop, take_append_drop]
+
+@[deprecated take_succ_cons (since := "2024-07-25")]
+theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl
+
+@[deprecated take_of_length_le (since := "2024-07-25")]
+theorem take_all_of_le {n} {l : List α} (h : length l ≤ n) : take n l = l :=
+  take_of_length_le h
+
+theorem drop_left : ∀ l₁ l₂ : List α, drop (length l₁) (l₁ ++ l₂) = l₂
+  | [], _ => rfl
+  | _ :: l₁, l₂ => drop_left l₁ l₂
+
+@[simp]
+theorem drop_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : drop n (l₁ ++ l₂) = l₂ := by
+  rw [← h]; apply drop_left
+
+theorem take_left : ∀ l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
+  | [], _ => rfl
+  | a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
+
+@[simp]
+theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
+  rw [← h]; apply take_left
+
+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]
+
+@[deprecated (since := "2024-07-25")]
+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 dropLast_eq_take (l : List α) : l.dropLast = l.take (l.length - 1) := by
+  cases l with
+  | nil => simp [dropLast]
+  | cons x l =>
+    induction l generalizing x <;> simp_all [dropLast]
+
+@[simp] 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]
+
+@[simp] 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]
+
+@[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
-  | _, 0, _ => by simp
   | _, _, [] => by simp
-  | m+1, n+1, h :: t => by
-    simp [take_succ_cons, drop_succ_cons, drop_take m n t]
-    congr 1
-    omega
+  | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
-theorem take_reverse {α} {xs : List α} {n : Nat} (h : n ≤ xs.length) :
-    xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
-  induction xs generalizing n <;>
-    simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
-  next xs_hd xs_tl xs_ih =>
-  cases Nat.lt_or_eq_of_le h with
-  | inl h' =>
-    have h' := Nat.le_of_succ_le_succ h'
-    rw [take_append_of_le_length, xs_ih h']
-    rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
-    · rwa [succ_eq_add_one, Nat.sub_add_comm]
-    · rwa [length_reverse]
-  | inr h' =>
-    subst h'
-    rw [length, Nat.sub_self, drop]
-    suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
-      rw [this, take_length, reverse_cons]
-    rw [length_append, length_reverse]
-    rfl
+@[deprecated drop_drop (since := "2024-06-15")]
+theorem drop_add (m n) (l : List α) : drop (m + n) l = drop m (drop n l) := by
+  simp [drop_drop]
 
-@[deprecated (since := "2024-06-15")] abbrev reverse_take := @take_reverse
+/-! ### takeWhile and dropWhile -/
 
-theorem drop_reverse {α} {xs : List α} {n : Nat} (h : n ≤ xs.length) :
-    xs.reverse.drop n = (xs.take (xs.length - n)).reverse := by
-  conv =>
-    rhs
-    rw [← reverse_reverse xs]
-  rw [← reverse_reverse xs] at h
-  generalize xs.reverse = xs' at h ⊢
-  rw [take_reverse]
-  · simp only [length_reverse, reverse_reverse] at *
-    congr
-    omega
-  · simp only [length_reverse, sub_le]
+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]
+
+@[simp] theorem takeWhile_cons_of_pos {p : α → Bool} {a : α} {l : List α} (h : p a) :
+    (a :: l).takeWhile p = a :: l.takeWhile p := by
+  simp [takeWhile_cons, h]
+
+@[simp] theorem takeWhile_cons_of_neg {p : α → Bool} {a : α} {l : List α} (h : ¬ p a) :
+    (a :: l).takeWhile p = [] := by
+  simp [takeWhile_cons, h]
+
+theorem dropWhile_cons :
+    (x :: xs : List α).dropWhile p = if p x then xs.dropWhile p else x :: xs := by
+  split <;> simp_all [dropWhile]
+
+@[simp] theorem dropWhile_cons_of_pos {a : α} {l : List α} (h : p a) :
+    (a :: l).dropWhile p = l.dropWhile p := by
+  simp [dropWhile_cons, h]
+
+@[simp] theorem dropWhile_cons_of_neg {a : α} {l : List α} (h : ¬ p a) :
+    (a :: l).dropWhile p = a :: l := by
+  simp [dropWhile_cons, h]
+
+theorem head?_takeWhile (p : α → Bool) (l : List α) : (l.takeWhile p).head? = l.head?.filter p := by
+  cases l with
+  | nil => rfl
+  | cons x xs =>
+    simp only [takeWhile_cons, head?_cons, Option.filter_some]
+    split <;> simp
+
+theorem head_takeWhile (p : α → Bool) (l : List α) (w) :
+    (l.takeWhile p).head w = l.head (by rintro rfl; simp_all) := by
+  cases l with
+  | nil => rfl
+  | cons x xs =>
+    simp only [takeWhile_cons, head_cons]
+    simp only [takeWhile_cons] at w
+    split <;> simp_all
+
+theorem head?_dropWhile_not (p : α → Bool) (l : List α) :
+    match (l.dropWhile p).head? with | some x => p x = false | none => True := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [dropWhile_cons]
+    split <;> rename_i h <;> split at h <;> simp_all
+
+theorem head_dropWhile_not (p : α → Bool) (l : List α) (w) :
+    p ((l.dropWhile p).head w) = false := by
+  simpa [head?_eq_head, w] using head?_dropWhile_not p l
+
+theorem takeWhile_map (f : α → β) (p : β → Bool) (l : List α) :
+    (l.map f).takeWhile p = (l.takeWhile (p ∘ f)).map f := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [map_cons, takeWhile_cons]
+    split <;> simp_all
+
+theorem dropWhile_map (f : α → β) (p : β → Bool) (l : List α) :
+    (l.map f).dropWhile p = (l.dropWhile (p ∘ f)).map f := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [map_cons, dropWhile_cons]
+    split <;> simp_all
+
+theorem takeWhile_filterMap (f : α → Option β) (p : β → Bool) (l : List α) :
+    (l.filterMap f).takeWhile p = (l.takeWhile fun a => (f a).all p).filterMap f := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [filterMap_cons]
+    split <;> rename_i h
+    · simp only [takeWhile_cons, h]
+      split <;> simp_all
+    · simp [takeWhile_cons, h, ih]
+      split <;> simp_all [filterMap_cons]
+
+theorem dropWhile_filterMap (f : α → Option β) (p : β → Bool) (l : List α) :
+    (l.filterMap f).dropWhile p = (l.dropWhile fun a => (f a).all p).filterMap f := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [filterMap_cons]
+    split <;> rename_i h
+    · simp only [dropWhile_cons, h]
+      split <;> simp_all
+    · simp [dropWhile_cons, h, ih]
+      split <;> simp_all [filterMap_cons]
+
+theorem takeWhile_filter (p q : α → Bool) (l : List α) :
+    (l.filter p).takeWhile q = (l.takeWhile fun a => !p a || q a).filter p := by
+  simp [← filterMap_eq_filter, takeWhile_filterMap]
+
+theorem dropWhile_filter (p q : α → Bool) (l : List α) :
+    (l.filter p).dropWhile q = (l.dropWhile fun a => !p a || q a).filter p := by
+  simp [← filterMap_eq_filter, dropWhile_filterMap]
+
+@[simp] theorem takeWhile_append_dropWhile (p : α → Bool) :
+    ∀ (l : List α), takeWhile p l ++ dropWhile p l = l
+  | [] => rfl
+  | x :: xs => by simp [takeWhile, dropWhile]; cases p x <;> simp [takeWhile_append_dropWhile p xs]
+
+theorem takeWhile_append {xs ys : List α} :
+    (xs ++ ys).takeWhile p =
+      if (xs.takeWhile p).length = xs.length then xs ++ ys.takeWhile p else xs.takeWhile p := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [cons_append, takeWhile_cons]
+    split
+    · simp_all only [length_cons, add_one_inj]
+      split <;> rfl
+    · simp_all
+
+@[simp] theorem takeWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) :
+    (l₁ ++ l₂).takeWhile p = l₁ ++ l₂.takeWhile p := by
+  induction l₁ with
+  | nil => simp
+  | cons x xs ih => simp_all [takeWhile_cons]
+
+theorem dropWhile_append {xs ys : List α} :
+    (xs ++ ys).dropWhile p =
+      if (xs.dropWhile p).isEmpty then ys.dropWhile p else xs.dropWhile p ++ ys := by
+  induction xs with
+  | nil => simp
+  | cons h t ih =>
+    simp only [cons_append, dropWhile_cons]
+    split <;> simp_all
+
+@[simp] theorem dropWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) :
+    (l₁ ++ l₂).dropWhile p = l₂.dropWhile p := by
+  induction l₁ with
+  | nil => simp
+  | cons x xs ih => simp_all [dropWhile_cons]
+
+@[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
+
+theorem take_takeWhile {l : List α} (p : α → Bool) n :
+    (l.takeWhile p).take n = (l.takeWhile p).take n := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    by_cases h : p x <;> simp [takeWhile_cons, h, ih]
+
+@[simp] theorem all_takeWhile {l : List α} : (l.takeWhile p).all p = true := by
+  induction l with
+  | nil => rfl
+  | cons h t ih => by_cases p h <;> simp_all
+
+@[simp] theorem any_dropWhile {l : List α} :
+    (l.dropWhile p).any (fun x => !p x) = !l.all p := by
+  induction l with
+  | nil => rfl
+  | cons h t ih => by_cases p h <;> simp_all
 
 /-! ### 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
+@[simp] theorem rotateLeft_zero (l : List α) : rotateLeft l 0 = l := by
+  simp [rotateLeft]
+
+-- TODO Batteries defines its own `getElem?_rotate`, which we need to adapt.
+-- TODO Prove `map_rotateLeft`, using `ext` and `getElem?_rotateLeft`.
 
 /-! ### rotateRight -/
 
-@[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
+@[simp] theorem rotateRight_zero (l : List α) : rotateRight l 0 = l := by
+  simp [rotateRight]
 
-/-! ### zipWith -/
-
-@[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
-    length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;>
-    simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
-
-theorem lt_length_left_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
-    (h : i < (zipWith f l l').length) : i < l.length := by rw [length_zipWith] at h; omega
-
-theorem lt_length_right_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
-    (h : i < (zipWith f l l').length) : i < l'.length := by rw [length_zipWith] at h; omega
-
-@[simp]
-theorem getElem_zipWith {f : α → β → γ} {l : List α} {l' : List β}
-    {i : Nat} {h : i < (zipWith f l l').length} :
-    (zipWith f l l')[i] =
-      f (l[i]'(lt_length_left_of_zipWith h))
-        (l'[i]'(lt_length_right_of_zipWith h)) := by
-  rw [← Option.some_inj, ← getElem?_eq_getElem, getElem?_zipWith_eq_some]
-  exact
-    ⟨l[i]'(lt_length_left_of_zipWith h), l'[i]'(lt_length_right_of_zipWith h),
-      by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem]; exact ⟨rfl, rfl⟩⟩
-
-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₂]
-
-theorem reverse_zipWith (h : l.length = l'.length) :
-    (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by
-  induction l generalizing l' with
-  | nil => simp
-  | cons hd tl hl =>
-    cases l' with
-    | nil => simp
-    | cons hd' tl' =>
-      simp only [Nat.add_right_cancel_iff, length] at h
-      have : tl.reverse.length = tl'.reverse.length := by simp [h]
-      simp [hl h, zipWith_append _ _ _ _ _ this]
-
-@[deprecated reverse_zipWith (since := "2024-07-28")] abbrev zipWith_distrib_reverse := @reverse_zipWith
-
-@[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 lt_length_left_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) :
-    i < l.length :=
-  lt_length_left_of_zipWith h
-
-theorem lt_length_right_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) :
-    i < l'.length :=
-  lt_length_right_of_zipWith h
-
-@[simp]
-theorem getElem_zip {l : List α} {l' : List β} {i : Nat} {h : i < (zip l l').length} :
-    (zip l l')[i] =
-      (l[i]'(lt_length_left_of_zip h), l'[i]'(lt_length_right_of_zip h)) :=
-  getElem_zipWith (h := h)
-
-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
+-- TODO Batteries defines its own `getElem?_rotate`, which we need to adapt.
+-- TODO Prove `map_rotateRight`, using `ext` and `getElem?_rotateRight`.
 
 end List

src/Init/Data/List/Zip.lean

@@ -0,0 +1,363 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.TakeDrop
+
+/-!
+# Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`.
+-/
+
+namespace List
+
+open Nat
+
+/-! ## Zippers -/
+
+/-! ### zip -/
+
+theorem zip_map (f : α → γ) (g : β → δ) :
+    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
+  | [], l₂ => rfl
+  | l₁, [] => by simp only [map, zip_nil_right]
+  | a :: l₁, b :: l₂ => by
+    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
+
+theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
+    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
+
+theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
+    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
+
+theorem zip_append :
+    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
+      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
+  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
+  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
+  | a :: l₁, r₁, b :: l₂, r₂, h => by
+    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
+
+theorem zip_map' (f : α → β) (g : α → γ) :
+    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
+  | [] => rfl
+  | a :: l => by simp only [map, zip_cons_cons, zip_map']
+
+theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
+  | _ :: l₁, _ :: l₂, h => by
+    cases h
+    case head => simp
+    case tail h =>
+    · have := of_mem_zip h
+      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
+
+@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
+
+theorem map_fst_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
+  | [], bs, _ => rfl
+  | _ :: as, _ :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.fst (zip as bs) = _ :: as
+    rw [map_fst_zip as bs h]
+  | a :: as, [], h => by simp at h
+
+theorem map_snd_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
+  | _, [], _ => by
+    rw [zip_nil_right]
+    rfl
+  | [], b :: bs, h => by simp at h
+  | a :: as, b :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.snd (zip as bs) = _ :: bs
+    rw [map_snd_zip as bs h]
+
+theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
+  rw [← zip_map']
+  congr
+  exact map_id _
+
+theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (f x, x)) = (l.map f).zip l := by
+  rw [← zip_map']
+  congr
+  exact map_id _
+
+/-- 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 zipWith_comm (f : α → β → γ) :
+    ∀ (la : List α) (lb : List β), zipWith f la lb = zipWith (fun b a => f a b) lb la
+  | [], _ => List.zipWith_nil_right.symm
+  | _ :: _, [] => rfl
+  | _ :: as, _ :: bs => congrArg _ (zipWith_comm f as bs)
+
+theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : List α) :
+    zipWith f l l' = zipWith f l' l := by
+  rw [zipWith_comm]
+  simp only [comm]
+
+@[simp]
+theorem zipWith_same (f : α → α → δ) : ∀ l : List α, zipWith f l l = l.map fun a => f a a
+  | [] => rfl
+  | _ :: xs => congrArg _ (zipWith_same f xs)
+
+/--
+See also `getElem?_zipWith'` for a variant
+using `Option.map` and `Option.bind` rather than a `match`.
+-/
+theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
+    (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with
+      | some a, some b => some (f a b) | _, _ => none := by
+  induction as generalizing bs i with
+  | nil => cases bs with
+    | nil => simp
+    | cons b bs => simp
+  | cons a as aih => cases bs with
+    | nil => simp
+    | cons b bs => cases i <;> simp_all
+
+/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/
+theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
+    (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by
+  induction l₁ generalizing l₂ i with
+  | nil => rw [zipWith] <;> simp
+  | cons head tail =>
+    cases l₂
+    · simp
+    · cases i <;> simp_all
+
+theorem getElem?_zipWith_eq_some (f : α → β → γ) (l₁ : List α) (l₂ : List β) (z : γ) (i : Nat) :
+    (zipWith f l₁ l₂)[i]? = some z ↔
+      ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by
+  induction l₁ generalizing l₂ i
+  · simp
+  · cases l₂ <;> cases i <;> simp_all
+
+theorem getElem?_zip_eq_some (l₁ : List α) (l₂ : List β) (z : α × β) (i : Nat) :
+    (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by
+  cases z
+  rw [zip, getElem?_zipWith_eq_some]; constructor
+  · rintro ⟨x, y, h₀, h₁, h₂⟩
+    simpa [h₀, h₁] using h₂
+  · rintro ⟨h₀, h₁⟩
+    exact ⟨_, _, h₀, h₁, rfl⟩
+
+@[deprecated getElem?_zipWith (since := "2024-06-12")]
+theorem get?_zipWith {f : α → β → γ} :
+    (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with
+      | some a, some b => some (f a b) | _, _ => none := by
+  simp [getElem?_zipWith]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_zipWith (since := "2024-06-07")] abbrev zipWith_get? := @get?_zipWith
+
+theorem head?_zipWith {f : α → β → γ} :
+    (List.zipWith f as bs).head? = match as.head?, bs.head? with
+      | some a, some b => some (f a b) | _, _ => none := by
+  simp [head?_eq_getElem?, getElem?_zipWith]
+
+theorem head_zipWith {f : α → β → γ} (h):
+    (List.zipWith f as bs).head h = f (as.head (by rintro rfl; simp_all)) (bs.head (by rintro rfl; simp_all)) := by
+  apply Option.some.inj
+  rw [← head?_eq_head, head?_zipWith, head?_eq_head, head?_eq_head]
+
+@[simp]
+theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
+    zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
+
+theorem zipWith_map_left (l₁ : List α) (l₂ : List β) (f : α → α') (g : α' → β → γ) :
+    zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
+
+theorem zipWith_map_right (l₁ : List α) (l₂ : List β) (f : β → β') (g : α → β' → γ) :
+    zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
+
+theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
+    (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
+
+theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
+    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by
+  induction l₁ generalizing i l₂ <;> cases l₂ <;> simp_all
+
+@[simp]
+theorem zipWith_eq_nil_iff {f : α → β → γ} {l l'} : zipWith f l l' = [] ↔ l = [] ∨ l' = [] := by
+  cases l <;> cases l' <;> simp
+
+theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : List γ) (l' : List δ) :
+    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by
+  induction l generalizing l' with
+  | nil => simp
+  | cons hd tl hl =>
+    · cases l'
+      · simp
+      · simp [hl]
+
+theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by
+  induction l generalizing l' n with
+  | nil => simp
+  | cons hd tl hl =>
+    cases l'
+    · simp
+    · cases n
+      · simp
+      · simp [hl]
+
+@[deprecated take_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_take := @take_zipWith
+
+theorem drop_zipWith : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n) := by
+  induction l generalizing l' n with
+  | nil => simp
+  | cons hd tl hl =>
+    · cases l'
+      · simp
+      · cases n
+        · simp
+        · simp [hl]
+
+@[deprecated drop_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_drop := @drop_zipWith
+
+theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
+  rw [← drop_one]; simp [drop_zipWith]
+
+@[deprecated tail_zipWith (since := "2024-07-28")] abbrev zipWith_distrib_tail := @tail_zipWith
+
+theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
+    (h : l.length = l'.length) :
+    zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by
+  induction l generalizing l' with
+  | nil =>
+    have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
+    simp [this]
+  | cons hl tl ih =>
+    cases l' with
+    | nil => simp at h
+    | cons head tail =>
+      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} :
+    (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
+  | nil => induction bs generalizing i with
+    | nil => simp
+    | cons b bs bih => cases i <;> simp_all
+  | cons a as aih => cases bs with
+    | nil =>
+      specialize @aih []
+      cases i <;> simp_all
+    | cons b bs => cases i <;> simp_all
+
+@[deprecated getElem?_zipWithAll (since := "2024-06-12")]
+theorem get?_zipWithAll {f : Option α → Option β → γ} :
+    (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with
+      | none, none => .none | a?, b? => some (f a? b?) := by
+  simp [getElem?_zipWithAll]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_zipWithAll (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll
+
+theorem head?_zipWithAll {f : Option α → Option β → γ} :
+    (zipWithAll f as bs).head? = match as.head?, bs.head? with
+      | none, none => .none | a?, b? => some (f a? b?) := by
+  simp [head?_eq_getElem?, getElem?_zipWithAll]
+
+theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
+    (zipWithAll f as bs).head h = f as.head? bs.head? := by
+  apply Option.some.inj
+  rw [← head?_eq_head, head?_zipWithAll]
+  split <;> simp_all
+
+theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
+    zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
+
+theorem zipWithAll_map_left (l₁ : List α) (l₂ : List β) (f : α → α') (g : Option α' → Option β → γ) :
+    zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂ := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
+
+theorem zipWithAll_map_right (l₁ : List α) (l₂ : List β) (f : β → β') (g : Option α → Option β' → γ) :
+    zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂ := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
+
+theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option δ → α) (l : List γ) (l' : List δ) :
+    map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l' := by
+  induction l generalizing l' with
+  | nil => simp
+  | cons hd tl hl =>
+    cases l' <;> simp_all
+
+@[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_fst : (unzip l).fst = l.map Prod.fst := by
+  induction l <;> simp_all
+
+@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
+  induction l <;> simp_all
+
+@[deprecated unzip_fst (since := "2024-07-28")] abbrev unzip_left := @unzip_fst
+@[deprecated unzip_snd (since := "2024-07-28")] abbrev unzip_right := @unzip_snd
+
+theorem unzip_eq_map : ∀ l : List (α × β), unzip l = (l.map Prod.fst, l.map Prod.snd)
+  | [] => rfl
+  | (a, b) :: l => by simp only [unzip_cons, map_cons, unzip_eq_map l]
+
+theorem zip_unzip : ∀ l : List (α × β), zip (unzip l).1 (unzip l).2 = l
+  | [] => rfl
+  | (a, b) :: l => by simp only [unzip_cons, zip_cons_cons, zip_unzip l]
+
+theorem unzip_zip_left :
+    ∀ {l₁ : List α} {l₂ : List β}, length l₁ ≤ length l₂ → (unzip (zip l₁ l₂)).1 = l₁
+  | [], l₂, _ => rfl
+  | l₁, [], h => by rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]; rfl
+  | a :: l₁, b :: l₂, h => by
+    simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)]
+
+theorem unzip_zip_right :
+    ∀ {l₁ : List α} {l₂ : List β}, length l₂ ≤ length l₁ → (unzip (zip l₁ l₂)).2 = l₂
+  | [], l₂, _ => by simp_all
+  | l₁, [], _ => by simp
+  | a :: l₁, b :: l₂, h => by
+    simp only [zip_cons_cons, unzip_cons, unzip_zip_right (le_of_succ_le_succ h)]
+
+theorem unzip_zip {l₁ : List α} {l₂ : List β} (h : length l₁ = length l₂) :
+    unzip (zip l₁ l₂) = (l₁, l₂) := by
+  ext
+  · rw [unzip_zip_left (Nat.le_of_eq h)]
+  · rw [unzip_zip_right (Nat.le_of_eq h.symm)]
+
+theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp.map Prod.fst = l)
+    (hr : lp.map Prod.snd = l') : lp = l.zip l' := by
+  rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
+
+@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
+    unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
+  ext1 <;> simp

src/Init/Data/Nat/Basic.lean

@@ -102,6 +102,13 @@ def blt (a b : Nat) : Bool :=
 attribute [simp] Nat.zero_le
 attribute [simp] Nat.not_lt_zero
 
+theorem and_forall_add_one {p : Nat → Prop} : p 0 ∧ (∀ n, p (n + 1)) ↔ ∀ n, p n :=
+  ⟨fun h n => Nat.casesOn n h.1 h.2, fun h => ⟨h _, fun _ => h _⟩⟩
+
+theorem or_exists_add_one : p 0 ∨ (Exists fun n => p (n + 1)) ↔ Exists p :=
+  ⟨fun h => h.elim (fun h0 => ⟨0, h0⟩) fun ⟨n, hn⟩ => ⟨n + 1, hn⟩,
+    fun ⟨n, h⟩ => match n with | 0 => Or.inl h | n+1 => Or.inr ⟨n, h⟩⟩
+
 /-! # Helper "packing" theorems -/
 
 @[simp] theorem zero_eq : Nat.zero = 0 := rfl

src/Init/Data/Nat/Lemmas.lean

@@ -20,7 +20,12 @@ and later these lemmas should be organised into other files more systematically.
 
 namespace Nat
 
-attribute [simp] not_lt_zero
+@[deprecated and_forall_add_one (since := "2024-07-30")] abbrev and_forall_succ := @and_forall_add_one
+@[deprecated or_exists_add_one (since := "2024-07-30")] abbrev or_exists_succ := @or_exists_add_one
+
+@[simp] theorem exists_ne_zero {P : Nat → Prop} : (∃ n, ¬ n = 0 ∧ P n) ↔ ∃ n, P (n + 1) :=
+  ⟨fun ⟨n, h, w⟩ => by cases n with | zero => simp at h | succ n => exact ⟨n, w⟩,
+    fun ⟨n, w⟩ => ⟨n + 1, by simp, w⟩⟩
 
 /-! ## add -/
 

src/Init/Omega/IntList.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 prelude
-import Init.Data.List.Lemmas
+import Init.Data.List.Zip
 import Init.Data.Int.DivModLemmas
 import Init.Data.Nat.Gcd
 

src/Init/PropLemmas.lean

@@ -202,6 +202,17 @@ theorem exists_imp : ((∃ x, p x) → b) ↔ ∀ x, p x → b := forall_exists_
 @[simp] theorem exists_const (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b :=
   ⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩
 
+@[congr]
+theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
+    Exists q ↔ ∃ h : p', q' (hp.2 h) :=
+  ⟨fun ⟨_, _⟩ ↦ ⟨hp.1 ‹_›, (hq _).1 ‹_›⟩, fun ⟨_, _⟩ ↦ ⟨_, (hq _).2 ‹_›⟩⟩
+
+theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (Exists fun h' : p => q h') ↔ q h :=
+  @exists_const (q h) p ⟨h⟩
+
+@[simp] theorem exists_true_left (p : True → Prop) : Exists p ↔ p True.intro :=
+  exists_prop_of_true _
+
 section forall_congr
 
 theorem forall_congr' (h : ∀ a, p a ↔ q a) : (∀ a, p a) ↔ ∀ a, q a :=

src/Lean/Elab/App.lean

@@ -743,7 +743,7 @@ structure State where
 abbrev M := ReaderT Context $ StateRefT State TermElabM
 
 /-- Infer the `motive` using the expected type by `kabstract`ing the discriminants. -/
-def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
+def mkMotive (discrs : Array Expr) (expectedType : Expr) : MetaM Expr := do
   discrs.foldrM (init := expectedType) fun discr motive => do
     let discr ← instantiateMVars discr
     let motiveBody ← kabstract motive discr
@@ -878,7 +878,16 @@ partial def main : M Expr := do
     main
   let idx := (← get).idx
   if (← read).elimInfo.motivePos == idx then
-    let motive ← mkImplicitArg binderType binderInfo
+    let motive ←
+      match (← getNextArg? binderName binderInfo) with
+      | .some arg =>
+        /- Due to `Lean.Elab.Term.elabAppArgs.elabAsElim?`, this must be a positional argument that is the syntax `_`. -/
+        elabArg arg binderType
+      | .none | .undef =>
+        /- Note: undef occurs when the motive is explicit but missing.
+           In this case, we treat it as if it were an implicit argument
+           to support writing `h.rec` when `h : False`, rather than requiring `h.rec _`. -/
+        mkImplicitArg binderType binderInfo
     setMotive motive
     addArgAndContinue motive
   else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then
@@ -970,15 +979,34 @@ where
     unless (← shouldElabAsElim declName) do return none
     let elimInfo ← getElimInfo declName
     forallTelescopeReducing (← inferType f) fun xs _ => do
-      if h : elimInfo.motivePos < xs.size then
-        let x := xs[elimInfo.motivePos]
+      /- Process arguments similar to `Lean.Elab.Term.ElabElim.main` to see if the motive has been
+         provided, in which case we use the standard app elaborator.
+         If the motive is explicit (like for `False.rec`), then a positional `_` counts as "not provided". -/
+      let mut args := args.toList
+      let mut namedArgs := namedArgs.toList
+      for x in xs[0:elimInfo.motivePos] do
         let localDecl ← x.fvarId!.getDecl
-        if findBinderName? namedArgs.toList localDecl.userName matches some _ then
+        match findBinderName? namedArgs localDecl.userName with
+        | some _ => namedArgs := eraseNamedArg namedArgs localDecl.userName
+        | none   => if localDecl.binderInfo.isExplicit then args := args.tailD []
+      -- Invariant: `elimInfo.motivePos < xs.size` due to construction of `elimInfo`.
+      let some x := xs[elimInfo.motivePos]? | unreachable!
+      let localDecl ← x.fvarId!.getDecl
+      if findBinderName? namedArgs localDecl.userName matches some _ then
+        -- motive has been explicitly provided, so we should use standard app elaborator
+        return none
+      else
+        match localDecl.binderInfo.isExplicit, args with
+        | true, .expr _ :: _  =>
           -- motive has been explicitly provided, so we should use standard app elaborator
           return none
-        return some elimInfo
-      else
-        return none
+        | true, .stx arg :: _ =>
+          if arg.isOfKind ``Lean.Parser.Term.hole then
+            return some elimInfo
+          else
+            -- positional motive is not `_`, so we should use standard app elaborator
+            return none
+        | _, _ => return some elimInfo
 
   /--
   Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`.

src/Lean/Elab/Deriving/DecEq.lean

@@ -91,8 +91,14 @@ def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): T
   let header  ← mkDecEqHeader indVal
   let body    ← mkMatch ctx header indVal
   let binders := header.binders
-  let type    ← `(Decidable ($(mkIdent header.targetNames[0]!) = $(mkIdent header.targetNames[1]!)))
-  `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term)
+  let target₁ := mkIdent header.targetNames[0]!
+  let target₂ := mkIdent header.targetNames[1]!
+  let termSuffix ← if indVal.isRec
+    then `(Parser.Termination.suffix|termination_by structural $target₁)
+    else `(Parser.Termination.suffix|)
+  let type    ← `(Decidable ($target₁ = $target₂))
+  `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term
+    $termSuffix:suffix)
 
 def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do
   let mut res : Array (TSyntax `command) := #[]

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

@@ -6,7 +6,7 @@ Authors: Scott Morrison
 prelude
 import Init.BinderPredicates
 import Init.Data.Int.Order
-import Init.Data.List.Lemmas
+import Init.Data.List.MinMax
 import Init.Data.Nat.MinMax
 import Init.Data.Option.Lemmas
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -339,19 +339,22 @@ inductive AppImplicitArg
   | skip
   /-- A regular argument. -/
   | regular (s : Term)
+  /-- A regular argument that, if it comes as the last argument, may be omitted. -/
+  | optional (name : Name) (s : Term)
   /-- It's a named argument. Named arguments inhibit applying unexpanders. -/
   | named (s : TSyntax ``Parser.Term.namedArgument)
   deriving Inhabited
 
 /-- Whether unexpanding is allowed with this argument. -/
 def AppImplicitArg.canUnexpand : AppImplicitArg → Bool
-  | .regular .. | .skip => true
+  | .regular .. | .optional .. | .skip => true
   | .named .. => false
 
 /-- If the argument has associated syntax, returns it. -/
 def AppImplicitArg.syntax? : AppImplicitArg → Option Syntax
   | .skip => none
   | .regular s => s
+  | .optional _ s => s
   | .named s => s
 
 /--
@@ -371,13 +374,13 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
       appFieldNotationCandidate?
     else
       pure none
-  let (fnStx, args) ←
+  let (fnStx, args') ←
     withBoundedAppFnArgs numArgs
       (do return ((← delabHead), Array.mkEmpty numArgs))
-      (fun (fnStx, args) => do
-        let idx := args.size
-        let arg ← mkArg (numArgs - idx - 1) paramKinds[idx]!
-        return (fnStx, args.push arg))
+      (fun (fnStx, args) => return (fnStx, args.push (← mkArg paramKinds[args.size]!)))
+
+  -- Strip off optional arguments. We save the original `args'` for structure instance notation
+  let args := args'.popWhile (· matches .optional ..)
 
   -- App unexpanders
   if ← pure unexpand <&&> getPPOption getPPNotation then
@@ -385,11 +388,10 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
     if let some stx ← (some <$> tryAppUnexpanders fnStx args) <|> pure none then
       return stx
 
-  let stx := Syntax.mkApp fnStx (args.filterMap (·.syntax?))
-
   -- Structure instance notation
-  if ← pure (unexpand && args.all (·.canUnexpand)) <&&> getPPOption getPPStructureInstances then
+  if ← pure (unexpand && args'.all (·.canUnexpand)) <&&> getPPOption getPPStructureInstances then
     -- Try using the structure instance unexpander.
+    let stx := Syntax.mkApp fnStx (args'.filterMap (·.syntax?))
     if let some stx ← (some <$> unexpandStructureInstance stx) <|> pure none then
       return stx
 
@@ -416,7 +418,7 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
         return Syntax.mkApp head (args'.filterMap (·.syntax?))
 
   -- Normal application
-  return stx
+  return Syntax.mkApp fnStx (args.filterMap (·.syntax?))
 where
   mkNamedArg (name : Name) : DelabM AppImplicitArg :=
     return .named <| ← `(Parser.Term.namedArgument| ($(mkIdent name) := $(← delab)))
@@ -424,15 +426,16 @@ where
   Delaborates the current argument.
   The argument `remainingArgs` is the number of arguments in the application after this one.
   -/
-  mkArg (remainingArgs : Nat) (param : ParamKind) : DelabM AppImplicitArg := do
+  mkArg (param : ParamKind) : DelabM AppImplicitArg := do
     let arg ← getExpr
     if ← getPPOption getPPAnalysisSkip then return .skip
     else if ← getPPOption getPPAnalysisHole then return .regular (← `(_))
     else if ← getPPOption getPPAnalysisNamedArg then
       mkNamedArg param.name
-    else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
-      -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
-      return .skip
+    else if param.defVal.isSome && param.defVal.get! == arg then
+      -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument, if it is the last one.
+      -- We will later remove all optional arguments from the end.
+      return .optional param.name (← delab)
     else if param.bInfo.isExplicit then
       return .regular (← delab)
     else if ← pure (param.name == `motive) <&&> shouldShowMotive arg (← getOptions) then

src/Lean/Util/FindExpr.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Expr
-import Lean.Util.PtrSet
 
 namespace Lean
 namespace Expr

src/Lean/Util/FoldConsts.lean

@@ -11,52 +11,35 @@ namespace Lean
 namespace Expr
 namespace FoldConstsImpl
 
-abbrev cacheSize : USize := 8192 - 1
+unsafe structure State where
+ visited       : PtrSet Expr := mkPtrSet
+ visitedConsts : NameHashSet := {}
 
-structure State where
-  visitedTerms  : Array Expr  -- Remark: cache based on pointer address. Our "unsafe" implementation relies on the fact that `()` is not a valid Expr
-  visitedConsts : NameHashSet -- cache based on structural equality
+unsafe abbrev FoldM := StateM State
 
-abbrev FoldM := StateM State
-
-unsafe def visited (e : Expr) (size : USize) : FoldM Bool := do
-  let s ← get
-  let h := ptrAddrUnsafe e
-  let i := h % size
-  let k := s.visitedTerms.uget i lcProof
-  if ptrAddrUnsafe k == h then pure true
-  else do
-    modify fun s => { s with visitedTerms := s.visitedTerms.uset i e lcProof }
-    pure false
-
-unsafe def fold {α : Type} (f : Name → α → α) (size : USize) (e : Expr) (acc : α) : FoldM α :=
+unsafe def fold {α : Type} (f : Name → α → α) (e : Expr) (acc : α) : FoldM α :=
   let rec visit (e : Expr) (acc : α) : FoldM α := do
-    if (← visited e size) then
-      pure acc
-    else
-      match e with
-      | Expr.forallE _ d b _   => visit b (← visit d acc)
-      | Expr.lam _ d b _       => visit b (← visit d acc)
-      | Expr.mdata _ b         => visit b acc
-      | Expr.letE _ t v b _    => visit b (← visit v (← visit t acc))
-      | Expr.app f a           => visit a (← visit f acc)
-      | Expr.proj _ _ b        => visit b acc
-      | Expr.const c _         =>
-        let s ← get
-        if s.visitedConsts.contains c then
-          pure acc
-        else do
-          modify fun s => { s with visitedConsts := s.visitedConsts.insert c };
-          pure $ f c acc
-      | _                      => pure acc
+    if (← get).visited.contains e then
+      return acc
+    modify fun s => { s with visited := s.visited.insert e }
+    match e with
+    | .forallE _ d b _   => visit b (← visit d acc)
+    | .lam _ d b _       => visit b (← visit d acc)
+    | .mdata _ b         => visit b acc
+    | .letE _ t v b _    => visit b (← visit v (← visit t acc))
+    | .app f a           => visit a (← visit f acc)
+    | .proj _ _ b        => visit b acc
+    | .const c _         =>
+      if (← get).visitedConsts.contains c then
+        return acc
+      else
+        modify fun s => { s with visitedConsts := s.visitedConsts.insert c };
+        return f c acc
+    | _ => return acc
   visit e acc
 
-unsafe def initCache : State :=
-  { visitedTerms  := mkArray cacheSize.toNat (cast lcProof ()),
-    visitedConsts := {} }
-
 @[inline] unsafe def foldUnsafe {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α :=
-  (fold f cacheSize e init).run' initCache
+  (fold f e init).run' {}
 
 end FoldConstsImpl
 

tests/lean/276.lean

@@ -5,5 +5,5 @@ set_option pp.all true in
 #check fun {α : Sort v} => PEmpty.rec (fun _ => α)
 
 -- but `def` doesn't work
--- error: (kernel) compiler failed to infer low level type, unknown declaration 'PEmpty.rec'
+-- error: code generator does not support recursor 'PEmpty.rec' yet
 def PEmpty.elim' {α : Sort v} := PEmpty.rec (fun _ => α)

tests/lean/276.lean.expected.out

@@ -1,3 +1,2 @@
-276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available
-fun {α : Sort v} => @?m α : {α : Sort v} → @?m α
-276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available
+fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α
+276.lean:9:4-9:16: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion

tests/lean/decEqMutualInductives.lean.expected.out

@@ -6,6 +6,7 @@
            let inst✝ := decEqListTree✝ @a✝ @b✝;
            if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝
            else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
+       termination_by structural x✝
        private def decEqListTree✝ (x✝² : @ListTree✝) (x✝³ : @ListTree✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @ListTree.nil, @ListTree.nil => isTrue✝¹ rfl✝¹
@@ -19,6 +20,7 @@
                if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝²
                else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption)
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption)
+       termination_by structural x✝²
      end,
      instance : DecidableEq✝ (@ListTree✝) :=
        decEqListTree✝]
@@ -33,18 +35,21 @@
            let inst✝ := decEqFoo₂✝ @a✝ @b✝;
            if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
            else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption)
+       termination_by structural x✝
        private def decEqFoo₂✝ (x✝² : @Foo₂✝) (x✝³ : @Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @Foo₂.foo₂ a✝¹, @Foo₂.foo₂ b✝¹ =>
            let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹;
            if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
            else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption)
+       termination_by structural x✝²
        private def decEqFoo₃✝ (x✝⁴ : @Foo₃✝) (x✝⁵ : @Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
          match x✝⁴, x✝⁵ with
          | @Foo₃.foo₃ a✝², @Foo₃.foo₃ b✝² =>
            let inst✝² := decEqFoo₁✝ @a✝² @b✝²;
            if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption)
+       termination_by structural x✝⁴
      end,
      instance : DecidableEq✝ (@Foo₁✝) :=
        decEqFoo₁✝]

tests/lean/delabApp.lean

@@ -1,51 +0,0 @@
-/-!
-# Testing features of the app delaborator, including overapplication
--/
-
-/-!
-Check that the optional value equality check is specialized to the supplied arguments
-(rather than, formerly, the locally-defined fvars from a telescope).
--/
-def foo (α : Type) [Inhabited α] (x : α := default) : α := x
-
-#check foo Nat
-#check foo Nat 1
-
-/-!
-Check that optional value omission is aware of unfolding.
--/
-def Ty := (x : Nat := 1) → Fin (x + 1)
-
-def f (y : Nat := 2) : Ty := fun x => 0
-
-#check f 3 4
-#check f 3
-#check (f)
-
-
-/-!
-Check that overapplied projections pretty print using projection notation.
--/
-
-structure Foo where
-  f : Nat → Nat
-
-#check ∀ (x : Foo), x.f 1 = 0
-
-/-!
-Overapplied `letFun`
--/
-#check (have f := id; f) 1
-
-/-!
-Overapplied `OfNat.ofNat`
--/
-instance : OfNat (Nat → Nat) 1 where
-  ofNat := id
-
-#check (1 : Nat → Nat) 2
-
-/-!
-Overapplied `dite`
--/
-#check (if h : True then id else id) 1

tests/lean/delabApp.lean.expected.out

@@ -1,11 +0,0 @@
-foo Nat : Nat
-foo Nat 1 : Nat
-f 3 4 : Fin (4 + 1)
-f 3 : Fin (1 + 1)
-f 2 : Fin (1 + 1)
-∀ (x : Foo), x.f 1 = 0 : Prop
-(let_fun f := id;
-  f)
-  1 : Nat
-1 2 : Nat
-(if h : True then id else id) 1 : Nat

tests/lean/run/1697.lean

@@ -8,7 +8,7 @@ error: cannot evaluate expression that depends on the `sorry` axiom.
 Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 -/
 #guard_msgs in
-#eval show Nat from False.rec (by decide)
+#eval show Nat from False.elim (by decide)
 
 /--
 warning: declaration uses 'sorry'

tests/lean/run/delabApp.lean

@@ -0,0 +1,79 @@
+/-!
+# Testing features of the app delaborator, including overapplication
+-/
+
+/-!
+Check that the optional value equality check is specialized to the supplied arguments
+(rather than, formerly, the locally-defined fvars from a telescope).
+-/
+def foo (α : Type) [Inhabited α] (x : α := default) : α := x
+
+/-- info: foo Nat : Nat -/
+#guard_msgs in #check foo Nat
+/-- info: foo Nat 1 : Nat -/
+#guard_msgs in #check foo Nat 1
+
+/-!
+Check that optional value omission is aware of unfolding.
+-/
+def Ty := (x : Nat := 1) → Fin (x + 1)
+
+def f (y : Nat := 2) : Ty := fun x => 0
+
+/-- info: f 3 4 : Fin (4 + 1) -/
+#guard_msgs in #check f 3 4
+/-- info: f 3 : Fin (1 + 1) -/
+#guard_msgs in #check f 3
+/-- info: f : Fin (1 + 1) -/
+#guard_msgs in #check (f)
+
+
+/-!
+Check that overapplied projections pretty print using projection notation.
+-/
+
+structure Foo where
+  f : Nat → Nat
+
+/-- info: ∀ (x : Foo), x.f 1 = 0 : Prop -/
+#guard_msgs in #check ∀ (x : Foo), x.f 1 = 0
+
+/-!
+Overapplied `letFun`
+-/
+/--
+info: (let_fun f := id;
+  f)
+  1 : Nat
+-/
+#guard_msgs in #check (have f := id; f) 1
+
+/-!
+Overapplied `OfNat.ofNat`
+-/
+instance : OfNat (Nat → Nat) 1 where
+  ofNat := id
+
+/-- info: 1 2 : Nat -/
+#guard_msgs in #check (1 : Nat → Nat) 2
+
+/-!
+Overapplied `dite`
+-/
+
+/-- info: (if _h : True then id else id) 1 : Nat -/
+#guard_msgs in #check (if _h : True then id else id) 1
+
+
+/-!
+Testing that multiple optional arguments are omitted rather than just the last (issue #4812)
+-/
+
+def g (a : Nat) (b := 1) (c := 2) (d := 3) := a + b + c + d
+
+/-- info: g 0 : Nat -/
+#guard_msgs in #check g 0
+
+-- Both the `start` and `stop` arguments are omitted.
+/-- info: fun a => Array.foldl (fun x y => x + y) 0 a : Array Nat → Nat -/
+#guard_msgs in #check fun (a : Array Nat) => a.foldl (fun x y => x + y) 0

tests/lean/run/elabAsElim.lean

@@ -175,3 +175,14 @@ def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k
 theorem leRecOn_self {C : Nat → Sort _} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
     (leRecOn n.le_refl next x : C n) = x :=
   sorry
+
+/-!
+Issue https://github.com/leanprover/lean4/issues/4347
+
+`False.rec` has `motive` as an explicit argument.
+-/
+
+example (h : False) : Nat := False.rec (fun _ => Nat) h
+example (h : False) : Nat := False.rec _ h
+example (h : False) : Nat := h.rec
+example (h : False) : Nat := h.rec _

tests/lean/run/emptyLcnf.lean

@@ -3,7 +3,7 @@ import Lean
 inductive MyEmpty
 
 def f (x : MyEmpty) : Nat :=
-  MyEmpty.casesOn x
+  MyEmpty.casesOn _ x
 
 set_option trace.Compiler.result true
 /--

tests/lean/run/simp_cache_perf_issue.lean

@@ -1,7 +1,3 @@
-@[congr]
-theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
-    Exists q ↔ ∃ h : p', q' (hp.2 h) := sorry
-
 set_option maxHeartbeats 1000 in
 example (x : Nat) :
   ∃ (h : x = x)