Init.Data.Array.Lemmas

@[simp] theorem toList_inj {xs ys : Array α} : xs.toList = ys.toList ↔ xs = ys := by
  cases xs; cases ys; simp

@[simp] theorem toList_eq_nil_iff {xs : Array α} : xs.toList = [] ↔ xs = #[] := by
  cases xs <;> simp

@[simp] theorem mem_toList_iff {a : α} {xs : Array α} : a ∈ xs.toLista ∈ xs.toList ↔ a ∈ xs := by
  cases xs <;> simp

@[simp] theorem length_toList {xs : Array α} : xs.toList.length = xs.size := rfl

theorem toArray_eq : List.toArrayList.toArray as = xs ↔ as = xs.toList := by
  cases xs
  simp

@[simp] theorem empty_eq {xs : Array α} : #[]#[] = xs ↔ xs = #[] := by
  cases xs <;> simp

theorem size_empty : (#[] : Array α).size = 0 := rfl

@[simp] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl

@[deprecated emptyWithCapacity_eq (since := "2025-03-12")]
theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl

theorem ne_empty_of_size_eq_add_one (h : xs.size = n + 1) : xs ≠ #[] := by
  cases xs
  simpa using List.ne_nil_of_length_eq_add_one h

theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
  cases xs
  simpa using List.ne_nil_of_length_pos h

theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
  ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩

@[deprecated size_eq_zero_iff (since := "2025-02-24")]
abbrev size_eq_zero := @size_eq_zero_iff

theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size := by
  cases xs
  simp only [mem_toArray] at h
  simpa using List.length_pos_of_mem h

theorem exists_mem_of_size_pos {xs : Array α} (h : 0 < xs.size) : ∃ a, a ∈ xs := by
  cases xs
  simpa using List.exists_mem_of_length_pos h

theorem size_pos_iff_exists_mem {xs : Array α} : 0 < xs.size ↔ ∃ a, a ∈ xs :=
  ⟨exists_mem_of_size_pos, fun ⟨_, h⟩ => size_pos_of_mem h⟩

theorem exists_mem_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) : ∃ a, a ∈ xs := by
  cases xs
  simpa using List.exists_mem_of_length_eq_add_one h

theorem size_pos_iff {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
  Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero_iff)

@[deprecated size_pos_iff (since := "2025-02-24")]
abbrev size_pos := @size_pos_iff

