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

eraseP

@[simp]

theorem List.eraseP_nil {α✝ : Type u_1} {p : α✝ → Bool} : eraseP p [] = []

theorem List.eraseP_cons {α : Type u_1} {p : α → Bool} {a : α} {l : List α} : eraseP p (a :: l) = bif p a then l else a :: eraseP p l

@[simp]

theorem List.eraseP_cons_of_pos {α : Type u_1} {a : α} {l : List α} {p : α → Bool} (h : p a = true) : eraseP p (a :: l) = l

@[simp]

theorem List.eraseP_cons_of_neg {α : Type u_1} {a : α} {l : List α} {p : α → Bool} (h : ¬p a = true) : eraseP p (a :: l) = a :: eraseP p l

theorem List.eraseP_of_forall_not {α : Type u_1} {p : α → Bool} {l : List α} (h : ∀ (a : α), a ∈ l → ¬p a = true) : eraseP p l = l

@[simp]

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

@[reducible, inline, deprecated List.eraseP_eq_nil_iff (since := "2025-01-30")]

abbrev List.eraseP_eq_nil {α : Type u_1} {xs : List α} {p : α → Bool} : eraseP p xs = [] ↔ xs = [] ∨ ∃ (x : α), p x = true ∧ xs = [x]

Equations

• @List.eraseP_eq_nil = @List.eraseP_eq_nil_iff

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

@[reducible, inline, deprecated List.eraseP_ne_nil_iff (since := "2025-01-30")]

abbrev List.eraseP_ne_nil {α : Type u_1} {xs : List α} {p : α → Bool} : eraseP p xs ≠ [] ↔ xs ≠ [] ∧ ∀ (x : α), p x = true → xs ≠ [x]

Equations

• @List.eraseP_ne_nil = @List.eraseP_ne_nil_iff

theorem List.exists_of_eraseP {α : Type u_1} {p : α → Bool} {l : List α} {a : α} : a ∈ l → p a = true → ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ eraseP p l = l₁ ++ l₂

theorem List.exists_or_eq_self_of_eraseP {α : Type u_1} (p : α → Bool) (l : List α) : eraseP p l = l ∨ ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ eraseP p l = l₁ ++ l₂

@[simp]

theorem List.length_eraseP_of_mem {α✝ : Type u_1} {l : List α✝} {a : α✝} {p : α✝ → Bool} (al : a ∈ l) (pa : p a = true) : (eraseP p l).length = l.length - 1

theorem List.length_eraseP {α : Type u_1} {p : α → Bool} {l : List α} : (eraseP p l).length = if l.any p = true then l.length - 1 else l.length

theorem List.eraseP_sublist {α : Type u_1} {p : α → Bool} {l : List α} : (eraseP p l).Sublist l

theorem List.eraseP_subset {α : Type u_1} {p : α → Bool} {l : List α} : eraseP p l ⊆ l

theorem List.Sublist.eraseP {α✝ : Type u_1} {l₁ l₂ : List α✝} {p : α✝ → Bool} : l₁.Sublist l₂ → (eraseP p l₁).Sublist (eraseP p l₂)

theorem List.length_eraseP_le {α : Type u_1} {p : α → Bool} {l : List α} : (eraseP p l).length ≤ l.length

theorem List.le_length_eraseP {α : Type u_1} {p : α → Bool} {l : List α} : l.length - 1 ≤ (eraseP p l).length

theorem List.mem_of_mem_eraseP {α : Type u_1} {p : α → Bool} {a : α} {l : List α} : a ∈ eraseP p l → a ∈ l

@[simp]

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

@[simp]

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

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

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

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

theorem List.eraseP_append_left {α : Type u_1} {p : α → Bool} {a : α} (pa : p a = true) {l₁ : List α} (l₂ : List α) : a ∈ l₁ → eraseP p (l₁ ++ l₂) = eraseP p l₁ ++ l₂

theorem List.eraseP_append_right {α : Type u_1} {p : α → Bool} {l₁ : List α} (l₂ : List α) : (∀ (b : α), b ∈ l₁ → ¬p b = true) → eraseP p (l₁ ++ l₂) = l₁ ++ eraseP p l₂

theorem List.eraseP_append {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} : eraseP p (l₁ ++ l₂) = if l₁.any p = true then eraseP p l₁ ++ l₂ else l₁ ++ eraseP p l₂

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

@[simp]

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

@[simp]

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

theorem List.IsPrefix.eraseP {α✝ : Type u_1} {l₁ l₂ : List α✝} {p : α✝ → Bool} (h : l₁ <+: l₂) : eraseP p l₁ <+: eraseP p l₂

