@[simp]

theorem List.sequence_singleton {α : Type u_1} {xs : List α} : sequence [xs] = map (fun (x : α) => [x]) xs

@[simp]

theorem List.combinations_one {α : Type u_1} {xs : List α} : xs.combinations 1 = map (fun (x : α) => [x]) xs

theorem List.combinations_succ {α : Type u_1} {xs : List α} {n : ℕ} : xs.combinations (n + 1) = flatMap (fun (x : α) => map (fun (x_1 : List α) => x :: x_1) (xs.combinations n)) xs

@[simp]

theorem List.length_combinations {α : Type u_1} {xs : List α} {n : ℕ} : (xs.combinations n).length = xs.length ^ n

@[simp]

theorem List.mem_combinations {α : Type u_1} {xs ys : List α} {n : ℕ} : ys ∈ xs.combinations n ↔ ys.length = n ∧ ys ⊆ xs

@[simp]

theorem List.sortedLe_cons {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x : α} : (x :: xs).SortedLE ↔ (∀ y ∈ xs, x ≤ y) ∧ xs.SortedLE

@[simp]

theorem List.sortedLt_cons {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x : α} : (x :: xs).SortedLT ↔ (∀ y ∈ xs, x < y) ∧ xs.SortedLT

@[simp]

theorem List.sortedLe_snoc {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x : α} : (xs ++ [x]).SortedLE ↔ xs.SortedLE ∧ ∀ y ∈ xs, y ≤ x

@[simp]

theorem List.sortedLT_snoc {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x : α} : (xs ++ [x]).SortedLT ↔ xs.SortedLT ∧ ∀ y ∈ xs, y < x

theorem List.sortedLE_append {α : Type u_1} {xs ys : List α} [ha : LinearOrder α] : (xs ++ ys).SortedLE ↔ xs.SortedLE ∧ ys.SortedLE ∧ ∀ x ∈ xs, ∀ y ∈ ys, x ≤ y

theorem List.sortedLT_append {α : Type u_1} {xs ys : List α} [ha : LinearOrder α] : (xs ++ ys).SortedLT ↔ xs.SortedLT ∧ ys.SortedLT ∧ ∀ x ∈ xs, ∀ y ∈ ys, x < y

theorem List.head!_eq_getd_head {α : Type u_1} {xs : List α} [ha : Inhabited α] : xs.head! = xs.head?.getd

@[simp]

theorem List.head!_mem_iff {α : Type u_1} {xs : List α} [ha : Inhabited α] : xs.head! ∈ xs ↔ xs ≠ []

theorem List.head!_mem {α : Type u_1} {xs : List α} [ha : Inhabited α] (h : xs ≠ []) : xs.head! ∈ xs

theorem List.map_init {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β} : map f xs.init = (map f xs).init

theorem List.init_map {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β} : (map f xs).init = map f xs.init

theorem List.tail_map {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β} : (map f xs).tail = map f xs.tail

theorem List.tail_init {α : Type u_1} {xs : List α} : xs.init.tail = xs.tail.init

theorem List.init_tail {α : Type u_1} {xs : List α} : xs.tail.init = xs.init.tail

@[simp]

theorem List.append_lt_append_iff_right {α : Type u_1} {xs ys zs : List α} [ha : LinearOrder α] : xs ++ ys < xs ++ zs ↔ ys < zs

@[simp]

theorem List.append_le_append_iff_right {α : Type u_1} {xs ys zs : List α} [ha : LinearOrder α] : xs ++ ys ≤ xs ++ zs ↔ ys ≤ zs

theorem List.ext_getd {α : Type u_1} {xs ys : List α} [ha : Inhabited α] : xs = ys ↔ xs.length = ys.length ∧ ∀ ⦃i : ℕ⦄, i < xs.length → i < ys.length → xs[i]?.getd = ys[i]?.getd

theorem List.ext_getElem!_iff {α : Type u_1} {xs ys : List α} [ha : Inhabited α] : xs = ys ↔ xs.length = ys.length ∧ ∀ ⦃i : ℕ⦄, i < xs.length → i < ys.length → xs[i]! = ys[i]!

@[simp]

