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

src/Init/Data/Array.lean

@@ -27,3 +27,4 @@ import Init.Data.Array.Range
 import Init.Data.Array.Erase
 import Init.Data.Array.Zip
 import Init.Data.Array.InsertIdx
+import Init.Data.Array.Extract

src/Init/Data/Array/Basic.lean

@@ -902,6 +902,10 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
     as
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
+@[simp] theorem popWhile_empty (p : α → Bool) :
+    popWhile p #[] = #[] := by
+  simp [popWhile]
+
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (r : Array α) : Array α :=

src/Init/Data/Array/Extract.lean

@@ -0,0 +1,427 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.TakeDrop
+
+/-!
+# Lemmas about `Array.extract`
+
+This file follows the contents of `Init.Data.List.TakeDrop` and `Init.Data.List.Nat.TakeDrop`.
+-/
+
+open Nat
+namespace Array
+
+/-! ### extract -/
+
+@[simp] theorem extract_of_size_lt {as : Array α} {i j : Nat} (h : as.size < j) :
+    as.extract i j = as.extract i as.size := by
+  ext l h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract] at h₁ h₂
+    simp [h]
+
+theorem size_extract_le {as : Array α} {i j : Nat} :
+    (as.extract i j).size ≤ j - i := by
+  simp
+  omega
+
+theorem size_extract_le' {as : Array α} {i j : Nat} :
+    (as.extract i j).size ≤ as.size - i := by
+  simp
+  omega
+
+theorem size_extract_of_le {as : Array α} {i j : Nat} (h : j ≤ as.size) :
+    (as.extract i j).size = j - i := by
+  simp
+  omega
+
+@[simp]
+theorem extract_push {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
+    (as.push b).extract start stop = as.extract start stop := by
+  ext i h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, size_push] at h₁ h₂
+    simp only [getElem_extract, getElem_push]
+    rw [dif_pos (by omega)]
+
+@[simp]
+theorem extract_eq_pop {as : Array α} {stop : Nat} (h : stop = as.size - 1) :
+    as.extract 0 stop = as.pop := by
+  ext i h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, size_pop] at h₁ h₂
+    simp [getElem_extract, getElem_pop]
+
+@[simp]
+theorem extract_append_extract {as : Array α} {i j k : Nat} :
+    as.extract i j ++ as.extract j k = as.extract (min i j) (max j k) := by
+  ext l h₁ h₂
+  · simp
+    omega
+  · simp only [size_append, size_extract] at h₁ h₂
+    simp only [getElem_append, size_extract, getElem_extract]
+    split <;>
+    · congr 1
+      omega
+
+@[simp]
+theorem extract_eq_empty_iff {as : Array α} :
+    as.extract i j = #[] ↔ min j as.size ≤ i := by
+  constructor
+  · intro h
+    replace h := congrArg Array.size h
+    simp at h
+    omega
+  · intro h
+    exact eq_empty_of_size_eq_zero (by simp; omega)
+
+theorem extract_eq_empty_of_le {as : Array α} (h : min j as.size ≤ i) :
+    as.extract i j = #[] :=
+  extract_eq_empty_iff.2 h
+
+theorem lt_of_extract_ne_empty {as : Array α} (h : as.extract i j ≠ #[]) :
+    i < min j as.size :=
+  gt_of_not_le (mt extract_eq_empty_of_le h)
+
+@[simp]
+theorem extract_eq_self_iff {as : Array α} :
+    as.extract i j = as ↔ as.size = 0 ∨ i = 0 ∧ as.size ≤ j := by
+  constructor
+  · intro h
+    replace h := congrArg Array.size h
+    simp at h
+    omega
+  · intro h
+    ext l h₁ h₂
+    · simp
+      omega
+    · simp only [size_extract] at h₁
+      simp only [getElem_extract]
+      congr 1
+      omega
+
+theorem extract_eq_self_of_le {as : Array α} (h : as.size ≤ j) :
+    as.extract 0 j = as :=
+  extract_eq_self_iff.2 (.inr ⟨rfl, h⟩)
+
+theorem le_of_extract_eq_self {as : Array α} (h : as.extract i j = as) :
+    as.size ≤ j := by
+  replace h := congrArg Array.size h
+  simp at h
+  omega
+
+@[simp]
+theorem extract_size_left {as : Array α} :
+    as.extract as.size j = #[] := by
+  simp
+  omega
+
+@[simp]
+theorem push_extract_getElem {as : Array α} {i j : Nat} (h : j < as.size) :
+    (as.extract i j).push as[j] = as.extract (min i j) (j + 1) := by
+  ext l h₁ h₂
+  · simp
+    omega
+  · simp only [size_push, size_extract] at h₁ h₂
+    simp only [getElem_push, size_extract, getElem_extract]
+    split <;>
+    · congr
+      omega
+
+theorem extract_succ_right {as : Array α} {i j : Nat} (w : i < j + 1) (h : j < as.size) :
+    as.extract i (j + 1) = (as.extract i j).push as[j] := by
+  ext l h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, push_extract_getElem] at h₁ h₂
+    simp only [getElem_extract, push_extract_getElem]
+    congr
+    omega
+
+theorem extract_sub_one {as : Array α} {i j : Nat} (h : j < as.size) :
+    as.extract i (j - 1) = (as.extract i j).pop := by
+  ext l h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, size_pop] at h₁ h₂
+    simp only [getElem_extract, getElem_pop]
+
+@[simp]
+theorem getElem?_extract_of_lt {as : Array α} {i j k : Nat} (h : k < min j as.size - i) :
+    (as.extract i j)[k]? = some (as[i + k]'(by omega)) := by
+  simp [getElem?_extract, h]
+
+theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
+    (as.extract 0 (j + 1))[j]? = as[j]? := by
+  simp [getElem?_extract]
+  omega
+
+@[simp] theorem extract_extract {as : Array α} {i j k l : Nat} :
+    (as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := by
+  ext m h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract] at h₁ h₂
+    simp [Nat.add_assoc]
+
+theorem extract_eq_empty_of_eq_empty {as : Array α} {i j : Nat} (h : as = #[]) :
+    as.extract i j = #[] := by
+  simp [h]
+
+theorem ne_empty_of_extract_ne_empty {as : Array α} {i j : Nat} (h : as.extract i j ≠ #[]) :
+    as ≠ #[] :=
+  mt extract_eq_empty_of_eq_empty h
+
+theorem extract_set {as : Array α} {i j k : Nat} (h : k < as.size) {a : α} :
+    (as.set k a).extract i j =
+      if _ : k < i then
+        as.extract i j
+      else if _ : k < min j as.size then
+        (as.extract i j).set (k - i) a (by simp; omega)
+      else as.extract i j := by
+  split
+  · ext l h₁ h₂
+    · simp
+    · simp at h₁ h₂
+      simp [getElem_set]
+      omega
+  · split
+    · ext l h₁ h₂
+      · simp
+      · simp only [getElem_extract, getElem_set]
+        split
+        · rw [if_pos]; omega
+        · rw [if_neg]; omega
+    · ext l h₁ h₂
+      · simp
+      · simp at h₁ h₂
+        simp [getElem_set]
+        omega
+
+theorem set_extract {as : Array α} {i j k : Nat} (h : k < (as.extract i j).size) {a : α} :
+    (as.extract i j).set k a = (as.set (i + k) a (by simp at h; omega)).extract i j := by
+  ext l h₁ h₂
+  · simp
+  · simp_all [getElem_set]
+
+@[simp]
+theorem extract_append {as bs : Array α} {i j : Nat} :
+    (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size) := by
+  ext l h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, size_append] at h₁ h₂
+    simp only [getElem_extract, getElem_append, size_extract]
+    split
+    · split
+      · rfl
+      · omega
+    · split
+      · omega
+      · congr 1
+        omega
+
+theorem extract_append_left {as bs : Array α} :
+    (as ++ bs).extract 0 as.size = as.extract 0 as.size := by
+  simp
+
+@[simp] theorem extract_append_right {as bs : Array α} :
+    (as ++ bs).extract as.size (as.size + i) = bs.extract 0 i := by
+  simp only [extract_append, extract_size_left, Nat.sub_self, empty_append]
+  congr 1
+  omega
+
+@[simp] theorem map_extract {as : Array α} {i j : Nat} :
+    (as.extract i j).map f = (as.map f).extract i j := by
+  ext l h₁ h₂
+  · simp
+  · simp only [size_map, size_extract] at h₁ h₂
+    simp only [getElem_map, getElem_extract]
+
+@[simp] theorem extract_mkArray {a : α} {n i j : Nat} :
+    (mkArray n a).extract i j = mkArray (min j n - i) a := by
+  ext l h₁ h₂
+  · simp
+  · simp only [size_extract, size_mkArray] at h₁ h₂
+    simp only [getElem_extract, getElem_mkArray]
+
+theorem extract_eq_extract_right {as : Array α} {i j j' : Nat} :
+    as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i) := by
+  rcases as with ⟨as⟩
+  simp
+
+theorem extract_eq_extract_left {as : Array α} {i i' j : Nat} :
+    as.extract i j = as.extract i' j ↔ min j as.size - i = min j as.size - i' := by
+  constructor
+  · intro h
+    replace h := congrArg Array.size h
+    simpa using h
+  · intro h
+    ext l h₁ h₂
+    · simpa
+    · simp only [size_extract] at h₁ h₂
+      simp only [getElem_extract]
+      congr 1
+      omega
+
+theorem extract_add_left {as : Array α} {i j k : Nat} :
+    as.extract (i + j) k = (as.extract i k).extract j (k - i) := by
+  simp [extract_eq_extract_right]
+  omega
+
+theorem mem_extract_iff_getElem {as : Array α} {a : α} {i j : Nat} :
+    a ∈ as.extract i j ↔ ∃ (k : Nat) (hm : k < min j as.size - i), as[i + k] = a := by
+  rcases as with ⟨as⟩
+  simp [List.mem_take_iff_getElem]
+  constructor <;>
+  · rintro ⟨k, h, rfl⟩
+    exact ⟨k, by omega, rfl⟩
+
+theorem set_eq_push_extract_append_extract {as : Array α} {i : Nat} (h : i < as.size) {a : α} :
+    as.set i a = (as.extract 0 i).push a ++ (as.extract (i + 1) as.size) := by
+  rcases as with ⟨as⟩
+  simp at h
+  simp [List.set_eq_take_append_cons_drop, h, List.take_of_length_le]
+
+theorem extract_reverse {as : Array α} {i j : Nat} :
+    as.reverse.extract i j = (as.extract (as.size - j) (as.size - i)).reverse := by
+  ext l h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, size_reverse] at h₁ h₂
+    simp only [getElem_extract, getElem_reverse, size_extract]
+    congr 1
+    omega
+
+theorem reverse_extract {as : Array α} {i j : Nat} :
+    (as.extract i j).reverse = as.reverse.extract (as.size - j) (as.size - i) := by
+  rw [extract_reverse]
+  simp
+  by_cases h : j ≤ as.size
+  · have : as.size - (as.size - j) = j := by omega
+    simp [this, extract_eq_extract_left]
+    omega
+  · have : as.size - (as.size - j) = as.size := by omega
+    simp only [Nat.not_le] at h
+    simp [h, this, extract_eq_extract_left]
+    omega
+
+/-! ### takeWhile -/
+
+theorem takeWhile_map (f : α → β) (p : β → Bool) (as : Array α) :
+    (as.map f).takeWhile p = (as.takeWhile (p ∘ f)).map f := by
+  rcases as with ⟨as⟩
+  simp [List.takeWhile_map]
+
+theorem popWhile_map (f : α → β) (p : β → Bool) (as : Array α) :
+    (as.map f).popWhile p = (as.popWhile (p ∘ f)).map f := by
+  rcases as with ⟨as⟩
+  simp [List.dropWhile_map, ← List.map_reverse]
+
+theorem takeWhile_filterMap (f : α → Option β) (p : β → Bool) (as : Array α) :
+    (as.filterMap f).takeWhile p = (as.takeWhile fun a => (f a).all p).filterMap f := by
+  rcases as with ⟨as⟩
+  simp [List.takeWhile_filterMap]
+
+theorem popWhile_filterMap (f : α → Option β) (p : β → Bool) (as : Array α) :
+    (as.filterMap f).popWhile p = (as.popWhile fun a => (f a).all p).filterMap f := by
+  rcases as with ⟨as⟩
+  simp [List.dropWhile_filterMap, ← List.filterMap_reverse]
+
+theorem takeWhile_filter (p q : α → Bool) (as : Array α) :
+    (as.filter p).takeWhile q = (as.takeWhile fun a => !p a || q a).filter p := by
+  rcases as with ⟨as⟩
+  simp [List.takeWhile_filter]
+
+theorem popWhile_filter (p q : α → Bool) (as : Array α) :
+    (as.filter p).popWhile q = (as.popWhile fun a => !p a || q a).filter p := by
+  rcases as with ⟨as⟩
+  simp [List.dropWhile_filter, ← List.filter_reverse]
+
+theorem takeWhile_append {xs ys : Array α} :
+    (xs ++ ys).takeWhile p =
+      if (xs.takeWhile p).size = xs.size then xs ++ ys.takeWhile p else xs.takeWhile p := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.takeWhile_toArray, List.takeWhile_append, size_toArray]
+  split <;> rfl
+
+@[simp] theorem takeWhile_append_of_pos {p : α → Bool} {l₁ l₂ : Array α} (h : ∀ a ∈ l₁, p a) :
+    (l₁ ++ l₂).takeWhile p = l₁ ++ l₂.takeWhile p := by
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp at h
+  simp [List.takeWhile_append_of_pos h]
+
+theorem popWhile_append {xs ys : Array α} :
+    (xs ++ ys).popWhile p =
+      if (ys.popWhile p).isEmpty then xs.popWhile p else xs ++ ys.popWhile p := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.popWhile_toArray, List.reverse_append, List.dropWhile_append,
+    List.isEmpty_eq_true, List.isEmpty_toArray, List.isEmpty_reverse]
+  -- Why do these not fire with `simp`?
+  rw [List.popWhile_toArray, List.isEmpty_toArray, List.isEmpty_reverse]
+  split
+  · rfl
+  · simp
+
+@[simp] theorem popWhile_append_of_pos {p : α → Bool} {l₁ l₂ : Array α} (h : ∀ a ∈ l₂, p a) :
+    (l₁ ++ l₂).popWhile p = l₁.popWhile p := by
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp at h
+  simp only [List.append_toArray, List.popWhile_toArray, List.reverse_append, mk.injEq,
+    List.reverse_inj]
+  rw [List.dropWhile_append_of_pos]
+  simpa
+
+@[simp] theorem takeWhile_mkArray_eq_filter (p : α → Bool) :
+    (mkArray n a).takeWhile p = (mkArray n a).filter p := by
+  simp [← List.toArray_replicate]
+
+theorem takeWhile_mkArray (p : α → Bool) :
+    (mkArray n a).takeWhile p = if p a then mkArray n a else #[] := by
+  simp [takeWhile_mkArray_eq_filter, filter_mkArray]
+
+@[simp] theorem popWhile_mkArray_eq_filter_not (p : α → Bool) :
+    (mkArray n a).popWhile p = (mkArray n a).filter (fun a => !p a) := by
+  simp [← List.toArray_replicate, ← List.filter_reverse]
+
+theorem popWhile_mkArray (p : α → Bool) :
+    (mkArray n a).popWhile p = if p a then #[] else mkArray n a := by
+  simp only [popWhile_mkArray_eq_filter_not, size_mkArray, filter_mkArray, Bool.not_eq_eq_eq_not,
+    Bool.not_true]
+  split <;> simp_all
+
+theorem extract_takeWhile {as : Array α} {i : Nat} :
+    (as.takeWhile p).extract 0 i = (as.extract 0 i).takeWhile p := by
+  rcases as with ⟨as⟩
+  simp [List.take_takeWhile]
+
+@[simp] theorem all_takeWhile {as : Array α} :
+    (as.takeWhile p).all p = true := by
+  rcases as with ⟨as⟩
+  rw [List.takeWhile_toArray] -- Not sure why this doesn't fire with `simp`.
+  simp
+
+@[simp] theorem any_popWhile {as : Array α} :
+    (as.popWhile p).any (fun a => !p a) = !as.all p := by
+  rcases as with ⟨as⟩
+  rw [List.popWhile_toArray] -- Not sure why this doesn't fire with `simp`.
+  simp
+
+theorem takeWhile_eq_extract_findIdx_not {xs : Array α} {p : α → Bool} :
+    takeWhile p xs = xs.extract 0 (xs.findIdx (fun a => !p a)) := by
+  rcases xs with ⟨xs⟩
+  simp [List.takeWhile_eq_take_findIdx_not]
+
+end Array

