Further lemmas about List.take, List.drop, List.zip and List.zipWith.

These are in a separate file from most of the list lemmas as they required importing more lemmas about natural numbers, and use omega.

take

@[simp]

theorem List.length_take {α : Type u_1} {i : Nat} {l : List α} : (take i l).length = min i l.length

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

theorem List.length_take_le' {α : Type u_1} (i : Nat) (l : List α) : (take i l).length ≤ l.length

theorem List.length_take_of_le {i : Nat} {α✝ : Type u_1} {l : List α✝} (h : i ≤ l.length) : (take i l).length = i

theorem List.getElem_take' {α : Type u_1} {xs : List α} {i j : Nat} (hi : i < xs.length) (hj : i < j) : xs[i] = (take j xs)[i]

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the big list to the small list.

@[simp]

theorem List.getElem_take {α : Type u_1} {xs : List α} {j i : Nat} {h : i < (take j xs).length} : (take j xs)[i] = xs[i]

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the small list to the big list.

theorem List.getElem?_take_eq_none {α : Type u_1} {l : List α} {i j : Nat} (h : i ≤ j) : (take i l)[j]? = none

theorem List.getElem?_take {α : Type u_1} {l : List α} {i j : Nat} : (take i l)[j]? = if j < i then l[j]? else none

theorem List.head?_take {α : Type u_1} {l : List α} {i : Nat} : (take i l).head? = if i = 0 then none else l.head?

theorem List.head_take {α : Type u_1} {l : List α} {i : Nat} (h : take i l ≠ []) : (take i l).head h = l.head ⋯

theorem List.getLast?_take {α : Type u_1} {i : Nat} {l : List α} : (take i l).getLast? = if i = 0 then none else l[i - 1]?.or l.getLast?

theorem List.getLast_take {α : Type u_1} {i : Nat} {l : List α} (h : take i l ≠ []) : (take i l).getLast h = l[i - 1]?.getD (l.getLast ⋯)

theorem List.take_take {α : Type u_1} {i j : Nat} {l : List α} : take i (take j l) = take (min i j) l

theorem List.take_set_of_le {α : Type u_1} {a : α} {i j : Nat} {l : List α} (h : j ≤ i) : take j (l.set i a) = take j l

@[reducible, inline, deprecated List.take_set_of_le (since := "2025-02-04")]

abbrev List.take_set_of_lt {α : Type u_1} {a : α} {i j : Nat} {l : List α} (h : j ≤ i) : take j (l.set i a) = take j l

Equations

• @List.take_set_of_lt = @List.take_set_of_le

@[simp]

theorem List.take_replicate {α : Type u_1} {a : α} {i n : Nat} : take i (replicate n a) = replicate (min i n) a

@[simp]

theorem List.drop_replicate {α : Type u_1} {a : α} {i n : Nat} : drop i (replicate n a) = replicate (n - i) a

theorem List.take_append {α : Type u_1} {l₁ l₂ : List α} {i : Nat} : take i (l₁ ++ l₂) = take i l₁ ++ take (i - l₁.length) l₂

Taking the first i elements in l₁ ++ l₂ is the same as appending the first i elements of l₁ to the first n - l₁.length elements of l₂.

@[reducible, inline, deprecated List.take_append (since := "2025-06-16")]

abbrev List.take_append_eq_append_take {α : Type u_1} {l₁ l₂ : List α} {i : Nat} : take i (l₁ ++ l₂) = take i l₁ ++ take (i - l₁.length) l₂

Equations

• @List.take_append_eq_append_take = @List.take_append

theorem List.take_append_of_le_length {α : Type u_1} {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) : take i (l₁ ++ l₂) = take i l₁

theorem List.take_length_add_append {α : Type u_1} {l₁ l₂ : List α} (i : Nat) : take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂

Taking the first l₁.length + i elements in l₁ ++ l₂ is the same as appending the first i elements of l₂ to l₁.

@[simp]

theorem List.take_eq_take_iff {α : Type u_1} {l : List α} {i j : Nat} : take i l = take j l ↔ min i l.length = min j l.length

@[reducible, inline, deprecated List.take_eq_take_iff (since := "2025-02-16")]

abbrev List.take_eq_take {α : Type u_1} {l : List α} {i j : Nat} : take i l = take j l ↔ min i l.length = min j l.length

Equations

• @List.take_eq_take = @List.take_eq_take_iff

theorem List.take_add {α : Type u_1} {l : List α} {i j : Nat} : take (i + j) l = take i l ++ take j (drop i l)

theorem List.take_one {α : Type u_1} {l : List α} : take 1 l = l.head?.toList

