theorem List.init_cons_of_ne_nil {α : Type u_4} {x : α} {xs : List α} (h : xs ≠ []) : (x :: xs).init = x :: xs.init

@[simp]

theorem List.init_snoc {α : Type u_1} {xs : List α} {x : α} : (xs ++ [x]).init = xs

@[simp]

theorem List.snoc_inj {α : Type u_4} {xs ys : List α} {x y : α} : xs ++ [x] = ys ++ [y] ↔ xs = ys ∧ x = y

@[simp]

theorem List.not_mem_failure {α : Type u_4} {x : α} : x ∉ failure

@[simp]

theorem List.unit_mem_guard_iff {P : Prop} [Decidable P] : () ∈ guard P ↔ P

theorem List.eq_of_prefix_and_length_eq {α : Type u_1} {xs ys zs : List α} (hx : xs <+: zs) (hy : ys <+: zs) (hn : xs.length = ys.length) : xs = ys

theorem List.eq_of_suffix_and_length_eq {α : Type u_1} {xs ys zs : List α} (hx : xs <:+ zs) (hy : ys <:+ zs) (hn : xs.length = ys.length) : xs = ys

theorem List.prefix_of_prefix_snoc_and_ne {α : Type u_4} {xs ys : List α} {y : α} (h₁ : xs <+: ys ++ [y]) (h₂ : xs ≠ ys ++ [y]) : xs <+: ys

@[simp]

theorem List.append_prefix_left_iff {α : Type u_4} {xs ys : List α} : xs ++ ys <+: xs ↔ ys = []

@[simp]

theorem List.prefix_snoc_iff {α : Type u_4} {xs ys : List α} {y : α} : xs <+: ys ++ [y] ↔ xs <+: ys ∨ xs = ys ++ [y]

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

theorem List.take_length_eq_of_prefix {α : Type u_4} {xs ys : List α} (h₁ : ys <+: xs) : take ys.length xs = ys

@[simp]

theorem List.nodup_inits {α : Type u_1} {xs : List α} : xs.inits.Nodup

theorem List.length_takeWhile_le {α : Type u_4} {P : α → Bool} {xs : List α} : (takeWhile P xs).length ≤ xs.length

theorem List.not_apply_of_takeWhile_append_cons_eq_self {α : Type u_4} {xs ys : List α} {P : α → Bool} {y : α} (h : takeWhile P xs ++ y :: ys = xs) : P y = false

theorem List.exists_takeWhile_eq {α : Type u_4} (xs : List α) (P : α → Bool) : ∃ k ≤ xs.length, takeWhile P xs = take k xs ∧ (∀ x ∈ take k xs, P x = true) ∧ ∀ (h : k < xs.length), P xs[k] = false

theorem List.suffix_cons_of_suffix {α : Type u_4} {xs ys : List α} {y : α} (h : xs <:+ ys) : xs <:+ y :: ys

@[simp]

theorem List.not_cons_suffix {α : Type u_1} {xs : List α} {x : α} : ¬x :: xs <:+ xs

theorem List.perm_swap_left {α : Type u_4} {xs ys : List α} {x y : α} : (x :: y :: xs).Perm ys ↔ (y :: x :: xs).Perm ys

theorem List.perm_swap_right {α : Type u_4} {xs ys : List α} {x y : α} : xs.Perm (x :: y :: ys) ↔ xs.Perm (y :: x :: ys)

@[simp]

theorem List.count_mergeSort {α : Type u_4} [ha : DecidableEq α] {xs : List α} {x : α} {r : α → α → Bool} : count x (xs.mergeSort r) = count x xs

