chore: alignment of Array and List lemmas

src/Init/Data/Array/Basic.lean

@@ -11,7 +11,7 @@ import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
-import Init.Data.List.ToArray
+import Init.Data.List.ToArrayImpl
 import Init.Data.Array.Set
 
 universe u v w
@@ -99,6 +99,9 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
 @[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
@@ -244,7 +247,7 @@ def singleton (v : α) : Array α :=
   mkArray 1 v
 
 def back! [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
+  a[a.size - 1]!
 
 @[deprecated back! (since := "2024-10-31")] abbrev back := @back!
 

src/Init/Data/Array/Find.lean

@@ -81,7 +81,7 @@ theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.siz
     (L.findSome? fun l => l[0]?).isSome := by
   cases L using array_array_induction
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
-    List.findSome?_isSome_iff, List.isSome_getElem?]
+    List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
     Nat.sum_pos_iff_exists_pos, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h

src/Init/Data/Array/Lemmas.lean

@@ -5,409 +5,21 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Lemmas
-import Init.Data.List.Impl
-import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
-import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
 import Init.TacticsExtra
+import Init.Data.List.ToArray
 
 /-!
 ## Theorems about `Array`.
 -/
 
 
-/-! ### Preliminaries about `Array` needed for `List.toArray` lemmas.
-
-This section contains only the bare minimum lemmas about `Array`
-that we need to write lemmas about `List.toArray`.
--/
-namespace Array
-
-@[simp] theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
-  getElem?_pos ..
-
-@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
-  by_cases h : i < a.size
-  · simp [getElem?_eq_getElem, h]
-  · rw [getElem?_neg a i h]
-    simp_all
-
-@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
-
-@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
-  simp [getElem!_def, get!, getD]
-  split <;> rename_i h
-  · simp [getElem?_eq_getElem h]
-  · simp [getElem?_eq_none_iff.2 (by simpa using h)]
-
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [mem_def]
-
-end Array
-
-/-! ### Lemmas about `List.toArray`.
-
-We prefer to pull `List.toArray` outwards.
--/
-namespace List
-
-open Array
-
-theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
-  cases a with
-  | nil => simpa using h
-  | cons a as =>
-    cases b with
-    | nil => simp at h
-    | cons b bs => simpa using h
-
-@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
-    (a.toArrayAux b).size = b.size + a.length := by
-  simp [size]
-
-@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
-  apply ext'
-  simp
-
-/-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
-@[simp] theorem push_toArray_fun (l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray := by
-  funext a
-  simp
-
-@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
-  cases l <;> simp
-
-@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
-
-@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
-  simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
-
-@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
-  simp [back?, List.getLast?_eq_getElem?]
-
-@[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
-    (l.toArray.set i a) = (l.set i a).toArray := rfl
-
-@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
-    (h : i ≤ l.length) (b : β) :
-    Array.forIn'.loop l.toArray f i h b =
-      forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by
-  induction i generalizing l b with
-  | zero =>
-    simp [Array.forIn'.loop]
-  | succ i ih =>
-    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
-    have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
-      simp only [Nat.sub_add_eq]
-      rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
-      simp only [Option.toList_some, singleton_append]
-    simp [t]
-    have t : l.length - 1 - i = l.length - i - 1 := by omega
-    simp only [t]
-    congr
-
-@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
-    forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
-  change Array.forIn' _ _ _ = List.forIn' _ _ _
-  rw [Array.forIn', forIn'_loop_toArray]
-  simp
-
-@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn l.toArray b f = forIn l b f := by
-  simpa using forIn'_toArray l b fun a m b => f a b
-
-theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
-    l.toArray.foldrM f init = l.foldrM f init := by
-  rw [foldrM_eq_reverse_foldlM_toList]
-  simp
-
-theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
-    l.toArray.foldlM f init = l.foldlM f init := by
-  rw [foldlM_toList]
-
-theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
-    l.toArray.foldr f init = l.foldr f init := by
-  rw [foldr_toList]
-
-theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
-    l.toArray.foldl f init = l.foldl f init := by
-  rw [foldl_toList]
-
-/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
-@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
-    (h : start = l.toArray.size) :
-    l.toArray.foldrM f init start 0 = l.foldrM f init := by
-  subst h
-  rw [foldrM_eq_reverse_foldlM_toList]
-  simp
-
-/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/
-@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.foldlM f init 0 stop = l.foldlM f init := by
-  subst h
-  rw [foldlM_toList]
-
-/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
-@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
-    (h : start = l.toArray.size) :
-    l.toArray.foldr f init start 0 = l.foldr f init := by
-  subst h
-  rw [foldr_toList]
-
-/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
-@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.foldl f init 0 stop = l.foldl f init := by
-  subst h
-  rw [foldl_toList]
-
-@[simp] theorem append_toArray (l₁ l₂ : List α) :
-    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
-  apply ext'
-  simp
-
-@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by
-  cases as
-  simp
-
-@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
-  induction l generalizing as <;> simp [*]
-
-@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
-  rw [foldr_eq_foldl_reverse, foldl_push]
-
-@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
-    l.toArray.findSomeM? f = l.findSomeM? f := by
-  rw [Array.findSomeM?]
-  simp only [bind_pure_comp, map_pure, forIn_toArray]
-  induction l with
-  | nil => simp
-  | cons a l ih =>
-    simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?]
-    congr
-    ext1 (_|_) <;> simp [ih]
-
-theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
-    (i : Nat) (h) :
-    findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by
-  induction i generalizing l with
-  | zero => simp [Array.findSomeRevM?.find.eq_def]
-  | succ i ih =>
-    rw [size_toArray] at h
-    rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
-    simp only [ih, reverse_append]
-    congr
-    ext1 (_|_) <;> simp
-
--- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`.
-theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
-    l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by
-  simp [Array.findSomeRevM?, findSomeRevM?_find_toArray]
-
--- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`.
-theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
-    l.toArray.findRevM? f = l.reverse.findM? f := by
-  rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]
-
-@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
-    l.toArray.findM? f = l.findM? f := by
-  rw [Array.findM?]
-  simp only [bind_pure_comp, map_pure, forIn_toArray]
-  induction l with
-  | nil => simp
-  | cons a l ih =>
-    simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]
-    congr
-    ext1 (_|_) <;> simp [ih]
-
-@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) :
-    l.toArray.findSome? f = l.findSome? f := by
-  rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
-
-@[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
-    l.toArray.find? f = l.find? f := by
-  rw [Array.find?]
-  simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
-  induction l with
-  | nil => simp
-  | cons a l ih =>
-    simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
-    by_cases f a <;> simp_all
-
-theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
-    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
-      Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
-  rw [Array.isPrefixOfAux]
-  conv => rhs; rw [Array.isPrefixOfAux]
-  simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail]
-  split <;> rename_i h₁ <;> split <;> rename_i h₂
-  · rw [isPrefixOfAux_toArray_succ]
-  · omega
-  · omega
-  · rfl
-
-theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
-    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
-      Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0 := by
-  induction i generalizing l₁ l₂ with
-  | zero => simp [isPrefixOfAux_toArray_succ]
-  | succ i ih =>
-    rw [isPrefixOfAux_toArray_succ, ih]
-    simp
-
-theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) :
-    Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 =
-      l₁.isPrefixOf l₂ := by
-  rw [Array.isPrefixOfAux]
-  match l₁, l₂ with
-  | [], _ => rw [dif_neg] <;> simp
-  | _::_, [] => simp at hle
-  | a::l₁, b::l₂ =>
-    simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]
-
-@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
-    l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by
-  rw [Array.isPrefixOf]
-  split <;> rename_i h
-  · simp [isPrefixOfAux_toArray_zero]
-  · simp only [Bool.false_eq]
-    induction l₁ generalizing l₂ with
-    | nil => simp at h
-    | cons a l₁ ih =>
-      cases l₂ with
-      | nil => simp
-      | cons b l₂ =>
-        simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]
-        intro w
-        rw [ih]
-        simp_all
-
-theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
-    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs := by
-  rw [zipWithAux]
-  conv => rhs; rw [zipWithAux]
-  simp only [size_toArray, getElem_toArray, length_tail, getElem_tail]
-  split <;> rename_i h₁
-  · split <;> rename_i h₂
-    · rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ]
-    · rw [dif_pos (by omega)]
-      rw [dif_neg (by omega)]
-  · rw [dif_neg (by omega)]
-
-theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
-    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 cs := by
-  induction i generalizing as bs cs with
-  | zero => simp [zipWithAux_toArray_succ]
-  | succ i ih =>
-    rw [zipWithAux_toArray_succ, ih]
-    simp
-
-theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) :
-    zipWithAux as.toArray bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray := by
-  rw [Array.zipWithAux]
-  match as, bs with
-  | [], _ => simp
-  | _, [] => simp
-  | a :: as, b :: bs =>
-    simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]
-
-@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
-    Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by
-  rw [Array.zipWith]
-  simp [zipWithAux_toArray_zero]
-
-@[simp] theorem zip_toArray (as : List α) (bs : List β) :
-    Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by
-  simp [Array.zip, zipWith_toArray, zip]
-
-theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) :
-    zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by
-  unfold zipWithAll.go
-  split <;> rename_i h
-  · rw [zipWithAll_go_toArray]
-    simp at h
-    simp only [getElem?_toArray, push_append_toArray]
-    if ha : i < as.length then
-      if hb : i < bs.length then
-        rw [List.drop_eq_getElem_cons ha, List.drop_eq_getElem_cons hb]
-        simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons]
-      else
-        simp only [Nat.not_lt] at hb
-        rw [List.drop_eq_getElem_cons ha]
-        rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)]
-        simp only [zipWithAll_nil, map_drop, map_cons]
-        rw [getElem?_eq_getElem ha]
-        rw [getElem?_eq_none hb]
-    else
-      if hb : i < bs.length then
-        simp only [Nat.not_lt] at ha
-        rw [List.drop_eq_getElem_cons hb]
-        rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)]
-        simp only [nil_zipWithAll, map_drop, map_cons]
-        rw [getElem?_eq_getElem hb]
-        rw [getElem?_eq_none ha]
-      else
-        omega
-  · simp only [size_toArray, Nat.not_lt] at h
-    rw [drop_eq_nil_of_le (by omega), drop_eq_nil_of_le (by omega)]
-    simp
-  termination_by max as.length bs.length - i
-  decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
-    Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by
-  simp [Array.zipWithAll, zipWithAll_go_toArray]
-
-@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
-    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
-  apply ext'
-  simp
-
-@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
-  apply ext'
-  simp
-
-theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
-    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
-  rw [takeWhile.go, takeWhile.go]
-  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
-    getElem_toArray, getElem_cons_succ]
-  split
-  rw [takeWhile_go_succ]
-  rfl
-
-theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
-    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
-  induction l generalizing i r with
-  | nil => simp [takeWhile.go]
-  | cons a l ih =>
-    rw [takeWhile.go]
-    cases i with
-    | zero =>
-      simp [takeWhile_go_succ, ih, takeWhile_cons]
-      split <;> simp
-    | succ i =>
-      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
-        getElem_toArray, getElem_cons_succ, drop_succ_cons]
-      split <;> rename_i h₁
-      · rw [takeWhile_go_succ, ih]
-        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
-        split <;> simp_all
-      · simp_all [drop_eq_nil_of_le]
-
-@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
-    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
-  simp [Array.takeWhile, takeWhile_go_toArray]
-
-end List
-
 
 namespace Array
 
