theorem List.getElem_mem_dropLast {α : Type u_1} {l : List α} {i : ℕ} (hi : i < l.length - 1) : l[i] ∈ l.dropLast

theorem List.Nodup.countP_eq_card {α : Type u_2} {l : List α} {P : α → Prop} [DecidableEq α] [DecidablePred P] (h : l.Nodup) : countP (fun (b : α) => decide (P b)) l = (Finset.filter P l.toFinset).card

theorem List.Nodup.eq_singleton_iff_head_getLast {α : Type u_2} {l : List α} (hnd : l.Nodup) (hne : l ≠ []) : l.head hne = l.getLast hne ↔ ∃ (x : α), l = [x]

theorem List.Nodup.head_notMem_tail {α : Type u_1} {l : List α} (hl : l.Nodup) {hne : l ≠ []} : l.head hne ∉ l.tail

theorem List.eq_of_length_eq_zero {α : Type u_2} {l : List α} (h : l.length = 0) : l = []

theorem List.eq_of_length_eq_one {α : Type u_2} {l : List α} (h : l.length = 1) : l = [l[0]]

theorem List.eq_of_length_eq_two {α : Type u_2} {l : List α} (h : l.length = 2) : l = [l[0], l[1]]

theorem List.eq_of_length_eq_three {α : Type u_2} {l : List α} (h : l.length = 3) : l = [l[0], l[1], l[2]]

theorem List.eq_of_map_eq_map {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → β} (h : map f l = map f l') (hinj : Set.InjOn f {x : α | x ∈ l ∨ x ∈ l'}) : l = l'

theorem List.mem_dropLast_iff {ι : Type u_2} {x : ι} {l : List ι} (hnd : l.Nodup) (hne : l ≠ []) : x ∈ l.dropLast ↔ x ∈ l ∧ x ≠ l.getLast hne

theorem List.mem_dropLast_of_mem_ne {ι : Type u_2} {x : ι} {l : List ι} (hne : l ≠ []) (hmem : x ∈ l) (hxne : x ≠ l.getLast hne) : x ∈ l.dropLast

theorem List.mem_iff_eq_head_or_mem_tail {α : Type u_2} {x : α} {l : List α} (hne : l ≠ []) : x ∈ l ↔ x = l.head hne ∨ x ∈ l.tail

theorem List.mem_iff_mem_dropLast_or_eq_getLast {α : Type u_2} {x : α} {l : List α} (hne : l ≠ []) : x ∈ l ↔ x ∈ l.dropLast ∨ x = l.getLast hne

theorem List.Nodup.eq_head_or_mem_tail_ne {α : Type u_2} {x : α} {l : List α} (hnd : l.Nodup) (hx : x ∈ l) : x = l.head ⋯ ∨ x ≠ l.head ⋯ ∧ x ∈ l.tail

theorem List.Nodup.mem_iff_eq_head_or_mem_tail {α : Type u_2} {x : α} {l : List α} (hnd : l.Nodup) (hne : l ≠ []) : x ∈ l ↔ x = l.head hne ∨ x ≠ l.head hne ∧ x ∈ l.tail

theorem List.Nodup.eq_getLast_or_mem_dropLast_ne {α : Type u_2} {x : α} {l : List α} (hnd : l.Nodup) (hx : x ∈ l) : x = l.getLast ⋯ ∨ x ≠ l.getLast ⋯ ∧ x ∈ l.dropLast

theorem List.Nodup.mem_iff_eq_getLast_or_mem_dropLast {α : Type u_2} {x : α} {l : List α} (hnd : l.Nodup) (hne : l ≠ []) : x ∈ l ↔ x = l.getLast hne ∨ x ≠ l.getLast hne ∧ x ∈ l.dropLast

@[simp]

theorem List.toSet_nonempty_iff {α : Type u_1} {l : List α} : {e : α | e ∈ l}.Nonempty ↔ l ≠ []

