LeanAide documentation

LeanAide GPT-4 documentation

Module: Std.Data.List.Lemmas

`List.length_range` theorem List.length_range : ∀ (n : ℕ), (List.range n).length = n The theorem `List.length_range` states that for any natural number `n`, the length of the list generated by `List.range n` is equal to `n`. This means that the function `List.range` generates a list of natural numbers from `0` to `n` exclusive, and the size of this list is exactly `n`. More concisely: For any natural number n, the length of List.range n is equal to n.
`List.infix_refl` theorem List.infix_refl : ∀ {α : Type u_1} (l : List α), l.IsInfix l This theorem, `List.infix_refl`, is a statement about lists in Lean 4. The theorem asserts that for any given list `l` of any type `α`, the list `l` is an infix of itself. The notation `<:+:` denotes the infix relation. In other words, the list `l` can be found within itself exactly as it is. More concisely: For any list `l` of type `α`, `l <:+ l` holds. (Infix `<:+` denotes list concatenation or infix relation in Lean 4.)
`List.eraseP_cons_of_pos` theorem List.eraseP_cons_of_pos : ∀ {α : Type u_1} {a : α} {l : List α} (p : α → Bool), p a = true → List.eraseP p (a :: l) = l The theorem `List.eraseP_cons_of_pos` states that for all types `α`, for every element `a` of type `α`, for every list `l` of elements of type `α`, and for every predicate `p` that maps elements of type `α` to boolean values, if the predicate `p` applied to the element `a` returns `true`, then the result of applying the function `List.eraseP` with predicate `p` to the list that has `a` at the head and `l` as the rest of the list, is equal to the list `l`. In other words, if `p a` is `true`, then `a` is removed from the head of the list `(a :: l)` using `List.eraseP`. More concisely: For all types `α`, lists `l` of length greater than 0 in `α`, and predicates `p` on `α`, if `a ∈ l` and `p(a)` holds, then `List.eraseP p (a :: l) = l`.
`List.Sublist.refl` theorem List.Sublist.refl : ∀ {α : Type u_1} (l : List α), l.Sublist l This theorem states that, for any type `α` and any list `l` of values of that type, the list `l` is a sublist of itself. In other words, every list is considered a sublist of itself in Lean 4. More concisely: For any type `α` and any list `l` of length `n` over `α`, `l` is a sublist of itself.
`List.nil_sublist` theorem List.nil_sublist : ∀ {α : Type u_1} (l : List α), [].Sublist l This theorem states that for any given list `l` of elements of some arbitrary type `α`, the empty list (denoted by `[]`) is a sublist of `l`. In other words, it asserts that the empty list is always a sublist of any list regardless of the type of elements in the list. More concisely: For any list `l` of type `α`, the empty list `[]` is a sublist of `l`.
`List.map_singleton` theorem List.map_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), List.map f [a] = [f a] The theorem `List.map_singleton` states that for all types `α` and `β`, and for any function `f` from `α` to `β` and any element `a` of type `α`, applying the `List.map` function with `f` to a list containing just `a` returns a new list containing `f(a)`. In other words, mapping a function over a singleton list results in a new singleton list where the function has been applied to the sole element of the original list. This theorem describes an elementary behavior of the `List.map` function in Lean 4. More concisely: For any type `α`, type `β`, function `f : α → β`, and element `a : α`, `List.map f [a] = [f a]`.
`List.range_succ_eq_map` theorem List.range_succ_eq_map : ∀ (n : ℕ), List.range (n + 1) = 0 :: List.map Nat.succ (List.range n) This theorem states that for any natural number `n`, the range of `n+1` (which is a list of natural numbers from `0` to `n+1`, exclusive) is equal to a list that starts with `0` and then maps the successor function `Nat.succ` (which adds one to a natural number) to each element in the range of `n`. In other words, it's stating that getting the range of `n+1` is the same as taking the range of `n`, adding one to each element, and prepending `0` to the list. More concisely: The range of `n+1` is the list obtained by adding 1 to each element of the range of `n` and prepending 0.
`List.Sublist.length_le` theorem List.Sublist.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length This theorem states that for any two lists `l₁` and `l₂` of any type `α`, if `l₁` is a sublist of `l₂` (denoted as `List.Sublist l₁ l₂`), then the length of `l₁` is less than or equal to the length of `l₂`. In other words, a sublist cannot be longer than the list it is contained within. The length of a list is calculated as the total number of elements in the list, with the length of an empty list being 0 and the length of a list with a head element and a tail list being 1 plus the length of the tail list. More concisely: For all types `α` and lists `l₁` and `l₂` of length `n₁` and `n₂` respectively, if `l₁` is a sublist of `l₂` then `n₁ ≤ n₂`.
`List.get?_range` theorem List.get?_range : ∀ {m n : ℕ}, m < n → (List.range n).get? m = some m The theorem `List.get?_range` states that for any natural numbers `m` and `n`, if `m` is less than `n`, then when you get the `m`th element from the list of natural numbers from `0` to `n` exclusive (generated by `List.range n`), you will get `m` back. In other words, the position of a natural number `m` in this list is the same as its value when `m` is less than `n`. More concisely: For all natural numbers `m` and `n` with `m < n`, the `m`-th element in the list `List.range n` is `m`.
`List.take_take` theorem List.take_take : ∀ {α : Type u_1} (n m : ℕ) (l : List α), List.take n (List.take m l) = List.take (min n m) l This theorem, `List.take_take`, states that for any list `l` of type `α`, and any two natural numbers `n` and `m`, taking `n` elements of the sublist created by taking `m` elements of `l` is equivalent to taking the minimum of `n` and `m` elements from the original list `l`. Essentially, it captures the property that taking a sublist of a sublist gives you the same result as taking a sublist directly, as long as the size of the sublist is limited by the smaller of the two original sizes. More concisely: For any list `l` of type `α` and natural numbers `n` and `m`, `List.take n (List.take m l)` is equal to `List.take (min n m) l`.
`List.Pairwise.sublist` theorem List.Pairwise.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α} {R : α → α → Prop}, l₁.Sublist l₂ → List.Pairwise R l₂ → List.Pairwise R l₁ := by sorry This theorem states that for any type `α` and any lists `l₁` and `l₂` of `α`, along with a binary relation `R` on `α`, if `l₁` is a sublist of `l₂` and `l₂` satisfies the pairwise property with respect to `R`, then `l₁` also satisfies the pairwise property with respect to `R`. The pairwise property here means that for any two elements in the list, the relation `R` holds. Therefore, this theorem is essentially saying that if a relation holds for all pairs of elements in a list, then it will also hold for all pairs of elements in any sublist of that list. More concisely: If `l₁` is a sublist of `l₂` and all pairs of elements in `l₂` relate under `R`, then all pairs of elements in `l₁` also relate under `R`.
`List.erase_cons_tail` theorem List.erase_cons_tail : ∀ {α : Type u_1} [inst : BEq α] {a b : α} (l : List α), ¬(b == a) = true → (b :: l).erase a = b :: l.erase a := by sorry This theorem, `List.erase_cons_tail`, states that for all types `α`, given an instance of `BEq α` (which allows for equality checks), and for any elements `a` and `b` of type `α` and a list `l` of type `α`, if `b` is not equal to `a` (i.e., `b == a` evaluates to `false`), then erasing `a` from the list that starts with `b` and is followed by `l` (`b :: l`) is equivalent to the list that starts with `b` and is followed by the list resulted from erasing `a` from `l`. More concisely: For all types `α` with equality `BEq α`, and for all `a`, `b` in `α` with `b != a`, the list `b :: List.erase a l` equals `b :: l` for any list `l` of type `α`.
`List.exists_of_eraseP` theorem List.exists_of_eraseP : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {a : α}, a ∈ l → p a = true → ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂ The theorem `List.exists_of_eraseP` states that for any type `α`, any predicate `p` from `α` to `Bool`, any list `l` of α, and any element `a` of α, if `a` is an element of `l` and `p(a)` equals true, then there exist elements `a`, `l₁`, and `l₂` such that for all `b` in `l₁`, `p(b)` is not true, `p(a)` is true, `l` is the concatenation of `l₁`, `a`, and `l₂`, and the list obtained upon erasing the first element in `l` that satisfies `p` equals the concatenation of `l₁` and `l₂`. In other words, if a list contains an element that satisfies a certain predicate, we can split the list into two parts where the first part contains no element satisfying the predicate and the second part starts with the first element satisfying the predicate; then, removing the first satisfying element from the list will result in the concatenation of the two parts. More concisely: If a list `l` of type `α` contains an element `a` such that `p(a) = true` and there exists no `b` in the prefix of `l` with `p(b) = true`, then removing the first such `a` from `l` results in the concatenation of the list of elements with `p(x) = false` and the list starting with `a`.
`List.subset_cons` theorem List.subset_cons : ∀ {α : Type u_1} (a : α) (l : List α), l ⊆ a :: l This theorem is stating that for any type `α`, any element `a` of type `α`, and any list `l` containing elements of type `α`, the list `l` is a subset of the list that results from prepending `a` to `l`. In more formal language, the theorem asserts that for all `α`, `a`, and `l`, `l` is a subset of `a :: l`. More concisely: For any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, `l` is a subset of the list obtained by prepending `a` to `l`.
`List.rel_of_chain_cons` theorem List.rel_of_chain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.Chain R a (b :: l) → R a b This theorem, `List.rel_of_chain_cons`, states that for any type `α`, a binary relation `R` on `α`, and any elements `a` and `b` of type `α`, if `a` has a relation `R` with every element of the list that starts with `b` (i.e., `b` followed by list `l`), then `a` has the relation `R` with `b`. In other words, if `a` is related to every element in the list `b :: l` through `R`, then `a` is directly related to `b` through the same relation `R`. More concisely: If for all `x` in a list `l`, `a` is related to `x` (via relation `R`), then `a` is related to the head `b` of the list (via relation `R`).
`List.filterMap_eq_map` theorem List.filterMap_eq_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), List.filterMap (some ∘ f) = List.map f This theorem, `List.filterMap_eq_map`, states that for any types `α` and `β`, and any function `f` from `α` to `β`, the function `List.filterMap` applied to the composition of `some` and `f` is equivalent to the function `List.map` applied to `f`. In simple terms, it means that if we use `filterMap` to apply `f` to each element of a list and then wrap the result in an `Option` (using `some`), we end up with the same result as if we simply used `map` to apply `f` directly to each element of the list. More concisely: For any type `α`, type `β`, and function `f` from `α` to `β`, `List.filterMap (λx => some (f x)) l = List.map f l`.
`List.leftpad_length` theorem List.leftpad_length : ∀ {α : Type u_1} (n : ℕ) (a : α) (l : List α), (List.leftpad n a l).length = max n l.length This theorem states that for any type `α`, natural number `n`, element `a` of type `α`, and list `l` of type `α`, the length of the list returned by the `List.leftpad n a l` function is equal to the maximum of `n` and the length of `l`. In other words, the `List.leftpad` function pads the given list `l` on the left with repetitions of the element `a` until its length is `n` or keeps the list as is if its initial length is greater than `n`, and this theorem asserts that the length of the result list is either `n` or the original list length, whichever is larger. More concisely: For any type `α`, natural number `n`, element `a` of type `α`, and list `l` of length `m` over `α`, the length of `List.leftpad n a l` is `max n m`.
`List.erase_eq_eraseP` theorem List.erase_eq_eraseP : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l : List α), l.erase a = List.eraseP (fun x => a == x) l This theorem states that for any type `α` that has a binary equality relation (`BEq α`) and obeys the laws of binary equality (`LawfulBEq α`), and for any specific element `a` of type `α` and list `l` of elements of type `α`, the function `List.erase l a` (which removes the first occurrence of `a` from `l`) is equal to `List.eraseP (fun x => a == x) l`. In other words, the operation of erasing a particular element from a list is the same as removing the first element that satisfies the condition of being equal to the given element. More concisely: For any type `α` with a lawful binary equality relation, the function `List.erase` that removes the first occurrence of an element from a list is equal to the function `List.eraseP` that removes elements satisfying equality to a given element.
`List.Pairwise.imp` theorem List.Pairwise.imp : ∀ {α : Type u_1} {R S : α → α → Prop}, (∀ {a b : α}, R a b → S a b) → ∀ {l : List α}, List.Pairwise R l → List.Pairwise S l This theorem states that for any type `α` and any two relations `R` and `S` on `α`, if all pairs of elements in `α` that satisfy `R` also satisfy `S`, then for any list of `α`, if all consecutive pairs of elements in the list satisfy `R`, they also satisfy `S`. In other words, it describes the preservation of pairwise properties of lists under implication of relations. More concisely: If `R` implies `S` as relations on type `α`, then any list of `α` where consecutive pairs satisfy `R` also satisfies `S`.
`List.getLast_append` theorem List.getLast_append : ∀ {α : Type u_1} {a : α} (l : List α) (h : l ++ [a] ≠ []), (l ++ [a]).getLast h = a := by sorry The theorem `List.getLast_append` states that for any type `α`, any element `a` of type `α` and any list `l` of elements of type `α`, if the list that is the result of appending `a` to `l` is not empty, then the last element of this appended list is `a`. In other words, when you append an element to the end of a list, that element becomes the last element of the new list. More concisely: For any type `α` and list `l` of length `n+1` in `α`, if `List.append a l` is non-empty, then `last (List.append a l) = a`.
`List.mem_range` theorem List.mem_range : ∀ {m n : ℕ}, m ∈ List.range n ↔ m < n This theorem states that for any natural numbers `m` and `n`, `m` is an element of the list generated by `List.range n` if and only if `m` is strictly less than `n`. In other words, `List.range n` generates a list of natural numbers from `0` to `n-1`, and a number `m` can only be in this list if it is less than `n`. More concisely: For natural numbers `m` and `n`, `m` is in the range `[0, n)` if and only if `m < n`.
`List.singleton_sublist` theorem List.singleton_sublist : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Sublist l ↔ a ∈ l This theorem, `List.singleton_sublist`, states that for any type `α`, any instance `a` of that type, and any list `l` of that type, a list containing only `a` is a sublist of `l` if and only if `a` is an element of `l`. In other words, it asserts that a singleton list is a sublist of a larger list precisely when the single element of the singleton list is also a member of the larger list. More concisely: For any type `α` and any list `l` of length 1 or more over `α`, the singleton list `[a]` is a sublist of `l` if and only if `a` is an element of `l`.
`List.eraseP_sublist` theorem List.eraseP_sublist : ∀ {α : Type u_1} {p : α → Bool} (l : List α), (List.eraseP p l).Sublist l The theorem `List.eraseP_sublist` states that for any type `α`, for any predicate function `p : α → Bool`, and any list `l : List α`, the list obtained by removing the first element of `l` that satisfies the predicate `p` (that is, `List.eraseP p l`), is a sublist of `l`. In other words, removing an element from a list (if it satisfies the given predicate), results in a sublist of the original list. More concisely: For any type `α`, any predicate `p : α → Bool`, and any list `l : List α`, `List.eraseP p l` is a sublist of `l`.
`List.length_zipWith` theorem List.length_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l₁ : List α) (l₂ : List β), (List.zipWith f l₁ l₂).length = min l₁.length l₂.length The theorem `List.length_zipWith` states that for any types `α`, `β`, and `γ`, and any function `f` from `α` and `β` to `γ`, the length of the list obtained by applying `f` element-wise to two lists `l₁` and `l₂` (using `List.zipWith`) is equal to the minimum of the lengths of `l₁` and `l₂`. In other words, if you have two lists and you combine them element-wise using some function, the length of the resulting list will be as long as the shorter of the two input lists. More concisely: For any types `α`, `β`, and `γ`, and functions `f : α -> β -> γ` and lists `l₁ : List α` and `l₂ : List β` of equal lengths, the length of `List.zipWith f l₁ l₂` is min(length l₁, length l₂).
`List.filter_eq_self` theorem List.filter_eq_self : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = l ↔ ∀ a ∈ l, p a = true The theorem `List.filter_eq_self` states that for any type `α`, any Boolean-valued function `p` on `α`, and any list `l` of elements of type `α`, the list obtained by filtering `l` with `p` is equal to `l` itself if and only if the function `p` returns `true` for all elements `a` in `l`. This means that every element of the list `l` satisfies the condition defined by the function `p`. More concisely: For any type `α`, list `l` of `α`, and Boolean-valued function `p` on `α`, `List.filter p l = l` if and only if `p a` holds for all `a` in `l`.
`List.get_singleton` theorem List.get_singleton : ∀ {α : Type u_1} (a : α) (n : Fin 1), [a].get n = a This theorem, `List.get_singleton`, states that for all types `α`, for any element `a` of type `α` and for any `n` of type `Fin 1`, retrieving the `n`th element (using the function `List.get`) from a singleton list that contains only `a` will always yield `a`. In simpler terms, it says that if you have a list with only one element, no matter at which index you look, you'll always get that one element. The `Fin 1` type represents a finite set of size 1, so `n` can only be zero, which is the first and only position in a singleton list. More concisely: For any type `α` and element `a` of type `α`, the function `List.get` on a singleton list `[a]` of length 1 returns `a`. In mathematical notation: `List.get (list.singleton a) = a`.
`List.erase_sublist` theorem List.erase_sublist : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), (l.erase a).Sublist l This theorem, `List.erase_sublist`, states that for any type `α`, given an instance of equality (BEq) and lawful equality (LawfulBEq) on this type, and for any element `a` of type `α` and any list `l` of type `List α`, the list that results from erasing the element `a` from `l` is a sublist of `l`. In other words, if you remove an element from a list, the resulting list is always a sublist of the original list. More concisely: For any type `α` with equality `BEq` and lawful equality `LawfulBEq`, if `a` is an element of list `l` of type `List α`, then the list obtained by erasing `a` from `l` is a sublist of `l`.
`List.filterMap_eq_filter` theorem List.filterMap_eq_filter : ∀ {α : Type u_1} (p : α → Bool), List.filterMap (Option.guard fun x => p x = true) = List.filter p The theorem `List.filterMap_eq_filter` states that for all types `α` and a Boolean function `p` applied to the elements of this type, the function `List.filterMap` combined with `Option.guard` applied to a function that checks if `p x` is true, is equivalent to directly using the `List.filter` function with `p`. In other words, filtering a list using `List.filterMap` and `Option.guard` gives the same result as directly filtering the list with `p` using `List.filter`. This theorem essentially shows that `List.filter` and `List.filterMap` combined with `Option.guard` are interchangeable under these conditions. More concisely: For all types α and Boolean functions p, List.filterMap (Option.guard p) equals List.filter p.
`List.append_sublist_append_left` theorem List.append_sublist_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Sublist (l ++ l₂) ↔ l₁.Sublist l₂ This theorem states that for any type `α` and any given lists `l`, `l₁`, and `l₂` of type `α`, a list `l₁` is a sublist of `l₂` if and only if the list formed by appending `l` to `l₁` (i.e., `l ++ l₁`) is a sublist of the list formed by appending `l` to `l₂` (i.e., `l ++ l₂`). In simple words, appending the same list `l` to both `l₁` and `l₂` does not change the sublist relation between `l₁` and `l₂`. More concisely: For any type `α` and lists `l₁`, `l₂` of type `α`, `l₁` is a sublist of `l₂` if and only if `l ++ l₁` is a sublist of `l ++ l₂`.
`List.eq_replicate_of_mem` theorem List.eq_replicate_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, (∀ b ∈ l, b = a) → l = List.replicate l.length a This theorem states that for any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, if every element `b` in `l` is equal to `a`, then `l` is equal to a list that consists of the element `a` replicated a number of times equal to the length of `l`. In other words, if all elements in a list are the same, then that list is a replication of that element for as many times as the length of the list. More concisely: If `α` is a type, `a : α`, and `l : list α` is such that ∀ b ∈ l, b = a, then l = list.repeat a (length l).
`List.range_succ` theorem List.range_succ : ∀ (n : ℕ), List.range n.succ = List.range n ++ [n] This theorem states that for any natural number `n`, the list of natural numbers up to `n+1` (exclusive of `n+1`) as generated by the `List.range` function, is equivalent to the list of natural numbers up to `n` (exclusive of `n`) appended with `n`. In other words, if you have a list of numbers from `0` to `n`, adding the next number `n+1` to the list can be achieved by appending `n` to the list of numbers up to `n`. More concisely: The list of natural numbers up to `n+1` (exclusive) is the same as the list of natural numbers up to `n` (exclusive) followed by `n`. In Lean, this can be expressed as `List.range (0 : nat) (n + 1) = List.append (List.range (0 : nat) n) [n]`.
`List.erase_of_not_mem` theorem List.erase_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List α}, a ∉ l → l.erase a = l This theorem states that for any list `l` of a certain type `α`, and an element `a` of that same type, if `a` is not a member of `l`, then erasing `a` from `l` results in the original list `l`. This is under the assumptions that there exists a Boolean equality function for type `α`, and that this function satisfies the properties of a lawful Boolean equality function. More concisely: If `α` has a lawful equality, then for any list `l` of type `α` and element `a` not in `l`, the list `l` is equal to the list obtained by erasing `a` from `l`.
`List.suffix_refl` theorem List.suffix_refl : ∀ {α : Type u_1} (l : List α), l.IsSuffix l This theorem, `List.suffix_refl`, states that for any type `α` and for any list `l` of that type, `l` is a suffix of itself. In other words, it's saying that any list is a suffix of itself, which is intuitively true because you can append nothing to the end of a list to 'form' the same list. More concisely: For any list `l` of type `α`, `l` is a suffix of `l`.
`List.take_all_of_le` theorem List.take_all_of_le : ∀ {α : Type u_1} {n : ℕ} {l : List α}, l.length ≤ n → List.take n l = l This theorem states that for any type `α`, any natural number `n`, and any list `l` of type `α`, if the length of the list `l` is less than or equal to `n`, then taking the first `n` elements of `l` results in `l` itself. In other words, if you attempt to take more elements than a list has, you just get the list itself. More concisely: For any type `α`, any natural number `n`, and any list `l` of length `\|l\|` of type `α`, `take n l = l` when `\|l\| ≤ n`.
`List.IsSuffix.sublist` theorem List.IsSuffix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsSuffix l₂ → l₁.Sublist l₂ This theorem states that for any type `α` and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a suffix of `l₂` (denoted by `l₁ <:+ l₂`), then `l₁` is also a sublist of `l₂` (denoted by `List.Sublist l₁ l₂`). In other words, if one list ends with the same elements as another list, then the first list is a subsection of the second list. More concisely: If `α` is a type and `l₁` is a suffix of `l₂` (`l₁ <:+ l₂`) in lists of type `α`, then `l₁` is a sublist of `l₂` (`List.Sublist l₁ l₂`).
`List.takeWhile_append_dropWhile` theorem List.takeWhile_append_dropWhile : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.takeWhile p l ++ List.dropWhile p l = l The theorem `List.takeWhile_append_dropWhile` states that for any type `α`, any predicate function `p` of type `α → Bool`, and any list `l` of type `List α`, concatenating the list obtained by taking the longest initial segment of `l` for which `p` holds (`List.takeWhile p l`) with the list obtained by dropping elements from `l` until `p` fails (`List.dropWhile p l`) yields the original list `l`. This theorem asserts the equivalence of the original list and the newly formed list from the 'takeWhile' and 'dropWhile' segments. More concisely: For any type `α` and predicate function `p` on `α`, the list `takeWhile p xs ++ dropWhile p xs` equals the original list `xs`, where `xs` is a list of type `List α`, `takeWhile p xs` is the longest prefix of `xs` where `p` holds, and `dropWhile p xs` is the rest of `xs` after the longest prefix where `p` holds.
`List.Sublist.filter` theorem List.Sublist.filter : ∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Sublist l₂ → (List.filter p l₁).Sublist (List.filter p l₂) This theorem states that for any type `α`, any boolean function `p`, and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then the list obtained by filtering `l₁` using `p` is also a sublist of the list obtained by filtering `l₂` using `p`. In simpler terms, if one list is inside another, applying the same filter to both will result in a smaller list still inside the larger one, assuming the filter function behaves the same for every element. More concisely: If `l₁` is a sublist of `l₂` and `p` is a boolean function, then the sublist of `l₁` obtained by applying `p` is a sublist of the sublist of `l₂` obtained by applying `p`.
`List.IsPrefix.isInfix` theorem List.IsPrefix.isInfix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsPrefix l₂ → l₁.IsInfix l₂ This theorem states that for any type `α` and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a prefix of `l₂` (`l₁ <+: l₂`), then `l₁` is also an infix of `l₂` (`l₁ <:+: l₂`). In other words, if all elements of `l₁` appear at the beginning of `l₂` in the same order, then `l₁` must be a sublist of `l₂`, possibly appearing somewhere in the middle as well. More concisely: If `l₁` is a prefix of `list l₂` of type `α`, then `l₁` is a sublist (infix) of `l₂`.
`List.mem_replicate` theorem List.mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ List.replicate n a ↔ n ≠ 0 ∧ b = a This theorem states that for any type `α`, any elements `a` and `b` of type `α`, and any natural number `n`, the element `b` is a member of the list obtained by replicating `a` `n` times if and only if `n` is not zero and `b` equals `a`. In other words, `b` is in the list containing `n` copies of `a` exactly when `n` is not zero and `b` is same as `a`. More concisely: For any type `α`, any natural number `n`, and any elements `a` and `b` of type `α`, `b` is an element of the list of length `n+1` consisting of `a` repeated `n` times if and only if `n` is nonzero and `b = a`.
`List.Sublist.append` theorem List.Sublist.append : ∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, l₁.Sublist l₂ → r₁.Sublist r₂ → (l₁ ++ r₁).Sublist (l₂ ++ r₂) This theorem states that for any type `α` and any lists `l₁`, `l₂`, `r₁`, and `r₂` of this type, if `l₁` is a sublist of `l₂` and `r₁` is a sublist of `r₂`, then the list formed by appending `l₁` and `r₁` will be a sublist of the list formed by appending `l₂` and `r₂`. In mathematical terms, this can be written as: ∀α, l₁, l₂, r₁, r₂ ∈ List(α), l₁ ⊆ l₂ ∧ r₁ ⊆ r₂ → (l₁ ++ r₁) ⊆ (l₂ ++ r₂). More concisely: If `l₁` is a sublist of `l₂` and `r₁` is a sublist of `r₂`, then the concatenation of `l₁` and `r₁` is a sublist of the concatenation of `l₂` and `r₂` (for all types `α`).
`List.sublist_append_left` theorem List.sublist_append_left : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁.Sublist (l₁ ++ l₂) This theorem asserts that for any type 'α' and any two lists 'l₁' and 'l₂' of that type, 'l₁' is a sublist of the concatenation of 'l₁' and 'l₂'. In other words, if you concatenate a list with any other list, the original list will always be a sublist of the resulting list. More concisely: For any type 'α' and any lists 'l₁' and 'l₂' of that type, 'l₁' is a sublist of the concatenation of 'l₁' and 'l₂'. In mathematical notation: if $l\_1$ and $l\_2$ are lists of type $\alpha$, then $l\_1 \subseteq l\_1 \oplus l\_2$, where $\oplus$ denotes list concatenation.
`List.Subset.trans` theorem List.Subset.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ ⊆ l₂ → l₂ ⊆ l₃ → l₁ ⊆ l₃ This theorem states that for any three lists `l₁`, `l₂`, and `l₃` of any type `α`, if `l₁` is a subset of `l₂` and `l₂` is a subset of `l₃`, then `l₁` is a subset of `l₃`. This is a formal encoding of the transitive property of subset relationships in the context of lists. More concisely: If `l₁ ⊆ l₂` and `l₂ ⊆ l₃`, then `l₁ ⊆ l₃` (`l₁` is a subset of `l₃`).
`List.zip_map` theorem List.zip_map : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (l₁ : List α) (l₂ : List β), (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂) The theorem `List.zip_map` states that for any types `α`, `γ`, `β`, and `δ`, and any functions `f : α → γ` and `g : β → δ`, if you have two lists `l₁ : List α` and `l₂ : List β`, applying `f` to each element of `l₁` and `g` to each element of `l₂`, and then zipping these two lists together is equal to first zipping `l₁` and `l₂` together and then applying the function `Prod.map f g` (which applies `f` to the first component of a pair and `g` to the second) to each pair in the zipped list. In other words, zipping two mapped lists is equivalent to mapping the zipped list with the appropriately pair-wise function. More concisely: For any types `α`, `γ`, `β`, and `δ`, and functions `f : α → γ` and `g : β → δ`, the zip of the lists `List.map f l₁` and `List.map g l₂` is equal to `List.map (Prod.map f g) (List.zip l₁ l₂)`.
`List.filter_congr'` theorem List.filter_congr' : ∀ {α : Type u_1} {p q : α → Bool} {l : List α}, (∀ x ∈ l, p x = true ↔ q x = true) → List.filter p l = List.filter q l The theorem `List.filter_congr'` states that for any list `l` of elements of an arbitrary type `α`, and any two predicates `p` and `q` from `α` to `Bool`, if for all elements `x` in `l`, `p` returns `true` if and only if `q` returns `true`, then the result of filtering `l` with `p` equals the result of filtering `l` with `q`. In other words, if two predicates agree on every element of a list, then filtering the list based on these predicates will produce the same results. More concisely: If for all elements x in a list l, the predicates p and q agree (i.e., p(x) <-> q(x) holds), then List.filter p l = List.filter q l.
`List.append_ne_nil_of_ne_nil_right` theorem List.append_ne_nil_of_ne_nil_right : ∀ {α : Type u_1} (s t : List α), t ≠ [] → s ++ t ≠ [] This theorem states that for any two lists `s` and `t` of a certain type `α`, if the list `t` is not empty, then the result of appending `t` to `s` (i.e., `s ++ t`) will also not be empty. This holds for all types `α` and lists `s` and `t` of type `α`. More concisely: For all types `α` and non-empty lists `s` and `t` of type `α`, the concatenation `s ++ t` is a non-empty list.
`List.IsSuffix.isInfix` theorem List.IsSuffix.isInfix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsSuffix l₂ → l₁.IsInfix l₂ The theorem `List.IsSuffix.isInfix` states that for any type `α` and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a suffix of `l₂` then `l₁` is also an infix of `l₂`. In other words, if list `l₁` appears at the end of `l₂`, then it is also true that `l₁` appears somewhere within `l₂` (including at the end). More concisely: If `l₁` is a suffix of `l₂`, then `l₁` is also an infix of `l₂`. In other words, if the list `l₁` appears at the end of the list `l₂`, then `l₁` also appears somewhere within `l₂`.
`List.mem_singleton` theorem List.mem_singleton : ∀ {α : Type u_1} {a b : α}, a ∈ [b] ↔ a = b This theorem, `List.mem_singleton`, states that for any type `α` and any two elements `a` and `b` of type `α`, `a` is an element of the list containing only `b` if and only if `a` is equal to `b`. In other words, an element is a member of a singleton list if and only if it is equal to the single item in that list. More concisely: For any type α and any elements a, b of α, the list [b] contains a if and only if a = b.
`List.eq_replicate` theorem List.eq_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ} {l : List α}, l = List.replicate n a ↔ l.length = n ∧ ∀ b ∈ l, b = a The theorem `List.eq_replicate` states that for any type `α`, element `a` of type `α`, natural number `n`, and list `l` of type `α`, `l` equals `n` replicates of `a` if and only if the length of `l` equals `n` and every element `b` in `l` equals `a`. In other words, a list is equivalent to a list containing `n` repeated instances of an element `a` if the list has `n` elements and each of these elements is equal to `a`. More concisely: For any type `α`, natural number `n`, element `a` of type `α`, and list `l` of length `n` over `α`, `l` is equal to the list obtained by replicating `a n` times if and only if every element of `l` is equal to `a`.
`List.suffix_append` theorem List.suffix_append : ∀ {α : Type u_1} (l₁ l₂ : List α), l₂.IsSuffix (l₁ ++ l₂) This theorem states that for any type `α` and for any two lists `l₁` and `l₂` of type `α`, `l₂` is a suffix of the concatenation of `l₁` and `l₂`. In other words, if you append `l₂` to `l₁`, you will always end up with a list where `l₂` is the end part. This holds true for all types and lists. More concisely: For all types `α` and lists `l₁` and `l₂` of type `α`, `l₂` is a suffix of `l₁ ++ l₂`.
`List.range_eq_range'` theorem List.range_eq_range' : ∀ (n : ℕ), List.range n = List.range' 0 n This theorem states that for any natural number `n`, the function `List.range n` generates the same list as `List.range' 0 n`. In other words, whether we use `List.range` or `List.range'` with a starting point of zero, we will obtain the same list of natural numbers from `0` to `n-1` in increasing order. More concisely: For any natural number `n`, `List.range n` equals `List.range' 0 n`. In mathematical terms, the sets generated by these functions are equal.
`List.Sublist.append_right` theorem List.Sublist.append_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (l : List α), (l₁ ++ l).Sublist (l₂ ++ l) This theorem states that for any type `α`, and for any lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then for any other list `l` of type `α`, the list formed by appending `l` to `l₁` (`l₁ ++ l`) is a sublist of the list formed by appending `l` to `l₂` (`l₂ ++ l`). Here, "sublist" is used in the sense that elements of the first list appear in the second list in the same order, but possibly with other elements in between. More concisely: For any type `α` and lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then `l₁ ++ l` is a sublist of `l₂ ++ l` for any list `l` of type `α`.
`List.drop_one` theorem List.drop_one : ∀ {α : Type u_1} (l : List α), List.drop 1 l = l.tail This theorem states that for all lists `l` of any type `α`, removing the first element from the list `l` using the `List.drop` function with 1 as the argument (i.e., `List.drop 1 l`) is equivalent to obtaining the tail of the list `l` using the `List.tail` function (i.e., `List.tail l`). In other words, dropping one item from the start of a list gives the same result as retrieving the tail of the list. More concisely: For all lists `l` of type `α`, `List.drop 1 l` equals `List.tail l`.
`List.sublist_append_right` theorem List.sublist_append_right : ∀ {α : Type u_1} (l₁ l₂ : List α), l₂.Sublist (l₁ ++ l₂) This theorem states that for any type `α` and any two lists `l₁` and `l₂` of that type, `l₂` is a sublist of the list formed by appending `l₁` and `l₂`. In other words, all elements of `l₂` will appear in the same order in the list `l₁ ++ l₂`, possibly interspersed with elements from `l₁`. More concisely: For any type `α` and lists `l₁`, `l₂` of type `list α`, `l₂` is a sublist of `l₁ ++ l₂`.
`List.mem_append_left` theorem List.mem_append_left : ∀ {α : Type u_1} {a : α} {l₁ : List α} (l₂ : List α), a ∈ l₁ → a ∈ l₁ ++ l₂ This theorem, `List.mem_append_left`, posits that for any element `a` of a certain type `α`, and any list `l₁` of elements of type `α`, if `a` belongs to `l₁`, then `a` will also belong to the list obtained by appending another list `l₂` to `l₁`. In other words, if an element is in a list, it will still be in the list even after we append other elements to the end of the list. More concisely: If `a` is an element of list `l₁` and `l₂` is any list, then `a` is an element of the list obtained by appending `l₂` to `l₁` (denoted as `l₁ ++ l₂`).
`List.mem_join` theorem List.mem_join : ∀ {α : Type u_1} {a : α} {L : List (List α)}, a ∈ L.join ↔ ∃ l ∈ L, a ∈ l This theorem, `List.mem_join`, states that for any type `α`, any element `a` of type `α`, and any list `L` of lists of type `α`, the element `a` is a member of the list resulting from joining all lists in `L` (i.e., `List.join L`) if and only if there exists a sublist `l` in `L` such that `a` is a member of `l`. In other words, an element is in the joined list if it was in one of the original sublists. More concisely: For any type `α`, list `L` of lists of `α`, and element `a` of `α`, `a` is in `List.join L` if and only if there exists `l` in `L` such that `a` is in `l`.
`List.take_prefix` theorem List.take_prefix : ∀ {α : Type u_1} (n : ℕ) (l : List α), (List.take n l).IsPrefix l This theorem, named `List.take_prefix`, states that for any list `l` of elements of an arbitrary type `α` and for any natural number `n`, the prefix of `l` of length `n` (obtained by the `List.take` function) is indeed a prefix of `l`. In other words, taking the first `n` elements from a list always results in a sublist that is a prefix of the original list. More concisely: For any list `l` of length `m` and any natural number `n` less than or equal to `m`, `List.take l n` is a prefix of `l`.
`List.length_filter_le` theorem List.length_filter_le : ∀ {α : Type u_1} (p : α → Bool) (l : List α), (List.filter p l).length ≤ l.length := by sorry This theorem states that for any type `α` and any Boolean predicate `p` on `α`, as well as any list `l` of elements of type `α`, the length of the list obtained by filtering `l` with `p` is always less than or equal to the length of `l` itself. In other words, if you filter a list with some criteria, the resulting list is always the same size or smaller. This is intuitively clear since filtering can only remove elements, not add new ones. More concisely: For any type `α`, list `l` of `α`, and Boolean predicate `p` on `α`, the length of the filtered list `l.filter p` is less than or equal to the length of `l`.
`List.exists_of_mem_map` theorem List.exists_of_mem_map : ∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {f : α_1 → α} {l : List α_1}, b ∈ List.map f l → ∃ a ∈ l, f a = b := by sorry This theorem, `List.exists_of_mem_map`, states that for any types `α` and `α_1`, any function `f` from `α_1` to `α`, any list `l` of elements of type `α_1`, and any element `b` of type `α`, if `b` is an element of the list that results from mapping `f` over `l`, then there exists an element `a` in `l` such that applying `f` to `a` yields `b`. In other words, if `b` is in the image of the list `l` under the function `f`, then `b` is the image of some element of `l` under `f`. More concisely: If a list `l` of elements `α_1` maps to an element `b` of type `α` under a function `f: α_1 → α`, then there exists an element `a` in `l` such that `f(a) = b`.
`List.take_append_eq_append_take` theorem List.take_append_eq_append_take : ∀ {α : Type u_1} {l₁ l₂ : List α} {n : ℕ}, List.take n (l₁ ++ l₂) = List.take n l₁ ++ List.take (n - l₁.length) l₂ This theorem states that for any type `α`, any lists `l₁` and `l₂` of that type, and any natural number `n`, taking the first `n` elements from the list formed by appending `l₂` to the end of `l₁` is equivalent to appending the first `n - l₁.length` elements of `l₂` to the end of the first `n` elements of `l₁`. In other words, it shows how the `take` operation distributes over the concatenation of two lists. More concisely: For any type `α`, any lists `l₁` and `l₂` of length `m` and `n` respectively, and any natural number `n ≥ m`, the sublist of length `n` obtained by appending `l₂` to `l₁` is equal to the concatenation of the first `n - m` elements of `l₂` and the first `m` elements of `l₁`.
`List.disjoint_comm` theorem List.disjoint_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ l₂.Disjoint l₁ The theorem `List.disjoint_comm` states that for any two lists, `l₁` and `l₂`, of elements of an arbitrary type `α`, the property of the lists being disjoint is commutative. In other words, `l₁` and `l₂` have no elements in common if and only if `l₂` and `l₁` have no elements in common. This means that the order in which we consider the lists does not affect whether or not they are disjoint. More concisely: For any lists `l₁` and `l₂` over an arbitrary type `α`, `l₁` and `l₂` have no common elements if and only if `l₂` and `l₁` have no common elements.
`List.mem_reverse` theorem List.mem_reverse : ∀ {α : Type u_1} {x : α} {as : List α}, x ∈ as.reverse ↔ x ∈ as This theorem, `List.mem_reverse`, states that for any type `α`, any element `x` of type `α`, and any list `as` of type `α`, the membership of `x` in the reversed list `List.reverse as` is equivalent to the membership of `x` in the original list `as`. In other words, reversing the list does not affect the presence of an element in the list. More concisely: For any type `α` and list `as` of type `α`, the element `x` belongs to the reversed list `List.reverse as` if and only if it belongs to the original list `as`.
`List.zip_append` theorem List.zip_append : ∀ {α : Type u_1} {β : Type u_2} {l₁ r₁ : List α} {l₂ r₂ : List β}, l₁.length = l₂.length → (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂ This theorem, `List.zip_append`, states that for any types `α` and `β`, and any lists `l₁`, `r₁` of type `α`, and `l₂`, `r₂` of type `β`, if the lengths of `l₁` and `l₂` are equal, then the result of zipping the concatenation of `l₁` and `r₁` with the concatenation of `l₂` and `r₂` is equivalent to the concatenation of the zip of `l₁` and `l₂` with the zip of `r₁` and `r₂`. Zipping, in this context, refers to combining two lists into a list of pairs, with one element from each list. The longer list is truncated to match the shorter list. More concisely: For any types `α` and `β` and lists `l₁ : List α`, `l₂ : List β`, `r₁ : List α`, and `r₂ : List β` of equal lengths, `List.zip (l₁ ++ r₁) (l₂ ++ r₂) = List.append (List.zip l₁ l₂) (List.zip r₁ r₂)`.
`List.length_dropLast` theorem List.length_dropLast : ∀ {α : Type u_1} (xs : List α), xs.dropLast.length = xs.length - 1 This theorem states that for any list of elements of some type `α`, the length of the list obtained by removing the last element from the original list is equal to the length of the original list minus one. In other words, if `xs` is a list, then the length of `List.dropLast xs` (i.e., `xs` with its last element removed) is `List.length xs - 1`. This property holds for all lists, regardless of their length or the type of their elements. More concisely: For any list `xs` of length `n` over type `α`, the length of `List.dropLast (xs : List α)` is `n - 1`.
`List.eraseP_cons_of_neg` theorem List.eraseP_cons_of_neg : ∀ {α : Type u_1} {a : α} {l : List α} (p : α → Bool), ¬p a = true → List.eraseP p (a :: l) = a :: List.eraseP p l The theorem `List.eraseP_cons_of_neg` states that for any type `α`, an element `a` of type `α`, a list `l` of elements of type `α`, and a predicate `p` that takes an input of type `α` and outputs a Boolean, if `p a` is not true, then the result of applying the `eraseP` function to the list that results from consing `a` onto `l` (i.e., `a :: l`) is equal to `a` consed onto the result of applying `eraseP` to `l` itself. In other words, if the predicate does not hold for the head of the list, we can move it outside of the `eraseP` operation. More concisely: If `p(a)` is false, then `List.eraseP (a :: l) = a :: List.eraseP l`.
`List.mem_append_right` theorem List.mem_append_right : ∀ {α : Type u_1} {a : α} (l₁ : List α) {l₂ : List α}, a ∈ l₂ → a ∈ l₁ ++ l₂ This theorem states that for any type `α`, any element `a` of type `α`, any list `l₁` of type `α`, and any list `l₂` of type `α`, if `a` is an element of `l₂`, then `a` is also an element of the list formed by appending `l₁` and `l₂`. In other words, if an item is in the second list, it is also in the list which results from appending the first and second lists. More concisely: If `a` is an element of list `l₂`, then `a` is an element of the list obtained by appending `l₁` and `l₂`.
`List.sublist_cons` theorem List.sublist_cons : ∀ {α : Type u_1} (a : α) (l : List α), l.Sublist (a :: l) This theorem states that for any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, `l` is a sublist of the list formed by prepending `a` to `l`. In other words, if you have a list of items and add a new item to the front of the list, the original list is always a sublist of the updated list. More concisely: For any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, `a :: l` is a sublist of `l`.
`List.nil_union` theorem List.nil_union : ∀ {α : Type u_1} [inst : BEq α] (l : List α), [] ∪ l = l This theorem, `List.nil_union`, states that for all types `α`, given a list `l` of type `α`, the union of an empty list and `l` is equal to `l` itself. This is under the condition that the type `α` has a binary equality instance. In terms of set theory, it means that the union of an empty set with any set is the set itself. More concisely: For all types `α` with equality, the union of an empty list of type `α` and a list `l` of type `α` is equal to `l`.
`List.mem_insert_iff` theorem List.mem_insert_iff : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a b : α} {l : List α}, a ∈ List.insert b l ↔ a = b ∨ a ∈ l This theorem, `List.mem_insert_iff`, states that for any type `α` with an equality test (BEq) and a lawful equality test (LawfulBEq), and given any elements `a` and `b` of type `α` and a list `l` of elements of type `α`, an element `a` is a member of the list obtained by inserting `b` into `l` if and only if `a` is equal to `b` or `a` is already a member of `l`. This theorem encapsulates the principle that inserting an element into a list without duplication either leaves the membership of other elements unchanged, or adds the new element to the set of members. More concisely: For any type `α` with equality (=) and lawful equality test (LawfulBEq), and any list `l` of elements of type `α` and elements `a` and `b` of `α`, `a` is in the list obtained by inserting `b` into `l` if and only if `a = b` or `a` is already in `l`.
`List.mem_range'_1` theorem List.mem_range'_1 : ∀ {m s n : ℕ}, m ∈ List.range' s n ↔ s ≤ m ∧ m < s + n This theorem, `List.mem_range'_1`, states that for any natural numbers `m`, `s`, and `n`, `m` is an element of the list produced by the `range'` function starting from `s` and of length `n` if and only if `m` is greater than or equal to `s` and less than `s + n`. In other words, `m` is in the list range from `s` up to, but not including, `s + n`. More concisely: For natural numbers m, s, and n, m is an element of the range' list [from s to s + n] if and only if s ≤ m < s + n.
`List.length_pos` theorem List.length_pos : ∀ {α : Type u_1} {l : List α}, 0 < l.length ↔ l ≠ [] This theorem states that for any list `l` of elements of an arbitrary type `α`, the length of `l` is greater than 0 if and only if `l` is not an empty list. In other words, a list in Lean 4 has a positive length if and only if that list is not empty. More concisely: For any list `l` in Lean 4 of type `α`, the length of `l` is non-zero if and only if `l` is non-empty.
`List.get_drop` theorem List.get_drop : ∀ {α : Type u_1} (L : List α) {i j : ℕ} (h : i + j < L.length), L.get ⟨i + j, h⟩ = (List.drop i L).get ⟨j, ⋯⟩ := by sorry The theorem `List.get_drop` states that for any list `L` of arbitrary type `α` and for any natural numbers `i` and `j`, if `i + j` is less than the length of `L`, then the `i + j`-th element of `L` is the same as the `j`-th element of the list that results from dropping the first `i` elements of `L`. This theorem is expressed in a form that allows rewriting an expression concerning the large list `L` into an equivalent expression concerning the smaller list that results from dropping elements from `L`. More concisely: For any list `L` of length `n` and natural numbers `i` and `j` with `i + j < n`, the `(i + j)`-th element of `L` equals the `j`-th element of the sublist starting at index `i` in `L`.
`List.pair_mem_product` theorem List.pair_mem_product : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {x : α} {y : β}, (x, y) ∈ xs.product ys ↔ x ∈ xs ∧ y ∈ ys This theorem states that for any pair `(x, y)` and any two lists `xs` and `ys` of arbitrary types `α` and `β`, the pair `(x, y)` is in the cartesian product of the lists `xs` and `ys` (computed by `xs.product ys`) if and only if `x` is in `xs` and `y` is in `ys`. In other words, the elements of the pair must each be present in their respective lists for the pair to be considered a part of the cartesian product of those lists. More concisely: For any types `α` and `β` and lists `xs : list α` and `ys : list β`, the pair `(x, y)` is an element of `xs.product ys` if and only if `x ∈ xs` and `y ∈ ys`.
`List.foldl_hom` theorem List.foldl_hom : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁), (∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) → List.foldl g₂ (f init) l = f (List.foldl g₁ init l) This theorem, `List.foldl_hom`, establishes a homomorphism property for the `List.foldl` operation. It assumes types `α₁`, `α₂` and `β`, and functions `f : α₁ → α₂`, `g₁ : α₁ → β → α₁` and `g₂ : α₂ → β → α₂`. It also takes a list `l : List β` and an initial accumulator `init : α₁`. If `g₂` composed with `f` is equivalent to `f` composed with `g₁` for any pair of inputs `(x : α₁, y : β)`, then folding `l` from the left with `g₂` and `f init` is the same as applying `f` to the result of folding `l` from the left with `g₁` and `init`. This basically states that the function `f` can be "distributed" across the fold operation, under certain conditions. More concisely: If `g₂ ∘ f = f ∘ g₁` for all `x : α₁` and `y : β`, then `List.foldl g₂ x (List.map (λx => (f x, x)) l) = List.foldl g₁ x l`.
`List.Sublist.eq_of_length` theorem List.Sublist.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length = l₂.length → l₁ = l₂ This theorem states that for any two lists `l₁` and `l₂` of the same type `α`, if `l₁` is a sublist of `l₂` and both lists have the same length, then `l₁` is equal to `l₂`. In other words, if a list is a sublist of another list, and they have the same number of elements, then they must be the same list. More concisely: If two lists `l₁` and `l₂` of the same type `α` have the same length and `l₁` is a sublist of `l₂`, then `l₁ = l₂`.
`List.take_append` theorem List.take_append : ∀ {α : Type u_1} {l₁ l₂ : List α} (i : ℕ), List.take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ List.take i l₂ This theorem states that for any two lists `l₁` and `l₂` of the same type `α`, and a natural number `i`, taking the first `l₁.length + i` elements from the concatenated list `l₁ ++ l₂` is equivalent to appending the first `i` elements of `l₂` to `l₁`. Essentially, it describes a property of taking elements from a list that has been formed by concatenating two other lists. More concisely: For any lists `l₁` and `l₂` of the same type `α` and natural number `i`, the sublist of length `l₁.length + i` starting from the beginning of the concatenated list `l₁ ++ l₂` is equal to the appended list `l₁ ++ l₂[0..i-1]`.
`List.drop_append` theorem List.drop_append : ∀ {α : Type u_1} {l₁ l₂ : List α} (i : ℕ), List.drop (l₁.length + i) (l₁ ++ l₂) = List.drop i l₂ This theorem states that for any lists `l₁` and `l₂` of any type `α`, and any natural number `i`, dropping the first `l₁.length + i` elements from the concatenation of `l₁` and `l₂` is equivalent to dropping the first `i` elements from `l₂`. In other words, the drop operation will first consume elements from the first list, `l₁`, before it starts dropping elements from the second list, `l₂`. More concisely: For any lists `l₁` and `l₂` of length `m` and `n` respectively, and natural number `i` less than `m + n`, the sublist obtained by dropping the first `m + i` elements from the concatenation of `l₁` and `l₂` equals the sublist obtained by dropping the first `i` elements from `l₂`.
`List.cons_union` theorem List.cons_union : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l₁ l₂ : List α), a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂) This theorem, `List.cons_union`, asserts that for any given type `α` equipped with a boolean equality operation, and any element `a` of this type along with two lists `l₁` and `l₂` of the same type, the union of the list created by prepending `a` to `l₁` with `l₂` is equal to the result of first taking the union of `l₁` and `l₂`, and then inserting `a` into the resulting list (without duplication). The theorem takes into account the fact that inserting an element that is already present in the list doesn't change the list. More concisely: For any type `α` with equality, list `l₁`, list `l₂`, and element `a`, the list obtained by prepending `a` to `l₁` and then taking the union with `l₂` equals the union of `l₁` and `l₂` followed by the insertion of `a` without duplication.
`List.replicate_sublist_replicate` theorem List.replicate_sublist_replicate : ∀ {α : Type u_1} {m n : ℕ} (a : α), (List.replicate m a).Sublist (List.replicate n a) ↔ m ≤ n The theorem `List.replicate_sublist_replicate` states that for any type `α`, natural numbers `m` and `n`, and an element `a` of type `α`, the list which is the replication of `a` `m` times is a sublist of the list which is the replication of `a` `n` times if and only if `m` is less than or equal to `n`. This essentially means that a list made up of `m` copies of an element is contained within a list made up of `n` copies of the same element precisely when `m` is less than or equal to `n`. More concisely: For all type α, natural numbers m and n, and element a of α, the sublist a :: ... :: a (repeated m times) is contained in the sublist a :: ... :: a (repeated n times) if and only if m ≤ n.
`List.filter_filter` theorem List.filter_filter : ∀ {α : Type u_1} {p : α → Bool} (q : α → Bool) (l : List α), List.filter p (List.filter q l) = List.filter (fun a => decide (p a = true ∧ q a = true)) l The theorem `List.filter_filter` states that for any type `α`, any two boolean-valued functions `p` and `q` on `α`, and any list `l` of elements of type `α`, the process of first filtering `l` with `q` and then filtering the result with `p` is equivalent to filtering `l` once with a function that returns `true` for an element if and only if both `p` and `q` return `true` for that element. In other words, the composition of the filter functions is the same as the filter function for the logical conjunction of the original predicate functions. More concisely: The `List.filter_filter` theorem in Lean 4 asserts that for any list `l` and functions `p` and `q`, `List.filter (λx => p x ∧ q x) l` is equal to `List.filter q (List.filter p l)`.
`List.pairwise_map` theorem List.pairwise_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {R : α_1 → α_1 → Prop} {l : List α}, List.Pairwise R (List.map f l) ↔ List.Pairwise (fun a b => R (f a) (f b)) l The theorem `List.pairwise_map` states that for any type `α`, type `α_1`, a function `f` from `α` to `α_1`, a relation `R` on `α_1`, and a list `l` of type `α`, the property of being Pairwise `R` on the list obtained by mapping `f` over `l` (i.e., `List.map f l`) is equivalent to the property of the relation `R` when applied to function `f` on each pair of elements in `l` (i.e., `List.Pairwise (fun a b => R (f a) (f b)) l`). This means that if every pair of elements in the list obtained by applying `f` to `l` has the relationship `R`, then every pair of elements in the original list `l`, when transformed by function `f`, also has the relationship `R`, and vice versa. More concisely: For any type `α`, function `f` from `α` to `α_1`, relation `R` on `α_1`, and list `l` of type `α`, `List.map f l` has pairwise relationship `R` if and only if `l` has pairwise relationship `R` on each pair applied by `f`.
`List.get_range` theorem List.get_range : ∀ {n : ℕ} (i : ℕ) (H : i < (List.range n).length), (List.range n).get ⟨i, H⟩ = i This theorem, `List.get_range`, states a property about the function `List.range` and `List.get` on lists of natural numbers in Lean 4. Specifically, for any natural number `n`, and any index `i` such that `i` is less than the length of the list generated by `List.range n` (i.e., a list of all natural numbers from 0 to `n`, exclusive), the function `List.get` applied to the list `List.range n` at the position `i` will return `i`. In other words, if you have a list of the first `n` natural numbers and you pick the `i`-th element from this list (using zero-based indexing), you will get the number `i` itself. More concisely: For any natural number `n` and index `i` less than the length of `List.range n`, `List.get (List.range n) i = i`.
`List.mem_union_iff` theorem List.mem_union_iff : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {x : α} {l₁ l₂ : List α}, x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂ := by sorry This theorem states that for any type `α`, under the conditions that `α` has an equality test (`BEq α`) and that this equality test is lawful (`LawfulBEq α`), an element `x` of type `α` is in the union of two lists (`l₁ ∪ l₂`) if and only if `x` is in the first list `l₁` or in the second list `l₂`. In mathematical terms, given two lists `l₁` and `l₂`, an element `x` is a member of the union of `l₁` and `l₂` if and only if `x` is a member of `l₁` or `l₂`. More concisely: For any type `α` with lawful equality `BEq α`, an element `x` belongs to the union of two lists `l₁ ∪ l₂` if and only if `x` is in `l₁` or `l₂`.
`List.chain_cons` theorem List.chain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.Chain R a (b :: l) ↔ R a b ∧ List.Chain R b l := by sorry This theorem states that for any type `α`, any relation `R` of type `α → α → Prop`, any elements `a` and `b` of type `α`, and any list `l` of type `List α`, the property of `List.Chain R a (b :: l)` (which means that the relation `R` forms a chain from `a` through the list starting with `b` followed by `l`) is equivalent to the conjunction of two conditions: `R a b` (the relation `R` holds between `a` and `b`) and `List.Chain R b l` (the relation `R` forms a chain from `b` through the list `l`). More concisely: For any type `α`, relation `R` on `α`, and elements `a`, `b` in `α` and list `l` of `α`, `List.Chain R a (b :: l)` if and only if `R a b` and `List.Chain R b l`.
`List.IsInfix.sublist` theorem List.IsInfix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsInfix l₂ → l₁.Sublist l₂ This theorem states that for any type `α` and any lists `l₁` and `l₂` of type `α`, if `l₁` is an infix of `l₂` (expressed by the notation `l₁ <:+: l₂`), then `l₁` is also a sublist of `l₂` (expressed by `List.Sublist l₁ l₂`). In other words, if one list appears contiguously within another, then it can be derived from the second list by deleting zero or more elements, not necessarily from the ends. More concisely: If `α` is a type and `l₁` is an infix sublist of `l₂` (`l₁ <:+: l₂`), then `l₁` is a sublist of `l₂` (`List.Sublist l₁ l₂`).
`List.Subset.refl` theorem List.Subset.refl : ∀ {α : Type u_1} (l : List α), l ⊆ l This theorem, `List.Subset.refl`, states that for every list `l` of any type `α`, the list `l` is a subset of itself. In other words, each element in list `l` belongs to the list `l`. This is a reflection property of the subset relation for lists in Lean. More concisely: For any list `l` of type `α`, `l` is a subset of `l`.
`List.diff_cons` theorem List.diff_cons : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (l₁ l₂ : List α) (a : α), l₁.diff (a :: l₂) = (l₁.erase a).diff l₂ This theorem, `List.diff_cons`, states that for any type `α` that has a defined equality operation (`BEq α`), and for which this equality operation obeys certain laws (`LawfulBEq α`), and for any two lists (`l₁` and `l₂`) of this type `α` and any element `a` of type `α`, the difference of the first list and a new list made by prepending the element `a` to the second list (`a :: l₂`) is the same as the difference of the list obtained by removing `a` from the first list (`List.erase l₁ a`) and the original second list `l₂`. In other words, the order in which we remove elements when calculating the difference of two lists does not matter. More concisely: For any type `α` with a lawful equality, and lists `l₁` and `l₂` of type `List α`, the set difference between `l₁` and the list `a :: l₂` is equal to the set difference between `List.erase l₁ a` and `l₂`.
`List.insert_of_not_mem` theorem List.insert_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List α}, a ∉ l → List.insert a l = a :: l := by sorry This theorem states that for any type `α`, where `α` has an equality comparison and that comparison is lawful, if an element `a` of type `α` is not a member of a list `l` of elements of type `α`, then the operation of inserting `a` into `l` using the `List.insert` function results in the list that starts with `a` followed by the elements of `l`. More concisely: For any type `α` with lawful equality and list `l` of elements from `α`, if `a ≠ ∃ x, x ∈ l`, then `List.insert a l = a :: l`.
`List.Sublist.subset` theorem List.Sublist.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁ ⊆ l₂ This theorem states that for all types `α` and for all lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then `l₁` is a subset of `l₂`. In other words, every element of `l₁` is also an element of `l₂`. More concisely: For all types `α` and lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then `l₁ ⊆ l₂` (`l₁` is a subset of `l₂`).
`List.ne_nil_of_mem` theorem List.ne_nil_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → l ≠ [] This theorem states that for any type `α`, any element `a` of this type, and any list `l` of elements of this type, if `a` is an element of `l` (denoted by `a ∈ l`), then `l` is not an empty list (denoted by `l ≠ []`). In other words, if a list contains at least one element, then it cannot be the empty list. More concisely: For any type `α` and list `l` of length greater than 0 in `α`, if `a ∈ l`, then `l ≠ []`.
`List.infix_append` theorem List.infix_append : ∀ {α : Type u_1} (l₁ l₂ l₃ : List α), l₂.IsInfix (l₁ ++ l₂ ++ l₃) This theorem states that for any type `α` and for any three lists `l₁`, `l₂`, and `l₃` of type `α`, `l₂` is a suffix of the concatenation of `l₁`, `l₂`, and `l₃`. In mathematical terms, if you append `l₂` and `l₃` to the end of `l₁`, `l₂` will always be a part of the resulting list starting from some point towards the end. More concisely: For any type `α` and lists `l₁`, `l₂`, `l₃` of type `α`, `l₂` is a suffix of the concatenation of `l₁` and `l₃`.
`List.erase_cons_head` theorem List.erase_cons_head : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l : List α), (a :: l).erase a = l This theorem states that for any type `α`, given an instance of binary equality (`BEq`) for `α` and an instance of lawful binary equality (`LawfulBEq`), for any element `a` of type `α` and any list `l` of type `α`, when `a` is appended at the head of `l` to form a new list, and then `a` is erased from this new list, the resulting list is equal to the original list `l`. In other words, "erasing" the head of a list returns the tail of the list. More concisely: For any type `α` with instances of binary equality and lawful binary equality, appending and then erasing the head element of a list `l` of type `α` results in the original list `l`. In symbols, `append (a :: l) (erase a (a :: l)) ≡ l`.
`List.drop_append_eq_append_drop` theorem List.drop_append_eq_append_drop : ∀ {α : Type u_1} {l₁ l₂ : List α} {n : ℕ}, List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ List.drop (n - l₁.length) l₂ This theorem states that for any list `l1` and `l2` of elements of any type `α`, and for any natural number `n`, the operation of dropping the first `n` elements from the combined list `l1 ++ l2` is equivalent to first dropping the first `n` elements from `l1` and `l2` separately, where from `l2`, we drop `n - length of l1` elements, and then appending the two resultant lists. This means that the `drop` operation is distributive over the list concatenation operation. More concisely: For any lists `l1` and `l2` of length `m` and `n` respectively, and natural number `k` such that `m + n - k ≥ 0`, the lists `drop k (l1 ++ l2)` and `drop k l1 ++ drop (k - m) l2` are equal.
`List.IsPrefix.sublist` theorem List.IsPrefix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsPrefix l₂ → l₁.Sublist l₂ This theorem states that for any type `α` and any two lists `l₁` and `l₂` of this type, if `l₁` is a prefix of `l₂` (denoted as `l₁ <+: l₂`), then `l₁` is also a sublist of `l₂`. In other words, if all the elements of `l₁` appear at the start of `l₂` in the same order, then `l₁` is considered a sublist of `l₂`, where the elements of `l₁` need not be consecutive in `l₂` but must maintain their order. More concisely: If `α` is a type and `l₁` is a prefix of `l₂` (`l₁ <+: l₂`), then `l₁` is a sublist of `l₂`.
`List.reverse_suffix` theorem List.reverse_suffix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse.IsSuffix l₂.reverse ↔ l₁.IsPrefix l₂ := by sorry This theorem states that for all types `α` and for any two lists `l₁` and `l₂` of type `α`, the reverse of `l₁` is a suffix of the reverse of `l₂` if and only if `l₁` is a prefix of `l₂`. This is to say, if we reverse both lists, the property of `l₁` being a prefix of `l₂` transforms to its reverse being a suffix of the reverse of `l₂`, and vice versa. More concisely: For all types `α`, the reverse of list `l₁` being a suffix of the reverse of list `l₂` if and only if list `l₁` is a prefix of list `l₂`.
`List.forall_mem_nil` theorem List.forall_mem_nil : ∀ {α : Type u_1} (p : α → Prop), ∀ x ∈ [], p x This theorem states that for any property `p` that elements of some type `α` can have, any element `x` of type `α` that is in an empty list (denoted by `[]` in Lean) has the property `p`. Since there are no elements in an empty list, the statement is vacuously true for any `p` and `x`. More concisely: For any property `p`, any element `x` of type `α` in an empty list `[]` has property `p`. (Vacuously true)
`List.Sublist.trans` theorem List.Sublist.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.Sublist l₂ → l₂.Sublist l₃ → l₁.Sublist l₃ := by sorry This theorem states that, for any type `α` and any lists `l₁`, `l₂`, and `l₃` of type `α`, if `l₁` is a sublist of `l₂` and `l₂` is a sublist of `l₃`, then `l₁` is a sublist of `l₃`. This property is known as the transitivity of the sublist relation. More concisely: If `l₁` is a sublist of `l₂` and `l₂` is a sublist of `l₃`, then `l₁` is a sublist of `l₃`.
`List.replicate_succ` theorem List.replicate_succ : ∀ {α : Type u_1} (a : α) (n : ℕ), List.replicate (n + 1) a = a :: List.replicate n a := by sorry The theorem `List.replicate_succ` states that for any type `α`, any element `a` of type `α`, and any natural number `n`, replicating `a` `n+1` times is equivalent to prepending `a` to the list obtained by replicating `a` `n` times. In other words, creating a list with `n+1` copies of `a` is the same as taking a list with `n` copies of `a` and adding another `a` at the beginning. More concisely: For any type `α` and natural number `n`, `List.replicate (n + 1) a = a :: List.replicate n a`.
`List.get_replicate` theorem List.get_replicate : ∀ {α : Type u_1} (a : α) {n : ℕ} (m : Fin (List.replicate n a).length), (List.replicate n a).get m = a This theorem states that for any type `α`, any element `a` of type `α`, and any natural number `n`, if `m` is a valid index in the list of `n` copies of `a` (obtained using the `List.replicate` function), then the element at index `m` of this list is equal to `a`. In other words, every element in the list that consists of `n` repetitions of `a` is `a`. More concisely: For any type `α`, any natural number `n`, and any `α` element `a`, the `n`-th element in the list obtained by repeating `a` using `List.replicate` is equal to `a`.
`List.iota_eq_reverse_range'` theorem List.iota_eq_reverse_range' : ∀ (n : ℕ), List.iota n = (List.range' 1 n).reverse This theorem states that for any natural number `n`, the list `iota n` - which is a list of numbers from `1` to `n` in decreasing order - is equal to the reverse of the list `range' 1 n` - which is a list of numbers from `1` to `n` in increasing order. In other words, if you generate a list of numbers from `1` to `n` in ascending order and then reverse it, you will get the same list as if you generated a list of numbers from `1` to `n` in descending order. More concisely: For any natural number `n`, the list of decreasing integers from `1` to `n` (`iota n`) is equal to the reverse of the list of increasing integers from `1` to `n` (`range' 1 n`).
`List.drop_left` theorem List.drop_left : ∀ {α : Type u_1} (l₁ l₂ : List α), List.drop l₁.length (l₁ ++ l₂) = l₂ This theorem states that for any type `α` and for any two lists `l₁` and `l₂` of this type, when you concatenate the two lists (`l₁ ++ l₂`) and then remove the first `List.length l₁` elements from the result, you end up with the second list `l₂`. In other terms, if you have two lists and you append the second list to the first one, dropping the elements of the combined list that are equivalent in length to the first list will leave you with the second list. This is in line with our intuitive understanding of list concatenation and element dropping. More concisely: For any type `α` and lists `l₁` and `l₂` of length `m` and `n` respectively, `(l₁ ++ l₂).drop(m) = l₂`.
`List.filter_sublist` theorem List.filter_sublist : ∀ {α : Type u_1} {p : α → Bool} (l : List α), (List.filter p l).Sublist l The theorem `List.filter_sublist` states that, for any given type `α`, any Boolean-valued function `p` on elements from `α`, and any list `l` of type `List α`, the list obtained by applying `List.filter` with `p` on `l` is a sublist of `l`. In other words, filtering a list with any predicate results in a list that is a sublist of the original list. More concisely: For any type `α`, if `l` is a list of elements from `α` and `p` is a Boolean-valued function on `α`, then `List.filter p l` is a sublist of `l`.
`List.length_take` theorem List.length_take : ∀ {α : Type u_1} (i : ℕ) (l : List α), (List.take i l).length = min i l.length This theorem, `List.length_take`, states that for any index `i` and any list `l` of arbitrary type `α`, the length of the list obtained by taking the first `i` elements of `l` is equal to the minimum of `i` and the length of `l`. In other words, it says that if you take `i` elements from a list `l`, the length of the resulting list will be `i` if `i` is less than or equal to the length of `l`, and the length of `l` if `i` is greater than the length of `l`. More concisely: Let `l` be a list of length `n` and `i` be an index. Then, the length of the list obtained by taking the first `i` elements of `l` is minimally `i` or `n`.
`List.get?_set_ne` theorem List.get?_set_ne : ∀ {α : Type u_1} (a : α) {m n : ℕ} (l : List α), m ≠ n → (l.set m a).get? n = l.get? n := by sorry The theorem `List.get?_set_ne` states that for all types `α`, for all elements `a` of type `α`, for all natural numbers `m` and `n`, and for all lists `l` of type `α`, if `m` and `n` are not equal, then the `n`th element of the list resulting from setting the `m`th element of `l` to `a` is the same as the `n`th element of the initial list `l`. In other words, changing the `m`th element of a list does not affect the `n`th element if `m` and `n` are different. More concisely: For all types `α`, lists `l` of length `m+1` in `α`, and natural numbers `m ≠ n`, the `n`th element of the list `l.set m a` is equal to the `n`th element of `l`, where `a` is an element of `α`.
`List.filterMap_append` theorem List.filterMap_append : ∀ {α : Type u_1} {β : Type u_2} (l l' : List α) (f : α → Option β), List.filterMap f (l ++ l') = List.filterMap f l ++ List.filterMap f l' This theorem, `List.filterMap_append`, states that for any two lists `l` and `l'` of the same type `α`, and a function `f` that maps from `α` to an `Option β`, filtering and mapping the concatenation of `l` and `l'` (i.e., `l ++ l'`) using `f` is equivalent to concatenating the filtering and mapping of `l` and `l'` separately. In other words, the operation of `filterMap` over the concatenation of two lists produces the same result as concatenating the `filterMap` results of each list individually. More concisely: For any lists `l` and `l'` of type `α` and function `f : α → Option β`, `List.filterMap (λx => f x) (l ++ l')` is equivalent to `List.filterMap f l ++ List.filterMap f l'`.
`List.get_of_eq` theorem List.get_of_eq : ∀ {α : Type u_1} {l l' : List α} (h : l = l') (i : Fin l.length), l.get i = l'.get ⟨↑i, ⋯⟩ This theorem, `List.get_of_eq`, states that for any two lists `l` and `l'` of the same type `α`, if `l` equals `l'` as per the assumption `h`, then for any index `i` that is a non-negative integer less than the length of the list `l`, the elements at the index `i` in both lists `l` and `l'` are the same. This theorem is useful for rewriting expressions involving the `get` function applied to `l` in terms of `l'`. In other words, if you have an expression of the form `get l i hi` and you have an equality `h : l = l'`, then you can replace `get l i hi` with `get l' { val := ↑i, isLt := ⋯ }` using the `rw (get_of_eq h)` rewrite rule. More concisely: If two lists `l` and `l'` of the same type `α` are equal, then for any index `i` less than the length of `l`, the element at index `i` in both lists is equal.
`List.get?_set_eq` theorem List.get?_set_eq : ∀ {α : Type u_1} (a : α) (n : ℕ) (l : List α), (l.set n a).get? n = (fun x => a) <$> l.get? n The theorem `List.get?_set_eq` states that for any type `α`, any element `a` of type `α`, any natural number `n`, and any list `l` of type `α`, obtaining the `n`-th element of the list obtained by setting the `n`-th element of `l` to `a` is equal to applying the function (that always returns `a`) on the `n`-th element of `l` (if it exists). In other words, it states that if you replace the `n`-th element of a list with a new value, then retrieving the `n`-th element of the updated list will give you this new value, provided that the `n`-th element existed in the original list. More concisely: For any type `α`, list `l` of length `n+1` in `α`, and `a` in `α`, if the `n`-th element of `l` exists, then `List.get! (List.set l n a) = a`.
`List.Chain.imp` theorem List.Chain.imp : ∀ {α : Type u_1} {R S : α → α → Prop}, (∀ (a b : α), R a b → S a b) → ∀ {a : α} {l : List α}, List.Chain R a l → List.Chain S a l This theorem states that for any type `α` and two properties `R` and `S` that relate elements of type `α`, if it holds for all pairs `(a, b)` of type `α` that `R a b` implies `S a b`, then for any element `a` of type `α` and any list `l` of elements of type `α`, if the list `l` is a chain with respect to the property `R` starting from `a`, then the list `l` is also a chain with respect to the property `S` starting from `a`. In simpler terms, if `R` implies `S` for all pairs, then a chain of `R` relationships in a list also forms a chain of `S` relationships in that list. More concisely: If `R` implies `S` between all pairs of elements in a type `α`, then any chain of `R` relationships in a list of `α` is also a chain of `S` relationships.
`List.bind_map` theorem List.bind_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (g : α → List β) (l : List α), List.map f (l.bind g) = l.bind fun a => List.map f (g a) The `List.bind_map` theorem states that, for any types `β`, `γ`, and `α`, and any functions `f : β → γ` and `g : α → List β`, and any list `l : List α`, mapping function `f` over the list obtained by binding `l` with `g` is equivalent to binding `l` with a function that maps `f` over the list obtained by applying `g` to each element. In other words, it is asserting the equality of two operations: first binding then mapping, versus first mapping then binding, where binding refers to applying a function to each element of a list and joining the results. This is a formal expression of one of the monadic laws in the context of the list monad. More concisely: For any functions `f : β → γ` and `g : α → List β`, and any list `l : List α`, the application of `f` to the list obtained by binding `l` with `g` is equivalent to binding each element of `l` with `g` and then applying `f` to the resulting list.
`List.eq_of_mem_replicate` theorem List.eq_of_mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ List.replicate n a → b = a The theorem `List.eq_of_mem_replicate` states that for any type `α`, and any elements `a` and `b` of type `α`, and any natural number `n`, if `b` is an element in the list created by replicating `a` n times, then `b` must be equal to `a`. In other words, if `b` is in a list made up of `n` copies of `a`, then `b` has to be `a`. More concisely: For any type `α`, if `b` is the `n-th` element of a list `[a \| _ \| ... \| _]` of length `n+1` where every element except the first `n` is `a`, then `b = a`.
`List.get_take` theorem List.get_take : ∀ {α : Type u_1} (L : List α) {i j : ℕ} (hi : i < L.length) (hj : i < j), L.get ⟨i, hi⟩ = (List.take j L).get ⟨i, ⋯⟩ This theorem states that the `i`-th element of a list is the same as the `i`-th element of any of its prefixes whose length is greater than `i`. More specifically, given a list `L` of elements of any type `α`, and two natural numbers `i` and `j` such that `i` is less than the length of `L` and `i` is less than `j`, the `i`-th element of `L` and the `i`-th element of the list obtained by taking the first `j` elements of `L` are the same. This is intended to be used for rewriting expressions involving the `i`-th element of a large list to expressions involving the `i`-th element of a smaller list obtained by taking a prefix of the larger list. More concisely: For any list L of length n and natural numbers i and j with i < j < n, the ith element of L is equal to the ith element of the prefix of L of length j.
`List.drop_suffix` theorem List.drop_suffix : ∀ {α : Type u_1} (n : ℕ) (l : List α), (List.drop n l).IsSuffix l The theorem `List.drop_suffix` states that for any type `α`, any natural number `n`, and any list `l` of type `α`, the result of dropping the first `n` elements from `l` is a suffix of `l`. In other words, the list obtained by removing the first `n` elements from `l` is a sequence that can be found at the end of `l`. More concisely: For any type `α`, natural number `n`, and list `l` of length `m` over `α`, `List.drop n l` is a suffix of `l` of length `m-n`.
`List.Pairwise.chain` theorem List.Pairwise.chain : ∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α}, List.Pairwise R (a :: l) → List.Chain R a l This theorem states that for any type `α`, any binary relation `R` on `α`, any element `a` of `α`, and any list `l` of `α`, if the list that results from prepending `a` to `l` satisfies the property of being pairwise related by `R`, then `a` and every element of `l` are related by the chain relation `R`. This theorem is a part of the List module in Lean 4, which includes a variety of useful theorems and definitions related to lists. More concisely: If a list prefixed by an element `a` is pairwise related by a binary relation `R`, then `a` is related to every element in the list via the chain relation `R`.
`List.get_take'` theorem List.get_take' : ∀ {α : Type u_1} (L : List α) {j : ℕ} {i : Fin (List.take j L).length}, (List.take j L).get i = L.get ⟨↑i, ⋯⟩ := by sorry This theorem states that for any list `L` of type `α` and any natural number `j`, the `i`-th element of the list `L` is the same as the `i`-th element of any of its prefixes of length greater than `i`. This version of the theorem is designed to rewrite from the small list (the prefix of `L`) to the big list (`L`). Here, `i` is a finite number within the length of the small list, and the theorem ensures its validity within the length of the big list. More concisely: For any list `L` and natural number `i`, the `i`-th element of `L` equals the `i`-th element of any of its prefixes of length greater than `i`.
`List.findIdx_cons` theorem List.findIdx_cons : ∀ {α : Type u_1} (p : α → Bool) (b : α) (l : List α), List.findIdx p (b :: l) = bif p b then 0 else List.findIdx p l + 1 The theorem `List.findIdx_cons` states that for any type `α`, a boolean function `p` on `α`, an element `b` of type `α`, and a list `l` of elements of type `α`, the index of the first element in the list `b :: l` that satisfies function `p` is either 0 if `b` satisfies `p`, or it is one more than the index of the first element in list `l` that satisfies `p`. In other words, the function `List.findIdx` searches for the first element satisfying `p` in a list, and if the first element of the list `b` satisfies `p`, it returns 0, otherwise it proceeds to the rest of the list `l` and increases the index by 1. More concisely: For any list `l` of length `n+1` and any index `i` with `0 ≤ i ≤ n`, if `p(l(i))` holds and `p(l(j))` fails for all `0 ≤ j < i`, then `List.findIdx p l = Some i`. Otherwise, `List.findIdx p l = None` or `List.findIdx p l = Some (i + 1)`.
`List.zipWith_map_left` theorem List.zipWith_map_left : ∀ {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : α → α') (g : α' → β → γ), List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun a b => g (f a) b) l₁ l₂ The theorem `List.zipWith_map_left` states that for any two lists `l₁` of type `α` and `l₂` of type `β`, a function `f` that maps from `α` to `α'`, and a function `g` that maps from `α'` and `β` to `γ`, applying `List.zipWith` to the result of mapping `f` over `l₁` and `l₂` using `g` is the same as applying `List.zipWith` to `l₁` and `l₂` where the function applied for each pair is `g` composed with `f` on the element from `l₁`. In other words, it states the property that mapping a function over the first list before zipping is equivalent to zipping with the function composed with the mapping function. More concisely: For lists `l₁` of type `α` and `l₂` of type `β`, functions `f : α → α'` and `g : α' × β → γ`, `List.zipWith (g ∘ (f × id)) (f <$> l₁) l₂` is equivalent to `List.zipWith g l₁ l₂`.
`List.length_range'` theorem List.length_range' : ∀ (s step n : ℕ), (List.range' s n step).length = n The theorem `List.length_range'` asserts that for any natural numbers `s`, `step`, and `n`, the length of the list produced by the function `List.range'` with start point `s`, count `n`, and step size `step` is exactly `n`. In other words, when we create a list of natural numbers starting from `s`, with increments defined by `step`, and a total of `n` numbers, the length of this list will always be `n`, regardless of the values of `s` and `step`. More concisely: For any natural numbers `n`, `s`, and `step`, the length of the sequence `List.range' s (s + n - 1) step` equals `n`.
`List.prefix_refl` theorem List.prefix_refl : ∀ {α : Type u_1} (l : List α), l.IsPrefix l This theorem, `List.prefix_refl`, states that for any type of data `α` and a certain list `l` of that type, `l` is always a prefix of itself. In other words, any list `l` is considered as the starting subsequence of itself. More concisely: For any list `l` of type `α`, `l` is a prefix of itself.
`List.tail_eq_of_cons_eq` theorem List.tail_eq_of_cons_eq : ∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → t₁ = t₂ This theorem, `List.tail_eq_of_cons_eq`, states that for any given type `α`, if two lists `h₁ :: t₁` and `h₂ :: t₂` of type `α` are equal, where `h₁` and `h₂` are the head elements of the lists and `t₁` and `t₂` are their respective tails, then the tails `t₁` and `t₂` must be equal. In simpler terms, if two lists are equal, their tails must also be equal. More concisely: If `h₁ :: t₁` and `h₂ :: t₂` are equal lists, then `t₁` is equal to `t₂`.
`List.filter_append` theorem List.filter_append : ∀ {α : Type u_1} {p : α → Bool} (l₁ l₂ : List α), List.filter p (l₁ ++ l₂) = List.filter p l₁ ++ List.filter p l₂ The theorem `List.filter_append` is a property about lists in Lean 4. It states that for all types `α`, for any predicate function `p` from `α` to Boolean, and for any two lists `l₁` and `l₂` of type `α`, filtering (`List.filter`) the concatenation (`++`) of `l₁` and `l₂` with `p` is the same as concatenating the result of filtering `l₁` with `p` and filtering `l₂` with `p`. In other words, applying the filter before or after concatenating the lists does not change the result. More concisely: For all types `α` and predicate functions `p` on `α`, the filtered concatenation of lists `l₁` and `l₂` with predicate `p` is equal to the concatenation of the filtered lists `l₁` and `l₂`: `List.filter (p ++) l₁ (l₂++) = (List.filter p l₁) ++ (List.filter p l₂)`.
`List.erase_comm` theorem List.erase_comm : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a b : α) (l : List α), (l.erase a).erase b = (l.erase b).erase a The theorem `List.erase_comm` states that for any type `α` that has an equality comparison (`BEq α`) and respects the laws of equality (`LawfulBEq α`), given any two elements `a` and `b` of type `α` and a list `l` of elements of type `α`, the order of erasing `a` and `b` from the list `l` doesn't matter. In other words, erasing `a` first and then `b` from the list `l` is the same as erasing `b` first and then `a`. More concisely: For any type `α` with `BEq α` and `LawfulBEq α`, and any `a`, `b` in `α` and list `l` of `α`, erasing `a` then `b` from `l` is equal to erasing `b` then `a` from `l`.
`List.map_subset` theorem List.map_subset : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → β), l₁ ⊆ l₂ → List.map f l₁ ⊆ List.map f l₂ The theorem `List.map_subset` states that for all types `α` and `β`, and for all lists `l₁` and `l₂` of type `α`, and a function `f` from `α` to `β`, if `l₁` is a subset of `l₂`, then the list obtained by mapping `f` over `l₁` is a subset of the list obtained by mapping `f` over `l₂`. In other words, if every element of list `l₁` is also in list `l₂`, then applying a function to each element of `l₁` will yield a list where each element is also in the list obtained by applying the same function to each element of `l₂`. More concisely: For all types `α` and `β`, if `l₁ ⊆ l₂` are lists of type `α` and `f : α → β`, then `List.map f l₁ ⊆ List.map f l₂`.
`List.forall_mem_map_iff` theorem List.forall_mem_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {P : β → Prop}, (∀ i ∈ List.map f l, P i) ↔ ∀ j ∈ l, P (f j) This theorem states that for any two types `α` and `β`, a function `f` from `α` to `β`, a list `l` of type `α`, and a property `P` applicable on elements of type `β`, the property `P` holds for all elements in the list obtained by mapping `f` over `l` if and only if the property `P` holds for the result of applying `f` to all elements in `l`. In other words, applying `f` to each element of `l` and then checking if `P` holds for all elements is equivalent to checking if `P` holds for `f` of each element in `l`. More concisely: For any types `α`, `β`, property `P` on `β`, function `f` from `α` to `β`, and list `l` of type `α`, if `P` holds for all `x ∈ l` implies `P` holds for `f(x)`, then `P` holds for the list obtained by mapping `f` over `l`. Conversely, if `P` holds for each `f(x)` with `x ∈ l`, then `P` holds for the entire mapped list.
`List.take_left` theorem List.take_left : ∀ {α : Type u_1} (l₁ l₂ : List α), List.take l₁.length (l₁ ++ l₂) = l₁ The theorem `List.take_left` states that for any two lists `l₁` and `l₂` of elements of an arbitrary type `α`, if we append `l₁` and `l₂` and then take the first `n` elements of the resulting list, where `n` is the length of `l₁`, we get back the list `l₁`. In other words, taking the first `n` elements of the appended list is equivalent to simply retrieving the original list `l₁`. More concisely: For any lists `l₁` and `l₂` of length `n` over an arbitrary type `α`, `List.take_left l₁ (l₁ ++ l₂) = l₁`.
`List.sublist_nil` theorem List.sublist_nil : ∀ {α : Type u_1} {l : List α}, l.Sublist [] ↔ l = [] This theorem states that for all types `α` and any list `l` of type `α`, `l` is a sublist of an empty list if and only if `l` is also an empty list. In other words, non-empty lists cannot be sublists of an empty list. More concisely: For all types `α`, a list `l` of type `α` is a sublist of the empty list if and only if `l` is empty.
`List.reverse_prefix` theorem List.reverse_prefix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse.IsPrefix l₂.reverse ↔ l₁.IsSuffix l₂ := by sorry This theorem, `List.reverse_prefix`, states that for all types `α` and two lists of type `α`, `l₁` and `l₂`, the reverse of `l₁` is a prefix of the reverse of `l₂` if and only if `l₁` is a suffix of `l₂`. Here, a prefix of a list is a sublist that appears at the start of the list, and a suffix of a list is a sublist that appears at the end of the list. More concisely: For all types α and lists l₁ and l₂ of length m and n with m ≤ n, respectively, the reverses of l₁ and l₂ are equal as suffixes if and only if l₁ is a suffix of l₂.
`List.prefix_cons_inj` theorem List.prefix_cons_inj : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), (a :: l₁).IsPrefix (a :: l₂) ↔ l₁.IsPrefix l₂ This theorem states that for any type `α`, any lists `l₁` and `l₂`, and any element `a` of type `α`, `l₁` is a prefix of `l₂` if and only if the list resulting from prepending `a` to `l₁` is a prefix of the list resulting from prepending `a` to `l₂`. In other words, adding the same element to the start of two lists doesn't change their prefix relation. More concisely: For any type `α`, lists `l₁` and `l₂` of type `list α`, and element `a` of type `α`, the lists `l₁` is a prefix of `l₂` if and only if the list obtained by prepending `a` to `l₁` is a prefix of the list obtained by prepending `a` to `l₂`.
`List.mem_of_ne_of_mem` theorem List.mem_of_ne_of_mem : ∀ {α : Type u_1} {a y : α} {l : List α}, a ≠ y → a ∈ y :: l → a ∈ l This theorem states that for any type `α`, and any elements `a` and `y` of this type, and any list `l` of elements of type `α`, if `a` is not equal to `y` and `a` is an element of the list that results from prepending `y` to `l`, then `a` must be an element of `l`. In other words, if an item is in a list with a head it's not equal to, then it must be somewhere in the tail of the list. More concisely: If `a` is distinct from `y` and appears in the list `y :: l`, then `a` is an element of `l`.
`List.cons_ne_nil` theorem List.cons_ne_nil : ∀ {α : Type u_1} (a : α) (l : List α), a :: l ≠ [] This theorem, named `List.cons_ne_nil`, states that for any type of data `α` and any element `a` of type `α`, and any list `l` of type `α`, a list that begins with `a` and is followed by `l` is not equal to an empty list. This is a fundamental property of lists, asserting that a list with at least one element (the head of the list) is never equal to an empty list. More concisely: For any type `α` and elements `a : α` and `l : list α`, the list `[a] :: l` is not equal to the empty list `[]`.
`List.insert_of_mem` theorem List.insert_of_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List α}, a ∈ l → List.insert a l = l This theorem, `List.insert_of_mem`, states that for any type `α` that has a binary equality operation (`BEq`) and for which this equality operation obeys certain laws (`LawfulBEq`), if an element of type `α` named `a` is an element of a list `l` of elements of type `α` (written as `a ∈ l`), then inserting `a` into `l` using the `List.insert` function doesn't change the list; i.e., `List.insert a l = l`. This means that if the list already contains the element, the `List.insert` function does not duplicate it. More concisely: If `α` is a type with a `BEq` relation satisfying `LawfulBEq`, and `a ∈ l` is an element in list `l` of type `α`, then `List.insert a l = l`.
`List.disjoint_append_left` theorem List.disjoint_append_left : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l ↔ l₁.Disjoint l ∧ l₂.Disjoint l The theorem `List.disjoint_append_left` states that for any type `α` and any three lists of type `α`, `l₁`, `l₂`, and `l`, the proposition that `l₁` and `l₂` concatenated together are disjoint from `l` is equivalent to the conjunction of the propositions that `l₁` is disjoint from `l` and `l₂` is disjoint from `l`. In other words, a list `l` has no elements in common with the concatenation of `l₁` and `l₂` if and only if `l` has no elements in common with both `l₁` and `l₂`. More concisely: The theorem `List.disjoint_append_left` asserts that for any type `α` and lists `l₁`, `l₂`, and `l` of type `α`, `l₁` and `l₂` have no common elements with `l` if and only if `l₁` and `l₂` each have no common elements with `l`.
`List.map_add_range'` theorem List.map_add_range' : ∀ (a s n step : ℕ), List.map (fun x => a + x) (List.range' s n step) = List.range' (a + s) n step This theorem states that for all natural numbers `a`, `s`, `n` and `step`, the operation of mapping a function over a range of numbers, where the function adds `a` to each number in the list, is equivalent to creating a new range that starts at `a + s`. In other words, adding a constant `a` to each element of a list generated by `List.range' s n step` results in the same list as that generated by `List.range' (a + s) n step`. More concisely: For all natural numbers `a`, `s`, `n`, and `step`, the operation of adding `a` to each number in `List.range' s n step` is equivalent to generating `List.range' (a + s) n step`.
`List.Sublist.eq_of_length_le` theorem List.Sublist.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.length ≤ l₁.length → l₁ = l₂ The theorem `List.Sublist.eq_of_length_le` states that for any type `α`, and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂` and the length of `l₂` is less than or equal to the length of `l₁`, then `l₁` must be equal to `l₂`. Essentially, this means that if a list is a sublist of another, and they have the same length, they must be the same list. More concisely: If `l₁` is a sublist of `l₂` and the length of `l₁` is less than or equal to the length of `l₂`, then `l₁` equals `l₂`.
`List.cons_subset_cons` theorem List.cons_subset_cons : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁ ⊆ l₂ → a :: l₁ ⊆ a :: l₂ This theorem states that for any type `α` and any lists `l₁` and `l₂` of this type, along with any element `a` of this type, if `l₁` is a subset of `l₂`, then the list that starts with `a` followed by `l₁` is a subset of the list that starts with `a` followed by `l₂`. In other words, prepending the same element to two lists preserves the subset relationship between them. More concisely: If `l₁ ⊆ l₂` are lists of type `α`, then `a :: l₁ ⊆ a :: l₂`.
`List.diff_eq_foldl` theorem List.diff_eq_foldl : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (l₁ l₂ : List α), l₁.diff l₂ = List.foldl List.erase l₁ l₂ This theorem, `List.diff_eq_foldl`, states that for any type `α` that has an equality comparison operation and adheres to the laws of equality, and for any two lists `l₁` and `l₂` of type `α`, the difference of `l₁` and `l₂`, computed by the `List.diff` function, is equal to the result of folding the list `l₂` with the `List.erase` function starting with `l₁`. Folding here means applying the `List.erase` function successively to elements of `l₂` and the current result, starting with `l₁`. The `List.diff` function computes the difference by removing each element in `l₂` from `l₁`. The `List.erase` function removes the first occurrence of a particular element from a list. More concisely: For any type `α` with an equality operation adhering to the laws of equality, `List.diff (l₁ : list α) (l₂ : list α) = foldl (fun acc x => List.erase x acc) l₁ l₂`.
`List.get_drop'` theorem List.get_drop' : ∀ {α : Type u_1} (L : List α) {i : ℕ} {j : Fin (List.drop i L).length}, (List.drop i L).get j = L.get ⟨i + ↑j, ⋯⟩ The theorem `List.get_drop'` states that for any list `L` of elements of an arbitrary type `α`, and for any natural numbers `i` and `j` such that `j` is less than the length of the list obtained by dropping the first `i` elements of `L`, the `j`-th element of the list obtained by dropping the first `i` elements of `L` is equal to the `(i+j)`-th element of `L`. In other words, if we remove the first `i` elements from `L` and then take the `j`-th element, it is the same as if we directly took the `(i+j)`-th element from `L`. This theorem is useful when we want to transform expressions involving a larger list into expressions involving a smaller sublist. More concisely: For any list `L` of length `n+i` and natural numbers `i` and `j` with `0 <= j < n`, the `j`-th element of the sublist `L.drop i` is equal to the `(i+j)`-th element of `L`.
`List.mem_append` theorem List.mem_append : ∀ {α : Type u_1} {a : α} {s t : List α}, a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t This theorem, `List.mem_append`, states that for any type `α`, any element `a` of type `α`, and any two lists `s` and `t` of type `α`, `a` is a member of the list formed by appending `s` and `t` if and only if `a` is a member of `s` or `a` is a member of `t`. In other words, an element is in the concatenated list if it is in either of the original lists. More concisely: For any type `α`, list `s` and list `t` of type `α`, and element `a` of type `α`, `a ∈ s ++ t` if and only if `a ∈ s` or `a ∈ t`.
`List.dropLast_concat` theorem List.dropLast_concat : ∀ {α : Type u_1} {l₁ : List α} {b : α}, (l₁ ++ [b]).dropLast = l₁ The theorem `List.dropLast_concat` is stating that for any type `α`, any list `l₁` of type `α`, and any element `b` of type `α`, if we append `b` to the end of `l₁` to form a new list and then remove the last element of this new list, we will be left with the original list `l₁`. In other words, dropping the last element from the concatenation of a list `l₁` and a single-element list `[b]` results in the original list `l₁`. More concisely: For any type `α` and list `l₁` of length `n` over `α`, `List.dropLast (Suc n) (l₁ ++ [b]) = l₁` for all `b : α`.
`List.range'_append` theorem List.range'_append : ∀ (s m n step : ℕ), List.range' s m step ++ List.range' (s + step * m) n step = List.range' s (n + m) step := by sorry This theorem states that for any four natural numbers `s`, `m`, `n`, and `step`, the concatenation of the range from `s` to `s + step * m` with step size `step` and the range from `s + step * m` to `s + step * m + step * n` with step size `step` is equal to the range from `s` to `s + step * (n + m)` with step size `step`. The function `List.range'` generates a list of natural numbers starting from a specific number, increasing by a given step size. More concisely: For any natural numbers `s`, `m`, `n`, and `step`, the list of numbers from `s` to `s + step * (m + n)` with step size `step` is equal to the concatenation of the lists generated by `List.range'` with step `step` from `s` to `s + step * m` and from `s + step * m` to `s + step * (m + n)`.
`List.length_singleton` theorem List.length_singleton : ∀ {α : Type u_1} (a : α), [a].length = 1 This theorem states that for any type `α` and any element `a` of type `α`, the length of the list containing only `a` (`[a]`) is equal to 1. In other words, for any single-element list, its length is always 1, regardless of the type or value of the element contained in the list. More concisely: For any type `α` and any `a : α`, the length of the list `[a]` is equal to 1.
`List.set_eq_modifyNth` theorem List.set_eq_modifyNth : ∀ {α : Type u_1} (a : α) (n : ℕ) (l : List α), l.set n a = List.modifyNth (fun x => a) n l The theorem `List.set_eq_modifyNth` states that for any type `α`, element `a` of type `α`, natural number `n`, and list `l` of elements of type `α`, setting the `n`th element of `l` to `a` using the function `List.set` is equivalent to modifying the `n`th element of `l` with a function that always returns `a`, using the function `List.modifyNth`. In other words, these two operations on a list produce the same result. More concisely: For any type `α`, natural number `n`, element `a` of type `α`, and list `l` of length `n+1` over `α`, `List.set l n a` is equal to `List.modifyNth l n (λ x => if h: n = succ (Pred x.length then a else x) : list α)`.
`List.filterMap_filterMap` theorem List.filterMap_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → Option γ) (l : List α), List.filterMap g (List.filterMap f l) = List.filterMap (fun x => (f x).bind g) l The theorem `List.filterMap_filterMap` states that for any types `α`, `β`, and `γ`, and any functions `f : α → Option β`, `g : β → Option γ`, and any list `l` of type `List α`, filtering and mapping the list `l` with `f` first, and then with `g`, is equivalent to filtering and mapping `l` with a function that, given an element `x` of `l`, binds `f(x)` to `g`. This binding is done using the `Option.bind` function, which takes an optional value and a function, and if the optional value is `some a`, applies the function to `a`, resulting in a new optional value. More concisely: For any types `α`, `β`, and `γ`, and functions `f : α → Option β` and `g : β → Option γ`, the application of `List.filterMap` with `f` followed by `g` on a list `l` of type `List α` is equivalent to applying `List.filterMap` with the composed function `x ↦ Option.bind (f x) g`.
`List.length_pos_of_mem` theorem List.length_pos_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → 0 < l.length The theorem `List.length_pos_of_mem` states that for any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, if `a` is an element in `l` (denoted by `a ∈ l`), then the length of the list `l` is greater than zero. In other words, if a list contains an element, its length must be positive. More concisely: If `a` is an element of list `l` of length `n`, then `n` is a positive natural number.
`List.Sublist.filterMap` theorem List.Sublist.filterMap : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → Option β), l₁.Sublist l₂ → (List.filterMap f l₁).Sublist (List.filterMap f l₂) This theorem states that for any two lists `l₁` and `l₂` of any type `α`, and any function `f` from `α` to `Option β`, if `l₁` is a sublist of `l₂`, then the result of applying `filterMap` with `f` to `l₁` is also a sublist of the result of applying `filterMap` with `f` to `l₂`. In other words, the `filterMap` function preserves the sublist relation between `l₁` and `l₂`. More concisely: For any lists `l₁` and `l₂` of type `α` and any function `f : α → Option β`, if `l₁` is a sublist of `l₂`, then `filterMap f l₁` is a sublist of `filterMap f l₂`.