theorem List.getElem!_eq_getElem_simp {α : Type u_1} {xs : List α} [ha : Inhabited α] {i : ℕ} {h : i < xs.length} : xs[i]! = xs[i] ↔ True

@[simp]

theorem List.getElem_eq_getElem!_simp {α : Type u_1} {xs : List α} [ha : Inhabited α] {i : ℕ} {h : i < xs.length} : xs[i] = xs[i]! ↔ True

@[simp]

theorem List.mapWith_append {α : Type u_1} {β : Type u_2} {xs ys : List α} {f : (x : α) → x ∈ xs ++ ys → β} : (xs ++ ys).mapWith f = (xs.mapWith fun (x : α) (h : x ∈ xs) => f x ⋯) ++ ys.mapWith fun (x : α) (h : x ∈ ys) => f x ⋯

theorem List.eq_mapWith_getElem_range' {α : Type u_1} {xs : List α} : xs = (range xs.length).mapWith fun (i : ℕ) (h : i ∈ range xs.length) => xs[i]

theorem List.eq_mapWith_getElem_range {α : Type u_1} {xs : List α} {n : ℕ} (h : xs.length = n) : xs = (range n).mapWith fun (i : ℕ) (h_1 : i ∈ range n) => xs[i]

theorem List.length_le_sum_of {α : Type u_1} {xs : List α} [ha₁ : LinearOrder α] [ha₂ : Semiring α] [ha₃ : AddLeftMono α] (h : ∀ x ∈ xs, 1 ≤ x) : ↑xs.length ≤ xs.sum

theorem List.length_lt_sum_of {α : Type u_1} {xs : List α} [ha₁ : LinearOrder α] [ha₂ : Semiring α] [ha₃ : AddLeftMono α] : ∀ [AddLeftStrictMono α] (h₁ : ∀ x ∈ xs, 1 ≤ x) (h₂ : ∃ x ∈ xs, 1 < x), ↑xs.length < xs.sum

theorem List.mem_zip_iff {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {xy : α × β} : xy ∈ xs.zip ys ↔ ∃ (i : ℕ) (h₁ : i < xs.length) (h₂ : i < ys.length), xs[i] = xy.1 ∧ ys[i] = xy.2

@[simp]

theorem List.mem_zip_range_length_iff {α : Type u_1} {xs : List α} {xy : α × ℕ} : xy ∈ xs.zip (range xs.length) ↔ ∃ (h : xy.2 < xs.length), xs[xy.2] = xy.1

theorem List.take_eq_take_of_prefix {α : Type u_1} {xs ys : List α} {n : ℕ} (h₁ : xs <+: ys) (h₂ : n ≤ xs.length) : take n xs = take n ys

theorem List.sum_le_of_prefix {xs ys : List ℕ} (h : xs <+: ys) : xs.sum ≤ ys.sum

theorem List.sum_lt_of_prefix {xs ys : List ℕ} (h₁ : xs <+: ys) (h₂ : xs.length ≠ ys.length) (h₃ : ∃ n ∈ drop xs.length ys, n ≠ 0) : xs.sum < ys.sum

theorem List.le_max_of_le_mem {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x : α} (h : ∃ y ∈ xs, x ≤ y) : x ≤ xs.max ⋯

theorem List.foldl_eq_foldlWith' {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] {f : β → α → β} {z : β} : foldl f z xs = xs.foldlWith (fun (acc : β) (x : α) (x_1 : x ∈ xs) => f acc x) z

theorem List.foldl_eq_foldlWith {α : Type u_1} {β : Type u_2} : foldl = fun (f : β → α → β) (z : β) (xs : List α) => xs.foldlWith (fun (acc : β) (x : α) (x_1 : x ∈ xs) => f acc x) z

theorem List.foldl_dite_mem_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List α} [ha : DecidableEq α] {f : (x : α) → x ∈ xs → β} {g : γ → α → β → γ} {z : γ} (z' : β) : (fun (init : γ) => foldl (fun (acc : γ) (x : α) => if h : x ∈ xs then g acc x (f x h) else z) init xs) = fun (init : γ) => foldl (fun (acc : γ) (x : α) => g acc x (if h : x ∈ xs then f x h else z')) init xs