src/Init/Data/Array/Find.lean

@@ -412,6 +412,21 @@ theorem findIdx_le_findIdx {l : Array α} {p q : α → Bool} (h : ∀ x ∈ l,
   cases l
   simp [hf]
 
+theorem false_of_mem_extract_findIdx {xs : Array α} {p : α → Bool} (h : x ∈ xs.extract 0 (xs.findIdx p)) :
+    p x = false := by
+  rcases xs with ⟨xs⟩
+  exact List.false_of_mem_take_findIdx (by simpa using h)
+
+@[simp] theorem findIdx_extract {xs : Array α} {i : Nat} {p : α → Bool} :
+    (xs.extract 0 i).findIdx p = min i (xs.findIdx p) := by
+  cases xs
+  simp
+
+@[simp] theorem min_findIdx_findIdx {xs : Array α} {p q : α → Bool} :
+    min (xs.findIdx p) (xs.findIdx q) = xs.findIdx (fun a => p a || q a) := by
+  cases xs
+  simp
+
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := rfl
@@ -525,6 +540,11 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
   cases l
   simp [hf]
 
+@[simp] theorem findIdx?_take {xs : Array α} {i : Nat} {p : α → Bool} :
+    (xs.take i).findIdx? p = (xs.findIdx? p).bind (Option.guard (fun j => j < i)) := by
+  cases xs
+  simp
+
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.

src/Init/Data/Array/Lemmas.lean

@@ -2385,6 +2385,10 @@ theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j
 theorem reverse_ne_empty_iff {xs : Array α} : xs.reverse ≠ #[] ↔ xs ≠ #[] :=
   not_congr reverse_eq_empty_iff
 
+@[simp] theorem isEmpty_reverse {xs : Array α} : xs.reverse.isEmpty = xs.isEmpty := by
+  cases xs
+  simp
+
 /-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
 theorem getElem?_reverse' {l : Array α} (i j) (h : i + j + 1 = l.size) : l.reverse[i]? = l[j]? := by
   rcases l with ⟨l⟩

src/Init/Data/Array/TakeDrop.lean

@@ -7,6 +7,20 @@ prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop
 
+/-!
+These lemmas are used in the internals of HashMap.
+They should find a new home and/or be reformulated.
+-/
+
+namespace List
+
+theorem exists_of_set {i : Nat} {a' : α} {l : List α} (h : i < l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l[i] :: l₂ ∧ l₁.length = i ∧ l.set i a' = l₁ ++ a' :: l₂ := by
+  refine ⟨l.take i, l.drop (i + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩
+  simp [set_eq_take_append_cons_drop, h]
+
+end List
+
 namespace Array
 
 theorem exists_of_uset (self : Array α) (i d h) :

src/Init/Data/List/Lemmas.lean

@@ -2395,6 +2395,9 @@ theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈
 theorem reverse_ne_nil_iff {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ [] :=
   not_congr reverse_eq_nil_iff
 
+@[simp] theorem isEmpty_reverse {xs : List α} : xs.reverse.isEmpty = xs.isEmpty := by
+  cases xs <;> simp
+
 /-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
 theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
     l.reverse[i]? = l[j]?

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

@@ -148,20 +148,23 @@ theorem take_append {l₁ l₂ : List α} (i : Nat) :
   rw [take_append_eq_append_take, take_of_length_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
 
 @[simp]
-theorem take_eq_take :
+theorem take_eq_take_iff :
     ∀ {l : List α} {i j : Nat}, l.take i = l.take j ↔ min i l.length = min j l.length
   | [], i, j => by simp [Nat.min_zero]
   | _ :: xs, 0, 0 => by simp
   | x :: xs, i + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
   | x :: xs, 0, j + 1 => by simp [Nat.zero_min, succ_min_succ]
-  | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, take_eq_take]
+  | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, take_eq_take_iff]
+
+@[deprecated take_eq_take_iff (since := "2025-02-16")]
+abbrev take_eq_take := @take_eq_take_iff
 
 theorem take_add (l : List α) (i j : Nat) : l.take (i + j) = l.take i ++ (l.drop i).take j := by
   suffices take (i + j) (take i l ++ drop i l) = take i l ++ take j (drop i 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]
+  · simp only [take_eq_take_iff, length_take, length_drop]
     omega
   apply Nat.le_trans (m := i)
   · apply length_take_le
@@ -350,11 +353,6 @@ theorem set_eq_take_append_cons_drop (l : List α) (i : Nat) (a : α) :
   · rw [set_eq_of_length_le]
     omega
 
-theorem exists_of_set {i : Nat} {a' : α} {l : List α} (h : i < l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l[i] :: l₂ ∧ l₁.length = i ∧ l.set i a' = l₁ ++ a' :: l₂ := by
-  refine ⟨l.take i, l.drop (i + 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 : α) {i j : Nat} (l : List α)
     (hnm : i < j) : drop j (l.set i a) = l.drop j :=
   ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)
@@ -474,6 +472,16 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
       · simp
       · rw [Nat.add_min_add_right]
 
+@[simp] theorem min_findIdx_findIdx {xs : List α} {p q : α → Bool} :
+    min (xs.findIdx p) (xs.findIdx q) = xs.findIdx (fun a => p a || q a) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp [findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]
+    split <;> split <;> simp_all [Nat.add_min_add_right]
+
+/-! ### findIdx? -/
+
 @[simp] theorem findIdx?_take {xs : List α} {i : Nat} {p : α → Bool} :
     (xs.take i).findIdx? p = (xs.findIdx? p).bind (Option.guard (fun j => j < i)) := by
   induction xs generalizing i with
@@ -486,14 +494,6 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
       · simp
       · simp [ih, Option.guard_comp, Option.bind_map]
 
-@[simp] theorem min_findIdx_findIdx {xs : List α} {p q : α → Bool} :
-    min (xs.findIdx p) (xs.findIdx q) = xs.findIdx (fun a => p a || q a) := by
-  induction xs with
-  | nil => simp
-  | cons x xs ih =>
-    simp [findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]
-    split <;> split <;> simp_all [Nat.add_min_add_right]
-
 /-! ### takeWhile -/
 
 theorem takeWhile_eq_take_findIdx_not {xs : List α} {p : α → Bool} :

src/Init/Data/List/TakeDrop.lean

@@ -149,7 +149,7 @@ theorem take_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.take i =
 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 α} {i j : Nat} {a : α} :
+theorem take_set {l : List α} {i j : Nat} {a : α} :
     (l.set j a).take i = (l.take i).set j a := by
   induction i generalizing l j with
   | zero => simp
@@ -158,6 +158,9 @@ theorem set_take {l : List α} {i j : Nat} {a : α} :
     | nil => simp
     | cons hd tl => cases j <;> simp_all
 
+@[deprecated take_set (since := "2025-02-17")]
+abbrev set_take := @take_set
+
 theorem drop_set {l : List α} {i j : Nat} {a : α} :
     (l.set j a).drop i = if j < i then l.drop i else (l.drop i).set (j - i) a := by
   induction i generalizing l j with

src/Init/Data/List/ToArray.lean

@@ -489,6 +489,21 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
+private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) :
+    l.reverse.toArray.popWhile p = (l.dropWhile p).reverse.toArray := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    unfold popWhile
+    simp [ih, dropWhile_cons]
+    split
+    · rfl
+    · simp
+
+@[simp] theorem popWhile_toArray (p : α → Bool) (l : List α) :
+    l.toArray.popWhile p = (l.reverse.dropWhile p).reverse.toArray := by
+  simp [← popWhile_toArray_aux]
+
 @[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
     l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
   apply ext'

src/Init/Data/Vector.lean

@@ -16,3 +16,4 @@ import Init.Data.Vector.Range
 import Init.Data.Vector.Erase
 import Init.Data.Vector.Monadic
 import Init.Data.Vector.InsertIdx
+import Init.Data.Vector.Extract

src/Init/Data/Vector/Extract.lean

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Lemmas
+import Init.Data.Array.Extract
+
+/-!
+# Lemmas about `Vector.extract`
+-/
+
+open Nat
+
+namespace Vector
+
+/-! ### extract -/
+
+@[simp] theorem extract_of_size_lt {as : Vector α n} {i j : Nat} (h : n < j) :
+    as.extract i j = (as.extract i n).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [h]
+
+@[simp]
+theorem extract_push {as : Vector α n} {b : α} {start stop : Nat} (h : stop ≤ n) :
+    (as.push b).extract start stop = (as.extract start stop).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [h]
+
+@[simp]
+theorem extract_eq_pop {as : Vector α n} {stop : Nat} (h : stop = n - 1) :
+    as.extract 0 stop = as.pop.cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [h]
+
+@[simp]
+theorem extract_append_extract {as : Vector α n} {i j k : Nat} :
+    as.extract i j ++ as.extract j k =
+      (as.extract (min i j) (max j k)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp
+
+@[simp]
+theorem push_extract_getElem {as : Vector α n} {i j : Nat} (h : j < n) :
+    (as.extract i j).push as[j] = (as.extract (min i j) (j + 1)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [h]
+
+theorem extract_succ_right {as : Vector α n} {i j : Nat} (w : i < j + 1) (h : j < n) :
+    as.extract i (j + 1) = ((as.extract i j).push as[j]).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.extract_succ_right, w, h]
+
+theorem extract_sub_one {as : Vector α n} {i j : Nat} (h : j < n) :
+    as.extract i (j - 1) = (as.extract i j).pop.cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.extract_sub_one, h]
+
+@[simp]
+theorem getElem?_extract_of_lt {as : Vector α n} {i j k : Nat} (h : k < min j n - i) :
+    (as.extract i j)[k]? = some (as[i + k]'(by omega)) := by
+  simp [getElem?_extract, h]
+
+theorem getElem?_extract_of_succ {as : Vector α n} {j : Nat} :
+    (as.extract 0 (j + 1))[j]? = as[j]? := by
+  simp only [Nat.sub_zero]
+  erw [getElem?_extract] -- Why does this not fire by `simp` or `rw`?
+  by_cases h : j < n
+  · rw [if_pos (by omega)]
+    simp
+  · rw [if_neg (by omega)]
+    simp_all
+
+@[simp] theorem extract_extract {as : Vector α n} {i j k l : Nat} :
+    (as.extract i j).extract k l = (as.extract (i + k) (min (i + l) j)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp
+
+theorem extract_set {as : Vector α n} {i j k : Nat} (h : k < n) {a : α} :
+    (as.set k a).extract i j =
+      if _ : k < i then
+        as.extract i j
+      else if _ : k < min j as.size then
+        (as.extract i j).set (k - i) a (by omega)
+      else as.extract i j := by
+  rcases as with ⟨as, rfl⟩
+  simp only [set_mk, extract_mk, Array.extract_set]
+  split
+  · simp
+  · split <;> simp
+
+theorem set_extract {as : Vector α n} {i j k : Nat} (h : k < min j n - i) {a : α} :
+    (as.extract i j).set k a = (as.set (i + k) a).extract i j := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.set_extract]
+
+@[simp]
+theorem extract_append {as : Vector α n} {bs : Vector α m} {i j : Nat} :
+    (as ++ bs).extract i j =
+      (as.extract i j ++ bs.extract (i - n) (j - n)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  rcases bs with ⟨bs, rfl⟩
+  simp
+
+theorem extract_append_left {as : Vector α n} {bs : Vector α m} :
+    (as ++ bs).extract 0 n = (as.extract 0 n).cast (by omega) := by
+  ext i h
+  simp only [Nat.sub_zero, extract_append, extract_size, getElem_cast, getElem_append, Nat.min_self,
+    getElem_extract, Nat.zero_sub, Nat.zero_add, cast_cast]
+  split
+  · rfl
+  · omega
+
+@[simp] theorem extract_append_right {as : Vector α n} {bs : Vector α m} :
+    (as ++ bs).extract n (n + i) = (bs.extract 0 i).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  rcases bs with ⟨bs, rfl⟩
+  simp only [mk_append_mk, extract_mk, Array.extract_append, Array.extract_size_left, Nat.sub_self,
+    Array.empty_append, Nat.sub_zero, cast_mk, eq_mk]
+  congr 1
+  omega
+
+@[simp] theorem map_extract {as : Vector α n} {i j : Nat} :
+    (as.extract i j).map f = (as.map f).extract i j := by
+  ext k h
+  simp
+
+@[simp] theorem extract_mkVector {a : α} {n i j : Nat} :
+    (mkVector n a).extract i j = mkVector (min j n - i) a := by
+  ext i h
+  simp
+
+theorem extract_add_left {as : Vector α n} {i j k : Nat} :
+    as.extract (i + j) k = ((as.extract i k).extract j (k - i)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp only [extract_mk, Array.extract_extract, cast_mk, eq_mk]
+  rw [Array.extract_add_left]
+  simp
+
+theorem mem_extract_iff_getElem {as : Vector α n} {a : α} {i j : Nat} :
+    a ∈ as.extract i j ↔ ∃ (k : Nat) (hm : k < min j n - i), as[i + k] = a := by
+  rcases as with ⟨as⟩
+  simp [Array.mem_extract_iff_getElem]
+  constructor <;>
+  · rintro ⟨k, h, rfl⟩
+    exact ⟨k, by omega, rfl⟩
+
+theorem set_eq_push_extract_append_extract {as : Vector α n} {i : Nat} (h : i < n) {a : α} :
+    as.set i a = ((as.extract 0 i).push a ++ (as.extract (i + 1) n)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.set_eq_push_extract_append_extract, h]
+
+theorem extract_reverse {as : Vector α n} {i j : Nat} :
+    as.reverse.extract i j = (as.extract (n - j) (n - i)).reverse.cast (by omega) := by
+  ext i h
+  simp only [getElem_extract, getElem_reverse, getElem_cast]
+  congr 1
+  omega
+
+theorem reverse_extract {as : Vector α n} {i j : Nat} :
+    (as.extract i j).reverse = (as.reverse.extract (n - j) (n - i)).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.reverse_extract]
+
+end Vector

src/Init/Data/Vector/Find.lean

@@ -10,7 +10,9 @@ import Init.Data.Vector.Range
 import Init.Data.Array.Find
 
 /-!
-# Lemmas about `Vector.findSome?`, `Vector.find?, `Vector.findIdx?`, `Vector.idxOf?`.
+# Lemmas about `Vector.findSome?`, `Vector.find?`, `Vector.findFinIdx?`.
+
+We are still missing results about `idxOf?`, `findIdx`, and `findIdx?`.
 -/
 
 namespace Vector

src/Init/Data/Vector/Lemmas.lean

@@ -730,6 +730,17 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
   rcases l with ⟨l, rfl⟩
   simp
 
+/-- In an equality between two casts, push the casts to the right hand side. -/
+@[simp] theorem cast_eq_cast {as : Vector α n} {bs : Vector α m} {wa : n = k} {wb : m = k} :
+    as.cast wa = bs.cast wb ↔ as = bs.cast (by omega) := by
+  constructor
+  · intro w
+    ext i h
+    replace w := congrArg (fun v => v[i]) w
+    simpa using w
+  · rintro rfl
+    simp
+
 /-! ### mkVector -/
 
 @[simp] theorem mkVector_zero : mkVector 0 a = #v[] := rfl
@@ -2017,6 +2028,10 @@ theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f
   cases as
   simp
 
+@[simp] theorem isEmpty_reverse {xs : Vector α n} : xs.reverse.isEmpty = xs.isEmpty := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
 @[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
     (a.reverse)[i] = a[n - 1 - i] := by
   rcases a with ⟨a, rfl⟩
@@ -2101,7 +2116,7 @@ theorem flatMap_reverse {β} (l : Vector α n) (f : α → Vector β m) :
   simp
 
 theorem getElem?_extract {as : Vector α n} {start stop : Nat} :
-    (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none := by
+    (as.extract start stop)[i]? = if i < min stop n - start then as[start + i]? else none := by
   rcases as with ⟨as, rfl⟩
   simp [Array.getElem?_extract]