LeanAide GPT-4 documentation

Module: Std.Data.List.Lemmas

List.length_range

theorem List.length_range : ∀ (n : ℕ), (List.range n).length = n

List.infix_refl

theorem List.infix_refl : ∀ {α : Type u_1} (l : List α), l.IsInfix l

List.eraseP_cons_of_pos

theorem List.eraseP_cons_of_pos : ∀ {α : Type u_1} {a : α} {l : List α} (p : α → Bool), p a = true → List.eraseP p (a :: l) = l

List.Sublist.refl

theorem List.Sublist.refl : ∀ {α : Type u_1} (l : List α), l.Sublist l

List.nil_sublist

theorem List.nil_sublist : ∀ {α : Type u_1} (l : List α), [].Sublist l

List.map_singleton

theorem List.map_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), List.map f [a] = [f a]

List.range_succ_eq_map

theorem List.range_succ_eq_map : ∀ (n : ℕ), List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)

List.Sublist.length_le

theorem List.Sublist.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length

List.get?_range

theorem List.get?_range : ∀ {m n : ℕ}, m < n → (List.range n).get? m = some m

List.take_take

theorem List.take_take : ∀ {α : Type u_1} (n m : ℕ) (l : List α), List.take n (List.take m l) = List.take (min n m) l

List.Pairwise.sublist

