deprecations

Closes #2710

src/Init/Data/Array/Bootstrap.lean

@@ -73,7 +73,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
 
 @[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
 
-@[simp] theorem append_toList (arr arr' : Array α) :
+@[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
   rw [foldl_eq_foldl_toList]
@@ -111,8 +111,8 @@ abbrev toList_eq := @toListImpl_eq
 @[deprecated pop_toList (since := "2024-09-09")]
 abbrev pop_data := @pop_toList
 
-@[deprecated append_toList (since := "2024-09-09")]
-abbrev append_data := @append_toList
+@[deprecated toList_append (since := "2024-09-09")]
+abbrev append_data := @toList_append
 
 @[deprecated appendList_toList (since := "2024-09-09")]
 abbrev appendList_data := @appendList_toList

src/Init/Data/Array/Lemmas.lean

@@ -91,6 +91,8 @@ abbrev toArray_data := @toArray_toList
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 
+@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
+
 @[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
 theorem toArray_concat {as : List α} {x : α} :
     (as ++ [x]).toArray = as.toArray.push x := by
@@ -98,7 +100,7 @@ theorem toArray_concat {as : List α} {x : α} :
   simp
 
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
-  apply Array.ext'
+  apply ext'
   simp
 
 /-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
@@ -123,6 +125,11 @@ theorem toArray_concat {as : List α} {x : α} :
     l.toArray.foldl f init = l.foldl f init := by
   rw [foldl_eq_foldl_toList]
 
+@[simp] theorem append_toArray (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
 end List
 
 namespace Array
@@ -136,10 +143,10 @@ attribute [simp] uset
 @[deprecated toArray_toList (since := "2024-09-09")]
 abbrev toArray_data := @toArray_toList
 
-@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
+@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
 
-@[deprecated toList_length (since := "2024-09-09")]
-abbrev data_length := @toList_length
+@[deprecated length_toList (since := "2024-09-09")]
+abbrev data_length := @length_toList
 
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
@@ -175,25 +182,25 @@ where
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
     unfold mapM.map; split
     · rw [← List.get_drop_eq_drop _ i ‹_›]
-      simp only [aux (i + 1), map_eq_pure_bind, toList_length, List.foldlM_cons, bind_assoc,
+      simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
     · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
   decreasing_by decreasing_trivial_pre_omega
 
-@[simp] theorem map_toList (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
+@[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
   rw [map, mapM_eq_foldlM]
   apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
   have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
     induction l generalizing arr <;> simp [*]
   simp [H]
 
-@[deprecated map_toList (since := "2024-09-09")]
-abbrev map_data := @map_toList
+@[deprecated toList_map (since := "2024-09-09")]
+abbrev map_data := @toList_map
 
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
-  simp only [← toList_length]
+  simp only [← length_toList]
   simp
 
 @[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@@ -201,6 +208,11 @@ abbrev map_data := @map_toList
 @[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
     arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
 
+@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
+    (arr ++ l).toList = arr.toList ++ l := by
+  cases arr
+  simp
+
 theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
     (F : Array β → α → Array β) (G : α → List β)
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
@@ -292,14 +304,14 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
 @[simp] theorem set!_is_setD : @set! = @setD := rfl
 
 @[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
-  (Array.setD a index val).size = a.size := by
+    (Array.setD a index val).size = a.size := by
   if h : index < a.size  then
     simp [setD, h]
   else
     simp [setD, h]
 
 @[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-  (setD a i v)[i]'h = v := by
+    (setD a i v)[i]'h = v := by
   simp at h
   simp only [setD, h, dite_true, getElem_set, ite_true]
 
@@ -309,7 +321,7 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a
 
 /-- Simplifies a normal form from `get!` -/
 @[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
-  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
+    Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
   by_cases h : i < a.size <;>
     simp [setD, Nat.not_lt_of_le, h,  getD_get?]
 
@@ -424,12 +436,18 @@ theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList :
 @[deprecated getElem_mem_toList (since := "2024-09-09")]
 abbrev getElem_mem_data := @getElem_mem_toList
 
+theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
+
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
 theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
   by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
 
-@[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
 
+set_option linter.deprecated false in
 theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
   getElem?_eq_toList_get? ..
 
@@ -439,11 +457,15 @@ abbrev get?_eq_data_get? := @get?_eq_toList_get?
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp [get!_eq_getD]
 
+theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
+  cases as
+  simp [List.getElem?_eq_some_iff]
+
 @[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
   simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_get?]
+  simp [back?, getElem?_eq_toList_getElem?]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
@@ -501,7 +523,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
-  (setD a i v)[i] = v := by
+    (setD a i v)[i] = v := by
   simp at h
   simp only [setD, h, dite_true, get_set, ite_true]
 
@@ -603,11 +625,11 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
   simp [getElem_eq_getElem_toList]
 
 set_option linter.deprecated false in
-@[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
+@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
   let rec go (as : Array α) (i j hj)
       (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
-      (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
+      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
+      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
     · match j with | j+1 => ?_
       simp only [Nat.add_sub_cancel]
@@ -615,34 +637,37 @@ set_option linter.deprecated false in
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
       · intro k
-        rw [← getElem?_eq_toList_get?, get?_swap]
-        simp only [H, getElem_eq_toList_get, ← List.get?_eq_get, Nat.le_of_lt h₁,
-          getElem?_eq_toList_get?]
+        rw [← getElem?_eq_toList_getElem?, get?_swap]
+        simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
+          getElem?_eq_toList_getElem?]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
         split <;> rename_i h₃
         · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.get?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
         simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
           Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
     · rw [H]; split <;> rename_i h₂
       · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
         cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.get?_reverse' _ _ h).symm
+        exact (List.getElem?_reverse' _ _ h).symm
       · rfl
     termination_by j - i
   simp only [reverse]
   split
   · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
   · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext_get? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
     split
     · rfl
     · rename_i h
       simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
         true_and, Nat.not_lt] at h
-      rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.toList.length_reverse ▸ ‹_›)]
+      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
+
+@[deprecated toList_reverse (since := "2024-09-30")]
+abbrev reverse_toList := @toList_reverse
 
 /-! ### foldl / foldr -/
 
@@ -708,16 +733,20 @@ theorem foldr_induction
 /-! ### map -/
 
 @[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
-  simp only [mem_def, map_toList, List.mem_map]
+  simp only [mem_def, toList_map, List.mem_map]
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = return mk (← arr.toList.mapM f) := by
+    arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
   rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
   | cons a l ih => simp [ih]
 
+@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
+    toList <$> arr.mapM f = arr.toList.mapM f := by
+  simp [mapM_eq_mapM_toList]
+
 @[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
 abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
 
@@ -774,16 +803,20 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
   simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
 
 @[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
-    ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
+    (as.map f)[i] = f (as[i]'(size_map .. ▸ h)) := by
   have := map_spec as f (fun i b => b = f (as[i]))
   simp only [implies_true, true_implies] at this
   obtain ⟨eq, w⟩ := this
   apply w
   simp_all
 
+@[simp] theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) :
+    (as.map f)[i]? = as[i]?.map f := by
+  simp [getElem?_def]
+
 /-! ### mapIdx -/
 
--- This could also be prove from `SatisfiesM_mapIdxM`.
+-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
 theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
     (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop)
@@ -823,10 +856,15 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
 
 @[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
     (h : i < (mapIdx a f).size) :
-    haveI : i < a.size := by simp_all
-    (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
+    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
   (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
 
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+    (a.mapIdx f)[i]? =
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
+  split <;> simp_all
+
 /-! ### modify -/
 
 @[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
@@ -918,34 +956,45 @@ abbrev empty_data := @toList_empty
 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
 
 @[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  simp only [mem_def, append_toList, List.mem_append]
+  simp only [mem_def, toList_append, List.mem_append]
 
-theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, append_toList, List.length_append]
+@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, toList_append, List.length_append]
 
-theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
+theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
+    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
+  cases as; cases bs
+  simp [List.getElem_append]
+
+theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
     (as ++ bs)[i] = as[i] := by
   simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
-  apply List.get_of_eq; rw [append_toList]
+  apply List.get_of_eq; rw [toList_append]
 
-theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
+@[deprecated getElem_append_left (since := "2024-09-30")]
+abbrev get_append_left := @getElem_append_left
+
+theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
     (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (as ++ bs)[i] = bs[i - as.size] := by
   simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
-  apply List.get_of_eq; rw [append_toList]
+  apply List.get_of_eq; rw [toList_append]
+
+@[deprecated getElem_append_right (since := "2024-09-30")]
+abbrev get_append_right := @getElem_append_right
 
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
-  apply ext'; simp only [append_toList, toList_empty, List.append_nil]
+  apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
 @[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
-  apply ext'; simp only [append_toList, toList_empty, List.nil_append]
+  apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
 theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
-  apply ext'; simp only [append_toList, List.append_assoc]
+  apply ext'; simp only [toList_append, List.append_assoc]
 
 /-! ### extract -/
 
@@ -995,20 +1044,20 @@ theorem size_extract_loop (as bs : Array α) (size start : Nat) :
   simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
     Nat.min_assoc, Nat.min_self]
 
-theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
+theorem getElem_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
     i < (extract.loop as size start bs).size := by
   rw [size_extract_loop]
   apply Nat.lt_of_lt_of_le hlt
   exact Nat.le_add_right ..
 
-theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
-    (h := get_extract_loop_lt_aux as bs size start hlt) :
+theorem getElem_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
+    (h := getElem_extract_loop_lt_aux as bs size start hlt) :
     (extract.loop as size start bs)[i] = bs[i] := by
-  apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
+  apply Eq.trans _ (getElem_append_left (bs:=extract.loop as size start #[]) hlt)
   · rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
   · congr; rw [extract_loop_eq_aux]
 
-theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+theorem getElem_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
     (h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
   have h : i < bs.size + (as.size - start) := by
       apply Nat.lt_of_lt_of_le h
@@ -1019,9 +1068,9 @@ theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i
   apply Nat.add_lt_of_lt_sub'
   exact Nat.sub_lt_left_of_lt_add hge h
 
-theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
     (h : i < (extract.loop as size start bs).size)
-    (h' := get_extract_loop_ge_aux as bs size start hge h) :
+    (h' := getElem_extract_loop_ge_aux as bs size start hge h) :
     (extract.loop as size start bs)[i] = as[start + i - bs.size] := by
   induction size using Nat.recAux generalizing start bs with
   | zero =>
@@ -1043,28 +1092,37 @@ theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ b
       have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
         rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
       have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
+        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
       rw [h]; congr; rw [Nat.add_sub_cancel]
     else
       have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
       rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
       congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
 
-theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
+theorem getElem_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
     start + i < as.size := by
   rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
   apply Nat.sub_le_sub_right; apply Nat.min_le_right
 
-@[simp] theorem get_extract {as : Array α} {start stop : Nat}
+@[simp] theorem getElem_extract {as : Array α} {start stop : Nat}
     (h : i < (as.extract start stop).size) :
-    (as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
+    (as.extract start stop)[i] = as[start + i]'(getElem_extract_aux h) :=
   show (extract.loop as (min stop as.size - start) start #[])[i]
-    = as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
+    = as[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
+
+theorem getElem?_extract {as : Array α} {start stop : Nat} :
+    (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none := by
+  simp only [getElem?_def, size_extract, getElem_extract]
+  split
+  · split
+    · rfl
+    · omega
+  · rfl
 
 @[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
   apply ext
   · rw [size_extract, Nat.min_self, Nat.sub_zero]
-  · intros; rw [get_extract]; congr; rw [Nat.zero_add]
+  · intros; rw [getElem_extract]; congr; rw [Nat.zero_add]
 
 theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
     as.extract start stop = #[] := by
@@ -1146,9 +1204,12 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
 theorem any_eq_true {p : α → Bool} {as : Array α} :
     any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
 
-theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.any p := by
+theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
-  exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
+  exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
+
+@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
+abbrev any_def := @any_toList
 
 /-! ### all -/
 
@@ -1180,22 +1241,25 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
 theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
   simp [all_iff_forall, Fin.isLt]
 
-theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p := by
+theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
   constructor
+  · intro w i
+    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
   · rintro w x ⟨r, h, rfl⟩
     rw [← getElem_eq_getElem_toList]
     exact w ⟨r, h⟩
-  · intro w i
-    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
+
+@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
+abbrev all_def := @all_toList
 
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
-  simp only [all_def, List.all_eq_true, mem_def]
+  simp only [← all_toList, List.all_eq_true, mem_def]
 
 /-! ### contains -/
 
 theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
-  rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
+  rw [mem_def, contains, ← any_toList, List.any_eq_true]; simp [and_comm]
 
 instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
   decidable_of_iff _ contains_def
@@ -1204,12 +1268,12 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
 
 open Fin
 
-@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
+@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
   by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
 
-@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
+@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
   if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
-    simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
+    simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
   else by
     apply Eq.trans
     · apply Array.get_set_ne
@@ -1217,7 +1281,7 @@ open Fin
       · assumption
     · simp [get_set_ne]
 
-@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
+@[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
     (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
   apply Eq.trans
   · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
@@ -1229,22 +1293,22 @@ open Fin
     · apply Ne.symm
       · assumption
 
-theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
+theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
     (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
   split
-  · simp_all only [get_swap_left]
+  · simp_all only [getElem_swap_left]
   · split <;> simp_all
 
-theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
+theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.swap i j).size) :
     (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
-  apply get_swap
+  apply getElem_swap'
 
 @[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
     (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
   apply ext
   · simp only [size_swap]
   · intros
-    simp only [get_swap']
+    simp only [getElem_swap]
     split
     · simp_all
     · split <;> simp_all
@@ -1253,11 +1317,35 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
   apply ext
   · simp only [size_swap]
   · intros
-    simp only [get_swap']
+    simp only [getElem_swap]
     split
     · split <;> simp_all
     · split <;> simp_all
 
+@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
+abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
+@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
+abbrev get_extract_loop_lt := @getElem_extract_loop_lt
+@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
+abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
+@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
+abbrev get_extract_loop_ge := @getElem_extract_loop_ge
+@[deprecated getElem_extract_aux (since := "2024-09-30")]
+abbrev get_extract_aux := @getElem_extract_aux
+@[deprecated getElem_extract (since := "2024-09-30")]
+abbrev get_extract := @getElem_extract
+
+@[deprecated getElem_swap_right (since := "2024-09-30")]
+abbrev get_swap_right := @getElem_swap_right
+@[deprecated getElem_swap_left (since := "2024-09-30")]
+abbrev get_swap_left := @getElem_swap_left
+@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
+abbrev get_swap_of_ne := @getElem_swap_of_ne
+@[deprecated getElem_swap (since := "2024-09-30")]
+abbrev get_swap := @getElem_swap
+@[deprecated getElem_swap' (since := "2024-09-30")]
+abbrev get_swap' := @getElem_swap'
+
 end Array
 
 
@@ -1274,9 +1362,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[simp] theorem getElem?_toArray (l : List α) (i : Nat) : l.toArray[i]? = l[i]? := by
-  simp [getElem?_eq_getElem?_toList]
-
 @[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
   simp
 
@@ -1331,14 +1416,14 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   rw [← anyM_toList]
 
 @[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [Array.any_def]
+  rw [any_toList]
 
 @[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
     l.toArray.allM p = l.allM p := by
   rw [← allM_toList]
 
 @[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [Array.all_def]
+  rw [all_toList]
 
 @[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
     l.toArray.swap i j = ((l.set i l[j]).set j l[i]).toArray := by
@@ -1363,11 +1448,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
 
-@[simp] theorem append_toArray (l₁ l₂ : List α) :
-    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
   apply ext'
   simp

src/Init/Data/List/Lemmas.lean

@@ -203,6 +203,9 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
 
 @[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl
 
+theorem getElem?_eq_some {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i]'h = a := by
+  simpa using get?_eq_some
+
 /--
 If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
 `rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the

src/Init/Data/Option.lean

@@ -8,3 +8,5 @@ import Init.Data.Option.Basic
 import Init.Data.Option.BasicAux
 import Init.Data.Option.Instances
 import Init.Data.Option.Lemmas
+import Init.Data.Option.Attach
+import Init.Data.Option.List

src/Init/Data/Option/Attach.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Option.Basic
+import Init.Data.Option.List
+import Init.Data.List.Attach
+import Init.BinderPredicates
+
+namespace Option
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`Option {x // P x}` is the same as the input `Option α`.
+-/
+@[inline] private unsafe def attachWithImpl
+    (o : Option α) (P : α → Prop) (_ : ∀ x ∈ o, P x) : Option {x // P x} := unsafeCast o
+
+/-- "Attach" a proof `P x` that holds for the element of `o`, if present,
+to produce a new option with the same element but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (xs : Option α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Option {x // P x} :=
+  match xs with
+  | none => none
+  | some x => some ⟨x, H x (mem_some_self x)⟩
+
+/-- "Attach" the proof that the element of `xs`, if present, is in `xs`
+to produce a new option with the same elements but in the type `{x // x ∈ xs}`. -/
+@[inline] def attach (xs : Option α) : Option {x // x ∈ xs} := xs.attachWith _ fun _ => id
+
+@[simp] theorem attach_none : (none : Option α).attach = none := rfl
+@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
+
+@[simp] theorem attach_some {x : α} :
+    (some x).attach = some ⟨x, rfl⟩ := rfl
+@[simp] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) :
+    (some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl
+
+theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
+    o₁.attach = o₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
+  subst h
+  simp
+
+theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
+    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
+  subst w
+  simp
+
+theorem attach_map_coe (o : Option α) (f : α → β) :
+    (o.attach.map fun (i : {i // i ∈ o}) => f i) = o.map f := by
+  cases o <;> simp
+
+theorem attach_map_val (o : Option α) (f : α → β) :
+    (o.attach.map fun i => f i.val) = o.map f :=
+  attach_map_coe _ _
+
+@[simp]
+theorem attach_map_subtype_val (o : Option α) :
+    o.attach.map Subtype.val = o :=
+  (attach_map_coe _ _).trans (congrFun Option.map_id _)
+
+theorem attachWith_map_coe {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
+    ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
+  cases o <;> simp [H]
+
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
+    ((o.attachWith p H).map fun i => f i.val) = o.map f :=
+  attachWith_map_coe _ _ _
+
+@[simp]
+theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).map Subtype.val = o :=
+  (attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
+
+@[simp] theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
+  | none, ⟨x, h⟩ => by simp at h
+  | some a, ⟨x, h⟩ => by simpa using h
+
+@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
+  cases o <;> simp
+
+@[simp] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).isNone = o.isNone := by
+  cases o <;> simp
+
+@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
+  cases o <;> simp
+
+@[simp] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).isSome = o.isSome := by
+  cases o <;> simp
+
+@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none ↔ o = none := by
+  cases o <;> simp
+
+@[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} :
+    o.attach = some x ↔ o = some x.val := by
+  cases o <;> cases x <;> simp
+
+@[simp] theorem attachWith_eq_none_iff {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    o.attachWith p H = none ↔ o = none := by
+  cases o <;> simp
+
+@[simp] theorem attachWith_eq_some_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) {x : {x // p x}} :
+    o.attachWith p H = some x ↔ o = some x.val := by
+  cases o <;> cases x <;> simp
+
+@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
+    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ := by
+  cases o
+  · simp at h
+  · simp [get_some]
+
+@[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) (h : (o.attachWith p H).isSome) :
+    (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
+  cases o
+  · simp at h
+  · simp [get_some]
+
+@[simp] theorem toList_attach (o : Option α) :
+    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  cases o <;> simp
+
+theorem attach_map {o : Option α} (f : α → β) :
+    (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
+  cases o <;> simp
+
+theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
+    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
+      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
+  cases o <;> simp
+
+theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
+    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
+  cases o <;> simp
+
+theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
+    (f : { x // P x } → β) :
+    (o.attachWith P H).map f =
+      o.pmap (fun a (h : a ∈ o ∧ P a) => f ⟨a, h.2⟩) (fun a h => ⟨h, H a h⟩) := by
+  cases o <;> simp
+
+theorem attach_bind {o : Option α} {f : α → Option β} :
+    (o.bind f).attach =
+      o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, mem_bind_iff.mpr ⟨x, h, h'⟩⟩ := by
+  cases o <;> simp
+
+theorem bind_attach {o : Option α} {f : {x // x ∈ o} → Option β} :
+    o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
+  cases o <;> simp
+
+theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → a ∈ o → Option β} :
+    o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
+  cases o <;> simp
+
+theorem attach_filter {o : Option α} {p : α → Bool} :
+    (o.filter p).attach =
+      o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [filter_some, attach_some]
+    ext
+    simp only [mem_def, attach_eq_some_iff, ite_none_right_eq_some, some.injEq, some_bind,
+      dite_none_right_eq_some]
+    constructor
+    · rintro ⟨h, w⟩
+      refine ⟨h, by ext; simpa using w⟩
+    · rintro ⟨h, rfl⟩
+      simp [h]
+
+theorem filter_attach {o : Option α} {p : {x // x ∈ o} → Bool} :
+    o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
+  cases o <;> simp [filter_some]
+
+end Option

src/Init/Data/Option/Lemmas.lean

@@ -138,6 +138,10 @@ theorem bind_eq_none' {o : Option α} {f : α → Option β} :
     o.bind f = none ↔ ∀ b a, a ∈ o → b ∉ f a := by
   simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]
 
+theorem mem_bind_iff {o : Option α} {f : α → Option β} :
+    b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
+  cases o <;> simp
+
 theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β) :
     (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
   cases a <;> cases b <;> rfl
@@ -232,9 +236,27 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
   cases o <;> simp at h ⊢
 
 @[simp] theorem filter_eq_none {p : α → Bool} :
-    Option.filter p o = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
+    o.filter p = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
   cases o <;> simp [filter_some]
 
+@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} :
+    o.filter p = some a ↔ a ∈ o ∧ p a := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp [filter_some]
+    split <;> rename_i h
+    · simp only [some.injEq, iff_self_and]
+      rintro rfl
+      exact h
+    · simp only [reduceCtorEq, false_iff, not_and, Bool.not_eq_true]
+      rintro rfl
+      simpa using h
+
+theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
+    a ∈ o.filter p ↔ a ∈ o ∧ p a := by
+  simp
+
 @[simp] theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
     Option.all q (guard p a) = (!p a || q a) := by
   simp only [guard]
@@ -350,6 +372,8 @@ end choice
 
 @[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
 
+-- See `Init.Data.Option.List` for lemmas about `toList`.
+
 @[simp] theorem or_some : (some a).or o = some a := rfl
 @[simp] theorem none_or : none.or o = o := rfl
 

src/Init/Data/Option/List.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Lemmas
+
+namespace Option
+
+@[simp] theorem mem_toList (a : α) (o : Option α) : a ∈ o.toList ↔ a ∈ o := by
+  cases o <;> simp [eq_comm]
+
+end Option

src/Lean/Elab/Structure.lean

@@ -733,7 +733,8 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
         throwError "invalid default value for field, it contains metavariables{indentExpr value}"
       /- The identity function is used as "marker". -/
       let value ← mkId value
-      discard <| mkAuxDefinition declName type value (zetaDelta := true)
+      -- No need to compile the definition, since it is only used during elaboration.
+      discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
       setReducibleAttribute declName
 
 /--

src/Std/Data/DHashMap/Internal/Model.lean

@@ -186,7 +186,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
     have := (hg (l := []) (l' := [])).length_eq
     rw [List.length_append, List.append_nil] at this
     omega
-  rw [updateAllBuckets, toListModel, Array.map_toList, List.bind_eq_foldl, List.foldl_map,
+  rw [updateAllBuckets, toListModel, Array.toList_map, List.bind_eq_foldl, List.foldl_map,
     toListModel, List.bind_eq_foldl]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
       Perm (g l'') l' →

src/Std/Sat/AIG/RefVec.lean

@@ -104,10 +104,10 @@ def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) :=
     by
       intro i h
       by_cases hsplit : i < lrefs.size
-      · rw [Array.get_append_left]
+      · rw [Array.getElem_append_left]
         apply hl2
         omega
-      · rw [Array.get_append_right]
+      · rw [Array.getElem_append_right]
         · apply hr2
           omega
         · omega
@@ -124,9 +124,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
   simp only [get, append]
   split
   · simp [Ref.mk.injEq]
-    rw [Array.get_append_left]
+    rw [Array.getElem_append_left]
   · simp only [Ref.mk.injEq]
-    rw [Array.get_append_right]
+    rw [Array.getElem_append_right]
     · simp [lhs.hlen]
     · rw [lhs.hlen]
       omega

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -502,7 +502,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
@@ -535,7 +535,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
@@ -595,7 +595,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               have idx_in_bounds2 : idx < f.clauses.size := by
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
               rw [hidx] at heq
               simp only [Option.some.injEq] at heq

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -468,10 +468,10 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
   rcases List.get_of_mem h with ⟨j, h'⟩
   have j_in_bounds : j < ratHints.size := by
     have j_property := j.2
-    simp only [Array.map_toList, List.length_map] at j_property
+    simp only [Array.toList_map, List.length_map] at j_property
     dsimp at *
     omega
-  simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
+  simp only [List.get_eq_getElem, Array.toList_map, Array.length_toList, List.getElem_map] at h'
   rw [← Array.getElem_eq_getElem_toList] at h'
   rw [← Array.getElem_eq_getElem_toList] at c'_in_f
   exists ⟨j.1, j_in_bounds⟩

tests/lean/run/2710.lean

@@ -0,0 +1,8 @@
+/-!
+# Structure field default values can be noncomputable
+-/
+
+noncomputable def ohno := 1
+
+structure OhNo where
+  x := ohno