chore: alignment of Array and List lemmas (#6342)

Further alignment of `Array` and `List` lemmas. Moved lemmas about
`List.toArray` to a separate file, and aligned lemmas about membership.

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