theorem List.take_eq_append_getElem_of_pos {α : Type u_1} {i : Nat} {l : List α} (h₁ : 0 < i) (h₂ : i < l.length) : take i l = take (i - 1) l ++ [l[i - 1]]

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

theorem List.take_eq_dropLast {α : Type u_1} {l : List α} {i : Nat} (h : i + 1 = l.length) : take i l = l.dropLast

theorem List.take_prefix_take_left {α : Type u_1} {l : List α} {i j : Nat} (h : i ≤ j) : take i l <+: take j l

theorem List.take_sublist_take_left {α : Type u_1} {l : List α} {i j : Nat} (h : i ≤ j) : (take i l).Sublist (take j l)

theorem List.take_subset_take_left {α : Type u_1} (l : List α) {i j : Nat} (h : i ≤ j) : take i l ⊆ take j l

drop

theorem List.lt_length_drop {α : Type u_1} {xs : List α} {i j : Nat} (h : i + j < xs.length) : j < (drop i xs).length

theorem List.getElem_drop' {α : Type u_1} {xs : List α} {i j : Nat} (h : i + j < xs.length) : xs[i + j] = (drop i xs)[j]

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the big list to the small list.

@[simp]

theorem List.getElem_drop {α : Type u_1} {xs : List α} {i j : Nat} {h : j < (drop i xs).length} : (drop i xs)[j] = xs[i + j]

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the small list to the big list.

@[simp]

theorem List.getElem?_drop {α : Type u_1} {xs : List α} {i j : Nat} : (drop i xs)[j]? = xs[i + j]?

theorem List.mem_take_iff_getElem {α : Type u_1} {i : Nat} {l : List α} {a : α} : a ∈ take i l ↔ ∃ (j : Nat), ∃ (hm : j < min i l.length), l[j] = a

theorem List.mem_drop_iff_getElem {α : Type u_1} {i : Nat} {l : List α} {a : α} : a ∈ drop i l ↔ ∃ (j : Nat), ∃ (hm : j + i < l.length), l[i + j] = a

@[simp]

theorem List.head?_drop {α : Type u_1} {l : List α} {i : Nat} : (drop i l).head? = l[i]?

@[simp]

theorem List.head_drop {α : Type u_1} {l : List α} {i : Nat} (h : drop i l ≠ []) : (drop i l).head h = l[i]

theorem List.getLast?_drop {α : Type u_1} {i : Nat} {l : List α} : (drop i l).getLast? = if l.length ≤ i then none else l.getLast?

@[simp]

theorem List.getLast_drop {α : Type u_1} {i : Nat} {l : List α} (h : drop i l ≠ []) : (drop i l).getLast h = l.getLast ⋯

theorem List.drop_length_cons {α : Type u_1} {l : List α} (h : l ≠ []) (a : α) : drop l.length (a :: l) = [l.getLast h]

theorem List.drop_append {α : Type u_1} {l₁ l₂ : List α} {i : Nat} : drop i (l₁ ++ l₂) = drop i l₁ ++ drop (i - l₁.length) l₂

Dropping the elements up to i in l₁ ++ l₂ is the same as dropping the elements up to i in l₁, dropping the elements up to i - l₁.length in l₂, and appending them.

@[reducible, inline, deprecated List.drop_append (since := "2025-06-16")]

abbrev List.drop_append_eq_append_drop {α : Type u_1} {l₁ l₂ : List α} {i : Nat} : drop i (l₁ ++ l₂) = drop i l₁ ++ drop (i - l₁.length) l₂

Equations

• @List.drop_append_eq_append_drop = @List.drop_append

theorem List.drop_append_of_le_length {α : Type u_1} {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) : drop i (l₁ ++ l₂) = drop i l₁ ++ l₂

@[simp]