theorem size_eq_one_iff {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
  cases xs
  simpa using List.length_eq_one_iff

@[deprecated size_eq_one_iff (since := "2025-02-24")]
abbrev size_eq_one := @size_eq_one_iff

@[simp] theorem getElem?_eq_none_iff {xs : Array α} : xs[i]?xs[i]? = none ↔ xs.size ≤ i := by
  by_cases h : i < xs.size
  · simp [getElem?_pos, h]
  · rw [getElem?_neg xs i h]
    simp_all

@[simp] theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : nonenone = xs[i]? ↔ xs.size ≤ i := by
  simp [eq_comm (a := none)]

theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by
  simp [getElem?_eq_none_iff, h]

@[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
  getElem?_pos ..

theorem getElem?_eq_some_iff {xs : Array α} : xs[i]?xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b := by
  simp [getElem?_def]

theorem some_eq_getElem?_iff {xs : Array α} : somesome b = xs[i]? ↔ ∃ h : i < xs.size, xs[i] = b := by
  rw [eq_comm, getElem?_eq_some_iff]

@[simp] theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
    (some xs[i] = xs[i]?) ↔ True := by
  simp [h]

@[simp] theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
    (xs[i]? = some xs[i]) ↔ True := by
  simp [h]

theorem getElem_eq_iff {xs : Array α} {i : Nat} {h : i < xs.size} : xs[i]xs[i] = x ↔ xs[i]? = some x := by
  simp only [getElem?_eq_some_iff]
  exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩

theorem getElem_eq_getElem?_get {xs : Array α} {i : Nat} (h : i < xs.size) :
    xs[i] = xs[i]?.get (by simp [getElem?_eq_getElem, h]) := by
  simp [getElem_eq_iff]

theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
    xs[i]?.getD d = if p : i < xs.size then xs[i]'p else d := by
  if h : i < xs.size then
    simp [h, getElem?_def]
  else
    have p : i ≥ xs.size := Nat.le_of_not_gt h
    simp [getElem?_eq_none p, h]

@[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl

theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
    have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
    (xs.push x)[i] = xs[i] := by
  simp only [push, ← getElem_toList, List.concat_eq_append, List.getElem_append_left, h]

@[simp] theorem getElem_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size] = x := by
  simp only [push, ← getElem_toList, List.concat_eq_append]
  rw [List.getElem_append_right] <;> simp [← getElem_toList, Nat.zero_lt_one]

theorem getElem_push {xs : Array α} {x : α} {i : Nat} (h : i < (xs.push x).size) :
    (xs.push x)[i] = if h : i < xs.size then xs[i] else x := by
  by_cases h' : i < xs.size
  · simp [getElem_push_lt, h']
  · simp at h
    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]

theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]? := by
  simp [getElem?_def, getElem_push]
  (repeat' split) <;> first | rfl | omega

@[simp] theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
  simp [getElem?_push]

@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a]#[a][i] = a :=
  match i, h with
  | 0, _ => rfl

theorem getElem?_singleton {a : α} {i : Nat} : #[a]#[a][i]? = if i = 0 then some a else none := by
  simp [List.getElem?_singleton]

theorem ext_getElem? {xs ys : Array α} (h : ∀ i : Nat, xs[i]? = ys[i]?) : xs = ys := by
  rcases xs with ⟨xs⟩
  rcases ys with ⟨ys⟩
  simpa using List.ext_getElem? (by simpa using h)

@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl

@[simp] theorem pop_push {xs : Array α} {x : α} : (xs.push x).pop = xs := by simp [pop]

@[simp] theorem getElem_pop {xs : Array α} {i : Nat} (h : i < xs.pop.size) :
    xs.pop[i] = xs[i]'(by simp at h; omega) := by
  rcases xs with ⟨xs⟩
  simp [List.getElem_dropLast]

theorem getElem?_pop {xs : Array α} {i : Nat} :
    xs.pop[i]? = if i < xs.size - 1 then xs[i]? else none := by
  rcases xs with ⟨xs⟩
  simp [List.getElem?_dropLast]

theorem back_pop {xs : Array α} (h) :
   xs.pop.back h =
     xs[xs.size - 2]'(by simp at h; omega) := by
  rcases xs with ⟨xs⟩
  simp [List.getLast_dropLast]

theorem back?_pop {xs : Array α} :
    xs.pop.back? = if xs.size ≤ 1 then none else xs[xs.size - 2]? := by
  rcases xs with ⟨xs⟩
  simp [List.getLast?_dropLast]

@[simp] theorem pop_append_of_ne_empty {xs : Array α} {ys : Array α} (h : ys ≠ #[]) :
    (xs ++ ys).pop = xs ++ ys.pop := by
  rcases xs with ⟨xs⟩
  rcases ys with ⟨ys⟩
  simp only [List.append_toArray, List.pop_toArray, mk.injEq]
  rw [List.dropLast_append_of_ne_nil (by simpa using h)]

@[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by
  cases xs
  simp

@[simp] theorem push_ne_self {a : α} {xs : Array α} : xs.push a ≠ xs := by
  cases xs
  simp

@[simp] theorem ne_push_self {a : α} {xs : Array α} : xs ≠ xs.push a := by
  rw [ne_eq, eq_comm]
  simp

theorem back_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : a = b := by
  cases xs
  cases ys
  simp only [List.push_toArray, mk.injEq] at h
  replace h := List.append_inj_right' h (by simp)
  simpa using h

theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys := by
  cases xs
  cases ys
  simp at h
  replace h := List.append_inj_left' h (by simp)
  simp [h]

theorem push_inj_left {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs = ys :=
  ⟨pop_eq_of_push_eq, fun h => by simp [h]⟩

theorem push_inj_right {a b : α} {xs : Array α} : xs.push a = xs.push b ↔ a = b :=
  ⟨back_eq_of_push_eq, fun h => by simp [h]⟩

theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
  constructor
  · intro h
    exact ⟨back_eq_of_push_eq h, pop_eq_of_push_eq h⟩
  · rintro ⟨rfl, rfl⟩
    rfl

theorem push_eq_append_singleton {as : Array α} {x : α} : as.push x = as ++ #[x] := rfl

theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
    ∃ (ys : Array α) (a : α), xs = ys.push a := by
  rcases xs with ⟨xs⟩
  simp only [ne_eq, mk.injEq] at h
  exact ⟨(xs.take (xs.length - 1)).toArray, xs.getLast h, by simp⟩

theorem ne_empty_iff_exists_push {xs : Array α} :
    xs ≠ #[]xs ≠ #[] ↔ ∃ (ys : Array α) (a : α), xs = ys.push a :=
  ⟨exists_push_of_ne_empty, fun ⟨_, _, eq⟩ => eq.symm ▸ push_ne_empty⟩

theorem exists_push_of_size_pos {xs : Array α} (h : 0 < xs.size) :
    ∃ (ys : Array α) (a : α), xs = ys.push a := by
  replace h : xs ≠ #[] := size_pos_iff.mp h
  exact exists_push_of_ne_empty h

theorem size_pos_iff_exists_push {xs : Array α} :
    0 < xs.size ↔ ∃ (ys : Array α) (a : α), xs = ys.push a :=
  ⟨exists_push_of_size_pos, fun ⟨_, _, eq⟩ => by simp [eq]⟩

theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
    ∃ (ys : Array α) (a : α), xs = ys.push a :=
  exists_push_of_size_pos (by simp [h])

theorem singleton_inj : #[a]#[a] = #[b] ↔ a = b := by
  simp

@[simp] theorem size_replicate {n : Nat} {v : α} : (replicate n v).size = n :=
  List.length_replicate ..

@[deprecated size_replicate (since := "2025-03-18")]
abbrev size_mkArray := @size_replicate

@[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by
  simp only [replicate]

@[deprecated toList_replicate (since := "2025-03-18")]
abbrev toList_mkArray := @toList_replicate

@[simp] theorem replicate_zero : replicate 0 a = #[] := rfl

@[deprecated replicate_zero (since := "2025-03-18")]
abbrev mkArray_zero := @replicate_zero

theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
  apply toList_inj.1
  simp [List.replicate_succ']

@[deprecated replicate_succ (since := "2025-03-18")]
abbrev mkArray_succ := @replicate_succ

@[simp] theorem getElem_replicate {n : Nat} {v : α} {i : Nat} (h : i < (replicate n v).size) :
    (replicate n v)[i] = v := by simp [← getElem_toList]

@[deprecated getElem_replicate (since := "2025-03-18")]
abbrev getElem_mkArray := @getElem_replicate

@[simp] theorem getElem?_replicate {n : Nat} {v : α} {i : Nat} :
    (replicate n v)[i]? = if i < n then some v else none := by
  simp [getElem?_def]

@[deprecated getElem?_replicate (since := "2025-03-18")]
abbrev getElem?_mkArray := @getElem?_replicate

theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp

@[simp] theorem mem_push {xs : Array α} {x y : α} : x ∈ xs.push yx ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
  simp only [mem_def]
  simp

theorem mem_push_self {xs : Array α} {x : α} : x ∈ xs.push x :=
  mem_push.2 (Or.inr rfl)

theorem mem_push_of_mem {xs : Array α} {x : α} (y : α) (h : x ∈ xs) : x ∈ xs.push y :=
  mem_push.2 (Or.inl h)

theorem exists_mem_of_ne_empty (xs : Array α) (h : xs ≠ #[]) : ∃ x, x ∈ xs := by
  simpa using List.exists_mem_of_ne_nil xs.toList (by simpa using h)

@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {xs : ¬ p → Array α} :
    (x ∈ if h : p then #[] else xs h) ↔ ∃ h : ¬ p, x ∈ xs h := by
  split <;> simp_all

@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {xs : p → Array α} :
    (x ∈ if h : p then xs h else #[]) ↔ ∃ h : p, x ∈ xs h := by
  split <;> simp_all

@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {xs : Array α} :
    (x ∈ if p then #[] else xs) ↔ ¬ p ∧ x ∈ xs := by
  split <;> simp_all

@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {xs : Array α} :
    (x ∈ if p then xs else #[]) ↔ p ∧ x ∈ xs := by
  split <;> simp_all

@[simp] theorem mem_singleton {a b : α} : a ∈ #[b]a ∈ #[b] ↔ a = b :=
  ⟨eq_of_mem_singleton, (by simp [·])⟩

theorem forall_mem_push {p : α → Prop} {xs : Array α} {a : α} :
    (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by
  cases xs
  simp [or_comm, forall_eq_or_imp]

theorem forall_mem_ne {a : α} {xs : Array α} : (∀ a' : α, a' ∈ xs → ¬a = a') ↔ a ∉ xs :=
  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩

theorem forall_mem_ne' {a : α} {xs : Array α} : (∀ a' : α, a' ∈ xs → ¬a' = a) ↔ a ∉ xs :=
  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩

theorem exists_mem_empty (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ #[], p x) := nofun

theorem forall_mem_empty (p : α → Prop) : ∀ (x) (_ : x ∈ #[]), p x := nofun

theorem exists_mem_push {p : α → Prop} {a : α} {xs : Array α} :
    (∃ x, ∃ _ : x ∈ xs.push a, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ xs, p x := by
  simp only [mem_push, exists_prop]
  constructor
  · rintro ⟨x, (h | rfl), h'⟩
    · exact .inr ⟨x, h, h'⟩
    · exact .inl h'
  · rintro (h | ⟨x, h, h'⟩)
    · exact ⟨a, by simp, h⟩
    · exact ⟨x, .inl h, h'⟩

theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ (x) (_ : x ∈ #[a]), p x) ↔ p a := by
  simp only [mem_singleton, forall_eq]

theorem mem_empty_iff (a : α) : a ∈ (#[] : Array α)a ∈ (#[] : Array α) ↔ False := by simp

theorem mem_singleton_self (a : α) : a ∈ #[a] := by simp

theorem mem_of_mem_push_of_mem {a b : α} {xs : Array α} : a ∈ xs.push b → b ∈ xs → a ∈ xs := by
  cases xs
  simp only [List.push_toArray, mem_toArray, List.mem_append, List.mem_singleton]
  rintro (h | rfl)
  · intro _
    exact h
  · exact id

theorem ne_empty_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : xs ≠ #[] := by
  cases xs
  simp [List.ne_nil_of_mem (by simpa using h)]

theorem mem_of_ne_of_mem {a y : α} {xs : Array α} (h₁ : a ≠ y) (h₂ : a ∈ xs.push y) : a ∈ xs := by
  simpa [h₁] using h₂

theorem ne_of_not_mem_push {a b : α} {xs : Array α} (h : a ∉ xs.push b) : a ≠ b := by
  simp only [mem_push, not_or] at h
  exact h.2

theorem not_mem_of_not_mem_push {a b : α} {xs : Array α} (h : a ∉ xs.push b) : a ∉ xs := by
  simp only [mem_push, not_or] at h
  exact h.1

theorem not_mem_push_of_ne_of_not_mem {a y : α} {xs : Array α} : a ≠ y → a ∉ xs → a ∉ xs.push y :=
  mtmt ∘ mem_of_ne_of_mem

theorem ne_and_not_mem_of_not_mem_push {a y : α} {xs : Array α} : a ∉ xs.push y → a ≠ ya ≠ y ∧ a ∉ xs := by
  simp +contextual

theorem getElem_of_mem {a} {xs : Array α} (h : a ∈ xs) : ∃ (i : Nat) (h : i < xs.size), xs[i]'h = a := by
  cases xs
  simp [List.getElem_of_mem (by simpa using h)]

theorem getElem?_of_mem {a} {xs : Array α} (h : a ∈ xs) : ∃ i : Nat, xs[i]? = some a :=
  let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩

theorem mem_of_getElem {xs : Array α} {i : Nat} {h} {a : α} (e : xs[i] = a) : a ∈ xs := by
  subst e
  simp

theorem mem_of_getElem? {xs : Array α} {i : Nat} {a : α} (e : xs[i]? = some a) : a ∈ xs :=
  let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..

theorem mem_iff_getElem {a} {xs : Array α} : a ∈ xsa ∈ xs ↔ ∃ (i : Nat) (h : i < xs.size), xs[i]'h = a :=
  ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩

theorem mem_iff_getElem? {a} {xs : Array α} : a ∈ xsa ∈ xs ↔ ∃ i : Nat, xs[i]? = some a := by
  simp [getElem?_eq_some_iff, mem_iff_getElem]

theorem forall_getElem {xs : Array α} {p : α → Prop} :
    (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a := by
  cases xs; simp [List.forall_getElem]

@[simp] theorem isEmpty_toList {xs : Array α} : xs.toList.isEmpty = xs.isEmpty := by
  rcases xs with ⟨_ | _⟩ <;> simp

theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
    xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
  cases xs
  simpa using List.isEmpty_eq_false_iff_exists_mem

@[simp] theorem isEmpty_iff {xs : Array α} : xs.isEmpty ↔ xs = #[] := by
  cases xs <;> simp

@[deprecated isEmpty_iff (since := "2025-02-17")]
abbrev isEmpty_eq_true := @isEmpty_iff

@[simp] theorem isEmpty_eq_false_iff {xs : Array α} : xs.isEmpty = false ↔ xs ≠ #[] := by
  cases xs <;> simp

@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
abbrev isEmpty_eq_false := @isEmpty_eq_false_iff

theorem isEmpty_iff_size_eq_zero {xs : Array α} : xs.isEmpty ↔ xs.size = 0 := by
  rw [isEmpty_iff, size_eq_zero_iff]

instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
    Decidable (∀ x, x ∈ xs → p x) :=
  decidable_of_iff (∀ (i : Nat) h, p (xs[i]'h)) (by
    simp only [mem_iff_getElem, forall_exists_index]
    exact
      ⟨by rintro w _ i h rfl; exact w i h, fun w i h => w _ i h rfl⟩)

instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
    Decidable (∃ x, x ∈ xs ∧ p x) :=
  decidable_of_iff (∃ (i : Nat), ∃ (h : i < xs.size), p (xs[i]'h)) (by
    simp [mem_iff_getElem]
    exact
      ⟨by rintro ⟨i, h, w⟩; exact ⟨_, ⟨i, h, rfl⟩, w⟩, fun ⟨_, ⟨i, h, rfl⟩, w⟩ => ⟨i, h, w⟩⟩)

theorem anyM_eq_anyM_loop [Monad m] {p : α → m Bool} {as : Array α} {start stop} :
    anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
  simp only [anyM, Nat.min_def]; split <;> rfl

theorem anyM_stop_le_start [Monad m] {p : α → m Bool} {as : Array α} {start stop}
    (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
  rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]

theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {stop start : Nat}
    (h : stop + 1 ≤ (a :: as).length) :
    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) =
      anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
  rw [anyM.loop]
  conv => rhs; rw [anyM.loop]
  split <;> rename_i h'
  · simp only [Nat.add_lt_add_iff_right] at h'
    rw [dif_pos h', anyM_loop_cons]
    simp
  · rw [dif_neg]
    omega

@[simp] theorem anyM_toList [Monad m] {p : α → m Bool} {as : Array α} :
    as.toList.anyM p = as.anyM p :=
  match as with
  | ⟨[]⟩  => by simp [anyM, anyM.loop]
  | ⟨a :: as⟩ => by
    simp only [List.anyM, anyM, List.size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
    rw [anyM.loop, dif_pos (by omega)]
    congr 1
    funext b
    split
    · simp
    · simp only [Bool.false_eq_true, ↓reduceIte]
      rw [anyM_loop_cons]
      simpa [anyM] using anyM_toList

theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
    anyM.loopanyM.loop (m := Id) p as stop h start = true ↔
      ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true := by
  unfold anyM.loop
  split <;> rename_i h₁
  · dsimp
    split <;> rename_i h₂
    · simp only [true_iff]
      refine ⟨start, by omega, by omega, by omega, h₂⟩
    · rw [anyM_loop_iff_exists]
      constructor
      · rintro ⟨i, hi, ge, lt, h⟩
        have : start ≠ i := by rintro rfl; omega
        exact ⟨i, by omega, by omega, lt, h⟩
      · rintro ⟨i, hi, ge, lt, h⟩
        have : start ≠ i := by rintro rfl; erw [h] at h₂; simp_all
        exact ⟨i, by omega, by omega, lt, h⟩
  · simp
    omega
termination_by stop - start

theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
    as.any p start stop ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] := by
  dsimp [any, anyM, Id.run]
  split
  · rw [anyM_loop_iff_exists]
  · rw [anyM_loop_iff_exists]
    constructor
    · rintro ⟨i, hi, ge, _, h⟩
      exact ⟨i, by omega, by omega, by omega, h⟩
    · rintro ⟨i, hi, ge, _, h⟩
      exact ⟨i, by omega, by omega, by omega, h⟩

@[simp] theorem any_eq_true {p : α → Bool} {as : Array α} :
    as.any p = true ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
  simp [any_iff_exists]

@[simp] theorem any_eq_false {p : α → Bool} {as : Array α} :
    as.any p = false ↔ ∀ (i : Nat) (_ : i < as.size), ¬p as[i] := by
  rw [Bool.eq_false_iff, Ne, any_eq_true]
  simp

@[simp] 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_getElem, getElem_toList]
  exact ⟨fun ⟨_, ⟨i, w, rfl⟩, h⟩ => ⟨i, w, h⟩, fun ⟨i, w, h⟩ => ⟨_, ⟨i, w, rfl⟩, h⟩⟩

theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} :
    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
  dsimp [allM, anyM]
  simp

@[simp] theorem allM_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} :
    as.toList.allM p = as.allM p := by
  rw [allM_eq_not_anyM_not]
  rw [← anyM_toList]
  rw [List.allM_eq_not_anyM_not]

theorem all_eq_not_any_not {p : α → Bool} {as : Array α} {start stop} :
    as.all p start stop = !(as.any (!p ·) start stop) := by
  dsimp [all, allM]
  rfl

theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
    as.all p start stop ↔ ∀ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop → p as[i] := by
  rw [all_eq_not_any_not]
  suffices ¬(as.any (!p ·) start stop = true)¬(as.any (!p ·) start stop = true) ↔
      ∀ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop → p as[i] by
    simp_all
  simp only [any_iff_exists, Bool.not_eq_eq_eq_not, Bool.not_true, not_exists, not_and,
    Bool.not_eq_false, and_imp]

@[simp] theorem all_eq_true {p : α → Bool} {as : Array α} :
    as.all p = true ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
  simp [all_iff_forall]

@[simp] theorem all_eq_false {p : α → Bool} {as : Array α} :
    as.all p = false ↔ ∃ (i : Nat) (_ : i < as.size), ¬p as[i] := by
  rw [Bool.eq_false_iff, Ne, all_eq_true]
  simp

@[simp] 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, getElem_toList]
  constructor
  · intro w i h
    exact w as[i] ⟨i, h, getElem_toList h⟩
  · rintro w x ⟨i, h, rfl⟩
    exact w i h

theorem all_eq_true_iff_forall_mem {xs : Array α} : xs.all p ↔ ∀ x, x ∈ xs → p x := by
  simp only [← all_toList, List.all_eq_true, mem_def]

/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
@[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} {stop}
    (h : stop = l.toArray.size) :
    l.toArray.anyM p 0 stop = l.anyM p := by
  subst h
  rw [← anyM_toList]

/-- Variant of `any_toArray` with a side condition on `stop`. -/
@[simp] theorem _root_.List.any_toArray' {p : α → Bool} {l : List α} {stop}
    (h : stop = l.toArray.size) :
    l.toArray.any p 0 stop = l.any p := by
  subst h
  rw [any_toList]

/-- Variant of `allM_toArray` with a side condition on `stop`. -/
@[simp] theorem _root_.List.allM_toArray' [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} {stop}
    (h : stop = l.toArray.size) :
    l.toArray.allM p 0 stop = l.allM p := by
  subst h
  rw [← allM_toList]

/-- Variant of `all_toArray` with a side condition on `stop`. -/
@[simp] theorem _root_.List.all_toArray' {p : α → Bool} {l : List α} {stop}
    (h : stop = l.toArray.size) :
    l.toArray.all p 0 stop = l.all p := by
  subst h
  rw [all_toList]

theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} :
    l.toArray.anyM p = l.anyM p := by
  rw [← anyM_toList]

theorem _root_.List.any_toArray {p : α → Bool} {l : List α} : l.toArray.any p = l.any p := by
  rw [any_toList]

theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} :
    l.toArray.allM p = l.allM p := by
  rw [← allM_toList]

theorem _root_.List.all_toArray {p : α → Bool} {l : List α} : l.toArray.all p = l.all p := by
  rw [all_toList]

/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
theorem any_eq_true' {p : α → Bool} {as : Array α} :
    as.any p = true ↔ (∃ x, x ∈ as ∧ p x) := by
  cases as
  simp

/-- Variant of `any_eq_false` in terms of membership rather than an array index. -/
theorem any_eq_false' {p : α → Bool} {as : Array α} :
    as.any p = false ↔ ∀ x, x ∈ as → ¬p x := by
  rw [Bool.eq_false_iff, Ne, any_eq_true']
  simp

/-- Variant of `all_eq_true` in terms of membership rather than an array index. -/
theorem all_eq_true' {p : α → Bool} {as : Array α} :
    as.all p = true ↔ (∀ x, x ∈ as → p x) := by
  cases as
  simp

/-- Variant of `all_eq_false` in terms of membership rather than an array index. -/
theorem all_eq_false' {p : α → Bool} {as : Array α} :
    as.all p = false ↔ ∃ x, x ∈ as ∧ ¬p x := by
  rw [Bool.eq_false_iff, Ne, all_eq_true']
  simp

theorem any_eq {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
  by_cases h : xs.any p
  · simp_all [any_eq_true]
  · simp_all [any_eq_false]

/-- Variant of `any_eq` in terms of membership rather than an array index. -/
theorem any_eq' {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x) := by
  by_cases h : xs.any p
  · simp_all [any_eq_true', -any_eq_true]
  · simp only [Bool.not_eq_true] at h
    simp only [h]
    simp only [any_eq_false'] at h
    simpa using h

theorem all_eq {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < xs.size) → p xs[i]) := by
  by_cases h : xs.all p
  · simp_all [all_eq_true]
  · simp only [Bool.not_eq_true] at h
    simp only [h]
    simp only [all_eq_false] at h
    simpa using h

/-- Variant of `all_eq` in terms of membership rather than an array index. -/
theorem all_eq' {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x) := by
  by_cases h : xs.all p
  · simp_all [all_eq_true', -all_eq_true]
  · simp only [Bool.not_eq_true] at h
    simp only [h]
    simp only [all_eq_false'] at h
    simpa using h

theorem decide_exists_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
    decide (∃ x, x ∈ xs ∧ p x) = xs.any p := by
  simp [any_eq']

theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
    decide (∀ x, x ∈ xs → p x) = xs.all p := by
  simp [all_eq']

@[simp] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
    l.toArray.contains a = l.contains a := by
  simp [Array.contains, List.any_beq]

theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
    Array.elem a l.toArray = List.elem a l := by
  simp [Array.elem]

theorem any_beq [BEq α] {xs : Array α} {a : α} : (xs.any fun x => a == x) = xs.contains a := by
  cases xs
  simp [List.any_beq]

/-- Variant of `any_beq` with `==` reversed. -/
theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Array α} :
    (xs.any fun x => x == a) = xs.contains a := by
  simp only [BEq.comm, any_beq]

theorem all_bne [BEq α] {xs : Array α} : (xs.all fun x => a != x) = !xs.contains a := by
  cases xs
  simp [List.all_bne]

/-- Variant of `all_bne` with `!=` reversed. -/
theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
    (xs.all fun x => x != a) = !xs.contains a := by
  simp only [bne_comm, all_bne]

theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : as.contains a = true → a ∈ as := by
  cases as
  simp

@[deprecated mem_of_contains_eq_true (since := "2024-12-12")]
abbrev mem_of_elem_eq_true := @mem_of_contains_eq_true

theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
  cases as
  simpa using h

@[deprecated contains_eq_true_of_mem (since := "2024-12-12")]
abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem

instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
  decidable_of_decidable_of_iff (Iff.intro mem_of_contains_eq_true contains_eq_true_of_mem)

@[simp] theorem elem_eq_contains [BEq α] {a : α} {xs : Array α} :
    elem a xs = xs.contains a := by
  simp [elem]

theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
    elemelem a xs = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩

theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
    xs.contains a = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩

theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
    elem a xs = decide (a ∈ xs) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]

@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
    xs.contains a = decide (a ∈ xs) := by rw [← elem_eq_contains, elem_eq_mem]

/-- Variant of `any_push` with a side condition on `stop`. -/
@[simp] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
    (xs.push a).any p 0 stop = (xs.any p || p a) := by
  cases xs
  rw [List.push_toArray]
  simp [h]

theorem any_push [BEq α] {xs : Array α} {a : α} {p : α → Bool} :
    (xs.push a).any p = (xs.any p || p a) :=
  any_push' (by simp)

/-- Variant of `all_push` with a side condition on `stop`. -/
@[simp] theorem all_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
    (xs.push a).all p 0 stop = (xs.all p && p a) := by
  cases xs
  rw [List.push_toArray]
  simp [h]

theorem all_push [BEq α] {xs : Array α} {a : α} {p : α → Bool} :
    (xs.push a).all p = (xs.all p && p a) :=
  all_push' (by simp)

@[simp] theorem contains_push [BEq α] {xs : Array α} {a : α} {b : α} :
    (xs.push a).contains b = (xs.contains b || b == a) := by
  simp [contains]

@[simp] theorem getElem_set_self {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} :
    (xs.set i v)[i]'(by simp [h]) = v := by
  cases xs
  simp

@[deprecated getElem_set_self (since := "2024-12-11")]
abbrev getElem_set_eq := @getElem_set_self

@[simp] theorem getElem?_set_self {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} :
    (xs.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]

@[deprecated getElem?_set_self (since := "2024-12-11")]
abbrev getElem?_set_eq := @getElem?_set_self

@[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
    (pj : j < xs.size) (h : i ≠ j) :
    (xs.set i v)[j]'(by simp [*]) = xs[j] := by
  simp only [set, ← getElem_toList, List.getElem_set_ne h]

@[simp] theorem getElem?_set_ne {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat}
    (ne : i ≠ j) : (xs.set i v)[j]? = xs[j]? := by
  by_cases h : j < xs.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]

theorem getElem_set {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
    (h : j < (xs.set i v).size) :
    (xs.set i v)[j] = if i = j then v else xs[j]'(by simpa using h) := by
  simp at h
  by_cases p : i = j <;> simp [p, h]

theorem getElem?_set {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat} :
    (xs.set i v)[j]? = if i = j then some v else xs[j]? := by
  split <;> simp_all

@[simp] theorem set_getElem_self {xs : Array α} {i : Nat} (h : i < xs.size) :
    xs.set i xs[i] = xs := by
  cases xs
  simp

@[simp] theorem set_eq_empty_iff {xs : Array α} {i : Nat} {a : α} {h : i < xs.size} :
    xs.set i a = #[] ↔ xs = #[] := by
  cases xs <;> cases i <;> simp [set]

theorem set_comm (a b : α)
    {i j : Nat} {xs : Array α} {hi : i < xs.size} {hj : j < (xs.set i a).size} (h : i ≠ j) :
    (xs.set i a).set j b = (xs.set j b (by simpa using hj)).set i a (by simpa using hi) := by
  cases xs
  simp [List.set_comm _ _ h]

@[simp]
theorem set_set (a : α) {b : α} {xs : Array α} {i : Nat} (h : i < xs.size) :
    (xs.set i a).set i b (by simpa using h) = xs.set i b := by
  cases xs
  simp

theorem mem_set {xs : Array α} {i : Nat} (h : i < xs.size) {a : α} :
    a ∈ xs.set i a := by
  simp [mem_iff_getElem]
  exact ⟨i, (by simpa using h), by simp⟩

theorem mem_or_eq_of_mem_set
    {xs : Array α} {i : Nat} {a b : α} {w : i < xs.size} (h : a ∈ xs.set i b) : a ∈ xsa ∈ xs ∨ a = b := by
  cases xs
  simpa using List.mem_or_eq_of_mem_set (by simpa using h)

@[simp] theorem set!_eq_setIfInBounds : @set! = @setIfInBounds := rfl

@[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds

@[simp] theorem size_setIfInBounds {xs : Array α} {i : Nat} {a : α} :
    (xs.setIfInBounds i a).size = xs.size := by
  if h : i < xs.size  then
    simp [setIfInBounds, h]
  else
    simp [setIfInBounds, h]

theorem getElem_setIfInBounds {xs : Array α} {i : Nat} {a : α} {j : Nat}
    (hj : j < xs.size) :
    (xs.setIfInBounds i a)[j]'(by simp [hj]) = if i = j then a else xs[j] := by
  simp only [setIfInBounds]
  split
  · simp [getElem_set]
  · rw [if_neg]
    omega

@[simp] theorem getElem_setIfInBounds_self {xs : Array α} {i : Nat} {a : α} (h : i < (xs.setIfInBounds i a).size) :
    (xs.setIfInBounds i a)[i]'h = a := by
  simp at h
  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]

@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self

@[simp] theorem getElem_setIfInBounds_ne {xs : Array α} {i : Nat} {a : α} {j : Nat}
    (hj : j < xs.size) (h : i ≠ j) :
    (xs.setIfInBounds i a)[j]'(by simpa using hj) = xs[j] := by
  simp [getElem_setIfInBounds, hj, h]

theorem getElem?_setIfInBounds {xs : Array α} {i j : Nat} {a : α}  :
    (xs.setIfInBounds i a)[j]? = if i = j then if i < xs.size then some a else none else xs[j]? := by
  cases xs
  simp [List.getElem?_set]

theorem getElem?_setIfInBounds_self {xs : Array α} {i : Nat} {a : α} :
    (xs.setIfInBounds i a)[i]? = if i < xs.size then some a else none := by
  simp [getElem?_setIfInBounds]

@[simp]
theorem getElem?_setIfInBounds_self_of_lt {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
    (xs.setIfInBounds i a)[i]? = some a := by
  simp [getElem?_setIfInBounds, h]

@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self

@[simp] theorem getElem?_setIfInBounds_ne {xs : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
    (xs.setIfInBounds i a)[j]? = xs[j]? := by
  simp [getElem?_setIfInBounds, h]

theorem setIfInBounds_eq_of_size_le {xs : Array α} {i : Nat} (h : xs.size ≤ i) {a : α} :
    xs.setIfInBounds i a = xs := by
  cases xs
  simp [List.set_eq_of_length_le (by simpa using h)]

@[simp] theorem setIfInBounds_eq_empty_iff {xs : Array α} {i : Nat} {a : α} :
    xs.setIfInBounds i a = #[] ↔ xs = #[] := by
  cases xs <;> cases i <;> simp

theorem setIfInBounds_comm (a b : α)
    {i j : Nat} {xs : Array α} (h : i ≠ j) :
    (xs.setIfInBounds i a).setIfInBounds j b = (xs.setIfInBounds j b).setIfInBounds i a := by
  cases xs
  simp [List.set_comm _ _ h]

@[simp]
theorem setIfInBounds_setIfInBounds (a : α) {b : α} {xs : Array α} {i : Nat} :
    (xs.setIfInBounds i a).setIfInBounds i b = xs.setIfInBounds i b := by
  cases xs
  simp

theorem mem_setIfInBounds {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
    a ∈ xs.setIfInBounds i a := by
  simp [mem_iff_getElem]
  exact ⟨i, (by simpa using h), by simp⟩

theorem mem_or_eq_of_mem_setIfInBounds
    {xs : Array α} {i : Nat} {a b : α} (h : a ∈ xs.setIfInBounds i b) : a ∈ xsa ∈ xs ∨ a = b := by
  cases xs
  simpa using List.mem_or_eq_of_mem_set (by simpa using h)

/-- Simplifies a normal form from `get!` -/
@[simp] theorem getD_get?_setIfInBounds {xs : Array α} {i : Nat} {v d : α} :
    (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d := by
  by_cases h : i < xs.size <;>
    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]

@[simp] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} :
    (xs.setIfInBounds i x).toList = xs.toList.set i x := by
  simp only [setIfInBounds]
  split <;> rename_i h
  · simp
  · simp [List.set_eq_of_length_le (by simpa using h)]

@[simp] theorem beq_empty_iff [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
  cases xs
  simp

@[simp] theorem empty_beq_iff [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
  cases xs
  simp

@[simp] theorem push_beq_push [BEq α] {a b : α} {xs ys : Array α} :
    (xs.push a == ys.push b) = (xs == ys && a == b) := by
  cases xs
  cases ys
  simp

theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys.size := by
  cases xs
  cases ys
  simp [List.length_eq_of_beq (by simpa using h)]

@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
    (replicate n a == replicate n b) = (n == 0 || a == b) := by
  cases n with
  | zero => simp
  | succ n =>
    rw [replicate_succ, replicate_succ, push_beq_push, replicate_beq_replicate]
    rw [Bool.eq_iff_iff]
    simp +contextual

@[deprecated replicate_beq_replicate (since := "2025-03-18")]
abbrev mkArray_beq_mkArray := @replicate_beq_replicate

@[simp] theorem reflBEq_iff [BEq α] : ReflBEqReflBEq (Array α) ↔ ReflBEq α := by
  constructor
  · intro h
    constructor
    intro a
    apply beq_of_beq_singleton
    simp
  · intro h
    constructor
    apply Array.isEqv_self_beq

@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEqLawfulBEq (Array α) ↔ LawfulBEq α := by
  constructor
  · intro h
    constructor
    · intro a b h
      apply singleton_inj.1
      apply eq_of_beq
      simpa [instBEq, isEqv, isEqvAux]
    · intro a
      apply beq_of_beq_singleton
      simp
  · intro h
    constructor
    · intro xs ys h
      obtain ⟨hs, hi⟩ := isEqv_iff_rel.mp h
      ext i h₁ h₂
      · exact hs
      · simpa using hi _ h₁
    · intro xs
      apply Array.isEqv_self_beq

@[simp] theorem isEqv_eq [DecidableEq α] {xs ys : Array α} : xs.isEqv ys (· == ·) = (xs = ys) := by
  cases xs
  cases ys
  simp

theorem back_eq_getElem {xs : Array α} (h : 0 < xs.size) : xs.back = xs[xs.size - 1] := by
  cases xs
  simp [List.getLast_eq_getElem]

theorem back?_eq_getElem? {xs : Array α} : xs.back? = xs[xs.size - 1]? := by
  cases xs
  simp [List.getLast?_eq_getElem?]

@[simp] theorem back_mem {xs : Array α} (h : 0 < xs.size) : xs.back h ∈ xs := by
  cases xs
  simp

theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α} :
    xs.mapM f = xs.foldlM (fun bs a => bs.push <$> f a) #[] := by
  rw [mapM, aux, ← foldlM_toList]; rfl
where
  aux (i bs) :
      mapM.map f xs i bs = (xs.toList.drop i).foldlM (fun bs a => bs.push <$> f a) bs := by
    unfold mapM.map; split
    · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
      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 xs.size - i
  decreasing_by decreasing_trivial_pre_omega

@[simp] theorem toList_map {f : α → β} {xs : Array α} : (xs.map f).toList = xs.toList.map f := by
  rw [map, mapM_eq_foldlM]
  apply congrArg toList (foldl_toList fun bs a => push bs (f a)).symm |>.trans
  have H (l xs) : List.foldl (fun bs a => push bs (f a)) xs l = ⟨xs.toList ++ l.map f⟩ := by
    induction l generalizing xs <;> simp [*]
  simp [H]

@[simp] theorem _root_.List.map_toArray {f : α → β} {l : List α} :
    l.toArray.map f = (l.map f).toArray := by
  apply ext'
  simp

@[simp] theorem size_map {f : α → β} {xs : Array α} : (xs.map f).size = xs.size := by
  simp only [← length_toList]
  simp

@[simp] theorem getElem_map (f : α → β) {xs : Array α} {i : Nat} (hi : i < (xs.map f).size) :
    (xs.map f)[i] = f (xs[i]'(by simpa using hi)) := by
  cases xs
  simp

@[simp] theorem getElem?_map {f : α → β} {xs : Array α} {i : Nat} :
    (xs.map f)[i]? = xs[i]?.map f := by
  simp [getElem?_def]

@[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
  rw [mapM, mapM.map]; rfl

@[simp] theorem map_empty {f : α → β} : map f #[] = #[] := mapM_empty f

@[simp] theorem map_push {f : α → β} {as : Array α} {x : α} :
    (as.push x).map f = (as.map f).push (f x) := by
  ext
  · simp
  · simp only [getElem_map, getElem_push, size_map]
    split <;> rfl

@[simp] theorem map_id_fun : map (id : α → α) = id := by
  funext xs
  induction xs <;> simp_all

/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun

theorem map_id (xs : Array α) : map (id : α → α) xs = xs := by
  cases xs <;> simp_all

/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
-- The argument `xs : Array α` is explicit to allow rewriting from right to left.
theorem map_id' (xs : Array α) : map (fun (a : α) => a) xs = xs := map_id xs

/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
-- The argument `xs : Array α` is explicit to allow rewriting from right to left.
theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (xs : Array α) : map f xs = xs := by
  simp [show f = id from funext h]

theorem map_singleton {f : α → β} {a : α} : map f #[a] = #[f a] := by simp

@[simp 500] theorem mem_map {f : α → β} {xs : Array α} : b ∈ xs.map fb ∈ xs.map f ↔ ∃ a, a ∈ xs ∧ f a = b := by
  simp only [mem_def, toList_map, List.mem_map]

theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h

theorem mem_map_of_mem {f : α → β} (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩

theorem forall_mem_map {f : α → β} {xs : Array α} {P : β → Prop} :
    (∀ (i) (_ : i ∈ xs.map f), P i) ↔ ∀ (j) (_ : j ∈ xs), P (f j) := by
  simp

@[simp] theorem map_eq_empty_iff {f : α → β} {xs : Array α} : mapmap f xs = #[] ↔ xs = #[] := by
  cases xs
  simp

@[simp] theorem map_inj_left {f g : α → β} : mapmap f xs = map g xs ↔ ∀ a ∈ xs, f a = g a := by
  cases xs <;> simp_all

theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : mapmap f xs = map f ys ↔ xs = ys := by
  cases xs
  cases ys
  simp [List.map_inj_right w]

theorem map_congr_left (h : ∀ a ∈ xs, f a = g a) : map f xs = map g xs :=
  map_inj_left.2 h

theorem map_inj : mapmap f = map g ↔ f = g := by
  constructor
  · intro h; ext a; replace h := congrFun h #[a]; simpa using h
  · intro h; subst h; rfl

theorem map_eq_push_iff {f : α → β} {xs : Array α} {ys : Array β} {b : β} :
    mapmap f xs = ys.push b ↔ ∃ zs a, xs = zs.push a ∧ map f zs = ys ∧ f a = b := by
  rcases xs with ⟨xs⟩
  rcases ys with ⟨ys⟩
  simp only [List.map_toArray, List.push_toArray, mk.injEq, List.map_eq_append_iff]
  constructor
  · rintro ⟨l₁, l₂, rfl, rfl, h⟩
    simp only [List.map_eq_singleton_iff] at h
    obtain ⟨a, rfl, rfl⟩ := h
    refine ⟨l₁.toArray, a, by simp⟩
  · rintro ⟨⟨l₁⟩, a, h₁, h₂, rfl⟩
    refine ⟨l₁, [a], by simp_all⟩

@[simp] theorem map_eq_singleton_iff {f : α → β} {xs : Array α} {b : β} :
    mapmap f xs = #[b] ↔ ∃ a, xs = #[a] ∧ f a = b := by
  cases xs
  simp

theorem map_eq_map_iff {f g : α → β} {xs : Array α} :
    mapmap f xs = map g xs ↔ ∀ a ∈ xs, f a = g a := by
  cases xs <;> simp_all

theorem map_eq_iff {f : α → β} {xs : Array α} {ys : Array β} :
    mapmap f xs = ys ↔ ∀ i : Nat, ys[i]? = xs[i]?.map f := by
  cases xs
  cases ys
  simp [List.map_eq_iff]

theorem map_eq_foldl {f : α → β} {xs : Array α} :
    map f xs = foldl (fun bs a => bs.push (f a)) #[] xs := by
  simpa using mapM_eq_foldlM

@[simp] theorem map_set {f : α → β} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} :
    (xs.set i a).map f = (xs.map f).set i (f a) (by simpa using h) := by
  cases xs
  simp

@[simp] theorem map_setIfInBounds {f : α → β} {xs : Array α} {i : Nat} {a : α} :
    (xs.setIfInBounds i a).map f = (xs.map f).setIfInBounds i (f a) := by
  cases xs
  simp

@[simp] theorem map_pop {f : α → β} {xs : Array α} : xs.pop.map f = (xs.map f).pop := by
  cases xs
  simp

@[simp] theorem back?_map {f : α → β} {xs : Array α} : (xs.map f).back? = xs.back?.map f := by
  cases xs
  simp

@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Array α} :
    (as.map f).map g = as.map (g ∘ f) := by
  cases as; simp

theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α} :
    xs.mapM f = List.toArrayList.toArray <$> (xs.toList.mapM f) := by
  rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
  conv => rhs; rw [← List.reverse_reverse xs.toList]
  induction xs.toList.reverse with
  | nil => simp
  | cons a l ih => simp [ih]

@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α} :
    toListtoList <$> xs.mapM f = xs.toList.mapM f := by
  simp [mapM_eq_mapM_toList]

@[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} :
    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun acc a => acc.push (f a)) b := by
  unfold mapM.map
  split <;> rename_i h
  · simp only [Id.bind_eq]
    dsimp [foldl, Id.run, foldlM]
    rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
    -- Calling `split` here gives a bad goal.
    have : size as - i = Nat.succ (size as - i - 1) := by omega
    rw [this]
    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
  · dsimp [foldl, Id.run, foldlM]
    rw [dif_pos (by omega), foldlM.loop, dif_neg h]
    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)
    (xss : Array (Array α)) : P xss := by
  specialize of (xss.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)
    (xss : Array (Array (Array α))) : P xss := by
  specialize of ((xss.toList.map toList).map (fun as => as.map toList))
  simpa [← toList_map, Function.comp_def, map_id] using of

@[congr]
theorem filter_congr {xs ys : Array α} (h : xs = ys)
    {f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
    (h₁ : start = start') (h₂ : stop = stop') :
    filter f xs start stop = filter g ys start' stop' := by
  congr

@[simp] theorem toList_filter' {p : α → Bool} {xs : Array α} {stop : Nat} (h : stop = xs.size) :
    (xs.filter p 0 stop).toList = xs.toList.filter p := by
  subst h
  dsimp only [filter]
  rw [← foldl_toList]
  generalize xs.toList = xs
  suffices ∀ as, (List.foldl (fun acc a => if p a = true then push acc a else acc) as xs).toList =
      as.toList ++ List.filter p xs by
    simpa using this #[]
  induction xs with simp
  | cons => split <;> simp [*]

theorem toList_filter {p : α → Bool} {xs : Array α} :
    (xs.filter p).toList = xs.toList.filter p := by
  simp

@[simp] theorem _root_.List.filter_toArray' {p : α → Bool} {l : List α} {stop : Nat} (h : stop = l.length) :
    l.toArray.filter p 0 stop = (l.filter p).toArray := by
  apply ext'
  simp [h]

theorem _root_.List.filter_toArray {p : α → Bool} {l : List α} :
    l.toArray.filter p = (l.filter p).toArray := by
  simp

@[simp] theorem filter_push_of_pos {p : α → Bool} {a : α} {xs : Array α}
    (h : p a) (w : stop = xs.size + 1):
    (xs.push a).filter p 0 stop = (xs.filter p).push a := by
  subst w
  rcases xs with ⟨xs⟩
  simp [h]

@[simp] theorem filter_push_of_neg {p : α → Bool} {a : α} {xs : Array α}
    (h : ¬p a) (w : stop = xs.size + 1) :
    (xs.push a).filter p 0 stop = xs.filter p := by
  subst w
  rcases xs with ⟨xs⟩
  simp [h]

theorem filter_push {p : α → Bool} {a : α} {xs : Array α} :
    (xs.push a).filter p = if p a then (xs.filter p).push a else xs.filter p := by
  split <;> simp [*]

theorem size_filter_le {p : α → Bool} {xs : Array α} :
    (xs.filter p).size ≤ xs.size := by
  rcases xs with ⟨xs⟩
  simpa using List.length_filter_le p xs

@[simp] theorem filter_eq_self {p : α → Bool} {xs : Array α} :
    filterfilter p xs = xs ↔ ∀ a ∈ xs, p a := by
  rcases xs with ⟨xs⟩
  simp

@[simp] theorem filter_size_eq_size {p : α → Bool} {xs : Array α} :
    (xs.filter p).size = xs.size ↔ ∀ a ∈ xs, p a := by
  rcases xs with ⟨xs⟩
  simp

@[simp] theorem mem_filter {p : α → Bool} {xs : Array α} {a : α} :
    a ∈ xs.filter pa ∈ xs.filter p ↔ a ∈ xs ∧ p a := by
  rcases xs with ⟨xs⟩
  simp