@@ -418,6 +30,12 @@ namespace Array
 theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
   cases a; cases b; simpa using h
 
+@[simp] theorem toList_eq_nil_iff (l : Array α) : l.toList = [] ↔ l = #[] := by
+  cases l <;> simp
+
+@[simp] theorem mem_toList_iff (a : α) (l : Array α) : a ∈ l.toList ↔ a ∈ l := by
+  cases l <;> simp
+
 /-! ### empty -/
 
 @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by
@@ -529,24 +147,27 @@ theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
 
 /-! ## L[i] and L[i]? -/
 
--- getElem?_eq_none_iff is above.
+@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
+  by_cases h : i < a.size
+  · simp [getElem?_pos, h]
+  · rw [getElem?_neg a i h]
+    simp_all
 
 @[simp] theorem none_eq_getElem?_iff {a : Array α} {i : Nat} : none = a[i]? ↔ a.size ≤ i := by
   simp [eq_comm (a := none)]
 
-theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b ↔ ∃ h : i < a.size, a[i] = b := by
-  simp [getElem?_def]
-
 theorem getElem?_eq_none {a : Array α} (h : a.size ≤ i) : a[i]? = none := by
   simp [getElem?_eq_none_iff, h]
 
--- getElem?_eq_getElem is above.
+@[simp] theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
+  getElem?_pos ..
+
+theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b ↔ ∃ h : i < a.size, a[i] = b := by
+  simp [getElem?_def]
 
 theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? ↔ ∃ h : i < a.size, a[i] = b := by
   rw [eq_comm, getElem?_eq_some_iff]
 