theorem List.foldl_dite_mem_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List α} [ha : DecidableEq α] {f : (x : α) → x ∈ xs → β} {g : γ → α → β → γ} {z z₁ : γ} (z' : β) : foldl (fun (acc : γ) (x : α) => if h : x ∈ xs then g acc x (f x h) else z) z₁ xs = foldl (fun (acc : γ) (x : α) => g acc x (if h : x ∈ xs then f x h else z')) z₁ xs

theorem List.mapWith_eq_map_attach {α : Type u_1} {β : Type u_2} {xs : List α} {f : (x : α) → x ∈ xs → β} : xs.mapWith f = map (fun (x : { x : α // x ∈ xs }) => f ↑x ⋯) xs.attach

theorem List.le_foldl_dite_max {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] [hb : LinearOrder β] {f : (x : α) → x ∈ xs → β} {x : α} {z z₁ : β} (h : x ∈ xs) : f x h ≤ foldl (fun (acc : β) (x : α) => if h : x ∈ xs then max acc (f x h) else z) z₁ xs

theorem List.flatMap_eq_flatten_map {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} : flatMap f xs = (map f xs).flatten

theorem List.foldr_fn_append_eq_flatMap {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {zs : List β} : foldr (fun (x : α) (acc : List β) => f x ++ acc) zs xs = flatMap f xs ++ zs

theorem List.map_eq_map_attach {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β} : map f xs = map (fun (x : { x : α // x ∈ xs }) => f ↑x) xs.attach

@[simp]

theorem List.getElem?_singleton_eq_some_iff {α : Type u_1} {x y : α} {i : ℕ} : [x][i]? = some y ↔ i = 0 ∧ x = y

theorem List.foldr_eq_foldl' {α : Type u_1} {xs : List α} {f : α → α → α} {z : α} [Std.Associative f] [Std.LawfulIdentity f z] : foldr f z xs = foldl f z xs

theorem List.foldr_eq_foldr_map {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β → β} {z : β} (g₁ : α → β) (g₂ : β → β → β) (h : ∀ ⦃x : α⦄ ⦃acc : β⦄, f x acc = g₂ (g₁ x) acc) : foldr f z xs = foldr g₂ z (map g₁ xs)

theorem List.foldl_eq_foldl_map {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z : β} (g₁ : α → β) (g₂ : β → β → β) (h : ∀ ⦃acc : β⦄ ⦃x : α⦄, f acc x = g₂ acc (g₁ x)) : foldl f z xs = foldl g₂ z (map g₁ xs)

@[simp]

theorem List.min!!_nil {α : Type u_1} [Top α] [Min α] : [].min!! = ⊤

@[simp]

theorem List.max!!_nil {α : Type u_1} [Bot α] [Max α] : [].max!! = ⊥

@[simp]

theorem List.min!!_cons {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] {x : α} : (x :: xs).min!! = x ⊓ xs.min!!

@[simp]

theorem List.max!!_cons {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] {x : α} : (x :: xs).max!! = x ⊔ xs.max!!

theorem List.elim_min?_eq_min!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] {f : α → α} {z : α} : xs.min?.elim z f = if xs = [] then z else f xs.min!!

theorem List.elim_max?_eq_max!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] {f : α → α} {z : α} : xs.max?.elim z f = if xs = [] then z else f xs.max!!

@[simp]

theorem List.elim_min?_id_eq_min!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] {z : α} : xs.min?.elim z id = if z = ⊤ ∨ xs ≠ [] then xs.min!! else z

@[simp]

theorem List.elim_max?_id_eq_max!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] {z : α} : xs.max?.elim z id = if z = ⊥ ∨ xs ≠ [] then xs.max!! else z

@[simp]

theorem List.min_append {α : Type u_1} {xs ys : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] : (xs ++ ys).min!! = xs.min!! ⊓ ys.min!!

@[simp]

theorem List.max_append {α : Type u_1} {xs ys : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] : (xs ++ ys).max!! = xs.max!! ⊔ ys.max!!

theorem List.min!!_eq_min {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] (h : xs ≠ []) : xs.min!! = xs.min ⋯

theorem List.max!!_eq_max {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] (h : xs ≠ []) : xs.max!! = xs.max ⋯

@[simp]

theorem List.min_cons_cons' {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] {x y : α} : (x :: y :: xs).min ⋯ = x ⊓ (y :: xs).min ⋯

@[simp]

theorem List.max_cons_cons' {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] {x y : α} : (x :: y :: xs).max ⋯ = x ⊔ (y :: xs).max ⋯

theorem List.Perm.min {α : Type u_1} {xs ys : List α} [ha₁ : SemilatticeInf α] {h₁ : xs ≠ []} {h₂ : ys ≠ []} (h : xs.Perm ys) : xs.min h₁ = ys.min h₂

theorem List.Perm.max {α : Type u_1} {xs ys : List α} [ha₁ : SemilatticeSup α] {h₁ : xs ≠ []} {h₂ : ys ≠ []} (h : xs.Perm ys) : xs.max h₁ = ys.max h₂

theorem List.Perm.min!! {α : Type u_1} {xs ys : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] (h : xs.Perm ys) : xs.min!! = ys.min!!

theorem List.Perm.max!! {α : Type u_1} {xs ys : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] (h : xs.Perm ys) : xs.max!! = ys.max!!

@[simp]

theorem List.min!!_reverse {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] : xs.reverse.min!! = xs.min!!

@[simp]

theorem List.max!!_reverse {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] : xs.reverse.max!! = xs.max!!

@[simp]

theorem List.foldr_min_eq_min!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] {z : α} : foldr min z xs = z ⊓ xs.min!!

@[simp]

theorem List.foldr_max_eq_max!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] {z : α} : foldr max z xs = z ⊔ xs.max!!

@[simp]

theorem List.foldl_min_eq_min!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] {z : α} : foldl min z xs = z ⊓ xs.min!!