theorem List.Pairwise.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α} {R : α → α → Prop}, l₁.Sublist l₂ → List.Pairwise R l₂ → List.Pairwise R l₁ := by sorry

List.erase_cons_tail

theorem List.erase_cons_tail : ∀ {α : Type u_1} [inst : BEq α] {a b : α} (l : List α), ¬(b == a) = true → (b :: l).erase a = b :: l.erase a := by sorry

List.exists_of_eraseP

theorem List.exists_of_eraseP : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {a : α}, a ∈ l → p a = true → ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂

List.subset_cons

theorem List.subset_cons : ∀ {α : Type u_1} (a : α) (l : List α), l ⊆ a :: l

List.rel_of_chain_cons

theorem List.rel_of_chain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.Chain R a (b :: l) → R a b

List.filterMap_eq_map

theorem List.filterMap_eq_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), List.filterMap (some ∘ f) = List.map f

List.leftpad_length

theorem List.leftpad_length : ∀ {α : Type u_1} (n : ℕ) (a : α) (l : List α), (List.leftpad n a l).length = max n l.length

List.erase_eq_eraseP

theorem List.erase_eq_eraseP : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l : List α), l.erase a = List.eraseP (fun x => a == x) l

List.Pairwise.imp

theorem List.Pairwise.imp : ∀ {α : Type u_1} {R S : α → α → Prop}, (∀ {a b : α}, R a b → S a b) → ∀ {l : List α}, List.Pairwise R l → List.Pairwise S l