theorem List.count_eq_count_unattach {α : Type u_4} [ha : DecidableEq α] {xs : List α} {ys : List { x : α // x ∈ xs }} {x : { x : α // x ∈ xs }} : count x ys = count (↑x) ys.unattach

theorem List.count_unattach_eq_ite {α : Type u_4} [ha : DecidableEq α] {xs : List α} {ys : List { x : α // x ∈ xs }} {x : α} : count x ys.unattach = if h : x ∈ xs then count ⟨x, h⟩ ys else 0

theorem List.mergeSort_attach_perm {α : Type u_1} {xs : List α} {r : α → α → Bool} : (xs.attach.mergeSort fun (x1 x2 : { x : α // x ∈ xs }) => r ↑x1 ↑x2).unattach.Perm (xs.mergeSort r)

@[simp]

theorem List.pairwise_unattach {α : Type u_4} {xs : List α} {ys : List { x : α // x ∈ xs }} {r : α → α → Prop} : Pairwise r ys.unattach ↔ Pairwise (fun (x1 x2 : { x : α // x ∈ xs }) => r ↑x1 ↑x2) ys

theorem List.mergeSort_attach {α : Type u_1} {xs : List α} {r : α → α → Bool} : (xs.attach.mergeSort fun (x1 x2 : { x : α // x ∈ xs }) => r ↑x1 ↑x2).unattach = xs.mergeSort r

theorem List.eq_of_perm_of_pairwise {α : Type u_4} {xs ys : List α} {r : α → α → Prop} (hp : xs.Perm ys) (hx : Pairwise r xs) (hy : Pairwise r ys) (h_tra : ∀ (a b c : α), a ∈ xs → b ∈ xs → c ∈ xs → r a b → r b c → r a c) (h_tot : ∀ (a b : α), a ∈ xs → b ∈ xs → r a b ∨ r b a) (h_ant : ∀ (a b : α), a ∈ xs → b ∈ xs → r a b → r b a → a = b) : xs = ys

theorem List.pairwise_mergeSort_loc' {α : Type u_1} {xs : List α} {r : α → α → Bool} (h_tra : ∀ (a b c : α), a ∈ xs → b ∈ xs → c ∈ xs → r a b = true → r b c = true → r a c = true) (h_tot : ∀ (a b : α), a ∈ xs → b ∈ xs → r a b = true ∨ r b a = true) : Pairwise (fun (x1 x2 : α) => r x1 x2 = true) (xs.mergeSort r)

theorem List.pairwise_mergeSort_loc {α : Type u_1} {xs : List α} {r : α → α → Prop} [hr : DecidableRel r] (h_tra : ∀ (a b c : α), a ∈ xs → b ∈ xs → c ∈ xs → r a b → r b c → r a c) (h_tot : ∀ (a b : α), a ∈ xs → b ∈ xs → r a b ∨ r b a) : Pairwise r (xs.mergeSort fun (x1 x2 : α) => decide (r x1 x2))

theorem List.eq_iff_of_nodup_and_pairwise {α : Type u_4} (r : α → α → Prop) {xs ys : List α} (hx₁ : xs.Nodup) (hy₁ : ys.Nodup) (h_ant : ∀ (a b : α), a ∈ xs → b ∈ xs → r a b → r b a → a = b) (hx₂ : Pairwise r xs) (hy₂ : Pairwise r ys) : xs = ys ↔ ∀ (x : α), x ∈ xs ↔ x ∈ ys

theorem List.eq_iff_of_nodup_and_pairwise' {α : Type u_4} [ha : LinearOrder α] {xs ys : List α} (hx₁ : xs.Nodup) (hy₁ : ys.Nodup) (hx₂ : Pairwise (fun (x1 x2 : α) => x1 ≤ x2) xs) (hy₂ : Pairwise (fun (x1 x2 : α) => x1 ≤ x2) ys) : xs = ys ↔ ∀ (x : α), x ∈ xs ↔ x ∈ ys

@[simp]

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

@[simp]

theorem List.mergeSort_perm' {α : Type u_1} {xs : List α} {r : α → α → Bool} : (xs.mergeSort r).Perm xs

@[simp]

theorem List.perm_mergeSort {α : Type u_1} {xs : List α} {r : α → α → Bool} : xs.Perm (xs.mergeSort r)

theorem List.perm_of_mergeSort_perm_mergeSort {α : Type u_4} {xs ys : List α} {r₁ r₂ : α → α → Bool} (h : (xs.mergeSort r₁).Perm (ys.mergeSort r₂)) : xs.Perm ys

theorem List.perm_of_mergeSort_eq_mergeSort {α : Type u_4} {xs ys : List α} {r₁ r₂ : α → α → Bool} (h : xs.mergeSort r₁ = ys.mergeSort r₂) : xs.Perm ys

@[simp]

theorem List.mergeSort_eq_nil_iff {α : Type u_1} {xs : List α} {r : α → α → Bool} : xs.mergeSort r = [] ↔ xs = []

theorem List.foldl_eq_foldl_of_perm {α : Type u_4} {β : Type u_5} {f : β → α → β} {z : β} {xs ys : List α} (h_assoc : ∀ {acc : β} {x y : α}, x ∈ xs ∧ y ∈ xs ∨ x ∈ ys ∧ y ∈ ys → f (f acc x) y = f (f acc y) x) (h : xs.Perm ys) : foldl f z xs = foldl f z ys

theorem List.foldl_bool_to_prop {α : Type u_4} {xs : List α} {f : Bool → α → Bool} {z : Bool} : foldl f z xs = decide (foldl (fun (acc : Prop) (x : α) => f (decide acc) x = true) (z = true) xs)

@[simp]

theorem List.snoc_perm_iff {α : Type u_4} {xs ys : List α} {x : α} : (xs ++ [x]).Perm ys ↔ (x :: xs).Perm ys

@[simp]

theorem List.perm_snoc_iff {α : Type u_4} {xs ys : List α} {y : α} : xs.Perm (ys ++ [y]) ↔ xs.Perm (y :: ys)

@[simp]

theorem List.cons_reverse_perm_iff {α : Type u_4} {xs ys : List α} {x : α} : (x :: xs.reverse).Perm ys ↔ (x :: xs).Perm ys

@[simp]

theorem List.perm_cons_reverse_iff {α : Type u_4} {xs ys : List α} {y : α} : xs.Perm (y :: ys.reverse) ↔ xs.Perm (y :: ys)

theorem List.mem_iff_mem_iff_subset {α : Type u_4} {xs ys : List α} : (∀ (x : α), x ∈ xs ↔ x ∈ ys) ↔ xs ⊆ ys ∧ ys ⊆ xs

theorem List.perm_iff_subset_of_nodup {α : Type u_4} {xs ys : List α} (hx : xs.Nodup) (hy : ys.Nodup) : xs.Perm ys ↔ xs ⊆ ys ∧ ys ⊆ xs

@[simp]

theorem List.nil_subset' {α : Type u_1} {xs : List α} : [] ⊆ xs

theorem List.perm_of_nodup_and_subperm_and_length_eq {α : Type u_4} {xs ys : List α} (h₁ : xs.Subperm ys) (h₂ : xs.length = ys.length) : ys.Perm xs

theorem List.subset_iff_subperm_of_nodup {α : Type u_4} {xs ys : List α} (h : xs.Nodup) : xs ⊆ ys ↔ xs.Subperm ys

theorem List.nodup_of_nodup_and_subset_and_length_eq {α : Type u_4} {xs ys : List α} (h₁ : xs.Nodup) (h₂ : xs ⊆ ys) (h₃ : xs.length = ys.length) : ys.Nodup

theorem List.perm_iff_mem_iff_of_nodup {α : Type u_4} {xs ys : List α} (hx : xs.Nodup) (hy : ys.Nodup) : xs.Perm ys ↔ ∀ (x : α), x ∈ xs ↔ x ∈ ys

theorem List.subset_iff_exi_get {α : Type u_4} {xs ys : List α} : xs ⊆ ys ↔ ∀ x ∈ xs, ∃ (i : ℕ) (x_1 : i < ys.length), ys[i] = x

theorem List.exi_get_iff_subset {α : Type u_4} {xs ys : List α} : (∀ x ∈ xs, ∃ (i : ℕ) (x_1 : i < ys.length), ys[i] = x) ↔ xs ⊆ ys

instance List.instIsEquivPerm_projects {α : Type u_4} : IsEquiv (List α) Perm

@[simp]

theorem List.mergeSort_perm_mergeSort {α : Type u_4} {r₁ r₂ : α → α → Bool} {xs ys : List α} : (xs.mergeSort r₁).Perm (ys.mergeSort r₂) ↔ xs.Perm ys

theorem List.eq_nil_of_isEmpty {α : Type u_4} [ha : IsEmpty α] {xs : List α} : xs = []

@[simp]

theorem List.atMostOne_nil : [].atMostOne = true

@[simp]

theorem List.atMostOne_singleton {b : Bool} : [b].atMostOne = true

@[simp]

theorem List.atMostOne_true_succ {bs : List Bool} : (true :: bs).atMostOne = !bs.or

@[simp]

theorem List.atMostOne_false_succ {bs : List Bool} : (false :: bs).atMostOne = bs.atMostOne

@[simp]

theorem List.atMostOne_pair {b₁ b₂ : Bool} : [b₁, b₂].atMostOne = (!b₁ || !b₂)

@[simp]

theorem List.nodup_snoc {α : Type u_1} {xs : List α} {x : α} : (xs ++ [x]).Nodup ↔ x ∉ xs ∧ xs.Nodup

@[simp]

theorem List.pairwise_snoc {α : Type u_1} {xs : List α} {x : α} {p : α → α → Prop} : Pairwise p (xs ++ [x]) ↔ Pairwise p xs ∧ ∀ y ∈ xs, p y x

theorem List.filterMap_eq {α : Type u_1} {β : Type u_2} {xs : List α} [hb : Inhabited β] {f : α → Option β} : filterMap f xs = map Option.get! (filter Option.isSome (map f xs))

theorem List.foldl_some_some {α : Type u_1} {xs : List α} {f : α → α → α} {z : α} : foldl (fun (acc : Option α) (x : α) => some (acc.elim x fun (x_1 : α) => f x_1 x)) (some z) xs = some (foldl f z xs)

theorem List.min?_eq_foldl {α : Type u_1} {xs : List α} [ha : LinearOrder α] : xs.min? = foldl (fun (acc : Option α) (x : α) => some (acc.elim x fun (x_1 : α) => min x_1 x)) none xs

theorem List.max?_eq_foldl {α : Type u_1} {xs : List α} [ha : LinearOrder α] : xs.max? = foldl (fun (acc : Option α) (x : α) => some (acc.elim x fun (x_1 : α) => max x_1 x)) none xs

theorem List.foldl_comm {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z : β} {x : α} (h_assoc : ∀ {x : β} {y z : α}, f (f x y) z = f (f x z) y) : foldl f (f z x) xs = f (foldl f z xs) x

theorem List.foldl_append_comm {α : Type u_1} {β : Type u_2} {xs ys : List α} {f : β → α → β} {z : β} (h_assoc : ∀ {x : β} {y z : α}, f (f x y) z = f (f x z) y) : foldl f z (xs ++ ys) = foldl f z (ys ++ xs)

theorem List.min?_append_comm {α : Type u_1} {xs : List α} [ha : LinearOrder α] {ys : List α} : (xs ++ ys).min? = (ys ++ xs).min?

theorem List.max?_append_comm {α : Type u_1} {xs : List α} [ha : LinearOrder α] {ys : List α} : (xs ++ ys).max? = (ys ++ xs).max?

@[simp]

theorem List.min?_reverse {α : Type u_1} {xs : List α} [ha : LinearOrder α] : xs.reverse.min? = xs.min?

@[simp]

theorem List.max?_reverse {α : Type u_1} {xs : List α} [ha : LinearOrder α] : xs.reverse.max? = xs.max?

theorem List.max?_eq_getLast? {α : Type u_1} {xs : List α} [ha : LinearOrder α] (h : xs.SortedLE) : xs.max? = xs.getLast?

@[simp]

theorem List.foldlWith_snoc {α : Type u_1} {xs : List α} {β : Sort u_4} {x : α} {f : β → (y : α) → y ∈ xs ++ [x] → β} {z : β} : (xs ++ [x]).foldlWith f z = f (xs.foldlWith (fun (acc : β) (y : α) (h : y ∈ xs) => f acc y ⋯) z) x ⋯

theorem List.foldl_eq_foldl_of_fn_congr {α : Type u_1} {β : Type u_2} {xs : List α} {f g : β → α → β} {z : β} (h : ∀ (acc : β), ∀ x ∈ xs, f acc x = g acc x) : foldl f z xs = foldl g z xs

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

theorem List.rec_eq_foldr {α : Type u_1} {β : Type u_2} {xs : List α} {z : β} {f : α → β → β} : rec z (fun (x : α) (x_1 : List α) (acc : β) => f x acc) xs = foldr f z xs

theorem List.foldr_max_eq_max?_map {α : Type u_1} {β : Type u_2} {xs : List α} [hb : LinearOrder β] {f : α → β} {z : β} : foldr (fun (x : α) => max (f x)) z xs = (map f xs).max?.elim z (max z)

theorem List.foldr_max_eq_max?_map' {α : Type u_1} {β : Type u_2} {xs : List α} [hb : LinearOrder β] {f : α → β} {z : β} : foldr (fun (x : α) => max (f x)) z xs = (z :: map f xs).max?.getD z

theorem List.max?_eq_max?_of_perm {α : Type u_1} {xs ys : List α} [ha : LinearOrder α] (h : xs.Perm ys) : xs.max? = ys.max?

theorem List.apply_of_pairwise_and_lt {α : Type u_1} {xs : List α} {p : α → α → Prop} {i j : ℕ} {hh₁ : i < xs.length} {hh₂ : j < xs.length} (h₁ : Pairwise p xs) (h₂ : i < j) : p xs[i] xs[j]

theorem List.dfltMapWith_eq_dfltMapWith {α : Type u_1} {β : Type u_2} {xs : List α} {f₁ f₂ : (x : α) → x ∈ xs → β} {h : xs ≠ []} : dfltMapWith f₁ h = dfltMapWith f₂ h

@[simp]

theorem List.dfltMapWith_eq_some_of_nonempty {α : Type u_1} {β : Type u_2} {xs : List α} [hb : Nonempty β] {f : (x : α) → x ∈ xs → β} {h : xs ≠ []} : dfltMapWith f h = hb.some

theorem List.mapWith_eq_map {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] {f : (x : α) → x ∈ xs → β} : xs.mapWith f = if h : xs = [] then [] else map (fun (x : α) => if h₁ : x ∈ xs then f x h₁ else dfltMapWith f h) xs

theorem List.foldl_max_eq_max?_map {α : Type u_1} {β : Type u_2} {xs : List α} [hb : LinearOrder β] {f : α → β} {z : β} : foldl (fun (acc : β) (x : α) => max acc (f x)) z xs = (map f xs).max?.elim z (max z)

theorem List.foldlWith_max_eq_max?_mapWith {α : Type u_1} {β : Type u_2} {xs : List α} [hb : LinearOrder β] {f : (x : α) → x ∈ xs → β} {z : β} : xs.foldlWith (fun (acc : β) (x : α) (h : x ∈ xs) => max acc (f x h)) z = (xs.mapWith f).max?.elim z (max z)

theorem List.max?_eq_some_iff₁ {α : Type u_1} {xs : List α} [ha : LinearOrder α] {m : α} : xs.max? = some m ↔ m ∈ xs ∧ ∀ b ∈ xs, b ≤ m

theorem List.le_of_max?_eq_some {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x m : α} (h₁ : x ∈ xs) (h₂ : xs.max? = some m) : x ≤ m

theorem List.le_getD_max?_of_mem {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x y : α} (h : x ∈ xs) : x ≤ xs.max?.getD y

theorem List.le_elim_max_max?_of_mem {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x y z : α} (h : x ∈ xs) : x ≤ xs.max?.elim y (max z)

@[simp]

theorem List.mem_mapWith {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] {f : (x : α) → x ∈ xs → β} {y : β} : y ∈ xs.mapWith f ↔ ∃ (x : α) (h : x ∈ xs), f x h = y

theorem List.pairwise_of_pairwise_and_imp {α : Type u_1} {xs : List α} {r₁ r₂ : α → α → Prop} (h₁ : Pairwise r₁ xs) (h₂ : ∀ {a b : α}, r₁ a b → r₂ a b) : Pairwise r₂ xs

theorem List.pairwise_le_of_pairwise_lt {α : Type u_1} {xs : List α} [ha : LinearOrder α] (h : Pairwise (fun (x1 x2 : α) => x1 < x2) xs) : Pairwise (fun (x1 x2 : α) => x1 ≤ x2) xs

@[simp]

theorem List.flatMap_fn_singleton {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β} : flatMap (fun (x : α) => [f x]) xs = map f xs

theorem List.reverse_snoc {α : Type u_1} {xs : List α} {x : α} : (xs ++ [x]).reverse = x :: xs.reverse

theorem List.append_take_eq_of_suffix {α : Type u_1} {xs ys : List α} (h : ys <:+ xs) : take (xs.length - ys.length) xs ++ ys = xs

theorem List.take_length_sub_append_eq_of_suffix {α : Type u_1} {xs ys : List α} (h : ys <:+ xs) : take (xs.length - ys.length) xs ++ ys = xs

@[simp]

theorem List.take_length_sub_append_eq_self_iff_suffix {α : Type u_1} {xs ys : List α} : take (xs.length - ys.length) xs ++ ys = xs ↔ ys <:+ xs

@[simp]

theorem List.self_eq_take_length_sub_append_iff_suffix {α : Type u_1} {xs ys : List α} : xs = take (xs.length - ys.length) xs ++ ys ↔ ys <:+ xs

theorem List.mem_of_count_ne_zero {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x : α} (h : count x xs ≠ 0) : x ∈ xs

theorem List.mem_of_count_pos {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x : α} (h : 0 < count x xs) : x ∈ xs

theorem List.mem_of_lt_count {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x : α} {n : ℕ} (h : n < count x xs) : x ∈ xs

@[simp]

theorem List.mem_toSet {α : Type u_1} {xs : List α} {x : α} : x ∈ xs.toSet ↔ x ∈ xs

@[simp]

theorem List.toSet_nil {α : Type u_1} : [].toSet = ∅

@[simp]

theorem List.toSet_cons {α : Type u_1} {xs : List α} {x : α} : (x :: xs).toSet = insert x xs.toSet

theorem List.Perm.toSet_eq {α : Type u_1} {xs ys : List α} (h : xs.Perm ys) : xs.toSet = ys.toSet

theorem List.linearIndep_iff_toSet {α : Type u_1} {xs : List α} [ha₁ : One α] [ha₂ : Mul α] [ha₃ : HPow α ℤ α] : linearIndep xs ↔ linearIndep xs.toSet

@[simp]

theorem List.linearIndep_nil {α : Type u_1} [ha₁ : One α] [ha₂ : Mul α] [ha₃ : HPow α ℤ α] : linearIndep []

@[simp]

theorem List.linearIndep_singleton {α : Type u_1} [ha₁ : One α] [ha₂ : Mul α] [ha₃ : HPow α ℤ α] {x : α} : linearIndep [x]

theorem List.Perm.linearIndep_iff {α : Type u_1} {xs ys : List α} [ha₁ : One α] [ha₂ : Mul α] [ha₃ : HPow α ℤ α] (h : xs.Perm ys) : linearIndep xs ↔ linearIndep ys

theorem List.min?_eq_some_iff₁ {α : Type u_1} {xs : List α} {ha : LinearOrder α} {x : α} : xs.min? = some x ↔ x ∈ xs ∧ ∀ y ∈ xs, x ≤ y

theorem List.mem_iff_append_of_nodup {α : Type u_1} {xs : List α} {x : α} (h : xs.Nodup) : x ∈ xs ↔ ∃ (ys : List α) (zs : List α), x ∉ ys ∧ x ∉ zs ∧ xs = ys ++ x :: zs

theorem List.mem_erase_iff_of_nodup {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x y : α} (h : xs.Nodup) : y ∈ xs.erase x ↔ y ≠ x ∧ y ∈ xs

theorem List.erase_append_cons_eq_of_not_mem {α : Type u_1} {xs ys : List α} [ha : DecidableEq α] {x : α} (h : x ∉ xs) : (xs ++ x :: ys).erase x = xs ++ ys

@[simp]

theorem List.drop_length_reverse {α : Type u_1} {xs : List α} : drop xs.length xs.reverse = []

@[simp]

theorem List.drop_succ_length_reverse {α : Type u_1} {xs : List α} : drop (xs.length + 1) xs.reverse = []

@[simp]

theorem List.drop_succ_length_reverse_snoc {α : Type u_1} {xs : List α} {x : α} : drop (xs.length + 1) (xs.reverse ++ [x]) = []

@[simp]

theorem List.drop_reverse_append_cons_length_succ {α : Type u_1} {xs ys : List α} {x : α} : drop xs.length (xs.reverse ++ x :: ys) = x :: ys

@[simp]

theorem List.drop_reverse_append_cons_succ_length_succ {α : Type u_1} {xs ys : List α} {x : α} : drop (xs.length + 1) (xs.reverse ++ x :: ys) = ys

theorem List.pairwise_of_pairwise_and_sublist {α : Type u_1} {xs ys : List α} {r : α → α → Prop} (h₁ : Pairwise r xs) (h₂ : ys.Sublist xs) : Pairwise r ys

theorem List.find?_cons' {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : find? p (x :: xs) = if p x = true then some x else find? p xs

theorem List.find?_eq_some_equiv_iff {α : Type u_1} {xs : List α} {e : α ≃ α} {p : α → Bool} {x : α} : find? p xs = some (e x) ↔ find? (p ∘ ⇑e) (map (⇑e.symm) xs) = some x

theorem List.cons_eq_append {α : Type u_1} {xs : List α} {x : α} : x :: xs = [x] ++ xs

theorem List.getElem?_eq_of_getElem_eq {α : Type u_1} {xs ys : List α} {i j : ℕ} {hi : i < xs.length} {hj : j < ys.length} (h : xs[i] = ys[j]) : xs[i]? = ys[j]?

theorem List.getElem_eq_of_getElem?_eq {α : Type u_1} {xs ys : List α} {i j : ℕ} {hi : i < xs.length} {hj : j < ys.length} (h : xs[i]? = ys[j]?) : xs[i] = ys[j]

theorem List.getElem_eq_iff_getElem?_eq {α : Type u_1} {xs ys : List α} {i j : ℕ} {hi : i < xs.length} {hj : j < ys.length} : xs[i] = ys[j] ↔ xs[i]? = ys[j]?

theorem List.nodup_iff_getElem_ne_getElem {α : Type u_1} {xs : List α} : xs.Nodup ↔ ∀ (i j : ℕ) (hi : i < xs.length) (hj : j < xs.length), i < j → xs[i] ≠ xs[j]

theorem List.nodup_flatMap_flatMap_pair {α : Type u_1} {xs ys : List α} [ha : LinearOrder α] {r : α → α → Prop} [hp : DecidableRel r] (hxs : xs.Nodup) (hys : ys.Nodup) : (flatMap (fun (x : α) => flatMap (fun (y : α) => if x < y ∧ r x y then [(x, y)] else []) ys) xs).Nodup

theorem List.nodup_flatMap_flatMap_upair {α : Type u_1} {xs ys : List α} [ha : LinearOrder α] {r : α → α → Prop} [hp : DecidableRel r] (hxs : xs.Nodup) (hys : ys.Nodup) : (flatMap (fun (x : α) => flatMap (fun (y : α) => if x < y ∧ r x y then [{x, y}] else []) ys) xs).Nodup

theorem List.getElem_scanl' {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z : β} {i : ℕ} {hi : i < (scanl f z xs).length} : (scanl f z xs)[i] = foldl f z (take i xs)

theorem List.take_scanl' {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z : β} {n : ℕ} : take (n + 1) (scanl f z xs) = scanl f z (take n xs)

theorem List.drop_scanl {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z : β} {n : ℕ} (hn : n ≤ xs.length) : drop n (scanl f z xs) = scanl f (foldl f z (take n xs)) (drop n xs)

theorem List.mem_scanl_iff_exists_prefix {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z x : β} : x ∈ scanl f z xs ↔ ∃ (ys : List α), ys <+: xs ∧ foldl f z ys = x

@[simp]

theorem List.mem_scanl_iff_exists_take {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z x : β} : x ∈ scanl f z xs ↔ ∃ (n : ℕ), foldl f z (take n xs) = x

@[simp]

theorem List.foldl_add_length {α : Type u_1} {L : List (List α)} {z : ℕ} : foldl (fun (x1 : ℕ) (x2 : List α) => x1 + x2.length) z L = (map length L).sum + z

theorem List.findIdx_le_of_getElem {α : Type u_1} {xs : List α} {i : ℕ} {hi : i < xs.length} {p : α → Bool} (h : p xs[i] = true) : findIdx p xs ≤ i

theorem List.getElem_eq_getElem_zero_drop {α : Type u_1} {xs : List α} {i : ℕ} {hi : i < xs.length} : xs[i] = (drop i xs)[0]

theorem List.drop_add {α : Type u_1} {xs : List α} {n m : ℕ} : drop (n + m) xs = drop m (drop n xs)

theorem List.drop_add' {α : Type u_1} {xs : List α} {n m : ℕ} : drop (n + m) xs = drop n (drop m xs)

theorem List.lt_length_of_getElem?_eq_some {α : Type u_1} {xs : List α} {i : ℕ} {x : α} (h : xs[i]? = some x) : i < xs.length

theorem List.eq_append_getElem {α : Type u_1} {xs : List α} {i : ℕ} (h : i < xs.length) : xs = take i xs ++ xs[i] :: drop (i + 1) xs

theorem List.take_eq_self_of_le {α : Type u_1} {xs : List α} {n : ℕ} (h : xs.length ≤ n) : take n xs = xs

theorem List.sum_take_le_sum {xs : List ℕ} {n : ℕ} : (take n xs).sum ≤ xs.sum

theorem List.findIdx_eq_zero_iff {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx p xs = 0 ↔ xs = [] ∨ ∃ (h : 0 < xs.length), p xs[0] = true

theorem List.max?_eq_max?_of_mem_iff {α : Type u_1} {xs ys : List α} [ha : LinearOrder α] (h : ∀ (x : α), x ∈ xs ↔ x ∈ ys) : xs.max? = ys.max?

@[simp]

theorem List.getD_getElem?_replicate {α : Type u_1} {n i : ℕ} {x : α} : (replicate n x)[i]?.getD x = x

@[simp]

theorem List.getD_getElem?_append_replicate {α : Type u_1} {xs : List α} {n i : ℕ} {x : α} : (xs ++ replicate n x)[i]?.getD x = xs[i]?.getD x

theorem List.foldl_bool_iff_foldl_prop {α : Type u_1} {xs : List α} {f : Bool → α → Bool} {z : Bool} : foldl f z xs = true ↔ foldl (fun (acc : Prop) (x : α) => f (decide (acc = (true = true))) x = true) (z = true) xs

theorem List.foldl_prop_iff_foldl_bool {α : Type u_1} {xs : List α} [H : (P : Prop) → Decidable P] {f : Prop → α → Prop} {z : Prop} : foldl f z xs ↔ foldl (fun (acc : Bool) (x : α) => decide (f (acc = true) x)) (decide z) xs = true

theorem List.foldl_bool_and_eq_all {α : Type u_1} {xs : List α} {p : α → Bool} : foldl (fun (a : Bool) (x : α) => a && p x) true xs = xs.all p

theorem List.foldl_bool_and_iff_forall {α : Type u_1} {xs : List α} {p : α → Bool} : foldl (fun (a : Bool) (x : α) => a && p x) true xs = true ↔ ∀ x ∈ xs, p x = true

theorem List.foldl_and_iff_forall {α : Type u_1} {xs : List α} {p : α → Prop} : foldl (fun (a : Prop) (x : α) => a ∧ p x) True xs ↔ ∀ x ∈ xs, p x

theorem List.foldlWith_bool_iff_foldlWith_prop {α : Type u_1} {xs : List α} {f : Bool → (x : α) → x ∈ xs → Bool} {z : Bool} : xs.foldlWith f z = true ↔ xs.foldlWith (fun (acc : Prop) (x : α) (h : x ∈ xs) => f (decide (acc = (true = true))) x h = true) (z = true)

theorem List.foldlWith_prop_iff_foldlWith_bool {α : Type u_1} {xs : List α} [H : (P : Prop) → Decidable P] {f : Prop → (x : α) → x ∈ xs → Prop} {z : Prop} : xs.foldlWith f z ↔ xs.foldlWith (fun (acc : Bool) (x : α) (h : x ∈ xs) => decide (f (acc = true) x h)) (decide z) = true

theorem List.foldlWith_bool_and_iff_forall {α : Type u_1} {xs : List α} {p : (x : α) → x ∈ xs → Bool} : xs.foldlWith (fun (a : Bool) (x : α) (h : x ∈ xs) => a && p x h) true = true ↔ ∀ (x : α) (h : x ∈ xs), p x h = true

theorem List.foldlWith_and_iff_forall {α : Type u_1} {xs : List α} {p : (x : α) → x ∈ xs → Prop} : xs.foldlWith (fun (a : Prop) (x : α) (h : x ∈ xs) => a ∧ p x h) True ↔ ∀ (x : α) (h : x ∈ xs), p x h

theorem List.getElem!_eq_getElem {α : Type u_1} {xs : List α} [ha : Inhabited α] {i : ℕ} (h : i < xs.length) : xs[i]! = xs[i]

theorem List.nodup_of_pairwise {α : Type u_1} {xs : List α} {p : α → α → Prop} (h₁ : Pairwise p xs) (h₂ : ∀ {x y : α}, x ∈ xs → y ∈ xs → p x y → x ≠ y) : xs.Nodup

@[simp]

theorem List.nodup_append_self_iff {α : Type u_1} {xs : List α} : (xs ++ xs).Nodup ↔ xs = []

theorem List.nodup_flatMap_of {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} (h₁ : xs.Nodup) (h₂ : ∀ x ∈ xs, (f x).Nodup ∧ ∀ y ∈ xs, ∀ z ∈ f x, z ∈ f y → x = y) : (flatMap f xs).Nodup

theorem List.flatMap_fn_replicate_guard {α : Type u_1} {xs : List α} {p : α → Prop} [hp : DecidablePred p] : flatMap (fun (x : α) => replicate (guard (p x)).length x) xs = filter (fun (b : α) => decide (p b)) xs

theorem List.find?_eq_some_iff_of_at_most_one {α : Type u_1} {xs : List α} {p : α → Bool} {x : α} (h : ∀ {x y : α}, x ∈ xs → y ∈ xs → p x = true → p y = true → x = y) : find? p xs = some x ↔ x ∈ xs ∧ p x = true

theorem List.forall_of_find?_eq_some_imp {α : Type u_1} {xs : List α} {p₁ : α → Bool} {p₂ : α → Prop} (h₁ : ∀ (x : α), find? p₁ xs = some x → p₂ x) (h₂ : ∀ (x : α), p₂ x ↔ p₁ x = false) (x : α) : x ∈ xs → p₂ x

theorem List.eq_of_getElem_and_nodup {α : Type u_1} {xs : List α} {i j : ℕ} {hi : i < xs.length} {hj : j < xs.length} (h₁ : xs[i] = xs[j]) (h₂ : xs.Nodup) : i = j

theorem List.sum_eq_sum_toFinset {α : Type u_1} {xs : List α} [ha₁ : DecidableEq α] [ha₂ : Ring α] (h : xs.Nodup) : xs.sum = ∑ x ∈ xs.toFinset, x

theorem List.sum_map_eq_sum_toFinset {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] [hb : Ring β] {f : α → β} (h : xs.Nodup) : (map f xs).sum = ∑ x ∈ xs.toFinset, f x

theorem List.sum_map_eq_sum_getElem_finset_range {α : Type u_1} {β : Type u_2} {xs : List α} [hb : Ring β] {f : α → β} : (map f xs).sum = ∑ i ∈ Finset.range xs.length, if h : i < xs.length then f xs[i] else 0

@[simp]

theorem List.take_length_sub_one {α : Type u_1} {xs : List α} : take (xs.length - 1) xs = xs.init

@[simp]

theorem List.length_init {α : Type u_1} {xs : List α} : xs.init.length = xs.length - 1

theorem List.nodup_of_pairwise_lt {α : Type u_1} {xs : List α} [ha : LinearOrder α] (h : Pairwise (fun (x1 x2 : α) => x1 < x2) xs) : xs.Nodup

theorem List.foldl_apply_comm {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {z : β} {x : α} (h : ∀ ⦃x : β⦄ ⦃y z : α⦄, f (f x y) z = f (f x z) y) : foldl f (f z x) xs = f (foldl f z xs) x

@[simp]

theorem List.perm_comm_simp {α : Type u_1} {xs ys : List α} : (xs.Perm ys ↔ ys.Perm xs) ↔ True

@[simp]

theorem List.equivalence_perm {α : Type u_1} : Equivalence Perm

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

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

@[simp]

theorem List.mergeSort_perm_iff {α : Type u_1} {xs ys : List α} {p : α → α → Bool} : (xs.mergeSort p).Perm ys ↔ xs.Perm ys

@[simp]

theorem List.perm_mergeSort_iff {α : Type u_1} {xs ys : List α} {p : α → α → Bool} : xs.Perm (ys.mergeSort p) ↔ xs.Perm ys

@[simp]

theorem List.cons_mergeSort_perm_iff {α : Type u_1} {xs ys : List α} {p : α → α → Bool} {x : α} : (x :: xs.mergeSort p).Perm ys ↔ (x :: xs).Perm ys

@[simp]

theorem List.perm_cons_mergeSort_iff {α : Type u_1} {xs ys : List α} {p : α → α → Bool} {y : α} : xs.Perm (y :: ys.mergeSort p) ↔ xs.Perm (y :: ys)

@[simp]

theorem List.modify_length_append {α : Type u_1} {xs ys : List α} {f : α → α} : (xs ++ ys).modify xs.length f = xs ++ ys.modify 0 f

theorem List.pairwise_lt_of_pairwise_le {α : Type u_1} {xs : List α} [ha : LinearOrder α] (h₁ : Pairwise (fun (x1 x2 : α) => x1 ≤ x2) xs) (h₂ : xs.Nodup) : Pairwise (fun (x1 x2 : α) => x1 < x2) xs

theorem List.eq_and_eq_of_append_cons_eq {α : Type u_1} {xs ys xs' ys' : List α} {x : α} (h₁ : xs ++ x :: ys = xs' ++ x :: ys') (h₂ : x ∉ xs) (h₃ : x ∉ xs') : xs = xs' ∧ ys = ys'

theorem List.map_modify_eq_of {α : Type u_1} {β : Type u_2} {xs : List α} {i : ℕ} {f : α → α} {g : α → β} (h : ∀ x ∈ xs, g (f x) = g x) : map g (xs.modify i f) = map g xs

theorem List.nodup_take {α : Type u_1} {xs : List α} {n : ℕ} (h : xs.Nodup) : (take n xs).Nodup

theorem List.nodup_drop {α : Type u_1} {xs : List α} {n : ℕ} (h : xs.Nodup) : (drop n xs).Nodup

theorem List.take_take_append {α : Type u_1} {xs ys : List α} {k : ℕ} (h : k ≤ xs.length) : take k (take k xs ++ ys) = take k xs

theorem List.sum_nonpos {α : Type u_1} {xs : List α} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] (h : ∀ x ∈ xs, x ≤ 0) : xs.sum ≤ 0

@[simp]

theorem List.sum_map_neg {α : Type u_1} {xs : List α} [ha : Ring α] : (map (fun (x : α) => -x) xs).sum = -xs.sum

theorem List.sum_take_le_of_nonneg {α : Type u_1} {xs : List α} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] {k : ℕ} (h₁ : ∀ x ∈ xs, 0 ≤ x) : (take k xs).sum ≤ xs.sum

theorem List.le_sum_take_of_nonpos {α : Type u_1} {xs : List α} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] {k : ℕ} (h₁ : ∀ x ∈ xs, x ≤ 0) : xs.sum ≤ (take k xs).sum

@[simp]

theorem List.combinations_zero {α : Type u_1} {xs : List α} : xs.combinations 0 = [[]]

@[simp]

theorem List.sequence_nil_cons {α : Type u_1} {L : List (List α)} : sequence ([] :: L) = []

theorem List.sequence_cons {α : Type u_1} {xs : List α} {L : List (List α)} : sequence (xs :: L) = flatMap (fun (x : α) => map (fun (x_1 : List α) => x :: x_1) (sequence L)) xs

@[simp]

theorem List.sequence_snoc_nil {α : Type u_1} {L : List (List α)} : sequence (L ++ [[]]) = []

@[simp]

theorem List.combinations_nil_succ {α : Type u_1} {n : ℕ} : [].combinations (n + 1) = []

@[simp]

theorem List.sequence_nil {α : Type u_1} : sequence [] = [[]]

@[simp]

theorem List.sequence_eq_nil_iff {α : Type u_1} {L : List (List α)} : sequence L = [] ↔ [] ∈ L