--- getElem?_eq_some_iff is above.
-
 @[simp] theorem some_getElem_eq_getElem?_iff (a : Array α) (i : Nat) (h : i < a.size) :
     (some a[i] = a[i]?) ↔ True := by
   simp [h]
@@ -588,15 +209,134 @@ theorem getElem?_push {a : Array α} {x} : (a.push x)[i]? = if i = a.size then s
 @[simp] theorem getElem?_push_size {a : Array α} {x} : (a.push x)[a.size]? = some x := by
   simp [getElem?_push]
 
+@[simp] theorem getElem_singleton (a : α) (h : i < 1) : #[a][i] = a :=
+  match i, h with
+  | 0, _ => rfl
+
+theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a else none := by
+  simp [List.getElem?_singleton]
+
+/-! ### mem -/
+
+@[simp] theorem not_mem_empty (a : α) : ¬ a ∈ #[] := nofun
+
 @[simp] theorem mem_push {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y := by
-  simp [mem_def]
+  simp only [mem_def]
+  simp
 
 theorem mem_push_self {a : Array α} {x : α} : x ∈ a.push x :=
   mem_push.2 (Or.inr rfl)
 
+theorem eq_push_append_of_mem {xs : Array α} {x : α} (h : x ∈ xs) :
+    ∃ (as bs : Array α), xs = as.push x ++ bs ∧ x ∉ as:= by
+  rcases xs with ⟨xs⟩
+  obtain ⟨as, bs, h, w⟩ := List.eq_append_cons_of_mem (mem_def.1 h)
+  simp only at h
+  obtain rfl := h
+  exact ⟨as.toArray, bs.toArray, by simp, by simpa using w⟩
+
 theorem mem_push_of_mem {a : Array α} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y :=
   mem_push.2 (Or.inl h)
 
+theorem exists_mem_of_ne_empty (l : Array α) (h : l ≠ #[]) : ∃ x, x ∈ l := by
+  simpa using List.exists_mem_of_ne_nil l.toList (by simpa using h)
+
+theorem eq_empty_iff_forall_not_mem {l : Array α} : l = #[] ↔ ∀ a, a ∉ l := by
+  cases l
+  simp [List.eq_nil_iff_forall_not_mem]
+
+@[simp] theorem mem_dite_nil_left {x : α} [Decidable p] {l : ¬ p → Array α} :
+    (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_dite_nil_right {x : α} [Decidable p] {l : p → Array α} :
+    (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_nil_left {x : α} [Decidable p] {l : Array α} :
+    (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l := by
+  split <;> simp_all
+
+@[simp] theorem mem_ite_nil_right {x : α} [Decidable p] {l : Array α} :
+    (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by
+  split <;> simp_all
+
+theorem eq_of_mem_singleton (h : a ∈ #[b]) : a = b := by
+  simpa using h
+
+@[simp] theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b :=
+  ⟨eq_of_mem_singleton, (by simp [·])⟩
+
+theorem forall_mem_push {p : α → Prop} {xs : Array α} {a : α} :
+    (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by
+  cases xs
+  simp [or_comm, forall_eq_or_imp]
+
+theorem forall_mem_ne {a : α} {l : Array α} : (∀ a' : α, a' ∈ l → ¬a = a') ↔ a ∉ l :=
+  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
+
+theorem forall_mem_ne' {a : α} {l : Array α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l :=
+  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
+
+theorem exists_mem_empty (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ #[], p x) := nofun
+
+theorem forall_mem_empty (p : α → Prop) : ∀ (x) (_ : x ∈ #[]), p x := nofun
+
+theorem exists_mem_push {p : α → Prop} {a : α} {xs : Array α} :
+    (∃ x, ∃ _ : x ∈ xs.push a, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ xs, p x := by
+  simp
+  constructor
+  · rintro ⟨x, (h | rfl), h'⟩
+    · exact .inr ⟨x, h, h'⟩
+    · exact .inl h'
+  · rintro (h | ⟨x, h, h'⟩)
+    · exact ⟨a, by simp, h⟩
+    · exact ⟨x, .inl h, h'⟩
+
+theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ (x) (_ : x ∈ #[a]), p x) ↔ p a := by
+  simp only [mem_singleton, forall_eq]
+
+theorem mem_empty_iff (a : α) : a ∈ (#[] : Array α) ↔ False := by simp
+
+theorem mem_singleton_self (a : α) : a ∈ #[a] := by simp
+
+theorem mem_of_mem_push_of_mem {a b : α} {l : Array α} : a ∈ l.push b → b ∈ l → a ∈ l := by
+  cases l
+  simp only [List.push_toArray, mem_toArray, List.mem_append, List.mem_singleton]
+  rintro (h | rfl)
+  · intro _
+    exact h
+  · exact id
+
+theorem eq_or_ne_mem_of_mem {a b : α} {l : Array α} (h' : a ∈ l.push b) :
+    a = b ∨ (a ≠ b ∧ a ∈ l) := by
+  if h : a = b then
+    exact .inl h
+  else
+    simp [h] at h'
+    exact .inr ⟨h, h'⟩
+
+theorem ne_empty_of_mem {a : α} {l : Array α} (h : a ∈ l) : l ≠ #[] := by
+  cases l
+  simp [List.ne_nil_of_mem (by simpa using h)]
+
+theorem mem_of_ne_of_mem {a y : α} {l : Array α} (h₁ : a ≠ y) (h₂ : a ∈ l.push y) : a ∈ l := by
+  simpa [h₁] using h₂
+
+theorem ne_of_not_mem_push {a b : α} {l : Array α} (h : a ∉ l.push b) : a ≠ b := by
+  simp only [mem_push, not_or] at h
+  exact h.2
+
+theorem not_mem_of_not_mem_push {a b : α} {l : Array α} (h : a ∉ l.push b) : a ∉ l := by
+  simp only [mem_push, not_or] at h
+  exact h.1
+
+theorem not_mem_push_of_ne_of_not_mem {a y : α} {l : Array α} : a ≠ y → a ∉ l → a ∉ l.push y :=
+  mt ∘ mem_of_ne_of_mem
+
+theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Array α} : a ∉ l.push y → a ≠ y ∧ a ∉ l := by
+  simp +contextual
+
 theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (n : Nat) (h : n < l.size), l[n]'h = a := by
   cases l
   simp [List.getElem_of_mem (by simpa using h)]
@@ -728,9 +468,6 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
     (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
   rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
 
-@[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
-  simp [mem_def]
-
 /-! # uset -/
 
 attribute [simp] uset
@@ -956,7 +693,7 @@ theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD
   simp only [get!_eq_getElem?, get?_eq_getElem?]
 
 theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
-  simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
+  simp [back!, back?, getElem!_def, Option.getD]; rfl
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
   simp [back?, ← getElem?_toList]
@@ -1064,7 +801,9 @@ theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as
     else
       have heq : i = as.pop.size :=
         Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [getElem_push_eq, back!, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+      cases heq
+      rw [getElem_push_eq, back!]
+      simp [← getElem!_pos]
 
 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
     ∃ (bs : Array α) (c : α), as = bs.push c :=

src/Init/Data/List.lean

@@ -24,6 +24,7 @@ import Init.Data.List.Zip
 import Init.Data.List.Perm
 import Init.Data.List.Sort
 import Init.Data.List.ToArray
+import Init.Data.List.ToArrayImpl
 import Init.Data.List.MapIdx
 import Init.Data.List.OfFn
 import Init.Data.List.FinRange

src/Init/Data/List/Lemmas.lean

@@ -253,12 +253,6 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
     l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
-  simp
-
-theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
-  simp
-
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
 theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
@@ -270,6 +264,11 @@ theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
   cases i <;> simp
 
+theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
+    (a :: l)[i] =
+      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
+  cases i <;> simp
+
 @[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a :=
   match i, h with
   | 0, _ => rfl
@@ -3532,7 +3531,12 @@ theorem getElem?_eq (l : List α) (i : Nat) :
   getElem?_def _ _
 @[deprecated getElem?_eq_none (since := "2024-11-29")] abbrev getElem?_len_le := @getElem?_eq_none
 
+@[deprecated _root_.isSome_getElem? (since := "2024-12-09")]
+theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
+  simp
 
-
+@[deprecated _root_.isNone_getElem? (since := "2024-12-09")]
+theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
+  simp
 
 end List

src/Init/Data/List/ToArray.lean

@@ -1,23 +1,366 @@
 /-
-Copyright (c) 2024 Lean FRO. All rights reserved.
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
+Authors: Mario Carneiro
 -/
 prelude
-import Init.Data.List.Basic
+import Init.Data.List.Impl
+import Init.Data.List.Nat.Erase
+import Init.Data.List.Monadic
 
-/--
-Auxiliary definition for `List.toArray`.
-`List.toArrayAux as r = r ++ as.toArray`
+/-! ### Lemmas about `List.toArray`.
+
+We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
-@[inline_if_reduce]
-def List.toArrayAux : List α → Array α → Array α
-  | nil,       r => r
-  | cons a as, r => toArrayAux as (r.push a)
+namespace List
 
-/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
--- This function is exported to C, where it is called by `Array.mk`
--- (the constructor) to implement this functionality.
-@[inline, match_pattern, pp_nodot, export lean_list_to_array]
-def List.toArrayImpl (as : List α) : Array α :=
-  as.toArrayAux (Array.mkEmpty as.length)
+open Array
+
+theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
+  cases a with
+  | nil => simpa using h
+  | cons a as =>
+    cases b with
+    | nil => simp at h
+    | cons b bs => simpa using h
+
+@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
+    (a.toArrayAux b).size = b.size + a.length := by
+  simp [size]
+
+@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
+  apply ext'
+  simp
+
+/-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
+@[simp] theorem push_toArray_fun (l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray := by
+  funext a
+  simp
+
+@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
+  cases l <;> simp
+
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
+
+@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
+  simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
+
+@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
+  simp [back?, List.getLast?_eq_getElem?]
+
+@[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
+    (l.toArray.set i a) = (l.set i a).toArray := rfl
+
+@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
+    (h : i ≤ l.length) (b : β) :
+    Array.forIn'.loop l.toArray f i h b =
+      forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by
+  induction i generalizing l b with
+  | zero =>
+    simp [Array.forIn'.loop]
+  | succ i ih =>
+    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
+    have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
+      simp only [Nat.sub_add_eq]
+      rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
+      simp only [Option.toList_some, singleton_append]
+    simp [t]
+    have t : l.length - 1 - i = l.length - i - 1 := by omega
+    simp only [t]
+    congr
+
+@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
+    forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
+  change Array.forIn' _ _ _ = List.forIn' _ _ _
+  rw [Array.forIn', forIn'_loop_toArray]
+  simp
+
+@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
+    forIn l.toArray b f = forIn l b f := by
+  simpa using forIn'_toArray l b fun a m b => f a b
+
+theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
+    l.toArray.foldrM f init = l.foldrM f init := by
+  rw [foldrM_eq_reverse_foldlM_toList]
+  simp
+
+theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
+    l.toArray.foldlM f init = l.foldlM f init := by
+  rw [foldlM_toList]
+
+theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
+    l.toArray.foldr f init = l.foldr f init := by
+  rw [foldr_toList]
+
+theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
+    l.toArray.foldl f init = l.foldl f init := by
+  rw [foldl_toList]
+
+/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
+@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
+    (h : start = l.toArray.size) :
+    l.toArray.foldrM f init start 0 = l.foldrM f init := by
+  subst h
+  rw [foldrM_eq_reverse_foldlM_toList]
+  simp
+
+/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/
+@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.foldlM f init 0 stop = l.foldlM f init := by
+  subst h
+  rw [foldlM_toList]
+
+/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
+@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
+    (h : start = l.toArray.size) :
+    l.toArray.foldr f init start 0 = l.foldr f init := by
+  subst h
+  rw [foldr_toList]
+
+/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
+@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.foldl f init 0 stop = l.foldl f init := by
+  subst h
+  rw [foldl_toList]
+
+@[simp] theorem append_toArray (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by
+  cases as
+  simp
+
+@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
+  induction l generalizing as <;> simp [*]
+
+@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
+  rw [foldr_eq_foldl_reverse, foldl_push]
+
+@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeM? f = l.findSomeM? f := by
+  rw [Array.findSomeM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
+    (i : Nat) (h) :
+    findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by
+  induction i generalizing l with
+  | zero => simp [Array.findSomeRevM?.find.eq_def]
+  | succ i ih =>
+    rw [size_toArray] at h
+    rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
+    simp only [ih, reverse_append]
+    congr
+    ext1 (_|_) <;> simp
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`.
+theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by
+  simp [Array.findSomeRevM?, findSomeRevM?_find_toArray]
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`.
+theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findRevM? f = l.reverse.findM? f := by
+  rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]
+
+@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findM? f = l.findM? f := by
+  rw [Array.findM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) :
+    l.toArray.findSome? f = l.findSome? f := by
+  rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
+
+@[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
+    l.toArray.find? f = l.find? f := by
+  rw [Array.find?]
+  simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
+    by_cases f a <;> simp_all
+
+theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
+      Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
+  rw [Array.isPrefixOfAux]
+  conv => rhs; rw [Array.isPrefixOfAux]
+  simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail]
+  split <;> rename_i h₁ <;> split <;> rename_i h₂
+  · rw [isPrefixOfAux_toArray_succ]
+  · omega
+  · omega
+  · rfl
+
+theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
+      Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0 := by
+  induction i generalizing l₁ l₂ with
+  | zero => simp [isPrefixOfAux_toArray_succ]
+  | succ i ih =>
+    rw [isPrefixOfAux_toArray_succ, ih]
+    simp
+
+theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 =
+      l₁.isPrefixOf l₂ := by
+  rw [Array.isPrefixOfAux]
+  match l₁, l₂ with
+  | [], _ => rw [dif_neg] <;> simp
+  | _::_, [] => simp at hle
+  | a::l₁, b::l₂ =>
+    simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]
+
+@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
+    l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by
+  rw [Array.isPrefixOf]
+  split <;> rename_i h
+  · simp [isPrefixOfAux_toArray_zero]
+  · simp only [Bool.false_eq]
+    induction l₁ generalizing l₂ with
+    | nil => simp at h
+    | cons a l₁ ih =>
+      cases l₂ with
+      | nil => simp
+      | cons b l₂ =>
+        simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]
+        intro w
+        rw [ih]
+        simp_all
+
+theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
+    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs := by
+  rw [zipWithAux]
+  conv => rhs; rw [zipWithAux]
+  simp only [size_toArray, getElem_toArray, length_tail, getElem_tail]
+  split <;> rename_i h₁
+  · split <;> rename_i h₂
+    · rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ]
+    · rw [dif_pos (by omega)]
+      rw [dif_neg (by omega)]
+  · rw [dif_neg (by omega)]
+
+theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
+    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 cs := by
+  induction i generalizing as bs cs with
+  | zero => simp [zipWithAux_toArray_succ]
+  | succ i ih =>
+    rw [zipWithAux_toArray_succ, ih]
+    simp
+
+theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) :
+    zipWithAux as.toArray bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray := by
+  rw [Array.zipWithAux]
+  match as, bs with
+  | [], _ => simp
+  | _, [] => simp
+  | a :: as, b :: bs =>
+    simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]
+
+@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
+    Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by
+  rw [Array.zipWith]
+  simp [zipWithAux_toArray_zero]
+
+@[simp] theorem zip_toArray (as : List α) (bs : List β) :
+    Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by
+  simp [Array.zip, zipWith_toArray, zip]
+
+theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) :
+    zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by
+  unfold zipWithAll.go
+  split <;> rename_i h
+  · rw [zipWithAll_go_toArray]
+    simp at h
+    simp only [getElem?_toArray, push_append_toArray]
+    if ha : i < as.length then
+      if hb : i < bs.length then
+        rw [List.drop_eq_getElem_cons ha, List.drop_eq_getElem_cons hb]
+        simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons]
+      else
+        simp only [Nat.not_lt] at hb
+        rw [List.drop_eq_getElem_cons ha]
+        rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)]
+        simp only [zipWithAll_nil, map_drop, map_cons]
+        rw [getElem?_eq_getElem ha]
+        rw [getElem?_eq_none hb]
+    else
+      if hb : i < bs.length then
+        simp only [Nat.not_lt] at ha
+        rw [List.drop_eq_getElem_cons hb]
+        rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)]
+        simp only [nil_zipWithAll, map_drop, map_cons]
+        rw [getElem?_eq_getElem hb]
+        rw [getElem?_eq_none ha]
+      else
+        omega
+  · simp only [size_toArray, Nat.not_lt] at h
+    rw [drop_eq_nil_of_le (by omega), drop_eq_nil_of_le (by omega)]
+    simp
+  termination_by max as.length bs.length - i
+  decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
+    Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by
+  simp [Array.zipWithAll, zipWithAll_go_toArray]
+
+@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
+  apply ext'
+  simp
+
+theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
+    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
+  rw [takeWhile.go, takeWhile.go]
+  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+    getElem_toArray, getElem_cons_succ]
+  split
+  rw [takeWhile_go_succ]
+  rfl
+
+theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
+    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
+  induction l generalizing i r with
+  | nil => simp [takeWhile.go]
+  | cons a l ih =>
+    rw [takeWhile.go]
+    cases i with
+    | zero =>
+      simp [takeWhile_go_succ, ih, takeWhile_cons]
+      split <;> simp
+    | succ i =>
+      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+        getElem_toArray, getElem_cons_succ, drop_succ_cons]
+      split <;> rename_i h₁
+      · rw [takeWhile_go_succ, ih]
+        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
+        split <;> simp_all
+      · simp_all [drop_eq_nil_of_le]
+
+@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
+    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
+  simp [Array.takeWhile, takeWhile_go_toArray]
+
+end List

src/Init/Data/List/ToArrayImpl.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.List.Basic
+
+/--
+Auxiliary definition for `List.toArray`.
+`List.toArrayAux as r = r ++ as.toArray`
+-/
+@[inline_if_reduce]
+def List.toArrayAux : List α → Array α → Array α
+  | nil,       r => r
+  | cons a as, r => toArrayAux as (r.push a)
+
+/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
+-- This function is exported to C, where it is called by `Array.mk`
+-- (the constructor) to implement this functionality.
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
+def List.toArrayImpl (as : List α) : Array α :=
+  as.toArrayAux (Array.mkEmpty as.length)

src/Init/GetElem.lean

@@ -243,6 +243,12 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get i h
 
+@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
+
+@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
+  simp only [get!, getD, get_eq_getElem, getElem!_def]
+  split <;> simp_all [getElem?_pos, getElem?_neg]
+
 end Array
 
 namespace Lean.Syntax