typo

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

src/Init/Data/Array/Lemmas.lean

@@ -38,6 +38,14 @@ namespace Array
 
 @[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
 
+theorem eq_toArray : v = List.toArray a ↔ v.toList = a := by
+  cases v
+  simp
+
+theorem toArray_eq : List.toArray a = v ↔ a = v.toList := by
+  cases v
+  simp
+
 /-! ### empty -/
 
 @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by
@@ -256,6 +264,11 @@ theorem getElem?_push {a : Array α} {x} : (a.push x)[i]? = if i = a.size then s
 theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a else none := by
   simp [List.getElem?_singleton]
 
+theorem ext_getElem? {l₁ l₂ : Array α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ := by
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simpa using List.ext_getElem? (by simpa using h)
+
 /-! ### mem -/
 
 theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
@@ -1089,9 +1102,21 @@ theorem forall_mem_map {f : α → β} {l : Array α} {P : β → Prop} :
     (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j) := by
   simp
 
+@[simp] theorem map_eq_empty_iff {f : α → β} {l : Array α} : map f l = #[] ↔ l = #[] := by
+  cases l
+  simp
+
+theorem eq_empty_of_map_eq_empty {f : α → β} {l : Array α} (h : map f l = #[]) : l = #[] :=
+  map_eq_empty_iff.mp h
+
 @[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
   cases l <;> simp_all
 
+theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l' := by
+  cases l
+  cases l'
+  simp [List.map_inj_right w]
+
 theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l :=
   map_inj_left.2 h
 
@@ -1100,13 +1125,6 @@ theorem map_inj : map f = map g ↔ f = g := by
   · intro h; ext a; replace h := congrFun h #[a]; simpa using h
   · intro h; subst h; rfl
 
-@[simp] theorem map_eq_empty_iff {f : α → β} {l : Array α} : map f l = #[] ↔ l = #[] := by
-  cases l
-  simp
-
-theorem eq_empty_of_map_eq_empty {f : α → β} {l : Array α} (h : map f l = #[]) : l = #[] :=
-  map_eq_empty_iff.mp h
-
 theorem map_eq_push_iff {f : α → β} {l : Array α} {l₂ : Array β} {b : β} :
     map f l = l₂.push b ↔ ∃ l₁ a, l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b := by
   rcases l with ⟨l⟩
@@ -1189,6 +1207,30 @@ theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
     rfl
 termination_by as.size - i
 
+/--
+Use this as `induction ass using array₂_induction` on a hypothesis of the form `ass : Array (Array α)`.
+The hypothesis `ass` will be replaced with a hypothesis `ass : List (List α)`,
+and former appearances of `ass` in the goal will be replaced with `(ass.map List.toArray).toArray`.
+-/
+-- We can't use `@[cases_eliminator]` here as
+-- `Lean.Meta.getCustomEliminator?` only looks at the top-level constant.
+theorem array₂_induction (P : Array (Array α) → Prop) (of : ∀ (xss : List (List α)), P (xss.map List.toArray).toArray)
+    (ass : Array (Array α)) : P ass := by
+  specialize of (ass.toList.map toList)
+  simpa [← toList_map, Function.comp_def, map_id] using of
+
+/--
+Use this as `induction ass using array₃_induction` on a hypothesis of the form `ass : Array (Array (Array α))`.
+The hypothesis `ass` will be replaced with a hypothesis `ass : List (List (List α))`,
+and former appearances of `ass` in the goal will be replaced with
+`((ass.map (fun xs => xs.map List.toArray)).map List.toArray).toArray`.
+-/
+theorem array₃_induction (P : Array (Array (Array α)) → Prop)
+    (of : ∀ (xss : List (List (List α))), P ((xss.map (fun xs => xs.map List.toArray)).map List.toArray).toArray)
+    (ass : Array (Array (Array α))) : P ass := by
+  specialize of ((ass.toList.map toList).map (fun as => as.map toList))
+  simpa [← toList_map, Function.comp_def, map_id] using of
+
 /-! ### filter -/
 
 @[congr]
@@ -1564,10 +1606,6 @@ theorem forall_mem_append {p : α → Prop} {l₁ l₂ : Array α} :
     (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
   simp only [mem_append, or_imp, forall_and]
 
-theorem empty_append (as : Array α) : #[] ++ as = as := by simp
-
-theorem append_empty (as : Array α) : as ++ #[] = as := by simp
-
 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
@@ -1664,13 +1702,13 @@ theorem append_left_inj {s₁ s₂ : Array α} (t) : s₁ ++ t = s₂ ++ t ↔ s
   ⟨fun h => append_inj_left' h rfl, congrArg (· ++ _)⟩
 
 @[simp] theorem append_left_eq_self {x y : Array α} : x ++ y = y ↔ x = #[] := by
-  rw [← append_left_inj (s₁ := x), nil_append]
+  rw [← append_left_inj (s₁ := x), empty_append]
 
 @[simp] theorem self_eq_append_left {x y : Array α} : y = x ++ y ↔ x = #[] := by
   rw [eq_comm, append_left_eq_self]
 
 @[simp] theorem append_right_eq_self {x y : Array α} : x ++ y = x ↔ y = #[] := by
-  rw [← append_right_inj (t₁ := y), append_nil]
+  rw [← append_right_inj (t₁ := y), append_empty]
 
 @[simp] theorem self_eq_append_right {x y : Array α} : x = x ++ y ↔ y = #[] := by
   rw [eq_comm, append_right_eq_self]
@@ -1808,6 +1846,189 @@ theorem append_eq_map_iff {f : α → β} :
     L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
   rw [eq_comm, map_eq_append_iff]
 
+/-! ### flatten -/
+
+@[simp] theorem flatten_empty : (#[] : Array (Array α)).flatten = #[] := by simp [flatten]; rfl
+
+@[simp] theorem toList_flatten {l : Array (Array α)} :
+    l.flatten.toList = (l.toList.map toList).flatten := by
+  dsimp [flatten]
+  simp only [← foldl_toList]
+  generalize l.toList = l
+  have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
+  exact this #[]
+  induction l with
+  | nil => simp
+  | cons h => induction h.toList <;> simp [*]
+
+@[simp] theorem flatten_map_toArray (l : List (List α)) :
+    (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
+  apply ext'
+  simp [Function.comp_def]
+
+@[simp] theorem flatten_toArray_map (l : List (List α)) :
+    (l.map List.toArray).toArray.flatten = l.flatten.toArray := by
+  rw [← flatten_map_toArray]
+  simp
+
+@[simp] theorem size_flatten (L : Array (Array α)) : L.flatten.size = (L.map size).sum := by
+  cases L using array₂_induction
+  simp [Function.comp_def]
+
+@[simp] theorem flatten_singleton (l : Array α) : #[l].flatten = l := by simp [flatten]; rfl
+
+theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by
+  simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map]
+  intro l
+  constructor
+  · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
+    exact ⟨s, m, h⟩
+  · rintro ⟨s, h₁, h₂⟩
+    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
+
+@[simp] theorem flatten_eq_nil_iff {L : Array (Array α)} : L.flatten = #[] ↔ ∀ l ∈ L, l = #[] := by
+  induction L using array₂_induction
+  simp
+
+@[simp] theorem nil_eq_flatten_iff {L : Array (Array α)} : #[] = L.flatten ↔ ∀ l ∈ L, l = #[] := by
+  rw [eq_comm, flatten_eq_nil_iff]
+
+theorem flatten_ne_nil_iff {xs : Array (Array α)} : xs.flatten ≠ #[] ↔ ∃ x, x ∈ xs ∧ x ≠ #[] := by
+  simp
+
+theorem exists_of_mem_flatten : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := mem_flatten.1
+
+theorem mem_flatten_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ flatten L := mem_flatten.2 ⟨l, lL, al⟩
+
+theorem forall_mem_flatten {p : α → Prop} {L : Array (Array α)} :
+    (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x := by
+  simp only [mem_flatten, forall_exists_index, and_imp]
+  constructor <;> (intros; solve_by_elim)
+
+theorem flatten_eq_flatMap {L : Array (Array α)} : flatten L = L.flatMap id := by
+  induction L using array₂_induction
+  rw [flatten_toArray_map, List.flatten_eq_flatMap]
+  simp [List.flatMap_map]
+
+@[simp] theorem map_flatten (f : α → β) (L : Array (Array α)) :
+    (flatten L).map f = (map (map f) L).flatten := by
+  induction L using array₂_induction with
+  | of xss =>
+    simp only [flatten_toArray_map, List.map_toArray, List.map_flatten, List.map_map,
+      Function.comp_def]
+    rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+
+@[simp] theorem filterMap_flatten (f : α → Option β) (L : Array (Array α)) :
+    filterMap f (flatten L) = flatten (map (filterMap f) L) := by
+  induction L using array₂_induction
+  simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filterMap_toArray',
+    List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]
+  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+
+@[simp] theorem filter_flatten (p : α → Bool) (L : Array (Array α)) :
+    filter p (flatten L) = flatten (map (filter p) L) := by
+  induction L using array₂_induction
+  simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filter_toArray',
+    List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
+  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+
+theorem flatten_filter_not_isEmpty {L : Array (Array α)} :
+    flatten (L.filter fun l => !l.isEmpty) = L.flatten := by
+  induction L using array₂_induction
+  simp [List.filter_map, Function.comp_def, List.flatten_filter_not_isEmpty]
+
+theorem flatten_filter_ne_empty [DecidablePred fun l : Array α => l ≠ #[]] {L : Array (Array α)} :
+    flatten (L.filter fun l => l ≠ #[]) = L.flatten := by
+  simp only [ne_eq, ← isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false,
+    flatten_filter_not_isEmpty]
+
+@[simp] theorem flatten_append (L₁ L₂ : Array (Array α)) :
+    flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂ := by
+  induction L₁ using array₂_induction
+  induction L₂ using array₂_induction
+  simp [← List.map_append]
+
+theorem flatten_push (L : Array (Array α)) (l : Array α) :
+    flatten (L.push l) = flatten L ++ l := by
+  induction L using array₂_induction
+  rcases l with ⟨l⟩
+  have this : [l.toArray] = [l].map List.toArray := by simp
+  simp only [List.push_toArray, flatten_toArray_map, List.append_toArray]
+  rw [this, ← List.map_append, flatten_toArray_map]
+  simp
+
+theorem flatten_flatten {L : Array (Array (Array α))} : flatten (flatten L) = flatten (map flatten L) := by
+  induction L using array₃_induction with
+  | of xss =>
+    rw [flatten_toArray_map]
+    have : (xss.map (fun xs => xs.map List.toArray)).flatten = xss.flatten.map List.toArray := by
+      induction xss with
+      | nil => simp
+      | cons xs xss ih =>
+        simp only [List.map_cons, List.flatten_cons, ih, List.map_append]
+    rw [this, flatten_toArray_map, List.flatten_flatten, ← List.map_toArray, Array.map_map,
+      ← List.map_toArray, map_map, Function.comp_def]
+    simp only [Function.comp_apply, flatten_toArray_map]
+    rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map]
+
+theorem flatten_eq_push_iff {xs : Array (Array α)} {ys : Array α} {y : α} :
+    xs.flatten = ys.push y ↔
+      ∃ (as : Array (Array α)) (bs : Array α) (cs : Array (Array α)),
+        xs = as.push (bs.push y) ++ cs ∧ (∀ l, l ∈ cs → l = #[]) ∧ ys = as.flatten ++ bs := by
+  induction xs using array₂_induction with
+  | of xs =>
+    rcases ys with ⟨ys⟩
+    rw [flatten_toArray_map, List.push_toArray, mk.injEq, List.flatten_eq_append_iff]
+    constructor
+    · rintro (⟨as, bs, rfl, rfl, h⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h⟩)
+      · rw [List.singleton_eq_flatten_iff] at h
+        obtain ⟨xs, ys, rfl, h₁, h₂⟩ := h
+        exact ⟨((as ++ xs).map List.toArray).toArray, #[], (ys.map List.toArray).toArray, by simp,
+          by simpa using h₂, by rw [flatten_toArray_map]; simpa⟩
+      · rw [List.singleton_eq_append_iff] at h
+        obtain (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) := h
+        · simp at h₁
+        · simp at h₁ h₂
+          obtain ⟨rfl, rfl⟩ := h₁
+          exact ⟨(as.map List.toArray).toArray, bs.toArray, (ds.map List.toArray).toArray, by simpa⟩
+    · rintro ⟨as, bs, cs, h₁, h₂, h₃⟩
+      replace h₁ := congrArg (List.map Array.toList) (congrArg Array.toList h₁)
+      simp [Function.comp_def] at h₁
+      subst h₁
+      replace h₃ := congrArg Array.toList h₃
+      simp at h₃
+      subst h₃
+      right
+      exact ⟨(as.map Array.toList).toList, bs.toList, y, [], (cs.map Array.toList).toList, by simpa⟩
+
+theorem push_eq_flatten_iff {xs : Array (Array α)} {ys : Array α} {y : α} :
+    ys.push y = xs.flatten ↔
+      ∃ (as : Array (Array α)) (bs : Array α) (cs : Array (Array α)),
+        xs = as.push (bs.push y) ++ cs ∧ (∀ l, l ∈ cs → l = #[]) ∧ ys = as.flatten ++ bs := by
+  rw [eq_comm, flatten_eq_push_iff]
+
+-- For now we omit `flatten_eq_append_iff`,
+-- because it is not easily obtainable from `List.flatten_eq_append_iff`.
+-- theorem flatten_eq_append_iff {xs : Array (Array α)} {ys zs : Array α} :
+--     xs.flatten = ys ++ zs ↔
+--       (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
+--         ∃ (as : Array (Array α)) (bs : Array α) (c : α) (cs : Array α) (ds : Array (Array α)),
+--           xs = as.push ((bs.push c ++ cs)) ++ ds ∧ ys = as.flatten ++ bs.push c ∧
+--           zs = cs ++ ds.flatten := by sorry
+
+
+/-- Two arrays of subarrays are equal iff their flattens coincide, as well as the sizes of the
+subarrays. -/
+theorem eq_iff_flatten_eq {L L' : Array (Array α)} :
+    L = L' ↔ L.flatten = L'.flatten ∧ map size L = map size L' := by
+  cases L using array₂_induction with
+  | of L =>
+    cases L' using array₂_induction with
+    | of L' =>
+      simp [Function.comp_def, ← List.eq_iff_flatten_eq]
+      rw [List.map_inj_right]
+      simp +contextual
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 -- This is a duplicate of `List.toArray_toList`.
@@ -2422,28 +2643,6 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-/-! ### flatten -/
-
-@[simp] theorem toList_flatten {l : Array (Array α)} :
-    l.flatten.toList = (l.toList.map toList).flatten := by
-  dsimp [flatten]
-  simp only [← foldl_toList]
-  generalize l.toList = l
-  have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
-  exact this #[]
-  induction l with
-  | nil => simp
-  | cons h => induction h.toList <;> simp [*]
-
-theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by
-  simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map]
-  intro l
-  constructor
-  · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
-    exact ⟨s, m, h⟩
-  · rintro ⟨s, h₁, h₂⟩
-    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
-
 /-! ### extract -/
 
 theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by
@@ -2460,16 +2659,16 @@ theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start ≥
 theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) :
     extract.loop as size start bs = bs ++ extract.loop as size start #[] := by
   induction size using Nat.recAux generalizing start bs with
-  | zero => rw [extract_loop_zero, extract_loop_zero, append_nil]
+  | zero => rw [extract_loop_zero, extract_loop_zero, append_empty]
   | succ size ih =>
     if h : start < as.size then
       rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
-      rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, nil_append]
+      rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, empty_append]
       rw [append_assoc]
     else
       rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
       rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
-      rw [append_nil]
+      rw [append_empty]
 
 theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size ≤ as.size) :
   extract.loop as size start bs = bs ++ as.extract start (start + size) := by
@@ -2825,11 +3024,6 @@ namespace Array
 
 /-! ### map -/
 
-theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : List (List α)), P (xss.map List.toArray).toArray)
-    (ass : Array (Array α)) : P ass := by
-  specialize h (ass.toList.map toList)
-  simpa [← toList_map, Function.comp_def, map_id] using h
-
 theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) :
     (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
   cases l; simp [List.foldl_map]
@@ -2866,8 +3060,6 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
 
 /-! ### flatten -/
 
-@[simp] theorem flatten_empty : flatten (#[] : Array (Array α)) = #[] := rfl
-
 @[simp] theorem flatten_toArray_map_toArray (xss : List (List α)) :
     (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
   simp [flatten]
@@ -2878,12 +3070,48 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
   | nil => simp
   | cons xs xss ih => simp [ih]
 
+/-! ### sum -/
+
+theorem sum_eq_sum_toList [Add α] [Zero α] (as : Array α) : as.sum = as.toList.sum := by
+  cases as
+  simp [Array.sum, List.sum]
+
 /-! ### mkArray -/
 
+theorem eq_mkArray_of_mem {a : α} {l : Array α} (h : ∀ (b) (_ : b ∈ l), b = a) : l = mkArray l.size a := by
+  rcases l with ⟨l⟩
+  have := List.eq_replicate_of_mem (by simpa using h)
+  rw [this]
+  simp
+
+theorem eq_mkArray_iff {a : α} {n} {l : Array α} :
+    l = mkArray n a ↔ l.size = n ∧ ∀ (b) (_ : b ∈ l), b = a := by
+  rcases l with ⟨l⟩
+  simp [← List.eq_replicate_iff, toArray_eq]
+
+theorem map_eq_mkArray_iff {l : Array α} {f : α → β} {b : β} :
+    l.map f = mkArray l.size b ↔ ∀ x ∈ l, f x = b := by
+  simp [eq_mkArray_iff]
+
 @[simp] theorem mem_mkArray (a : α) (n : Nat) : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a := by
   rw [mkArray, mem_toArray]
   simp
 
+@[simp] theorem map_const (l : Array α) (b : β) : map (Function.const α b) l = mkArray l.size b :=
+  map_eq_mkArray_iff.mpr fun _ _ => rfl
+
+@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (mkArray ·.size x) := by
+  funext l
+  simp
+
+/-- Variant of `map_const` using a lambda rather than `Function.const`. -/
+-- This can not be a `@[simp]` lemma because it would fire on every `Array.map`.
+theorem map_const' (l : Array α) (b : β) : map (fun _ => b) l = mkArray l.size b :=
+  map_const l b
+
+@[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkArray n a).sum = n * a := by
+  simp [sum_eq_sum_toList, List.sum_replicate_nat]
+
 /-! ### reverse -/
 
 @[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by

src/Init/Data/List/Lemmas.lean

@@ -1076,9 +1076,31 @@ theorem forall_mem_map {f : α → β} {l : List α} {P : β → Prop} :
 
 @[deprecated forall_mem_map (since := "2024-07-25")] abbrev forall_mem_map_iff := @forall_mem_map
 
+@[simp] theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
+  constructor <;> exact fun _ => match l with | [] => rfl
+
+@[deprecated map_eq_nil_iff (since := "2024-09-05")] abbrev map_eq_nil := @map_eq_nil_iff
+
+theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] :=
+  map_eq_nil_iff.mp h
+
 @[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
   induction l <;> simp_all
 
+theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l' := by
+  induction l generalizing l' with
+  | nil => simp
+  | cons a l ih =>
+    simp only [map_cons]
+    cases l' with
+    | nil => simp
+    | cons a' l' =>
+      simp only [map_cons, cons.injEq, ih, and_congr_left_iff]
+      intro h
+      constructor
+      · apply w
+      · simp +contextual
+
 theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l :=
   map_inj_left.2 h
 
@@ -1087,14 +1109,6 @@ theorem map_inj : map f = map g ↔ f = g := by
   · intro h; ext a; replace h := congrFun h [a]; simpa using h
   · intro h; subst h; rfl
 
-@[simp] theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
-  constructor <;> exact fun _ => match l with | [] => rfl
-
-@[deprecated map_eq_nil_iff (since := "2024-09-05")] abbrev map_eq_nil := @map_eq_nil_iff
-
-theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] :=
-  map_eq_nil_iff.mp h
-
 theorem map_eq_cons_iff {f : α → β} {l : List α} :
     map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂ := by
   cases l
@@ -1884,7 +1898,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
 
 /-! ### flatten -/
 
-@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = (L.map length).sum := by
+@[simp] theorem length_flatten (L : List (List α)) : L.flatten.length = (L.map length).sum := by
   induction L with
   | nil => rfl
   | cons =>
@@ -1899,6 +1913,9 @@ theorem flatten_singleton (l : List α) : [l].flatten = l := by simp
 @[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = [] := by
   induction L <;> simp_all
 
+@[simp] theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by
+  rw [eq_comm, flatten_eq_nil_iff]
+
 theorem flatten_ne_nil_iff {xs : List (List α)} : xs.flatten ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by
   simp
 
@@ -1924,7 +1941,8 @@ theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun
 -- `getLast?_flatten` is proved later, after the `reverse` section.
 -- `head_flatten` and `getLast_flatten` are proved in `Init.Data.List.Find`.
 
-@[simp] theorem map_flatten (f : α → β) (L : List (List α)) : map f (flatten L) = flatten (map (map f) L) := by
+@[simp] theorem map_flatten (f : α → β) (L : List (List α)) :
+    (flatten L).map f = (map (map f) L).flatten := by
   induction L <;> simp_all
 
 @[simp] theorem filterMap_flatten (f : α → Option β) (L : List (List α)) :
@@ -1977,6 +1995,26 @@ theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
   · rintro ⟨as, bs, cs, rfl, h₁, rfl⟩
     simp [flatten_eq_nil_iff.mpr h₁]
 
+theorem cons_eq_flatten_iff {xs : List (List α)} {y : α} {ys : List α} :
+    y :: ys = xs.flatten ↔
+      ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.flatten := by
+  rw [eq_comm, flatten_eq_cons_iff]
+
+theorem flatten_eq_singleton_iff {xs : List (List α)} {y : α} :
+    xs.flatten = [y] ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l, l ∈ as → l = []) ∧ (∀ l, l ∈ bs → l = []) := by
+  rw [flatten_eq_cons_iff]
+  constructor
+  · rintro ⟨as, bs, cs, rfl, h₁, h₂⟩
+    simp at h₂
+    obtain ⟨rfl, h₂⟩ := h₂
+    exact ⟨as, cs, by simp, h₁, h₂⟩
+  · rintro ⟨as, bs, rfl, h₁, h₂⟩
+    exact ⟨as, [], bs, rfl, h₁, by simpa⟩
+
+theorem singleton_eq_flatten_iff {xs : List (List α)} {y : α} :
+    [y] = xs.flatten ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l, l ∈ as → l = []) ∧ (∀ l, l ∈ bs → l = []) := by
+  rw [eq_comm, flatten_eq_singleton_iff]
+
 theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
     xs.flatten = ys ++ zs ↔
       (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
@@ -2005,6 +2043,13 @@ theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
     · simp
     · simp
 
+theorem append_eq_flatten_iff {xs : List (List α)} {ys zs : List α} :
+    ys ++ zs = xs.flatten ↔
+      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
+        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧
+          zs = c :: cs ++ ds.flatten := by
+  rw [eq_comm, flatten_eq_append_iff]
+
 /-- Two lists of sublists are equal iff their flattens coincide, as well as the lengths of the
 sublists. -/
 theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
@@ -2027,6 +2072,8 @@ theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (
 
 @[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def]
 
+@[simp] theorem flatMap_id' (l : List (List α)) : List.flatMap l (fun a => a) = l.flatten := by simp [flatMap_def]
+
 @[simp]
 theorem length_flatMap (l : List α) (f : α → List β) :
     length (l.flatMap f) = sum (map (length ∘ f) l) := by
@@ -2348,6 +2395,9 @@ theorem replicateRecOn {α : Type _} {p : List α → Prop} (m : List α)
     exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)
 termination_by m.length
 
+@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by
+  induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm]
+
 /-! ### reverse -/
 
 @[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by

src/Init/Data/List/ToArray.lean

@@ -143,6 +143,9 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
   subst h
   rw [foldl_toList]
 
+@[simp] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
+  simp [Array.sum, List.sum]
+
 @[simp] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'
@@ -394,4 +397,24 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
 @[deprecated toArray_replicate (since := "2024-12-13")]
 abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
 
+@[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
+
+theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
+    (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
+  simp [Array.flatMap]
+  suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
+      f a ++ List.foldl (fun bs a => bs ++ f a) cs as by
+    erw [empty_append] -- Why doesn't this work via `simp`?
+    simpa using this #[]
+  intro cs
+  induction as generalizing cs <;> simp_all
+
+@[simp] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) :
+    as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    apply ext'
+    simp [ih, flatMap_toArray_cons]
+
 end List

src/Init/Data/Option/Lemmas.lean

@@ -208,6 +208,15 @@ theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘
 
 theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some' ..
 
+theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y → x = y) :
+    o.map f = o'.map f ↔ o = o' := by
+  cases o with
+  | none => cases o' <;> simp
+  | some a =>
+    cases o' with
+    | none => simp
+    | some a' => simpa using ⟨fun h => w _ _ h, fun h => congrArg f h⟩
+
 @[simp] theorem map_if {f : α → β} [Decidable c] :
      (if c then some a else none).map f = if c then some (f a) else none := by
   split <;> rfl
@@ -629,6 +638,15 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → a ∈ o → Option
     · rintro ⟨h, rfl⟩
       rfl
 
+@[simp]
+theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
+    @pmap _ _ p (fun a _ => f a) o H = Option.map f o := by
+  cases o <;> simp
+
+theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) :
+    Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H := by
+  cases o <;> simp
+
 /-! ### pelim -/
 
 @[simp] theorem pelim_none : pelim none b f = b := rfl

src/Init/Data/Vector/Basic.lean

@@ -170,6 +170,10 @@ result is empty. If `stop` is greater than the size of the vector, the size is u
 @[inline] def map (f : α → β) (v : Vector α n) : Vector β n :=
   ⟨v.toArray.map f, by simp⟩
 
+@[inline] def flatten (v : Vector (Vector α n) m) : Vector α (m * n) :=
+  ⟨(v.toArray.map Vector.toArray).flatten,
+    by rcases v; simp_all [Function.comp_def, Array.map_const']⟩
+
 /-- Maps corresponding elements of two vectors of equal size using the function `f`. -/
 @[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n :=
   ⟨Array.zipWith a.toArray b.toArray f, by simp⟩

src/Init/Data/Vector/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison
 -/
 prelude
 import Init.Data.Vector.Basic
+import Init.Data.Array.Attach
 
 /-!
 ## Vectors
@@ -27,6 +28,9 @@ namespace Vector
 
 theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
 
+@[simp] theorem mk_toArray (v : Vector α n) : mk v.toArray v.2 = v := by
+  rfl
+
 @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
     (Vector.mk data size)[i] = data[i] := rfl
 
@@ -1115,6 +1119,11 @@ theorem forall_mem_map {f : α → β} {l : Vector α n} {P : β → Prop} :
 @[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
   cases l <;> simp_all
 
+theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l' := by
+  cases l
+  cases l'
+  simp [Array.map_inj_right w]
+
 theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l :=
   map_inj_left.2 h
 
@@ -1185,6 +1194,40 @@ theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} :
   cases as
   simp
 
+/--
+Use this as `induction ass using vector₂_induction` on a hypothesis of the form `ass : Vector (Vector α n) m`.
+The hypothesis `ass` will be replaced with a hypothesis `ass : Array (Array α)`
+along with additional hypotheses `h₁ : ass.size = m` and `h₂ : ∀ xs ∈ ass, xs.size = n`.
+Appearances of the original `ass` in the goal will be replaced with
+`Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk xs ⋯)) ⋯`.
+-/
+-- We can't use `@[cases_eliminator]` here as
+-- `Lean.Meta.getCustomEliminator?` only looks at the top-level constant.
+theorem vector₂_induction (P : Vector (Vector α n) m → Prop)
+    (of : ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ xs ∈ xss, xs.size = n),
+      P (mk (xss.attach.map (fun ⟨xs, m⟩ => mk xs (h₂ xs m))) (by simpa using h₁)))
+    (ass : Vector (Vector α n) m) : P ass := by
+  specialize of (ass.map toArray).toArray (by simp) (by simp)
+  simpa [Array.map_attach, Array.pmap_map] using of
+
+/--
+Use this as `induction ass using vector₃_induction` on a hypothesis of the form `ass : Vector (Vector (Vector α n) m) k`.
+The hypothesis `ass` will be replaced with a hypothesis `ass : Array (Array (Array α))`
+along with additional hypotheses `h₁ : ass.size = k`, `h₂ : ∀ xs ∈ ass, xs.size = m`,
+and `h₃ : ∀ xs ∈ ass, ∀ x ∈ xs, x.size = n`.
+Appearances of the original `ass` in the goal will be replaced with
+`Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk (xs.attach.map (fun ⟨x, m'⟩ => Vector.mk x ⋯)) ⋯)) ⋯`.
+-/
+theorem vector₃_induction (P : Vector (Vector (Vector α n) m) k → Prop)
+    (of : ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ xs ∈ xss, xs.size = m)
+      (h₃ : ∀ xs ∈ xss, ∀ x ∈ xs, x.size = n),
+      P (mk (xss.attach.map (fun ⟨xs, m⟩ =>
+        mk (xs.attach.map (fun ⟨x, m'⟩ =>
+          mk x (h₃ xs m x m'))) (by simpa using h₂ xs m))) (by simpa using h₁)))
+    (ass : Vector (Vector (Vector α n) m) k) : P ass := by
+  specialize of (ass.map (fun as => (as.map toArray).toArray)).toArray (by simp) (by simp) (by simp)
+  simpa [Array.map_attach, Array.pmap_map] using of
+
 /-! ### singleton -/
 
 @[simp] theorem singleton_def (v : α) : Vector.singleton v = #v[v] := rfl
@@ -1240,7 +1283,7 @@ theorem empty_append (as : Vector α n) : (#v[] : Vector α 0) ++ as = as.cast (
   simp
 
 theorem append_empty (as : Vector α n) : as ++ (#v[] : Vector α 0) = as := by
-  rw [← toArray_inj, toArray_append, Array.append_nil]
+  rw [← toArray_inj, toArray_append, Array.append_empty]
 
 theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) :
     (a ++ b)[i] = if h : i < n then a[i] else b[i - n] := by
@@ -1406,6 +1449,82 @@ theorem append_eq_map_iff {f : α → β} :
     L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
   rw [eq_comm, map_eq_append_iff]
 
+/-! ### flatten -/
+
+@[simp] theorem flatten_mk (L : Array (Vector α n)) (h : L.size = m) :
+    (mk L h).flatten =
+      mk (L.map toArray).flatten (by simp [Function.comp_def, Array.map_const', h]) := by
+  simp [flatten]
+
+@[simp] theorem flatten_singleton (l : Vector α n) : #v[l].flatten = l.cast (by simp) := by
+  simp [flatten]
+
+theorem mem_flatten {L : Vector (Vector α n) m} : a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by
+  rcases L with ⟨L, rfl⟩
+  simp [Array.mem_flatten]
+  constructor
+  · rintro ⟨_, ⟨l, h₁, rfl⟩, h₂⟩
+    exact ⟨l, h₁, by simpa using h₂⟩
+  · rintro ⟨l, h₁, h₂⟩
+    exact ⟨l.toArray, ⟨l, h₁, rfl⟩, by simpa using h₂⟩
+
+theorem exists_of_mem_flatten : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := mem_flatten.1
+
+theorem mem_flatten_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ flatten L := mem_flatten.2 ⟨l, lL, al⟩
+
+theorem forall_mem_flatten {p : α → Prop} {L : Vector (Vector α n) m} :
+    (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x := by
+  simp only [mem_flatten, forall_exists_index, and_imp]
+  constructor <;> (intros; solve_by_elim)
+
+@[simp] theorem map_flatten (f : α → β) (L : Vector (Vector α n) m) :
+    (flatten L).map f = (map (map f) L).flatten := by
+  induction L using vector₂_induction with
+  | of xss h₁ h₂ => simp
+
+@[simp] theorem flatten_append (L₁ : Vector (Vector α n) m₁) (L₂ : Vector (Vector α n) m₂) :
+    flatten (L₁ ++ L₂) = (flatten L₁ ++ flatten L₂).cast (by simp [Nat.add_mul]) := by
+  induction L₁ using vector₂_induction
+  induction L₂ using vector₂_induction
+  simp
+
+theorem flatten_push (L : Vector (Vector α n) m) (l : Vector α n) :
+    flatten (L.push l) = (flatten L ++ l).cast (by simp [Nat.add_mul]) := by
+  induction L using vector₂_induction
+  rcases l with ⟨l⟩
+  simp [Array.flatten_push]
+
+theorem flatten_flatten {L : Vector (Vector (Vector α n) m) k} :
+    flatten (flatten L) = (flatten (map flatten L)).cast (by simp [Nat.mul_assoc]) := by
+  induction L using vector₃_induction with
+  | of xss h₁ h₂ h₃ =>
+    -- simp [Array.flatten_flatten] -- FIXME: `simp` produces a bad proof here!
+    simp [Array.map_attach, Array.flatten_flatten, Array.map_pmap]
+
+/-- Two vectors of constant length vectors are equal iff their flattens coincide. -/
+theorem eq_iff_flatten_eq {L L' : Vector (Vector α n) m} :
+    L = L' ↔ L.flatten = L'.flatten := by
+  induction L using vector₂_induction with | of L h₁ h₂ =>
+  induction L' using vector₂_induction with | of L' h₁' h₂' =>
+  simp only [eq_mk, flatten_mk, Array.map_map, Function.comp_apply, Array.map_subtype,
+    Array.unattach_attach, Array.map_id_fun', id_eq]
+  constructor
+  · intro h
+    suffices L = L' by simp_all
+    apply Array.ext_getElem?
+    intro i
+    replace h := congrArg (fun x => x[i]?.map (fun x => x.toArray)) h
+    simpa [Option.map_pmap] using h
+  · intro h
+    have w : L.map Array.size = L'.map Array.size := by
+      ext i h h'
+      · simp_all
+      · simp only [Array.getElem_map]
+        rw [h₂ _ (by simp), h₂' _ (by simp)]
+    have := Array.eq_iff_flatten_eq.mpr ⟨h, w⟩
+    subst this
+    rfl
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :

src/Lean/Meta/Tactic/Grind/Arith/Offset.lean

@@ -133,8 +133,6 @@ private def propagateTrue (u v : NodeId) (k : Int) (c : Cnstr NodeId) (e : Expr)
     return true
   return false
 
-example (x y : Nat) : x + 2 ≤ y → ¬ (y ≤ x + 1) := by omega
-
 /--
 Tries to assign `e` to `False`, which is represented by constraint `c` (from `v` to `u`), using the
 path `u --(k)--> v`.

tests/lean/guessLexFailures.lean

@@ -21,14 +21,14 @@ def noArguments : Nat := noArguments
 
 def noNonFixedArguments (n : Nat) : Nat := noNonFixedArguments n
 
-def Array.sum (xs : Array Nat) : Nat := xs.foldl (init := 0) Nat.add
+def Array.sum' (xs : Array Nat) : Nat := xs.foldl (init := 0) Nat.add
 
 namespace InterestingMatrix
 def f : (n m l : Nat) → Nat
   | n+1, m+1, l+1 => #[
       f (n+1) (m+1) (l+1),
       f (n+1) (m-1) (l),
-      f (n)   (m+1) (l) ].sum
+      f (n)   (m+1) (l) ].sum'
   | _, _, _ => 0
 decreasing_by decreasing_tactic
 end InterestingMatrix
@@ -38,7 +38,7 @@ def f : (n m : Nat) → (h : True) → Nat → Nat
   | n+1, m+1, h, l+1 => #[
       f (n+1) (m+1) h (l+1),
       f (n+1) (m-1) h (l),
-      f (n)   (m+1) h (l) ].sum
+      f (n)   (m+1) h (l) ].sum'
   | _, _, _, _ => 0
 decreasing_by decreasing_tactic
 end InterestingMatrixWithForbiddenArguments
@@ -49,7 +49,7 @@ def f (n m l : Nat) : Nat := match n, m, l with
   | n+1, m+1, l+1 => #[
       f (n+1) (m+1) (l+1),
       f (n+1) (m-1) (l),
-      f (n)   (m+1) (l) ].sum
+      f (n)   (m+1) (l) ].sum'
   | _, _, _ => 0
 decreasing_by decreasing_tactic
 end InterestingMatrixWithNames
@@ -60,21 +60,21 @@ mutual
     | n+1, m+1, l+1 => #[
         f fixed (n+1) (m+1) (l+1),
         f fixed (n+1) (m-1) (l),
-        g fixed (n)   (m+1) trivial (l)].sum
+        g fixed (n)   (m+1) trivial (l)].sum'
     | _, _, _ => 0
 
   def g (fixed n m : Nat) (H : True) (l : Nat) : Nat := match n, m, l with
     | n+1, m+1, l+1 => #[
         g fixed (m+1) (n+1) H (l+1),
         g fixed (m+1) (n-1) H (l),
-        h fixed (m)   (n+1)  ].sum
+        h fixed (m)   (n+1)  ].sum'
     | _, _, _ => 0
 
   def h (fixed : Nat) : (n m : Nat) -> Nat
     | n+1, m+1 => #[
         f fixed (n+1) (m+1) (n+1),
         h fixed (n+1) (m-1),
-        h fixed (n)   (m+1) ].sum
+        h fixed (n)   (m+1) ].sum'
     | _, _ => 0
 end
 end Mutual