List.getLast_append

theorem List.getLast_append : ∀ {α : Type u_1} {a : α} (l : List α) (h : l ++ [a] ≠ []), (l ++ [a]).getLast h = a := by sorry

List.mem_range

theorem List.mem_range : ∀ {m n : ℕ}, m ∈ List.range n ↔ m < n

List.singleton_sublist

theorem List.singleton_sublist : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Sublist l ↔ a ∈ l

List.eraseP_sublist

theorem List.eraseP_sublist : ∀ {α : Type u_1} {p : α → Bool} (l : List α), (List.eraseP p l).Sublist l

List.length_zipWith

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

List.filter_eq_self

theorem List.filter_eq_self : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = l ↔ ∀ a ∈ l, p a = true

List.get_singleton

theorem List.get_singleton : ∀ {α : Type u_1} (a : α) (n : Fin 1), [a].get n = a

List.erase_sublist

theorem List.erase_sublist : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), (l.erase a).Sublist l

List.filterMap_eq_filter

theorem List.filterMap_eq_filter : ∀ {α : Type u_1} (p : α → Bool), List.filterMap (Option.guard fun x => p x = true) = List.filter p

List.append_sublist_append_left

theorem List.append_sublist_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Sublist (l ++ l₂) ↔ l₁.Sublist l₂