theorem List.drop_length_add_append {α : Type u_1} {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂

Dropping the elements up to l₁.length + i in l₁ + l₂ is the same as dropping the elements up to i in l₂.

theorem List.set_eq_take_append_cons_drop {α : Type u_1} {l : List α} {i : Nat} {a : α} : l.set i a = if i < l.length then take i l ++ a :: drop (i + 1) l else l

theorem List.drop_set_of_lt {α : Type u_1} {a : α} {i j : Nat} {l : List α} (hnm : i < j) : drop j (l.set i a) = drop j l

theorem List.drop_take {α : Type u_1} {i j : Nat} {l : List α} : drop i (take j l) = take (j - i) (drop i l)

@[simp]

theorem List.drop_take_self {i : Nat} {α✝ : Type u_1} {l : List α✝} : drop i (take i l) = []

theorem List.take_reverse {α : Type u_1} {xs : List α} {i : Nat} : take i xs.reverse = (drop (xs.length - i) xs).reverse

theorem List.drop_reverse {α : Type u_1} {xs : List α} {i : Nat} : drop i xs.reverse = (take (xs.length - i) xs).reverse

theorem List.reverse_take {α : Type u_1} {l : List α} {i : Nat} : (take i l).reverse = drop (l.length - i) l.reverse

theorem List.reverse_drop {α : Type u_1} {l : List α} {i : Nat} : (drop i l).reverse = take (l.length - i) l.reverse

theorem List.take_add_one {α : Type u_1} {l : List α} {i : Nat} : take (i + 1) l = take i l ++ l[i]?.toList

theorem List.drop_eq_getElem?_toList_append {α : Type u_1} {l : List α} {i : Nat} : drop i l = l[i]?.toList ++ drop (i + 1) l

theorem List.drop_sub_one {α : Type u_1} {l : List α} {i : Nat} (h : 0 < i) : drop (i - 1) l = l[i - 1]?.toList ++ drop i l

findIdx

theorem List.false_of_mem_take_findIdx {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} (h : x ∈ take (findIdx p xs) xs) : p x = false

@[simp]

theorem List.findIdx_take {α : Type u_1} {xs : List α} {i : Nat} {p : α → Bool} : findIdx p (take i xs) = min i (findIdx p xs)

@[simp]

theorem List.min_findIdx_findIdx {α : Type u_1} {xs : List α} {p q : α → Bool} : min (findIdx p xs) (findIdx q xs) = findIdx (fun (a : α) => p a || q a) xs

findIdx?

@[simp]

theorem List.findIdx?_take {α : Type u_1} {xs : List α} {i : Nat} {p : α → Bool} : findIdx? p (take i xs) = (findIdx? p xs).bind (Option.guard fun (j : Nat) => decide (j < i))

takeWhile

theorem List.takeWhile_eq_take_findIdx_not {α : Type u_1} {xs : List α} {p : α → Bool} : takeWhile p xs = take (findIdx (fun (a : α) => !p a) xs) xs

theorem List.dropWhile_eq_drop_findIdx_not {α : Type u_1} {xs : List α} {p : α → Bool} : dropWhile p xs = drop (findIdx (fun (a : α) => !p a) xs) xs

rotateLeft

@[simp]

theorem List.rotateLeft_replicate {α : Type u_1} {m n : Nat} {a : α} : (replicate m a).rotateLeft n = replicate m a

rotateRight

@[simp]

theorem List.rotateRight_replicate {α : Type u_1} {m n : Nat} {a : α} : (replicate m a).rotateRight n = replicate m a

zipWith

@[simp]

theorem List.length_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l₁ : List α} {l₂ : List β} : (zipWith f l₁ l₂).length = min l₁.length l₂.length

theorem List.lt_length_left_of_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : Nat} {l : List α} {l' : List β} (h : i < (zipWith f l l').length) : i < l.length

theorem List.lt_length_right_of_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : Nat} {l : List α} {l' : List β} (h : i < (zipWith f l l').length) : i < l'.length

@[simp]

theorem List.getElem_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β} {i : Nat} {h : i < (zipWith f l l').length} : (zipWith f l l')[i] = f l[i] l'[i]

theorem List.zipWith_eq_zipWith_take_min {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} {l₁ : List α} {l₂ : List β} : zipWith f l₁ l₂ = zipWith f (take (min l₁.length l₂.length) l₁) (take (min l₁.length l₂.length) l₂)

theorem List.reverse_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : List α✝} {l' : List α✝¹} (h : l.length = l'.length) : (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

@[simp]

theorem List.zipWith_replicate {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} {a : α} {b : β} {m n : Nat} : zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b)

zip

@[simp]

theorem List.length_zip {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} : (l₁.zip l₂).length = min l₁.length l₂.length

theorem List.lt_length_left_of_zip {α : Type u_1} {β : Type u_2} {i : Nat} {l : List α} {l' : List β} (h : i < (l.zip l').length) : i < l.length

theorem List.lt_length_right_of_zip {α : Type u_1} {β : Type u_2} {i : Nat} {l : List α} {l' : List β} (h : i < (l.zip l').length) : i < l'.length

@[simp]

theorem List.getElem_zip {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {i : Nat} {h : i < (l.zip l').length} : (l.zip l')[i] = (l[i], l'[i])

theorem List.zip_eq_zip_take_min {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} : l₁.zip l₂ = (take (min l₁.length l₂.length) l₁).zip (take (min l₁.length l₂.length) l₂)

@[simp]

theorem List.zip_replicate {α : Type u_1} {β : Type u_2} {a : α} {b : β} {m n : Nat} : (replicate m a).zip (replicate n b) = replicate (min m n) (a, b)