theorem Array.sizeOf_head?_of_mem {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) : sizeOf a < sizeOf as

theorem Array.sizeOf_head?_of_tail {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) : sizeOf as' < sizeOf as

theorem Array.sizeOf_dropLast_cons {α : Type u_1} [SizeOf α] (a : α) (as : List α) : sizeOf (a :: as).dropLast < sizeOf (a :: as)

theorem Array.sizeOf_dropLast_non_empty {α : Type u_1} [SizeOf α] (as : List α) (h : 0 < as.length) : sizeOf as.dropLast < sizeOf as

theorem Array.sizeOf_pop_non_empty {α : Type u_1} [SizeOf α] (as : Array α) (h : 0 < as.toList.length) : sizeOf as.pop < sizeOf as

theorem Array.sizeOf_pop? {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.pop? = some (a, as')) : sizeOf as' < sizeOf as

theorem Array.size_one {α : Type u_1} (a : α) : #[a].size = 1

theorem Array.default_size_zero {α : Type u_1} (arr : Array α) (h : arr = default) : arr.size = 0

theorem Array.non_empty_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) : 0 < arr.size

theorem Array.pop?_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) : ∃ (arr' : Array α), arr.pop? = some (last, arr')

theorem Array.pop?_of_non_empty {α : Type u_1} (arr : Array α) (h : 0 < arr.size) : ∃ (arr' : Array α), ∃ (last : α), arr.pop? = some (last, arr')

theorem Array.last?_eq_getLast {α : Type u_1} {last : α} (a : Array α) (h1 : a.last? = some last) (h2 : a.toList ≠ []) : a.toList.getLast h2 = last

theorem Array.lt_of_pop?_eq_last? {α : Type u_1} {last : α} {arr' arr : Array α} (h : arr.pop? = some (last, arr')) : 0 < arr.toList.length

theorem Array.get_last_of_pop? {α : Type u_1} {last : α} {arr' arr : Array α} (h1 : arr.pop? = some (last, arr')) (h2 : arr.toList.length - 1 < arr.toList.length) : arr.toList.get ⟨arr.toList.length - 1, h2⟩ = last

theorem Array.concat_of_pop? {α : Type u_1} {last : α} {arr' arr : Array α} (h : arr.pop? = some (last, arr')) : arr.toList = arr'.toList ++ [last]

theorem Array.get_eq_get?_some {α : Type u_1} {i : Nat} {a : α} {as : Array α} (hlt : i < as.size) (h : a = as[i]) : as[i]? = some a

@[simp]

theorem Array.size_of_head?_lt {α : Type u_1} {a : α} (as : Array α) (h : as.toList.head? = some a) : 0 < as.size

theorem Array.unique.mem_of_mem_unqiue {α : Type u_1} {a : α} [DecidableEq α] [LE α] (as : Array α) : a ∈ as.unique → a ∈ as

@[simp]

theorem Array.mem_unique {α : Type u_1} {a : α} [DecidableEq α] [LE α] (as : Array α) : a ∈ as.unique ↔ a ∈ as

@[simp]

theorem Array.nodup_unique {α : Type u_1} [DecidableEq α] [LE α] [LT α] [Std.IsPreorder α] [Std.LawfulOrderLT α] [Std.Antisymm fun (x1 x2 : α) => x1 ≤ x2] (as : Array α) (h : List.Pairwise LE.le as.toList) : as.unique.toList.Nodup

@[simp]

theorem Array.mergeSort_toList_eq {α : Type u_1} (as bs : Array α) (le : α → α → Bool := by exact fun a b => a ≤ b) (h : bs = as.mergeSort le) : as.toList.mergeSort le = bs.toList

@[simp]

theorem Array.mem_mergeSort {α : Type u_1} {a : α} [LT α] (as : Array α) (le : α → α → Bool := by exact (· ≤ ·)) : a ∈ as.mergeSort le ↔ a ∈ as

theorem Array.minWith_spec {α : Type u_1} [ord : Ord α] [Std.TransOrd α] (as : Array α) (init : α) (f : α → α → α) (hf : (fun (min x : α) => if compare x min = Ordering.lt then x else min) = f) (lt_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (le_notLt : ∀ (a b : α), ¬a < b ↔ b ≤ a) : ⦃⌜True⌝⦄ foldlM f init as ⦃Std.Do.PostCond.noThrow fun (r : α) => ⌜r ≤ init ∧ ∀ (a : α), a ∈ as → r ≤ a⌝⦄

theorem Array.min_le_mem {α : Type u_1} {m : α} [ord : Ord α] [Std.TransOrd α] (xs : Array α) (h : xs.min? = some m) (lt_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (le_notLt : ∀ (a b : α), ¬a < b ↔ b ≤ a) (a : α) : a ∈ xs → m ≤ a

theorem Array.mem_le_max {α : Type u_1} {m : α} [ord : Ord α] [Std.TransOrd α] (xs : Array α) (h : xs.max? = some m) (lt_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (le_iff : ∀ (a b : α), ¬a < b ↔ b ≤ a) (a : α) : a ∈ xs → a ≤ m