List.eq_replicate_of_mem

theorem List.eq_replicate_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, (∀ b ∈ l, b = a) → l = List.replicate l.length a

List.range_succ

theorem List.range_succ : ∀ (n : ℕ), List.range n.succ = List.range n ++ [n]

List.erase_of_not_mem

theorem List.erase_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List α}, a ∉ l → l.erase a = l

List.suffix_refl

theorem List.suffix_refl : ∀ {α : Type u_1} (l : List α), l.IsSuffix l

List.take_all_of_le

theorem List.take_all_of_le : ∀ {α : Type u_1} {n : ℕ} {l : List α}, l.length ≤ n → List.take n l = l

List.IsSuffix.sublist

theorem List.IsSuffix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsSuffix l₂ → l₁.Sublist l₂

List.takeWhile_append_dropWhile

theorem List.takeWhile_append_dropWhile : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.takeWhile p l ++ List.dropWhile p l = l

List.Sublist.filter

theorem List.Sublist.filter : ∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Sublist l₂ → (List.filter p l₁).Sublist (List.filter p l₂)

List.IsPrefix.isInfix

theorem List.IsPrefix.isInfix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsPrefix l₂ → l₁.IsInfix l₂

List.mem_replicate

theorem List.mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ List.replicate n a ↔ n ≠ 0 ∧ b = a

