feat: align List/Array/Vector flatten lemmas (#6640)

This PR completes aligning `List`/`Array`/`Vector` lemmas about
`flatten`. `Vector.flatten` was previously missing, and has been added
(for rectangular sizes only). A small number of missing `Option` lemmas
were also need to get the proofs to go through.

src/Init/Data/Array/Basic.lean

@@ -576,6 +576,12 @@ def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : A
 def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β :=
   Id.run <| as.foldrM f init start stop
 
+/-- Sum of an array.
+
+`Array.sum #[a, b, c] = a + (b + (c + 0))` -/
+def sum {α} [Add α] [Zero α] : Array α → α :=
+  foldr (· + ·) 0
+
 @[inline]
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
   Id.run <| as.mapM f

src/Init/Data/Array/Bootstrap.lean

@@ -81,12 +81,18 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
+@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
-@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
+@[deprecated append_empty (since := "2025-01-13")]
+abbrev append_nil := @append_empty
+
+@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by
   apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
+@[deprecated empty_append (since := "2025-01-13")]
+abbrev nil_append := @empty_append
+
 @[simp] theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 

src/Init/Data/Array/Find.lean

@@ -74,12 +74,12 @@ theorem findSome?_append {l₁ l₂ : Array α} : (l₁ ++ l₂).findSome? f = (
 
 theorem getElem?_zero_flatten (L : Array (Array α)) :
     (flatten L)[0]? = L.findSome? fun l => l[0]? := by
-  cases L using array_array_induction
+  cases L using array₂_induction
   simp [← List.head?_eq_getElem?, List.head?_flatten, List.findSome?_map, Function.comp_def]
 
 theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.size) :
     (L.findSome? fun l => l[0]?).isSome := by
-  cases L using array_array_induction
+  cases L using array₂_induction
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
     List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
@@ -95,7 +95,7 @@ theorem getElem_zero_flatten {L : Array (Array α)} (h) :
 
 theorem back?_flatten {L : Array (Array α)} :
     (flatten L).back? = (L.findSomeRev? fun l => l.back?) := by
-  cases L using array_array_induction
+  cases L using array₂_induction
   simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]
 
 theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
@@ -203,7 +203,7 @@ theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
 
 @[simp] theorem find?_flatten (xs : Array (Array α)) (p : α → Bool) :
     xs.flatten.find? p = xs.findSome? (·.find? p) := by
-  cases xs using array_array_induction
+  cases xs using array₂_induction
   simp [List.findSome?_map, Function.comp_def]
 
 theorem find?_flatten_eq_none {xs : Array (Array α)} {p : α → Bool} :
@@ -220,7 +220,7 @@ theorem find?_flatten_eq_some {xs : Array (Array α)} {p : α → Bool} {a : α}
       p a ∧ ∃ (as : Array (Array α)) (ys zs : Array α) (bs : Array (Array α)),
         xs = as.push (ys.push a ++ zs) ++ bs ∧
         (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
-  cases xs using array_array_induction
+  cases xs using array₂_induction
   simp only [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some]
   simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
   intro w