theorem List.eraseP_eq_iff {α : Type u_1} {l' : List α} {p : α → Bool} {l : List α} : eraseP p l = l' ↔ (∀ (a : α), a ∈ l → ¬p a = true) ∧ l = l' ∨ ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

theorem List.Pairwise.eraseP {α✝ : Type u_1} {p : α✝ → α✝ → Prop} {l : List α✝} (q : α✝ → Bool) : Pairwise p l → Pairwise p (List.eraseP q l)

theorem List.Nodup.eraseP {α✝ : Type u_1} {l : List α✝} (p : α✝ → Bool) : l.Nodup → (List.eraseP p l).Nodup

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

theorem List.head_eraseP_mem {α : Type u_1} {xs : List α} {p : α → Bool} (h : eraseP p xs ≠ []) : (eraseP p xs).head h ∈ xs

theorem List.getLast_eraseP_mem {α : Type u_1} {xs : List α} {p : α → Bool} (h : eraseP p xs ≠ []) : (eraseP p xs).getLast h ∈ xs

theorem List.eraseP_eq_eraseIdx {α : Type u_1} {xs : List α} {p : α → Bool} : eraseP p xs = match findIdx? p xs with | none => xs | some i => xs.eraseIdx i

erase

@[simp]

theorem List.erase_cons_head {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l

@[simp]

theorem List.erase_cons_tail {α : Type u_1} [BEq α] {a b : α} {l : List α} (h : ¬(b == a) = true) : (b :: l).erase a = b :: l.erase a

theorem List.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : ¬a ∈ l → l.erase a = l

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

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

@[simp]

theorem List.erase_eq_nil_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {a : α} : xs.erase a = [] ↔ xs = [] ∨ xs = [a]

@[reducible, inline, deprecated List.erase_eq_nil_iff (since := "2025-01-30")]

abbrev List.erase_eq_nil {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {a : α} : xs.erase a = [] ↔ xs = [] ∨ xs = [a]

Equations

• @List.erase_eq_nil = @List.erase_eq_nil_iff

theorem List.erase_ne_nil_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {a : α} : xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]

@[reducible, inline, deprecated List.erase_ne_nil_iff (since := "2025-01-30")]

abbrev List.erase_ne_nil {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {a : α} : xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]

Equations

• @List.erase_ne_nil = @List.erase_ne_nil_iff

theorem List.exists_erase_eq {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : ∃ (l₁ : List α), ∃ (l₂ : List α), ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂

@[simp]

theorem List.length_erase_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : (l.erase a).length = l.length - 1

theorem List.length_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : (l.erase a).length = if a ∈ l then l.length - 1 else l.length

theorem List.erase_sublist {α : Type u_1} [BEq α] {a : α} {l : List α} : (l.erase a).Sublist l

theorem List.erase_subset {α : Type u_1} [BEq α] {a : α} {l : List α} : l.erase a ⊆ l

theorem List.Sublist.erase {α : Type u_1} [BEq α] (a : α) {l₁ l₂ : List α} (h : l₁.Sublist l₂) : (l₁.erase a).Sublist (l₂.erase a)

theorem List.IsPrefix.erase {α : Type u_1} [BEq α] (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.erase a <+: l₂.erase a

theorem List.length_erase_le {α : Type u_1} [BEq α] {a : α} {l : List α} : (l.erase a).length ≤ l.length

theorem List.le_length_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : l.length - 1 ≤ (l.erase a).length

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

@[simp]

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

@[simp]

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

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

theorem List.erase_append_left {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) : (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

theorem List.erase_append_right {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : ¬a ∈ l₁) : (l₁ ++ l₂).erase a = l₁ ++ l₂.erase a

theorem List.erase_append {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} : (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a

theorem List.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

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

theorem List.erase_eq_iff {α : Type u_1} [BEq α] {l' : List α} [LawfulBEq α] {a : α} {l : List α} : l.erase a = l' ↔ ¬a ∈ l ∧ l = l' ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

@[simp]

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

@[simp]

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

theorem List.Pairwise.erase {α : Type u_1} [BEq α] {p : α → α → Prop} [LawfulBEq α] {l : List α} (a : α) : Pairwise p l → Pairwise p (l.erase a)

theorem List.Nodup.erase_eq_filter {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} (d : l.Nodup) (a : α) : l.erase a = filter (fun (x : α) => x != a) l

theorem List.Nodup.mem_erase_iff {α : Type u_1} [BEq α] {l : List α} {b : α} [LawfulBEq α] {a : α} (d : l.Nodup) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

theorem List.Nodup.not_mem_erase {α : Type u_1} [BEq α] {l : List α} [LawfulBEq α] {a : α} (h : l.Nodup) : ¬a ∈ l.erase a

theorem List.Nodup.erase {α : Type u_1} [BEq α] {l : List α} [LawfulBEq α] (a : α) : l.Nodup → (l.erase a).Nodup

theorem List.head_erase_mem {α : Type u_1} [BEq α] (xs : List α) (a : α) (h : xs.erase a ≠ []) : (xs.erase a).head h ∈ xs

theorem List.getLast_erase_mem {α : Type u_1} [BEq α] (xs : List α) (a : α) (h : xs.erase a ≠ []) : (xs.erase a).getLast h ∈ xs

theorem List.erase_eq_eraseIdx {α : Type u_1} [BEq α] (l : List α) (a : α) : l.erase a = match idxOf? a l with | none => l | some i => l.eraseIdx i

eraseIdx

theorem List.length_eraseIdx {α : Type u_1} {l : List α} {i : Nat} : (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length

theorem List.length_eraseIdx_of_lt {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) : (l.eraseIdx i).length = l.length - 1

@[simp]

theorem List.eraseIdx_zero {α : Type u_1} {l : List α} : l.eraseIdx 0 = l.tail

theorem List.eraseIdx_eq_take_drop_succ {α : Type u_1} (l : List α) (i : Nat) : l.eraseIdx i = take i l ++ drop (i + 1) l

@[simp]

theorem List.eraseIdx_eq_nil_iff {α : Type u_1} {l : List α} {i : Nat} : l.eraseIdx i = [] ↔ l = [] ∨ l.length = 1 ∧ i = 0

@[reducible, inline, deprecated List.eraseIdx_eq_nil_iff (since := "2025-01-30")]

abbrev List.eraseIdx_eq_nil {α : Type u_1} {l : List α} {i : Nat} : l.eraseIdx i = [] ↔ l = [] ∨ l.length = 1 ∧ i = 0

Equations

• @List.eraseIdx_eq_nil = @List.eraseIdx_eq_nil_iff

theorem List.eraseIdx_ne_nil_iff {α : Type u_1} {l : List α} {i : Nat} : l.eraseIdx i ≠ [] ↔ 2 ≤ l.length ∨ l.length = 1 ∧ i ≠ 0

@[reducible, inline, deprecated List.eraseIdx_ne_nil_iff (since := "2025-01-30")]

abbrev List.eraseIdx_ne_nil {α : Type u_1} {l : List α} {i : Nat} : l.eraseIdx i ≠ [] ↔ 2 ≤ l.length ∨ l.length = 1 ∧ i ≠ 0

Equations

• @List.eraseIdx_ne_nil = @List.eraseIdx_ne_nil_iff

theorem List.eraseIdx_sublist {α : Type u_1} (l : List α) (k : Nat) : (l.eraseIdx k).Sublist l

theorem List.mem_of_mem_eraseIdx {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l

theorem List.eraseIdx_subset {α : Type u_1} {l : List α} {k : Nat} : l.eraseIdx k ⊆ l

@[simp]

theorem List.eraseIdx_eq_self {α : Type u_1} {l : List α} {k : Nat} : l.eraseIdx k = l ↔ l.length ≤ k

theorem List.eraseIdx_of_length_le {α : Type u_1} {l : List α} {k : Nat} (h : l.length ≤ k) : l.eraseIdx k = l

theorem List.length_eraseIdx_le {α : Type u_1} (l : List α) (i : Nat) : (l.eraseIdx i).length ≤ l.length

theorem List.le_length_eraseIdx {α : Type u_1} (l : List α) (i : Nat) : l.length - 1 ≤ (l.eraseIdx i).length

theorem List.eraseIdx_append_of_lt_length {α : Type u_1} {l : List α} {k : Nat} (hk : k < l.length) (l' : List α) : (l ++ l').eraseIdx k = l.eraseIdx k ++ l'

theorem List.eraseIdx_append_of_length_le {α : Type u_1} {l : List α} {k : Nat} (hk : l.length ≤ k) (l' : List α) : (l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)

theorem List.eraseIdx_replicate {α : Type u_1} {n : Nat} {a : α} {k : Nat} : (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a

theorem List.Pairwise.eraseIdx {α : Type u_1} {p : α → α → Prop} {l : List α} (k : Nat) : Pairwise p l → Pairwise p (l.eraseIdx k)

theorem List.Nodup.eraseIdx {α : Type u_1} {l : List α} (k : Nat) : l.Nodup → (l.eraseIdx k).Nodup

theorem List.IsPrefix.eraseIdx {α : Type u_1} {l l' : List α} (h : l <+: l') (k : Nat) : l.eraseIdx k <+: l'.eraseIdx k

theorem List.erase_eq_eraseIdx_of_idxOf {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} (w : idxOf a l = i) : l.erase a = l.eraseIdx i

@[reducible, inline, deprecated List.erase_eq_eraseIdx_of_idxOf (since := "2025-01-29")]

abbrev List.erase_eq_eraseIdx_of_indexOf {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} (w : idxOf a l = i) : l.erase a = l.eraseIdx i

Equations

• @List.erase_eq_eraseIdx_of_indexOf = @List.erase_eq_eraseIdx_of_idxOf