inductive List.Exists {α : Type u_1} (P : α → Prop) : List α → Prop

• here {α : Type u_1} {P : α → Prop} {x : α} (xs : List α) : P x → Exists P (x :: xs)
• there {α : Type u_1} {P : α → Prop} (x : α) {xs : List α} : Exists P xs → Exists P (x :: xs)

theorem List.exists_iff_exists_mem {α : Type u_1} (p : α → Prop) {xs : List α} : Exists p xs ↔ ∃ x ∈ xs, p x

@[implicit_reducible]

instance List.instDecidablePredExists {α : Type u_1} (p : α → Prop) [DecidablePred p] : DecidablePred (Exists p)

Equations

• List.instDecidablePredExists p x✝ = decidable_of_iff' (∃ x ∈ x✝, p x) ⋯

theorem List.takeWhile_neg_eq {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} (h : p x = false) : takeWhile p (x :: xs) = []

theorem List.takeWhile_pos_eq {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} (h : p x = true) : takeWhile p (x :: xs) = x :: takeWhile p xs

theorem List.dropWhile_neg_eq {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} (h : p x = false) : dropWhile p (x :: xs) = x :: xs

theorem List.dropWhile_pos_eq {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} (h : p x = true) : dropWhile p (x :: xs) = dropWhile p xs

theorem List.mem_takeWhile {α : Type u_1} {p : α → Bool} {x y : α} {ys : List α} (h : x ∈ takeWhile p (y :: ys)) : x = y ∧ p x = true ∨ x ∈ takeWhile p ys

theorem List.mem_takeWhile_satisfies {α : Type u_1} {xs : List α} {p : α → Bool} {x : α} (h : x ∈ takeWhile p xs) : p x = true

