Lemmas about Array.eraseP, Array.erase, and Array.eraseIdx.

eraseP

theorem Array.eraseP_empty {α✝ : Type u_1} {p : α✝ → Bool} : #[].eraseP p = #[]

theorem Array.eraseP_of_forall_mem_not {α : Type u_1} {p : α → Bool} {xs : Array α} (h : ∀ (a : α), a ∈ xs → ¬p a = true) : xs.eraseP p = xs

theorem Array.eraseP_of_forall_getElem_not {α : Type u_1} {p : α → Bool} {xs : Array α} (h : ∀ (i : Nat) (h : i < xs.size), ¬p xs[i] = true) : xs.eraseP p = xs

@[simp]

theorem Array.eraseP_eq_empty_iff {α : Type u_1} {xs : Array α} {p : α → Bool} : xs.eraseP p = #[] ↔ xs = #[] ∨ ∃ (x : α), p x = true ∧ xs = #[x]

theorem Array.eraseP_ne_empty_iff {α : Type u_1} {xs : Array α} {p : α → Bool} : xs.eraseP p ≠ #[] ↔ xs ≠ #[] ∧ ∀ (x : α), p x = true → xs ≠ #[x]

theorem Array.exists_of_eraseP {α : Type u_1} {p : α → Bool} {xs : Array α} {a : α} (hm : a ∈ xs) (hp : p a = true) : ∃ (a : α), ∃ (ys : Array α), ∃ (zs : Array α), (∀ (b : α), b ∈ ys → ¬p b = true) ∧ p a = true ∧ xs = ys.push a ++ zs ∧ xs.eraseP p = ys ++ zs

theorem Array.exists_or_eq_self_of_eraseP {α : Type u_1} (p : α → Bool) (xs : Array α) : xs.eraseP p = xs ∨ ∃ (a : α), ∃ (ys : Array α), ∃ (zs : Array α), (∀ (b : α), b ∈ ys → ¬p b = true) ∧ p a = true ∧ xs = ys.push a ++ zs ∧ xs.eraseP p = ys ++ zs

@[simp]

theorem Array.size_eraseP_of_mem {α : Type u_1} {a : α} {p : α → Bool} {xs : Array α} (al : a ∈ xs) (pa : p a = true) : (xs.eraseP p).size = xs.size - 1

theorem Array.size_eraseP {α : Type u_1} {p : α → Bool} {xs : Array α} : (xs.eraseP p).size = if xs.any p = true then xs.size - 1 else xs.size

theorem Array.size_eraseP_le {α : Type u_1} {p : α → Bool} {xs : Array α} : (xs.eraseP p).size ≤ xs.size

theorem Array.le_size_eraseP {α : Type u_1} {p : α → Bool} {xs : Array α} : xs.size - 1 ≤ (xs.eraseP p).size

theorem Array.mem_of_mem_eraseP {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} : a ∈ xs.eraseP p → a ∈ xs

@[simp]