`List.length_range`

`List.infix_refl`

`List.eraseP_cons_of_pos`

`List.Sublist.refl`

`List.nil_sublist`

`List.map_singleton`

`List.range_succ_eq_map`

`List.Sublist.length_le`

`List.get?_range`

`List.take_take`

`List.Pairwise.sublist`

`List.erase_cons_tail`

`List.exists_of_eraseP`

`List.subset_cons`

`List.rel_of_chain_cons`

`List.filterMap_eq_map`

`List.leftpad_length`

`List.erase_eq_eraseP`

`List.Pairwise.imp`

`List.getLast_append`

`List.mem_range`

`List.singleton_sublist`

`List.eraseP_sublist`

`List.length_zipWith`

`List.filter_eq_self`

`List.get_singleton`

`List.erase_sublist`

`List.filterMap_eq_filter`

`List.append_sublist_append_left`

`List.eq_replicate_of_mem`

`List.range_succ`

`List.erase_of_not_mem`

`List.suffix_refl`

`List.take_all_of_le`

`List.IsSuffix.sublist`

`List.takeWhile_append_dropWhile`

`List.Sublist.filter`

`List.IsPrefix.isInfix`

`List.mem_replicate`

`List.Sublist.append`

`List.sublist_append_left`

`List.Subset.trans`

`List.zip_map`

`List.filter_congr'`

`List.append_ne_nil_of_ne_nil_right`

`List.IsSuffix.isInfix`

`List.mem_singleton`

`List.eq_replicate`

`List.suffix_append`

`List.range_eq_range'`

`List.Sublist.append_right`

`List.drop_one`

`List.sublist_append_right`

`List.mem_append_left`

`List.mem_join`

`List.take_prefix`

`List.length_filter_le`

`List.exists_of_mem_map`

`List.take_append_eq_append_take`

`List.disjoint_comm`

`List.mem_reverse`

`List.zip_append`

`List.length_dropLast`

`List.eraseP_cons_of_neg`

`List.mem_append_right`

`List.sublist_cons`

`List.nil_union`

`List.mem_insert_iff`

`List.mem_range'_1`

`List.length_pos`

`List.get_drop`

`List.pair_mem_product`

`List.foldl_hom`

`List.Sublist.eq_of_length`