theorem List.elem_iff_mem {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {ys : List α} : elem x ys = true ↔ x ∈ ys

theorem List.notElem_iff_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {ys : List α} : (!elem x ys) = true ↔ x ∉ ys

theorem List.mem_removeAll_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {xs ys : List α} : x ∈ xs.removeAll ys ↔ x ∈ xs ∧ x ∉ ys

theorem List.sum_replicate_eq {m n : ℕ} : (replicate m n).sum = m * n

theorem List.sum_map_const {α : Type u_1} {n : ℕ} {xs : List α} : (map (fun (x : α) => n) xs).sum = xs.length * n

theorem List.sum_map_length {α : Type u_2} {β : Type u_1} {f : α → List β} {xs : List α} (h : ∃ x ∈ xs, (f x).length > 0) : (map (length ∘ f) xs).sum > 0

theorem List.mem_map_if_mem {α : Type u_1} {β : Type u_2} {x : α} {xs : List α} {f : α → β} : x ∈ xs → f x ∈ map f xs

theorem List.prefix_append' {α : Type u_1} {xs ys zs : List α} : xs <+: ys → xs <+: ys ++ zs

theorem List.attachWith_eq_cons_exists_cons {α : Type u_1} {zs : List α} {Q : α → Prop} (R : ∀ z ∈ zs, Q z) {x : { x : α // Q x }} {xs : List { x : α // Q x }} : zs.attachWith Q R = x :: xs → ∃ (z : α) (zs' : List α), zs = z :: zs'

theorem List.forall₂_attachWith {α : Type u_1} {β : Type u_2} (P : α → β → Prop) {Q : α → Prop} (xs : List α) (R : ∀ x ∈ xs, Q x) (ys : List β) : Forall₂ (fun (x : { x : α // Q x }) (y : β) => P (↑x) y) (xs.attachWith Q R) ys ↔ Forall₂ P xs ys

theorem List.induction₂ {α : Type u_1} {β : Type u_2} {motive : (xs : List α) → (ys : List β) → xs.length = ys.length → Prop} (nil_nil : motive [] [] ⋯) (cons_cons : ∀ (x : α) (xs : List α) (y : β) (ys : List β) (len_eq : xs.length = ys.length), motive xs ys len_eq → motive (x :: xs) (y :: ys) ⋯) (xs : List α) (ys : List β) (len_eq : xs.length = ys.length) : motive xs ys len_eq

def List.induction₂' {α : Type u_1} {β : Type u_2} {motive : List α → List β → Sort u_3} (nil_nil : motive [] []) (nil_cons : (y : β) → (ys : List β) → motive [] (y :: ys)) (cons_nil : (x : α) → (xs : List α) → motive (x :: xs) []) (cons_cons : (x : α) → (y : β) → (xs : List α) → (ys : List β) → motive xs ys → motive (x :: xs) (y :: ys)) (xs : List α) (ys : List β) : motive xs ys

Equations

• List.induction₂' nil_nil nil_cons cons_nil cons_cons [] [] = nil_nil
• List.induction₂' nil_nil nil_cons cons_nil cons_cons [] (y :: ys) = nil_cons y ys
• List.induction₂' nil_nil nil_cons cons_nil cons_cons (x_2 :: xs) [] = cons_nil x_2 xs
• List.induction₂' nil_nil nil_cons cons_nil cons_cons (x_2 :: xs) (y :: ys) = cons_cons x_2 y xs ys (List.induction₂' nil_nil nil_cons cons_nil cons_cons xs ys)

theorem List.forall₂_of_attachWith {α : Type u_1} {xs : List α} (P : α → Prop) (H : ∀ x ∈ xs, P x) (R : (x : α) → P x → α → Prop) (R_refl : ∀ (x : α) (h : P x), R x h x) : Forall₂ (fun (x : { x : α // P x }) (y : α) => match x with | ⟨x, h⟩ => R x h y) (xs.attachWith P H) xs

theorem List.forall₂_of_attachWith' {α : Type u_1} {xs : List α} (P : α → Prop) (H : ∀ x ∈ xs, P x) (R : { x : α // P x } → α → Prop) (R_refl : ∀ (x : α) (h : P x), R ⟨x, h⟩ x) : Forall₂ (fun (x : { x : α // P x }) (y : α) => R x y) (xs.attachWith P H) xs

theorem List.forall₂_transitivity {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List α} {ys : List β} {zs : List γ} (P : α → β → Prop) (Q : β → γ → Prop) (R : α → γ → Prop) (P_Q_imp_R : ∀ (x : α) (y : β) (z : γ), P x y → Q y z → R x z) : Forall₂ P xs ys → Forall₂ Q ys zs → Forall₂ R xs zs

theorem List.Forall₂.flip_iff {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} (R : α → β → Prop) : Forall₂ (_root_.flip R) ys xs ↔ Forall₂ R xs ys

theorem List.forall₂_iff_forall₂_attach {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} (R : α → β → Prop) : Forall₂ (fun (x : { x : α // x ∈ xs }) (y : { x : β // x ∈ ys }) => R ↑x ↑y) xs.attach ys.attach ↔ Forall₂ R xs ys

def List.filterWhile {α : Type u_1} {β : Type u_2} (f : α → Option β) : List α → List β

Equations

• List.filterWhile f [] = []
• List.filterWhile f (x_1 :: xs) = match f x_1 with | some x => x :: List.filterWhile f xs | none => []

@[inline]

def List.zip₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} : List α → List β → List γ → List (α × β × γ)

Equations

• List.zip₃ = List.zipWith₃ fun (x1 : α) (x2 : β) (x3 : γ) => (x1, x2, x3)

def List.unzip₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} : List (α × β × γ) → List α × List β × List γ

Equations

• [].unzip₃ = ([], [], [])
• ((x_1, y, z) :: ts).unzip₃ = match ts.unzip₃ with | (xs, ys, zs) => (x_1 :: xs, y :: ys, z :: zs)

theorem List.unzip₃_length {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List (α × β × γ)} : xs.unzip₃.1.length = xs.unzip₃.2.1.length ∧ xs.unzip₃.2.1.length = xs.unzip₃.2.2.length

theorem List.unzip₃_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List (α × β × γ)} : xs.unzip₃.2 = xs.unzip.2.unzip

theorem List.length_cons_eq_if {α : Type u_1} {β : Type u_2} {x : α} {xs : List α} {y : β} {ys : List β} (h : xs.length = ys.length) : (x :: xs).length = (y :: ys).length

theorem List.max?_of_map_const_getD_eq {α : Type u_1} {β : Type u_2} [Max β] [Std.IdempotentOp max] [Std.Associative max] {xs : List α} {n : β} (f : α → β) (f_const : ∀ (x : α), f x = n) : (map f xs).max?.getD n = n

theorem List.prop_satisfies_elem_of_unattach {α : Type u_1} {p : α → Prop} {xs : List { x : α // p x }} (x : α) : x ∈ xs.unattach → p x

def List.unzipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) : List α → List β × List γ

Equations

• List.unzipWith f g [] = ([], [])
• List.unzipWith f g (x_1 :: xs) = Prod.map (List.cons (f x_1)) (List.cons (g x_1)) (List.unzipWith f g xs)

theorem List.unzip_eq_unzipWith {α : Type u_1} {β : Type u_2} {xs : List (α × β)} : xs.unzip = unzipWith Prod.fst Prod.snd xs

@[implicit_reducible]

instance List.instMonoid_extra {α : Type u_1} : Monoid (List α)

Equations

• List.instMonoid_extra = { mul := fun (x1 x2 : List α) => x1 ++ x2, mul_assoc := ⋯, one := [], one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

theorem List.mem_concat {α : Type u_1} {x y : α} {xs : List α} : x ∈ xs.concat y ↔ x ∈ xs ∨ x = y

def List.foldlRecOn₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {motive : β → γ → Sort u_4} (l : List α) (op₁ : β → α → β) (op₂ : γ → α → γ) (b : β) (c : γ) : motive b c → ((b : β) → (c : γ) → {x : α} → x ∈ l → motive b c → motive (op₁ b x) (op₂ c x)) → motive (foldl op₁ b l) (foldl op₂ c l)

Equations

• List.foldlRecOn₂ [] x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = x✝¹
• List.foldlRecOn₂ (x_7 :: xs) x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = List.foldlRecOn₂ xs x✝⁵ x✝⁴ (x✝⁵ x✝³ x_7) (x✝⁴ x✝² x_7) (x✝ x✝³ x✝² ⋯ x✝¹) fun (b : β) (c : γ) (x : α) (x_in_l : x ∈ xs) => x✝ b c ⋯

def List.foldrRecOn₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {motive : β → γ → Sort u_4} (l : List α) (op₁ : α → β → β) (op₂ : α → γ → γ) (b : β) (c : γ) : motive b c → ((b : β) → (c : γ) → {x : α} → x ∈ l → motive b c → motive (op₁ x b) (op₂ x c)) → motive (foldr op₁ b l) (foldr op₂ c l)

Equations

• One or more equations did not get rendered due to their size.
• List.foldrRecOn₂ [] x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = x✝¹

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

theorem List.foldl_concat_eq_append {α : Type u_1} {xs ys : List α} : foldl (fun (xs : List α) (x : α) => xs.concat x) xs ys = xs ++ ys

theorem List.kreplace_nil {α : Type u} [DecidableEq α] {β : α → Type v} {k : α} {v : β k} : kreplace k v [] = []

theorem List.kreplace_cons {α : Type u} [DecidableEq α] {β : α → Type v} {xs : List (Sigma β)} {k k' : α} {v : β k} {v' : β k'} : kreplace k v (⟨k', v'⟩ :: xs) = if k = k' then ⟨k, v⟩ :: xs else ⟨k', v'⟩ :: kreplace k v xs

theorem List.dlookup_kreplace {α : Type u} [DecidableEq α] {β : α → Type v} {x : List (Sigma β)} {k : α} {v : β k} : dlookup k (kreplace k v x) = v <$ dlookup k x

theorem List.dlookup_kreplace_ne {α : Type u} [DecidableEq α] {β : α → Type v} {x : List (Sigma β)} {k k' : α} {v : β k'} (k_ne : k ≠ k') : dlookup k (kreplace k' v x) = dlookup k x

theorem List.getLast_sizeOf_lt {α : Type u_1} [SizeOf α] {xs : List α} (h : xs ≠ []) : sizeOf (xs.getLast h) < sizeOf xs

theorem List.dropLast_sizeOf_le {α : Type u_1} [SizeOf α] {xs : List α} : sizeOf xs.dropLast ≤ sizeOf xs

theorem List.dropLast_getLast_add_sizeOf_eq {α : Type u_1} [SizeOf α] {xs : List α} (h : xs ≠ []) : 1 + sizeOf xs.dropLast + sizeOf (xs.getLast h) = sizeOf xs

theorem List.dropLast_concat_getLast! {α : Type u_1} [Inhabited α] {xs : List α} (h : xs ≠ []) : xs.dropLast.concat xs.getLast! = xs

dropLast_concat_getLast at the panicking accessor. A pass that splits a list into "all but the last" and "the last" reaches for getLast! rather than carry a non-emptiness proof through its own code; a proof about that pass still has the proof, and this is what spends it.

theorem List.forall₂_singleton {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {x : α} {y : β} : Forall₂ R [x] [y] ↔ R x y

theorem List.infix_append_of_infix {α : Type u_1} {xs ys zs : List α} (h : xs <:+: ys) : xs <:+: zs ++ ys

theorem List.infix_flatMap_of_mem' {α : Type u_1} {β : Type u_2} {x : α} {xs : List α} (h : x ∈ xs) (f : α → List β) : f x <:+: flatMap f xs

theorem List.not_mem_singleton {α : Type u_1} {x y : α} : x ∉ [y] ↔ x ≠ y

theorem List.concat_flatMap {α : Type u_2} {β : Type u_1} {f : α → List β} {xs : List α} {x : α} : flatMap f (xs.concat x) = flatMap f xs ++ f x

theorem List.not_mem_append_iff {α : Type u_1} {x : α} {xs ys : List α} : x ∉ xs ++ ys ↔ x ∉ xs ∧ x ∉ ys

theorem List.not_mem_cons_iff {α : Type u_1} {x y : α} {xs : List α} : x ∉ y :: xs ↔ x ≠ y ∧ x ∉ xs

theorem List.traverse_nil' {α : Type u_1} {β : Type u_2} {F : Type u_2 → Type u_3} [Applicative F] {f : α → F β} : List.traverse f [] = pure []

theorem List.traverse_cons' {α : Type u_1} {β : Type u_2} {F : Type u_2 → Type u_3} [Applicative F] {f : α → F β} {x : α} {xs : List α} : List.traverse f (x :: xs) = (fun (x1 : β) (x2 : List β) => x1 :: x2) <$> f x <*> List.traverse f xs

def List.zipper_induction {α : Type u_1} {motive : List α → List α → Sort u_2} (xs ys : List α) (nil : (xs : List α) → motive xs []) (cons : (xs : List α) → (y : α) → (ys : List α) → motive (xs ++ [y]) ys → motive xs (y :: ys)) : motive xs ys

Equations

• List.zipper_induction xs [] nil cons = nil xs
• List.zipper_induction xs (x_1 :: xs_1) nil cons = cons xs x_1 xs_1 (List.zipper_induction (xs ++ [x_1]) xs_1 nil cons)

theorem List.not_mem_union_iff {α : Type u_1} [DecidableEq α] {x : α} {l₁ l₂ : List α} : x ∉ l₁ ∪ l₂ ↔ x ∉ l₁ ∧ x ∉ l₂

theorem List.concat_perm_of_perm {α : Type u_1} {x : α} {xs ys : List α} (h : xs.Perm ys) : (xs.concat x).Perm (x :: ys)

theorem List.union_nil {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} (h : xs.Nodup) : xs ∪ [] = xs

theorem List.union_insert {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} {x : α} (h : xs.Nodup) : xs ∪ List.insert x ys = xs.concat x ∪ ys

theorem List.not_elem_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : List α} : elem a as = false ↔ a ∉ as

theorem List.suffix_union {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} : ys <:+ xs ∪ ys

theorem List.union_eq_append {α : Type u_1} [DecidableEq α] {xs ys : List α} : ys ∪ xs = (ys.removeAll xs).dedup ++ xs

theorem List.removeAll_perm_of_perm {α : Type u_1} [DecidableEq α] {xs ys zs : List α} (h : xs.Perm ys) : (xs.removeAll zs).Perm (ys.removeAll zs)

@[simp]

theorem List.nil_concat {α : Type u_1} {x : α} : [].concat x = [x]

@[simp]

theorem List.not_contains_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {xs : List α} : xs.contains x = false ↔ x ∉ xs

theorem List.removeAll_cons_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} {x : α} (h : x ∈ ys) : (x :: xs).removeAll ys = xs.removeAll ys

theorem List.removeAll_cons_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} {x : α} (h : x ∉ ys) : (x :: xs).removeAll ys = x :: xs.removeAll ys

theorem List.removeAll_concat_of_not_mem {α : Type u_1} [DecidableEq α] {xs ys : List α} {y : α} (h : y ∉ ys) : (xs.removeAll ys).concat y = (xs.concat y).removeAll ys

theorem List.filter_ne_of_nodup {α : Type u_1} [DecidableEq α] {xs ys zs : List α} {x : α} (h : xs.Nodup) (h' : xs = ys ++ [x] ++ zs) : filter (fun (x_1 : α) => decide (x_1 ≠ x)) xs = ys ++ zs

theorem List.dedup_singleton {α : Type u_1} [DecidableEq α] {x : α} : [x].dedup = [x]

theorem List.cons_perm_concat {α : Type u_1} [DecidableEq α] {x : α} {xs : List α} : (x :: xs).Perm (xs ++ [x])

@[simp]

theorem List.singleton_subset {α : Type u_1} {x : α} {xs : List α} : [x] ⊆ xs ↔ x ∈ xs

theorem List.non_empty_induction {α : Type u_1} {motive : (xs : List α) → xs ≠ [] → Prop} (singleton : ∀ (x : α), motive [x] ⋯) (cons : ∀ (x : α) (xs : List α) (h : xs ≠ []), motive xs h → motive (x :: xs) ⋯) (xs : List α) (h : xs ≠ []) : motive xs h

theorem List.forall₂_singleton_right_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {y : β} : Forall₂ R xs [y] ↔ ∃ (x : α), R x y ∧ xs = [x]

theorem List.forall₂_singleton_left_iff {α : Type u_2} {β : Type u_1} {R : α → β → Prop} {x : α} {ys : List β} : Forall₂ R [x] ys ↔ ∃ (y : β), R x y ∧ ys = [y]

theorem List.Forall₂.exists_left {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} (h : Forall₂ R xs ys) {y : β} (hy : y ∈ ys) : ∃ x ∈ xs, R x y

A member of the right list has a related member of the left one. Forall₂ is positional, so this is the projection that forgets the position — what a proof reaches for when it holds one element of one list and wants some related element of the other, with no interest in where.

theorem List.Forall₂.exists_right {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} (h : Forall₂ R xs ys) {x : α} (hx : x ∈ xs) : ∃ y ∈ ys, R x y

A member of the right list has a related member of the left one. Forall₂ is positional, so this is the projection that forgets the position — what a proof reaches for when it holds one element of one list and wants some related element of the other, with no interest in where.

theorem List.Forall₂.find?_right {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} (h : Forall₂ R xs ys) {P : α → Bool} {Q : β → Bool} (hPQ : ∀ (x : α) (y : β), R x y → P x = Q y) {y : β} (hy : find? Q ys = some y) : ∃ (x : α), find? P xs = some x ∧ R x y

Two find?s under a Forall₂ land on related elements. The predicates need not be the same — they need only agree on related pairs, which is the usual situation: a lookup keyed on a field both sides preserve.

Forall₂ is positional and find? returns the first match, so the two searches walk the lists in step and stop at the same index; the induction is that observation.

theorem List.Forall₂.find?_left {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} (h : Forall₂ R xs ys) {P : α → Bool} {Q : β → Bool} (hPQ : ∀ (x : α) (y : β), R x y → P x = Q y) {x : α} (hx : find? P xs = some x) : ∃ (y : β), find? Q ys = some y ∧ R x y

Two find?s under a Forall₂ land on related elements. The predicates need not be the same — they need only agree on related pairs, which is the usual situation: a lookup keyed on a field both sides preserve.

Forall₂ is positional and find? returns the first match, so the two searches walk the lists in step and stop at the same index; the induction is that observation.

theorem List.find?_eq_some_of_unique {α : Type u_1} {P : α → Bool} {l : List α} {x : α} (hx : x ∈ l) (hP : P x = true) (huniq : ∀ y ∈ l, P y = true → y = x) : find? P l = some x

find? lands on the only match. find? returns the first element satisfying the predicate, so knowing which element it returns generally needs to know where it sits; when the match is unique that positional information is not needed, and membership is enough.

theorem List.Forall₂.map_eq_map {α : Type u_2} {β : Type u_3} {R : α → β → Prop} {γ : Type u_1} {f : α → γ} {g : β → γ} {xs : List α} {ys : List β} (h : Forall₂ R xs ys) (hfg : ∀ (x : α) (y : β), R x y → f x = g y) : map f xs = map g ys

Two maps under a Forall₂ agree when the two functions agree on related pairs, so the two mapped lists are equal and anything said about one is said about the other.

theorem List.Forall₂.exists_append_left {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs₁ xs₂ : List α} {ys : List β} (h : Forall₂ R (xs₁ ++ xs₂) ys) : ∃ (ys₁ : List β) (ys₂ : List β), ys = ys₁ ++ ys₂ ∧ Forall₂ R xs₁ ys₁ ∧ Forall₂ R xs₂ ys₂

A Forall₂ whose left list is an append splits at the same point. Forall₂ is positional, so the right list has a prefix related to the left one's and a suffix related to the rest, with nothing about either left tangled up in the other.

theorem List.attach_eq_cons {α : Type u_1} {xs : List α} {ys : List { x : α // x ∈ xs }} {y : { x : α // x ∈ xs }} (h : xs.attach = y :: ys) : ∃ (x : α) (xs' : List α) (h' : xs = x :: xs'), x = ↑y ∧ ys = map (fun (x_1 : { x : α // x ∈ xs' }) => match x_1 with | ⟨y, h⟩ => ⟨y, ⋯⟩) xs'.attach

theorem List.traverse_map {α : Type u_3} {β : Type u_4} {γ : Type u_1} {F : Type u_1 → Type u_2} [Applicative F] {f : β → F γ} {g : α → β} {xs : List α} : List.traverse f (map g xs) = List.traverse (f ∘ g) xs

theorem List.attach_singleton {α : Type u_1} {x : α} : [x].attach = [⟨x, ⋯⟩]

theorem List.traverse_singleton {α : Type u_1} {β : Type u_2} {F : Type u_2 → Type u_3} [Applicative F] [LawfulApplicative F] {f : α → F β} {x : α} : List.traverse f [x] = (fun (x : β) => [x]) <$> f x

def List.sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderBot α] (xs : List β) (f : β → α) : α

Equations

• xs.sup f = List.foldl (fun (x1 : α) (x2 : β) => x1 ⊔ f x2) ⊥ xs

inductive List.RPerm {α : Type u_1} (R : α → α → Prop) : List α → List α → Prop

• nil {α : Type u_1} {R : α → α → Prop} : RPerm R [] []
• cons {α : Type u_1} {R : α → α → Prop} (x y : α) {xs ys : List α} : R x y → RPerm R xs ys → RPerm R (x :: xs) (y :: ys)
• swap {α : Type u_1} {R : α → α → Prop} (x y : α) {xs : List α} : RPerm R (y :: x :: xs) (x :: y :: xs)
• trans {α : Type u_1} {R : α → α → Prop} {xs ys zs : List α} : RPerm R xs ys → RPerm R ys zs → RPerm R xs zs

theorem List.rperm_eq_iff_perm {α : Type u_1} {xs ys : List α} : RPerm (fun (x1 x2 : α) => x1 = x2) xs ys ↔ xs.Perm ys

theorem List.ne_nil_iff_exists_snoc {α : Type u_1} {xs : List α} : xs ≠ [] ↔ ∃ (xs' : List α) (x : α), xs = xs' ++ [x]

theorem List.revInduction {α : Type u_1} {motive : List α → Prop} (xs : List α) (nil : motive []) (snoc : ∀ (xs : List α) (x : α), motive xs → motive (xs ++ [x])) : motive xs

theorem List.map_concat' {α : Type u_1} {β : Type u_2} {f : α → β} {xs : List α} {x : α} : map f (xs ++ [x]) = map f xs ++ [f x]

@[simp]

theorem List.drop_snoc {α : Type u_1} {i : ℕ} {xs : List α} {x : α} : 0 < i → ∀ (h' : i - 1 ≤ xs.length), drop (i - 1) (xs ++ [x]) = drop (i - 1) xs ++ [x]

theorem List.evenRevInduction {α : Type u_1} {motive : (xs : List α) → Even xs.length → Prop} (nil : motive [] ⋯) (snoc_snoc : ∀ (xs : List α) (x y : α) (h : Even xs.length), motive xs h → motive (xs ++ [x, y]) ⋯) (xs : List α) (h : Even xs.length) : motive xs h

theorem List.even_len_cons_cons_of_even_len {α : Type u_1} {ys : List α} {y₁ y₂ : α} (even_ys_len : Even ys.length) : Even (y₁ :: y₂ :: ys).length

theorem List.zipperEvenInduction {α : Type u_1} {motive : (xs ys : List α) → Even xs.length → Even ys.length → Prop} (xs ys : List α) (even_xs_len : Even xs.length) (even_ys_len : Even ys.length) (nil : ∀ (xs : List α) (even_xs_len : Even xs.length), motive xs [] even_xs_len ⋯) (cons_cons : ∀ (xs : List α) (y₁ y₂ : α) (ys : List α) (even_xs_len : Even xs.length) (even_ys_len : Even ys.length), motive (xs ++ [y₁, y₂]) ys ⋯ even_ys_len → motive xs (y₁ :: y₂ :: ys) even_xs_len ⋯) : motive xs ys even_xs_len even_ys_len

theorem List.exists_mem_zip_right_of_mem_left {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {x : α} (h : xs.length = ys.length) (h' : x ∈ xs) : ∃ (y : β), (x, y) ∈ xs.zip ys

theorem List.rel_of_forall₂_of_mem_zip {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {R : α → β → Prop} {x : α} {y : β} (mem_zip : (x, y) ∈ xs.zip ys) (rel : Forall₂ R xs ys) : R x y

theorem List.traverse_fmap {α : Type u_1} {β γ : Type u_2} {F : Type u_2 → Type u_3} {xs : List α} [Applicative F] [LawfulApplicative F] {f : β → γ} {g : α → F β} : List.traverse (fun (x : α) => f <$> g x) xs = map f <$> List.traverse g xs

theorem List.traverse_ext {α : Type u_3} {β : Type u_1} {F : Type u_1 → Type u_2} [Applicative F] {xs : List α} {f g : α → F β} (h : ∀ x ∈ xs, f x = g x) : List.traverse f xs = List.traverse g xs