theorem List.Nodup.toSet_eq_of_subset_of_length_ge {α : Type u_1} {l l' : List α} (hl : l.Nodup) (hss : l ⊆ l') (hlen : l'.length ≤ l.length) : {x : α | x ∈ l} = {x : α | x ∈ l'}

theorem List.IsSuffix.eq_of_first_mem {α : Type u_2} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (hnd : l₂.Nodup) (hne : l₂ ≠ []) (hl : l₂.head hne ∈ l₁) : l₁ = l₂

theorem List.IsPrefix.eq_of_last_mem {α : Type u_2} {l₁ l₂ : List α} (h : l₁ <+: l₂) (hnd : l₂.Nodup) (hne : l₂ ≠ []) (hl : l₂.getLast hne ∈ l₁) : l₁ = l₂

theorem List.IsPrefix.tail {α : Type u_2} {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.tail <+: l₂.tail

theorem List.IsPrefix.dropLast {α : Type u_2} {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.dropLast <+: l₂.dropLast

theorem List.IsSuffix.dropLast {α : Type u_2} {l₁ l₂ : List α} (h : l₁ <:+ l₂) : l₁.dropLast <:+ l₂.dropLast

theorem List.IsSuffix.drop {α : Type u_2} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (n : ℕ) : List.drop n l₁ <:+ List.drop n l₂

theorem List.IsSuffix.tail {α : Type u_2} {l₁ l₂ : List α} (h : l₁ <:+ l₂) : l₁.tail <:+ l₂.tail

theorem List.isChain_iff_all_zip_tail {α : Type u_2} (r : α → α → Prop) (l : List α) : IsChain r l ↔ ∀ x ∈ l.zip l.tail, r x.1 x.2

@[simp]

theorem List.isChain_and_iff {α : Type u_2} (r s : α → α → Prop) (l : List α) : IsChain (fun (x y : α) => r x y ∧ s x y) l ↔ IsChain r l ∧ IsChain s l

theorem List.findIdxs_sublist_range {α : Type u_1} (xs : List α) (p : α → Bool) : (findIdxs p xs).Sublist (range xs.length)

@[simp]

theorem List.findIxs_length {α : Type u_1} (xs : List α) (p : α → Bool) : (findIdxs p xs).length = (filter p xs).length

theorem List.range_three : range 3 = [0, 1, 2]

theorem List.range_add_one {n : ℕ} : range (n + 1) = range n ++ [n]

theorem List.range'_suffix_add (a b : ℕ) : range' a b <:+ range (a + b)

theorem List.range'_suffix (a b : ℕ) : range' a (b - a) <:+ range b

theorem List.range_prefix {a b : ℕ} (hab : a ≤ b) : range a <+: range b

theorem List.range'_sub_infix (a : ℕ) {b n : ℕ} (hbn : b ≤ n) : range' a (b - a) <:+: range n

theorem List.range'_infix {a b n : ℕ} (h : a + b ≤ n) : range' a b <:+: range n

@[simp]

theorem List.map_toFinset {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] (L : List α) (f : α → β) : (map f L).toFinset = Finset.image f L.toFinset

theorem List.map_toFinset_embedding {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] (L : List α) (f : α ↪ β) : (map (⇑f) L).toFinset = Finset.map f L.toFinset

theorem List.cons_range'_add_one (a b : ℕ) : a :: range' (a + 1) b = range' a (b + 1)

theorem List.cons_range'_sub_add_one {a b : ℕ} (hab : a < b) : a :: range' (a + 1) (b - (a + 1)) = range' a (b - a)

theorem List.range'_sub_add_one {a b : ℕ} (hab : a ≤ b) : range' a (b + 1 - a) = range' a (b - a) ++ [b]

theorem List.prefix_suffix_sublist {α : Type u_1} {A B L : List α} (hA : A <+: L) (hB : B <:+ L) (hAB : A.length + B.length ≤ L.length) : (A ++ B).Sublist L

theorem List.exists_eq_or_eq_concat_of_sublist_range_add_one {L : List ℕ} {n : ℕ} (h : L.Sublist (range (n + 1))) : ∃ (L₀ : List ℕ), L₀.Sublist (range n) ∧ (L = L₀ ∨ L = L₀ ++ [n])

theorem List.zipIdx_take {α : Type u_1} (L : List α) (k i : ℕ) : take k (L.zipIdx i) = (take k L).zipIdx i

theorem List.Subset.toFinset_subset {α : Type u_1} [DecidableEq α] {a b : List α} (hab : a ⊆ b) : a.toFinset ⊆ b.toFinset

@[simp]

theorem List.toFinset_range (n : ℕ) : (range n).toFinset = Finset.range n

theorem List.setOf_two {α : Type u_1} {a b : α} : {x : α | x ∈ [a, b]} = {a, b}

theorem List.setOf_three {α : Type u_1} {a b c : α} : {x : α | x ∈ [a, b, c]} = {a, b, c}

theorem List.setOf_four {α : Type u_1} {a b c d : α} : {x : α | x ∈ [a, b, c, d]} = {a, b, c, d}

theorem List.append_arc {α : Type u_1} (L : List α) (x y : α) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hsum : d + e = L.length) (hx : L.head? = some x) (hy : L[d] = y) : x :: (take (d - 1) L.tail ++ y :: (take (e - 1) (drop d L ++ take d L).tail ++ [x])) = L ++ [x]

Reassembling a list cut at index d: the head, the first arc, the element at d, the second arc read cyclically, and the head again, concatenate to the list closed up. Used to show that the two arcs of a polygon between two vertices cover it.

theorem List.getElem_reverse' {α : Type u_1} {l : List α} {i j : ℕ} (hij : i + j + 1 = l.length) : l.reverse[i] = l[j]

theorem List.toSet_cons_eq {α : Type u_1} {l : List α} {a : α} : {x : α | x ∈ a :: l} = insert a {x : α | x ∈ l}

theorem List.toSet_concat_eq {α : Type u_1} {l : List α} {a : α} : {x : α | x ∈ l ++ [a]} = insert a {x : α | x ∈ l}

theorem List.toSet_append_eq {α : Type u_1} {l l' : List α} : {x : α | x ∈ l ++ l'} = {x : α | x ∈ l} ∪ {x : α | x ∈ l'}

theorem List.Nodup.toSet_tail_eq {α : Type u_1} {l : List α} (hl : l.Nodup) (h0 : l ≠ []) : {x : α | x ∈ l.tail} = {x : α | x ∈ l} \ {l.head h0}

theorem List.Nodup.toSet_dropLast_eq {α : Type u_1} {l : List α} (hl : l.Nodup) (h0 : l ≠ []) : {x : α | x ∈ l.dropLast} = {x : α | x ∈ l} \ {l.getLast h0}

theorem List.Nodup.getLast_not_mem_dropLast {α : Type u_1} {l : List α} (hnd : l.Nodup) (hne : l ≠ []) : l.getLast hne ∉ l.dropLast

theorem List.nodup_map_iff_of_injOn {α : Type u_1} {L : List α} {β : Type u_2} {f : α → β} (hf : ∀ x ∈ L, ∀ y ∈ L, f x = f y → x = y) : (map f L).Nodup ↔ L.Nodup

theorem List.get_map {α : Type u_1} {β : Type u_2} {f : α → β} (L : List α) (i : Fin (map f L).length) : (map f L).get i = f (L.get (Fin.cast ⋯ i))

theorem List.get_map_image {α : Type u_1} {β : Type u_2} {f : α → β} (L : List α) (s : Set (Fin (map f L).length)) : (map f L).get '' s = f '' L.get '' Fin.cast ⋯ '' s

theorem List.toSet_map {α : Type u_1} {β : Type u_2} {f : α → β} (L : List α) : {e : β | e ∈ map f L} = f '' {e : α | e ∈ L}