@[simp]

theorem List.foldl_max_eq_max!! {α : Type u_1} {xs : List α} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] {z : α} : foldl max z xs = z ⊔ xs.max!!

theorem List.min!!_flatten {α : Type u_1} [ha₁ : SemilatticeInf α] [ha₂ : OrderTop α] {L : List (List α)} : L.flatten.min!! = (map min!! L).min!!

theorem List.max!!_flatten {α : Type u_1} [ha₁ : SemilatticeSup α] [ha₂ : OrderBot α] {L : List (List α)} : L.flatten.max!! = (map max!! L).max!!

theorem List.min!!_flatMap {α : Type u_1} {β : Type u_2} {xs : List α} [hb₁ : SemilatticeInf β] [hb₂ : OrderTop β] {f : α → List β} : (flatMap f xs).min!! = (map (fun (x : α) => (f x).min!!) xs).min!!

theorem List.max!!_flatMap {α : Type u_1} {β : Type u_2} {xs : List α} [hb₁ : SemilatticeSup β] [hb₂ : OrderBot β] {f : α → List β} : (flatMap f xs).max!! = (map (fun (x : α) => (f x).max!!) xs).max!!

theorem List.range_add' {n m : ℕ} : range (n + m) = range m ++ map (fun (x : ℕ) => m + x) (range n)

theorem List.range_succ' {n : ℕ} : range (n + 1) = 0 :: map (fun (x : ℕ) => x + 1) (range n)

@[simp]

theorem List.map_getElem!_range_length {α : Type u_1} {xs : List α} [ha : Inhabited α] : map (fun (x : ℕ) => xs[x]!) (range xs.length) = xs

theorem List.map_getElem!_range_of_le_length {α : Type u_1} {xs : List α} [ha : Inhabited α] {n : ℕ} (h : n ≤ xs.length) : map (fun (x : ℕ) => xs[x]!) (range n) = take n xs

theorem List.map_getElem!_range_of_length_le {α : Type u_1} {xs : List α} [ha : Inhabited α] {n : ℕ} (h : xs.length ≤ n) : map (fun (x : ℕ) => xs[x]!) (range n) = xs ++ replicate (n - xs.length) default

theorem List.map_getElem!_range {α : Type u_1} {xs : List α} [ha : Inhabited α] {n : ℕ} : map (fun (x : ℕ) => xs[x]!) (range n) = take n xs ++ replicate (n - xs.length) default