theorem Array.mem_eraseP_of_neg {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (pa : ¬p a = true) : a ∈ xs.eraseP p ↔ a ∈ xs

@[simp]

theorem Array.eraseP_eq_self_iff {α : Type u_1} {p : α → Bool} {xs : Array α} : xs.eraseP p = xs ↔ ∀ (a : α), a ∈ xs → ¬p a = true

theorem Array.eraseP_map {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β} : (map f xs).eraseP p = map f (xs.eraseP (p ∘ f))

theorem Array.eraseP_filterMap {α : Type u_1} {β : Type u_2} {p : β → Bool} {f : α → Option β} {xs : Array α} : (filterMap f xs).eraseP p = filterMap f (xs.eraseP fun (x : α) => match f x with | some y => p y | none => false)

theorem Array.eraseP_filter {α : Type u_1} {p f : α → Bool} {xs : Array α} : (filter f xs).eraseP p = filter f (xs.eraseP fun (x : α) => p x && f x)

theorem Array.eraseP_append_left {α : Type u_1} {p : α → Bool} {a : α} (pa : p a = true) {xs ys : Array α} (h : a ∈ xs) : (xs ++ ys).eraseP p = xs.eraseP p ++ ys

theorem Array.eraseP_append_right {α : Type u_1} {p : α → Bool} {xs : Array α} (ys : Array α) (h : ∀ (b : α), b ∈ xs → ¬p b = true) : (xs ++ ys).eraseP p = xs ++ ys.eraseP p

theorem Array.eraseP_append {α : Type u_1} {p : α → Bool} {xs ys : Array α} : (xs ++ ys).eraseP p = if xs.any p = true then xs.eraseP p ++ ys else xs ++ ys.eraseP p

theorem Array.eraseP_replicate {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} : (replicate n a).eraseP p = if p a = true then replicate (n - 1) a else replicate n a

@[reducible, inline, deprecated Array.eraseP_replicate (since := "2025-03-18")]

abbrev Array.eraseP_mkArray {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} : (replicate n a).eraseP p = if p a = true then replicate (n - 1) a else replicate n a

Equations

• @Array.eraseP_mkArray = @Array.eraseP_replicate

@[simp]

theorem Array.eraseP_replicate_of_pos {α : Type u_1} {p : α → Bool} {n : Nat} {a : α} (h : p a = true) : (replicate n a).eraseP p = replicate (n - 1) a

@[reducible, inline, deprecated Array.eraseP_replicate_of_pos (since := "2025-03-18")]

abbrev Array.eraseP_mkArray_of_pos {α : Type u_1} {p : α → Bool} {n : Nat} {a : α} (h : p a = true) : (replicate n a).eraseP p = replicate (n - 1) a

Equations

• @Array.eraseP_mkArray_of_pos = @Array.eraseP_replicate_of_pos

@[simp]

theorem Array.eraseP_replicate_of_neg {α : Type u_1} {p : α → Bool} {n : Nat} {a : α} (h : ¬p a = true) : (replicate n a).eraseP p = replicate n a

@[reducible, inline, deprecated Array.eraseP_replicate_of_neg (since := "2025-03-18")]

abbrev Array.eraseP_mkArray_of_neg {α : Type u_1} {p : α → Bool} {n : Nat} {a : α} (h : ¬p a = true) : (replicate n a).eraseP p = replicate n a

Equations

• @Array.eraseP_mkArray_of_neg = @Array.eraseP_replicate_of_neg

theorem Array.eraseP_eq_iff {α : Type u_1} {ys : Array α} {p : α → Bool} {xs : Array α} : xs.eraseP p = ys ↔ (∀ (a : α), a ∈ xs → ¬p a = true) ∧ xs = ys ∨ ∃ (a : α), ∃ (as : Array α), ∃ (bs : Array α), (∀ (b : α), b ∈ as → ¬p b = true) ∧ p a = true ∧ xs = as.push a ++ bs ∧ ys = as ++ bs

theorem Array.eraseP_comm {α : Type u_1} {p q : α → Bool} {xs : Array α} (h : ∀ (a : α), a ∈ xs → ¬p a = true ∨ ¬q a = true) : (xs.eraseP p).eraseP q = (xs.eraseP q).eraseP p

erase

theorem Array.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (h : ¬a ∈ xs) : xs.erase a = xs

theorem Array.erase_eq_eraseP' {α : Type u_1} [BEq α] (a : α) (xs : Array α) : xs.erase a = xs.eraseP fun (x : α) => x == a

theorem Array.erase_eq_eraseP {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (xs : Array α) : xs.erase a = xs.eraseP fun (x : α) => a == x

@[simp]

theorem Array.erase_eq_empty_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : xs.erase a = #[] ↔ xs = #[] ∨ xs = #[a]

theorem Array.erase_ne_empty_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : xs.erase a ≠ #[] ↔ xs ≠ #[] ∧ xs ≠ #[a]

theorem Array.exists_erase_eq {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (h : a ∈ xs) : ∃ (ys : Array α), ∃ (zs : Array α), ¬a ∈ ys ∧ xs = ys.push a ++ zs ∧ xs.erase a = ys ++ zs

@[simp]

theorem Array.size_erase_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (h : a ∈ xs) : (xs.erase a).size = xs.size - 1

theorem Array.size_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} : (xs.erase a).size = if a ∈ xs then xs.size - 1 else xs.size

theorem Array.size_erase_le {α : Type u_1} [BEq α] {a : α} {xs : Array α} : (xs.erase a).size ≤ xs.size

theorem Array.le_size_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} : xs.size - 1 ≤ (xs.erase a).size

theorem Array.mem_of_mem_erase {α : Type u_1} [BEq α] {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a ∈ xs

@[simp]

theorem Array.mem_erase_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) : a ∈ xs.erase b ↔ a ∈ xs

@[simp]

theorem Array.erase_eq_self_iff {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] {xs : Array α} : xs.erase a = xs ↔ ¬a ∈ xs

theorem Array.erase_filter {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] {f : α → Bool} {xs : Array α} : (filter f xs).erase a = filter f (xs.erase a)

theorem Array.erase_append_left {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] {xs : Array α} (ys : Array α) (h : a ∈ xs) : (xs ++ ys).erase a = xs.erase a ++ ys

theorem Array.erase_append_right {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (ys : Array α) (h : ¬a ∈ xs) : (xs ++ ys).erase a = xs ++ ys.erase a

theorem Array.erase_append {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs ys : Array α} : (xs ++ ys).erase a = if a ∈ xs then xs.erase a ++ ys else xs ++ ys.erase a

theorem Array.erase_replicate {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} : (replicate n a).erase b = if (b == a) = true then replicate (n - 1) a else replicate n a

@[reducible, inline, deprecated Array.erase_replicate (since := "2025-03-18")]

abbrev Array.erase_mkArray {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} : (replicate n a).erase b = if (b == a) = true then replicate (n - 1) a else replicate n a

Equations

• @Array.erase_mkArray = @Array.erase_replicate

theorem Array.erase_comm {α : Type u_1} [BEq α] [LawfulBEq α] (a b : α) {xs : Array α} : (xs.erase a).erase b = (xs.erase b).erase a

theorem Array.erase_eq_iff {α : Type u_1} [BEq α] {ys : Array α} [LawfulBEq α] {a : α} {xs : Array α} : xs.erase a = ys ↔ ¬a ∈ xs ∧ xs = ys ∨ ∃ (as : Array α), ∃ (bs : Array α), ¬a ∈ as ∧ xs = as.push a ++ bs ∧ ys = as ++ bs

@[simp]

theorem Array.erase_replicate_self {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a : α} : (replicate n a).erase a = replicate (n - 1) a

@[reducible, inline, deprecated Array.erase_replicate_self (since := "2025-03-18")]

abbrev Array.erase_mkArray_self {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a : α} : (replicate n a).erase a = replicate (n - 1) a

Equations

• @Array.erase_mkArray_self = @Array.erase_replicate_self

@[simp]

theorem Array.erase_replicate_ne {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a b : α} (h : (!b == a) = true) : (replicate n a).erase b = replicate n a

@[reducible, inline, deprecated Array.erase_replicate_ne (since := "2025-03-18")]

abbrev Array.erase_mkArray_ne {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a b : α} (h : (!b == a) = true) : (replicate n a).erase b = replicate n a

Equations

• @Array.erase_mkArray_ne = @Array.erase_replicate_ne

eraseIdx

theorem Array.eraseIdx_eq_eraseIdxIfInBounds {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) : xs.eraseIdx i h = xs.eraseIdxIfInBounds i

theorem Array.eraseIdx_eq_take_drop_succ {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) : xs.eraseIdx i h = xs.take i ++ xs.drop (i + 1)

theorem Array.getElem?_eraseIdx {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} : (xs.eraseIdx i h)[j]? = if j < i then xs[j]? else xs[j + 1]?

theorem Array.getElem?_eraseIdx_of_lt {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} (h' : j < i) : (xs.eraseIdx i h)[j]? = xs[j]?

theorem Array.getElem?_eraseIdx_of_ge {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} (h' : i ≤ j) : (xs.eraseIdx i h)[j]? = xs[j + 1]?

theorem Array.getElem_eraseIdx {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} (h' : j < (xs.eraseIdx i h).size) : (xs.eraseIdx i h)[j] = if h'' : j < i then xs[j] else xs[j + 1]

@[simp]

theorem Array.eraseIdx_eq_empty_iff {α : Type u_1} {xs : Array α} {i : Nat} {h : i < xs.size} : xs.eraseIdx i h = #[] ↔ xs.size = 1 ∧ i = 0

theorem Array.eraseIdx_ne_empty_iff {α : Type u_1} {xs : Array α} {i : Nat} {h : i < xs.size} : xs.eraseIdx i h ≠ #[] ↔ 2 ≤ xs.size

theorem Array.mem_of_mem_eraseIdx {α : Type u_1} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} : a ∈ xs.eraseIdx i h → a ∈ xs

theorem Array.eraseIdx_append_of_lt_size {α : Type u_1} {xs : Array α} {k : Nat} (hk : k < xs.size) (ys : Array α) (h : k < (xs ++ ys).size) : (xs ++ ys).eraseIdx k h = xs.eraseIdx k hk ++ ys

theorem Array.eraseIdx_append_of_size_le {α : Type u_1} {xs : Array α} {k : Nat} (hk : xs.size ≤ k) (ys : Array α) (h : k < (xs ++ ys).size) : (xs ++ ys).eraseIdx k h = xs ++ ys.eraseIdx (k - xs.size) ⋯

@[reducible, inline, deprecated Array.eraseIdx_append_of_size_le (since := "2025-06-11")]

abbrev Array.eraseIdx_append_of_length_le {α : Type u_1} {xs : Array α} {k : Nat} (hk : xs.size ≤ k) (ys : Array α) (h : k < (xs ++ ys).size) : (xs ++ ys).eraseIdx k h = xs ++ ys.eraseIdx (k - xs.size) ⋯

Equations

• @Array.eraseIdx_append_of_length_le = @Array.eraseIdx_append_of_size_le

theorem Array.eraseIdx_append {α : Type u_1} {k : Nat} {xs ys : Array α} (h : k < (xs ++ ys).size) : (xs ++ ys).eraseIdx k h = if h' : k < xs.size then xs.eraseIdx k h' ++ ys else xs ++ ys.eraseIdx (k - xs.size) ⋯

theorem Array.eraseIdx_replicate {α : Type u_1} {n : Nat} {a : α} {k : Nat} {h : k < (replicate n a).size} : (replicate n a).eraseIdx k h = replicate (n - 1) a

@[reducible, inline, deprecated Array.eraseIdx_replicate (since := "2025-03-18")]

abbrev Array.eraseIdx_mkArray {α : Type u_1} {n : Nat} {a : α} {k : Nat} {h : k < (replicate n a).size} : (replicate n a).eraseIdx k h = replicate (n - 1) a

Equations

• @Array.eraseIdx_mkArray = @Array.eraseIdx_replicate

theorem Array.mem_eraseIdx_iff_getElem {α : Type u_1} {x : α} {xs : Array α} {k : Nat} {h : k < xs.size} : x ∈ xs.eraseIdx k h ↔ ∃ (i : Nat), ∃ (w : i < xs.size), i ≠ k ∧ xs[i] = x

theorem Array.mem_eraseIdx_iff_getElem? {α : Type u_1} {x : α} {xs : Array α} {k : Nat} {h : k < xs.size} : x ∈ xs.eraseIdx k h ↔ ∃ (i : Nat), i ≠ k ∧ xs[i]? = some x

theorem Array.erase_eq_eraseIdx_of_idxOf {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : Nat} (w : idxOf a xs = i) (h : i < xs.size) : xs.erase a = xs.eraseIdx i h

theorem Array.getElem_eraseIdx_of_lt {α : Type u_1} {xs : Array α} {i : Nat} (w : i < xs.size) {j : Nat} (h : j < (xs.eraseIdx i w).size) (h' : j < i) : (xs.eraseIdx i w)[j] = xs[j]

theorem Array.getElem_eraseIdx_of_ge {α : Type u_1} {xs : Array α} {i : Nat} (w : i < xs.size) {j : Nat} (h : j < (xs.eraseIdx i w).size) (h' : i ≤ j) : (xs.eraseIdx i w)[j] = xs[j + 1]

theorem Array.eraseIdx_set_eq {α : Type u_1} {xs : Array α} {i : Nat} {a : α} {h : i < xs.size} : (xs.set i a h).eraseIdx i ⋯ = xs.eraseIdx i h

theorem Array.eraseIdx_set_lt {α : Type u_1} {xs : Array α} {i : Nat} {w : i < xs.size} {j : Nat} {a : α} (h : j < i) : (xs.set i a w).eraseIdx j ⋯ = (xs.eraseIdx j ⋯).set (i - 1) a ⋯

theorem Array.eraseIdx_set_gt {α : Type u_1} {xs : Array α} {i j : Nat} {a : α} (h : i < j) {w : j < xs.size} : (xs.set i a ⋯).eraseIdx j ⋯ = (xs.eraseIdx j w).set i a ⋯

theorem Array.eraseIdx_set {α : Type u_1} {xs : Array α} {i : Nat} {a : α} {hi : i < xs.size} {j : Nat} {hj : j < (xs.set i a hi).size} : (xs.set i a hi).eraseIdx j hj = if h' : j < i then (xs.eraseIdx j ⋯).set (i - 1) a ⋯ else if h'' : j = i then xs.eraseIdx i hi else (xs.eraseIdx j ⋯).set i a ⋯

theorem Array.set_eraseIdx_le {α : Type u_1} {xs : Array α} {i : Nat} {w : i < xs.size} {j : Nat} {a : α} (h : i ≤ j) (hj : j < (xs.eraseIdx i w).size) : (xs.eraseIdx i w).set j a hj = (xs.set (j + 1) a ⋯).eraseIdx i ⋯

theorem Array.set_eraseIdx_gt {α : Type u_1} {xs : Array α} {i : Nat} {w : i < xs.size} {j : Nat} {a : α} (h : j < i) (hj : j < (xs.eraseIdx i w).size) : (xs.eraseIdx i w).set j a hj = (xs.set j a ⋯).eraseIdx i ⋯

theorem Array.set_eraseIdx {α : Type u_1} {xs : Array α} {i : Nat} {w : i < xs.size} {j : Nat} {a : α} (hj : j < (xs.eraseIdx i w).size) : (xs.eraseIdx i w).set j a hj = if h' : i ≤ j then (xs.set (j + 1) a ⋯).eraseIdx i ⋯ else (xs.set j a ⋯).eraseIdx i ⋯

@[simp]

theorem Array.set_getElem_succ_eraseIdx_succ {α : Type u_1} {xs : Array α} {i : Nat} (h : i + 1 < xs.size) : (xs.eraseIdx (i + 1) h).set i xs[i + 1] ⋯ = xs.eraseIdx i ⋯