theorem List.foldr_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List α} {f : α → β → β} {z : β} (g₁ : β → γ) (g₂ : γ → β) (h : ∀ ⦃x : β⦄, g₂ (g₁ x) = x) : foldr f z xs = g₂ (foldr (fun (x : α) (acc : γ) => g₁ (f x (g₂ acc))) (g₁ z) xs)

theorem List.foldl_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List α} {f : β → α → β} {z : β} (g₁ : β → γ) (g₂ : γ → β) (h : ∀ ⦃x : β⦄, g₂ (g₁ x) = x) : foldl f z xs = g₂ (foldl (fun (acc : γ) (x : α) => g₁ (f (g₂ acc) x)) (g₁ z) xs)

@[simp]

theorem List.take_take_same {α : Type u_1} {xs : List α} {n : ℕ} : take n (take n xs) = take n xs

@[simp]

theorem List.nodup_filter_range {n : ℕ} {p : ℕ → Bool} : (filter p (range n)).Nodup

theorem List.sortedLE.filter {α : Type u_1} {xs : List α} [ha : LinearOrder α] {p : α → Bool} (h : xs.SortedLE) : (List.filter p xs).SortedLE

theorem List.sortedLT.filter {α : Type u_1} {xs : List α} [ha : LinearOrder α] {p : α → Bool} (h : xs.SortedLT) : (List.filter p xs).SortedLT

@[simp]

theorem List.sortedLE_range {n : ℕ} : (range n).SortedLE

@[simp]

theorem List.sortedLE_filter_range {n : ℕ} {p : ℕ → Bool} : (filter p (range n)).SortedLE

@[simp]

theorem List.sortedLT_filter_range {n : ℕ} {p : ℕ → Bool} : (filter p (range n)).SortedLT

@[simp]

theorem List.filter_eq_filter {α : Type u_1} {xs : List α} {p q : α → Bool} : filter p xs = filter q xs ↔ ∀ x ∈ xs, p x = true ↔ q x = true

theorem List.filter_eq_filter_of' {α : Type u_1} {xs ys : List α} {p : α → Bool} (q : α → Prop) (h₁ : ys = filter (fun (b : α) => decide (q b)) xs) (h₂ : ∀ x ∈ xs, p x = true → q x) : filter p xs = filter p ys

theorem List.filter_and {α : Type u_1} {xs : List α} {p q : α → Bool} : filter (fun (x : α) => p x && q x) xs = filter p (filter q xs)

theorem List.filter_and' {α : Type u_1} {xs : List α} {p q : α → Bool} : filter (fun (x : α) => p x && q x) xs = filter q (filter p xs)

theorem List.filter_eq_self_of {α : Type u_1} {xs : List α} {p : α → Bool} (h : ∀ x ∈ xs, p x = true) : filter p xs = xs

theorem List.suffix_antisymm {α : Type u_4} {xs ys : List α} (h₁ : xs <:+ ys) (h₂ : ys <:+ xs) : xs = ys

@[simp]

theorem List.drop_eq_self_iff {α : Type u_1} {xs : List α} {n : ℕ} : drop n xs = xs ↔ n = 0 ∨ xs.length = 0

@[simp]

theorem List.drop_length_add {α : Type u_1} {xs : List α} {n : ℕ} : drop (xs.length + n) xs = []

@[simp]

theorem List.drop_add_length {α : Type u_1} {xs : List α} {n : ℕ} : drop (n + xs.length) xs = []

theorem List.length_ge_iff_left {α : Type u_1} {xs : List α} {n : ℕ} : n ≤ xs.length ↔ ∃ (ys : List α) (zs : List α), ys.length = n ∧ xs = ys ++ zs

theorem List.length_ge_iff_right {α : Type u_1} {xs : List α} {n : ℕ} : n ≤ xs.length ↔ ∃ (ys : List α) (zs : List α), zs.length = n ∧ xs = ys ++ zs

@[simp]

theorem List.length_mkList {α : Type u_1} {n : ℕ} {f : ℕ → α} : (mkList n f).length = n

@[simp]

theorem List.mem_mkList {α : Type u_1} {n : ℕ} {f : ℕ → α} {x : α} : x ∈ mkList n f ↔ ∃ i < n, f i = x

theorem List.mergeSort_eq_mergeSort_iff {α : Type u_1} {xs ys : List α} {le : α → α → Bool} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) (antisymm : ∀ (a b : α), le a b = true → le b a = true → a = b) : xs.mergeSort le = ys.mergeSort le ↔ xs.Perm ys

@[simp]

theorem List.map_mkList {α : Type u_1} {β : Type u_2} {n : ℕ} {f : ℕ → α} {g : α → β} : map g (mkList n f) = mkList n fun (i : ℕ) => g (f i)

@[simp]

theorem List.getElem_mkList {α : Type u_1} {n : ℕ} {f : ℕ → α} {i : ℕ} {h : i < (mkList n f).length} : (mkList n f)[i] = f i

@[simp]

theorem List.mkList_length_getElem! {α : Type u_1} {xs : List α} [ha : Inhabited α] : (mkList xs.length fun (x : ℕ) => xs[x]!) = xs

theorem List.find?_eq_some_iff_of_nodup {α : Type u_1} {β : Type u_2} {xs : List α} [H : DecidableEq β] {f : α → β} {x : α} {y : β} (h : (map f xs).Nodup) : find? (fun (x : α) => decide (f x = y)) xs = some x ↔ x ∈ xs ∧ f x = y

theorem List.find?_eq_none_of {α : Type u_1} {xs : List α} {p : α → Bool} (h : ∀ x ∈ xs, p x = false) : find? p xs = none

theorem List.Perm.comm {α : Type u_1} {xs ys : List α} : xs.Perm ys ↔ ys.Perm xs

theorem List.perm_append_comm_left {α : Type u_1} {xs ys zs : List α} : (xs ++ ys).Perm zs ↔ (ys ++ xs).Perm zs

theorem List.perm_append_comm_right {α : Type u_1} {xs ys zs : List α} : zs.Perm (xs ++ ys) ↔ zs.Perm (ys ++ xs)

@[simp]

theorem List.append_mergeSort_perm {α : Type u_1} {xs ys zs : List α} [ha : LinearOrder α] : (xs ++ ys.mergeSort fun (a b : α) => decide (a ≤ b)).Perm zs ↔ (xs ++ ys).Perm zs

@[simp]

theorem List.mergeSort_append_perm {α : Type u_1} {xs ys zs : List α} [ha : LinearOrder α] : ((xs.mergeSort fun (a b : α) => decide (a ≤ b)) ++ ys).Perm zs ↔ (xs ++ ys).Perm zs

@[simp]

theorem List.mergeSort_two {α : Type u_1} {x y : α} {le : α → α → Bool} : [x, y].mergeSort le = if le x y = true then [x, y] else [y, x]

theorem List.length_eq_succ_iff_append {α : Type u_1} {xs : List α} {n : ℕ} : xs.length = n + 1 ↔ ∃ (x : α) (ys : List α) (zs : List α), xs = ys ++ x :: zs ∧ ys.length + zs.length = n

theorem List.exi_append {α : Type u_1} {xs : List α} (i : ℕ) (h : i ≤ xs.length) : ∃ (ys : List α) (zs : List α), xs = ys ++ zs ∧ ys.length = i

theorem List.exi_append_cons {α : Type u_1} {xs : List α} (i : ℕ) (h : i < xs.length) : ∃ (x : α) (ys : List α) (zs : List α), xs = ys ++ x :: zs ∧ ys.length = i

@[simp]

theorem List.forall_length_eq_succ_imp {α : Type u_1} {p : List α → Prop} {n : ℕ} : (∀ (xs : List α), xs.length = n + 1 → p xs) ↔ ∀ (x : α) (xs : List α), xs.length = n → p (x :: xs)

@[simp]

theorem List.forall_length_eq_succ_imp_and {α : Type u_1} {p q : List α → Prop} {n : ℕ} : (∀ (xs : List α), (xs.length = n + 1 → p xs) ∧ q xs) ↔ (∀ (x : α) (xs : List α), xs.length = n → p (x :: xs)) ∧ ∀ (xs : List α), q xs