doc-next-gen

Init.Data.List.Sublist

Module docstring

{"# Lemmas about List.Subset, List.Sublist, List.IsPrefix, List.IsSuffix, and List.IsInfix. ","### isPrefixOf ","### isSuffixOf ","### Subset ","### List subset ","### Sublist and isSublist ","### IsPrefix / IsSuffix / IsInfix ","### Deprecations "}

List.isPrefixOf_cons₂_self theorem
[LawfulBEq α] {a : α} : isPrefixOf (a :: as) (a :: bs) = isPrefixOf as bs
Full source 
@[simp] theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} :
    isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons₂]
Prefix Preservation Under Cons: $\text{isPrefixOf}(a :: as, a :: bs) = \text{isPrefixOf}(as, bs)$
Informal description
For any type $\alpha$ with a lawful boolean equality relation, and for any element $a \in \alpha$ and lists $as, bs \in \text{List } \alpha$, the boolean check whether $(a :: as)$ is a prefix of $(a :: bs)$ is equal to the boolean check whether $as$ is a prefix of $bs$. In other words, $\text{isPrefixOf}(a :: as, a :: bs) = \text{isPrefixOf}(as, bs)$.
List.isPrefixOf_length_pos_nil theorem
{l : List α} (h : 0 < l.length) : isPrefixOf l [] = false
Full source 
@[simp] theorem isPrefixOf_length_pos_nil {l : List α} (h : 0 < l.length) : isPrefixOf l [] = false := by
  cases l <;> simp_all [isPrefixOf]
Non-empty List is Not a Prefix of the Empty List
Informal description
For any non-empty list $l$ (i.e., a list with length greater than 0), the boolean check whether $l$ is a prefix of the empty list `[]` returns `false`.
List.isPrefixOf_replicate theorem
{a : α} : isPrefixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a))
Full source 
@[simp] theorem isPrefixOf_replicate {a : α} :
    isPrefixOf l (replicate n a) = (decidedecide (l.length ≤ n) && l.all (· == a)) := by
  induction l generalizing n with
  | nil => simp
  | cons _ _ ih =>
    cases n
    · simp
    · simp [replicate_succ, isPrefixOf_cons₂, ih, Nat.succ_le_succ_iff, Bool.and_left_comm]
Prefix Condition for Replicated List: $\text{isPrefixOf}\,l\,(\text{replicate}\,n\,a) \leftrightarrow (\text{length}\,l \leq n) \land (\forall x \in l, x = a)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of type $\text{List}\,\alpha$, the boolean check whether $l$ is a prefix of the list $\text{replicate}\,n\,a$ (a list containing $n$ copies of $a$) is equivalent to the conjunction of: 1. The length of $l$ being less than or equal to $n$, and 2. All elements of $l$ being equal to $a$ under boolean equality. In symbols: $$\text{isPrefixOf}\,l\,(\text{replicate}\,n\,a) = (\text{length}\,l \leq n) \land (\forall x \in l, x = a)$$
List.isSuffixOf_cons_nil theorem
: isSuffixOf (a :: as) ([] : List α) = false
Full source 
@[simp] theorem isSuffixOf_cons_nil : isSuffixOf (a::as) ([] : List α) = false := by
  simp [isSuffixOf]
Non-empty List is Not a Suffix of the Empty List
Informal description
For any element $a$ of type $\alpha$ and any list $as$ of elements of type $\alpha$, the boolean check whether the non-empty list $a :: as$ is a suffix of the empty list `[]` returns `false`.
List.isSuffixOf_replicate theorem
{a : α} : isSuffixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a))
Full source 
@[simp] theorem isSuffixOf_replicate {a : α} :
    isSuffixOf l (replicate n a) = (decidedecide (l.length ≤ n) && l.all (· == a)) := by
  simp [isSuffixOf, all_eq]
Suffix Condition for Replicated List: $\text{isSuffixOf}\,l\,(\text{replicate}\,n\,a) \leftrightarrow (\text{length}\,l \leq n) \land (\forall x \in l, x = a)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of type $\text{List}\,\alpha$, the boolean check whether $l$ is a suffix of the list $\text{replicate}\,n\,a$ (a list containing $n$ copies of $a$) is equivalent to the conjunction of: 1. The length of $l$ being less than or equal to $n$, and 2. All elements of $l$ being equal to $a$ under boolean equality. In symbols: $$\text{isSuffixOf}\,l\,(\text{replicate}\,n\,a) = (\text{length}\,l \leq n) \land (\forall x \in l, x = a)$$
List.subset_def theorem
{l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂
Full source 
theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂ := .rfl
Characterization of List Subset Relation: $l₁ \subseteq l₂ \leftrightarrow \forall a \in l₁, a \in l₂$
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the subset relation $l₁ \subseteq l₂$ holds if and only if every element $a$ in $l₁$ is also an element of $l₂$.
List.nil_subset theorem
(l : List α) : [] ⊆ l
Full source 
@[simp] theorem nil_subset (l : List α) : [][] ⊆ l := nofun
Empty List is Subset of Any List
Informal description
For any list $l$ of elements of type $\alpha$, the empty list is a subset of $l$, i.e., $[] \subseteq l$.
List.Subset.refl theorem
(l : List α) : l ⊆ l
Full source 
@[simp] theorem Subset.refl (l : List α) : l ⊆ l := fun _ i => i
Reflexivity of List Subset Relation
Informal description
For any list $l$ of elements of type $\alpha$, the list is a subset of itself, i.e., $l \subseteq l$.
List.Subset.trans theorem
{l₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃
Full source 
theorem Subset.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ :=
  fun _ i => h₂ (h₁ i)
Transitivity of List Subset Relation
Informal description
For any lists $l₁$, $l₂$, and $l₃$ of elements of type $\alpha$, if $l₁$ is a subset of $l₂$ and $l₂$ is a subset of $l₃$, then $l₁$ is a subset of $l₃$.
List.instTransSubsetMem instance
: Trans (fun l₁ l₂ => Subset l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem
Full source 
instance : Trans (fun l₁ l₂ => Subset l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem :=
  ⟨fun h₁ h₂ => h₁ h₂⟩
Transitivity of Subset and Membership for Lists
Informal description
For any type $\alpha$, the subset relation $\subseteq$ on lists of type $\alpha$ and the membership relation $\in$ on elements of $\alpha$ are transitive in the following sense: if $l_1 \subseteq l_2$ and $a \in l_1$, then $a \in l_2$.
List.instTransSubset instance
: Trans (Subset : List α → List α → Prop) Subset Subset
Full source 
instance : Trans (Subset : List α → List α → Prop) Subset Subset :=
  ⟨Subset.trans⟩
Transitivity of List Subset Relation
Informal description
For any type $\alpha$, the subset relation $\subseteq$ on lists of type $\text{List } \alpha$ is transitive. That is, for any lists $l_1, l_2, l_3$ of elements of type $\alpha$, if $l_1 \subseteq l_2$ and $l_2 \subseteq l_3$, then $l_1 \subseteq l_3$.
List.subset_cons_self theorem
(a : α) (l : List α) : l ⊆ a :: l
Full source 
theorem subset_cons_self (a : α) (l : List α) : l ⊆ a :: l := fun _ => Mem.tail _
List is subset of its extension by prepending an element
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ is a subset of the list obtained by prepending $a$ to $l$, i.e., $l \subseteq a \cons l$.
List.subset_of_cons_subset theorem
{a : α} {l₁ l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂
Full source 
theorem subset_of_cons_subset {a : α} {l₁ l₂ : List α} : a :: l₁a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
  fun s _ i => s (mem_cons_of_mem _ i)
Subset Preservation under List Cons Removal
Informal description
For any element $a$ of type $\alpha$ and any lists $l_1, l_2$ of type $\text{List } \alpha$, if the list obtained by prepending $a$ to $l_1$ is a subset of $l_2$, then $l_1$ is also a subset of $l_2$.
List.subset_cons_of_subset theorem
(a : α) {l₁ l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂
Full source 
@[simp] theorem subset_cons_of_subset (a : α) {l₁ l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂ :=
  fun s _ i => .tail _ (s i)
Subset Preservation under List Cons Extension
Informal description
For any element $a$ of type $\alpha$ and any lists $l_1$ and $l_2$ of type $\text{List } \alpha$, if $l_1$ is a subset of $l_2$, then $l_1$ is also a subset of the list obtained by prepending $a$ to $l_2$, i.e., $l_1 \subseteq a :: l_2$.
List.cons_subset_cons theorem
{l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂
Full source 
theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁a :: l₁ ⊆ a :: l₂ :=
  fun _ => by simp only [mem_cons]; exact Or.imp_right (@s _)
Subset Preservation under List Cons Operation: $a :: l_1 \subseteq a :: l_2$ if $l_1 \subseteq l_2$
Informal description
For any element $a$ of type $\alpha$ and any lists $l_1, l_2$ of type $\text{List } \alpha$, if $l_1$ is a subset of $l_2$, then the list obtained by prepending $a$ to $l_1$ is a subset of the list obtained by prepending $a$ to $l_2$, i.e., $a :: l_1 \subseteq a :: l_2$.
List.cons_subset theorem
: a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m
Full source 
@[simp] theorem cons_subset : a :: la :: l ⊆ ma :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m := by
  simp only [subset_def, mem_cons, or_imp, forall_and, forall_eq]
Subset Condition for Cons List: $a :: l \subseteq m \leftrightarrow a \in m \land l \subseteq m$
Informal description
For any element $a$ of type $\alpha$ and lists $l, m$ of elements of type $\alpha$, the list $a :: l$ is a subset of $m$ if and only if $a$ is an element of $m$ and $l$ is a subset of $m$.
List.map_subset theorem
{l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂
Full source 
theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : mapmap f l₁ ⊆ map f l₂ :=
  fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
Mapping Preserves Subset Relation on Lists
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a subset of $l_2$ (i.e., every element of $l_1$ appears in $l_2$), then for any function $f : \alpha \to \beta$, the mapped list $f(l_1)$ is a subset of the mapped list $f(l_2)$.
List.filter_subset theorem
{l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂
Full source 
theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filterfilter p l₁ ⊆ filter p l₂ :=
  fun x => by simp_all [mem_filter, subset_def.1 H]
Filter Preserves Subset Relation on Lists
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a subset of $l_2$ (i.e., every element of $l_1$ appears in $l_2$), then for any predicate $p : \alpha \to \text{Bool}$, the filtered list $\text{filter } p \ l_1$ is a subset of the filtered list $\text{filter } p \ l_2$.
List.filterMap_subset theorem
{l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) : filterMap f l₁ ⊆ filterMap f l₂
Full source 
theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
    filterMapfilterMap f l₁ ⊆ filterMap f l₂ := by
  intro x
  simp only [mem_filterMap]
  rintro ⟨a, h, w⟩
  exact ⟨a, H h, w⟩
Subset Preservation under `filterMap`
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a subset of $l_2$ (i.e., every element of $l_1$ appears in $l_2$), then for any function $f : \alpha \to \text{Option } \beta$, the list obtained by applying `filterMap` $f$ to $l_1$ is a subset of the list obtained by applying `filterMap` $f$ to $l_2$.
List.subset_append_left theorem
(l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂
Full source 
theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
Left List is Subset of Concatenated List
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the list $l₁$ is a subset of the concatenated list $l₁ \mathbin{+\kern-0.5em+} l₂$.
List.subset_append_right theorem
(l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂
Full source 
theorem subset_append_right (l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂ := fun _ => mem_append_right _
Right List Subset Under Concatenation
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $l_2$ is a subset of the concatenated list $l_1 \mathbin{+\kern-0.5em+} l_2$.
List.subset_append_of_subset_left theorem
(l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂
Full source 
@[simp] theorem subset_append_of_subset_left (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂ :=
fun s => Subset.trans s <| subset_append_left _ _
Subset Preservation Under Left Concatenation
Informal description
For any list $l$ of elements of type $\alpha$ and any lists $l₁, l₂$ of elements of type $\alpha$, if $l$ is a subset of $l₁$, then $l$ is also a subset of the concatenated list $l₁ \mathbin{+\kern-0.5em+} l₂$.
List.subset_append_of_subset_right theorem
(l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂
Full source 
@[simp] theorem subset_append_of_subset_right (l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ :=
fun s => Subset.trans s <| subset_append_right _ _
Right Subset Preservation Under List Concatenation
Informal description
For any list $l_1$ of elements of type $\alpha$, if a list $l$ is a subset of another list $l_2$, then $l$ is also a subset of the concatenated list $l_1 \mathbin{+\kern-0.5em+} l_2$.
List.append_subset theorem
{l₁ l₂ l : List α} : l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l
Full source 
@[simp] theorem append_subset {l₁ l₂ l : List α} :
    l₁ ++ l₂ ⊆ ll₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l := by simp [subset_def, or_imp, forall_and]
Concatenation Subset Property: $l_1 ++ l_2 \subseteq l \leftrightarrow l_1 \subseteq l \land l_2 \subseteq l$
Informal description
For any lists $l_1$, $l_2$, and $l$ of elements of type $\alpha$, the concatenation $l_1 ++ l_2$ is a subset of $l$ if and only if both $l_1$ is a subset of $l$ and $l_2$ is a subset of $l$.
List.replicate_subset theorem
{n : Nat} {a : α} {l : List α} : replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l
Full source 
theorem replicate_subset {n : Nat} {a : α} {l : List α} : replicatereplicate n a ⊆ lreplicate n a ⊆ l ↔ n = 0 ∨ a ∈ l := by
  induction n with
  | zero => simp
  | succ n ih => simp +contextual [replicate_succ, ih, cons_subset]
Subset Condition for Replicated List: $\text{replicate}(n, a) \subseteq l \leftrightarrow n = 0 \lor a \in l$
Informal description
For any natural number $n$, any element $a$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the list $\text{replicate}(n, a)$ (containing $n$ copies of $a$) is a subset of $l$ if and only if either $n = 0$ or $a$ is an element of $l$.
List.subset_replicate theorem
{n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆ replicate n a ↔ ∀ x ∈ l, x = a
Full source 
theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆ replicate n al ⊆ replicate n a ↔ ∀ x ∈ l, x = a := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [cons_subset, mem_replicate, ne_eq, ih, mem_cons, forall_eq_or_imp,
      and_congr_left_iff, and_iff_right_iff_imp]
    solve_by_elim
Subset of Replicated List is Uniform: $l \subseteq \text{replicate}(n, a) \leftrightarrow \forall x \in l, x = a$ for $n \neq 0$
Informal description
For any natural number $n \neq 0$, any element $a$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the list $l$ is a subset of the list $\text{replicate}(n, a)$ (which contains $n$ copies of $a$) if and only if every element $x$ in $l$ is equal to $a$.
List.reverse_subset theorem
{l₁ l₂ : List α} : reverse l₁ ⊆ l₂ ↔ l₁ ⊆ l₂
Full source 
@[simp] theorem reverse_subset {l₁ l₂ : List α} : reversereverse l₁ ⊆ l₂reverse l₁ ⊆ l₂ ↔ l₁ ⊆ l₂ := by
  simp [subset_def]
Subset Preservation under List Reversal: $\text{reverse}(l_1) \subseteq l_2 \leftrightarrow l_1 \subseteq l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the reversed list $\text{reverse}(l_1)$ is a subset of $l_2$ if and only if $l_1$ is a subset of $l_2$.
List.subset_reverse theorem
{l₁ l₂ : List α} : l₁ ⊆ reverse l₂ ↔ l₁ ⊆ l₂
Full source 
@[simp] theorem subset_reverse {l₁ l₂ : List α} : l₁ ⊆ reverse l₂l₁ ⊆ reverse l₂ ↔ l₁ ⊆ l₂ := by
  simp [subset_def]
Subset Relation Preserved Under List Reversal: $l_1 \subseteq \text{reverse}(l_2) \leftrightarrow l_1 \subseteq l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $l_1$ is a subset of the reverse of $l_2$ if and only if $l_1$ is a subset of $l_2$.
List.nil_sublist theorem
: ∀ l : List α, [] <+ l
Full source 
@[simp] theorem nil_sublist : ∀ l : List α, [][] <+ l
  | [] => .slnil
  | a :: l => (nil_sublist l).cons a
Empty List is Sublist of Any List
Informal description
For any list $l$ of type $\text{List} \alpha$, the empty list is a sublist of $l$, i.e., $[] <+ l$.
List.Sublist.refl theorem
: ∀ l : List α, l <+ l
Full source 
@[simp] theorem Sublist.refl : ∀ l : List α, l <+ l
  | [] => .slnil
  | a :: l => (Sublist.refl l).cons₂ a
Reflexivity of the Sublist Relation
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is a sublist of itself, i.e., $l <+ l$.
List.Sublist.trans theorem
{l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) : l₁ <+ l₃
Full source 
theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) : l₁ <+ l₃ := by
  induction h₂ generalizing l₁ with
  | slnil => exact h₁
  | cons _ _ IH => exact (IH h₁).cons _
  | @cons₂ l₂ _ a _ IH =>
    generalize e : a :: l₂ = l₂' at h₁
    match h₁ with
    | .slnil => apply nil_sublist
    | .cons a' h₁' => cases e; apply (IH h₁').cons
    | .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂
Transitivity of the Sublist Relation: $l₁ <+ l₂$ and $l₂ <+ l₃$ implies $l₁ <+ l₃$
Informal description
For any three lists $l₁, l₂, l₃$ of elements of type $\alpha$, if $l₁$ is a sublist of $l₂$ (denoted $l₁ <+ l₂$) and $l₂$ is a sublist of $l₃$ (denoted $l₂ <+ l₃$), then $l₁$ is a sublist of $l₃$ (denoted $l₁ <+ l₃$).
List.instTransSublist instance
: Trans (@Sublist α) Sublist Sublist
Full source 
instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩
Transitivity of the Sublist Relation
Informal description
The sublist relation `<+` on lists is transitive. That is, for any lists `l₁`, `l₂`, `l₃` of type `List α`, if `l₁` is a sublist of `l₂` and `l₂` is a sublist of `l₃`, then `l₁` is a sublist of `l₃`.
List.sublist_cons_self theorem
(a : α) (l : List α) : l <+ a :: l
Full source 
theorem sublist_cons_self (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _
Sublist Property of List Cons Operation
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ is a sublist of the list obtained by prepending $a$ to $l$, i.e., $l <+ a :: l$.
List.sublist_of_cons_sublist theorem
: a :: l₁ <+ l₂ → l₁ <+ l₂
Full source 
theorem sublist_of_cons_sublist : a :: l₁a :: l₁ <+ l₂ → l₁ <+ l₂ :=
  (sublist_cons_self a l₁).trans
Sublist Preservation Under Head Removal
Informal description
For any element $a$ of type $\alpha$ and any lists $l₁, l₂$ of elements of type $\alpha$, if the list obtained by prepending $a$ to $l₁$ (i.e., $a :: l₁$) is a sublist of $l₂$, then $l₁$ itself is a sublist of $l₂$.
List.cons_sublist_cons theorem
: a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂
Full source 
@[simp]
theorem cons_sublist_cons : a :: l₁a :: l₁ <+ a :: l₂a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ :=
  ⟨fun | .cons _ s => sublist_of_cons_sublist s | .cons₂ _ s => s, .cons₂ _⟩
Sublist Preservation Under Cons Operation: $a :: l₁ <+ a :: l₂ \leftrightarrow l₁ <+ l₂$
Informal description
For any element $a$ of type $\alpha$ and any lists $l₁, l₂$ of elements of type $\alpha$, the list $a :: l₁$ is a sublist of $a :: l₂$ if and only if $l₁$ is a sublist of $l₂$.
List.sublist_or_mem_of_sublist theorem
(h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l₂ ∨ a ∈ l
Full source 
theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l₂l <+ l₁ ++ l₂ ∨ a ∈ l := by
  induction l₁ generalizing l with
  | nil => match h with
    | .cons _ h => exact .inl h
    | .cons₂ _ h => exact .inr (.head ..)
  | cons b l₁ IH =>
    match h with
    | .cons _ h => exact (IH h).imp_left (Sublist.cons _)
    | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)
Sublist Decomposition: $l <+ l_1 \mathbin{+\kern-0.5em+} (a :: l_2)$ implies $l <+ l_1 \mathbin{+\kern-0.5em+} l_2$ or $a \in l$
Informal description
For any lists $l$, $l_1$, $l_2$ and element $a$ of type $\alpha$, if $l$ is a sublist of $l_1 \mathbin{+\kern-0.5em+} (a :: l_2)$, then either $l$ is a sublist of $l_1 \mathbin{+\kern-0.5em+} l_2$ or $a$ is an element of $l$.
List.Sublist.subset theorem
: l₁ <+ l₂ → l₁ ⊆ l₂
Full source 
theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
  | .slnil, _, h => h
  | .cons _ s, _, h => .tail _ (s.subset h)
  | .cons₂ .., _, .head .. => .head ..
  | .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h)
Sublist Implies Subset for Lists
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then $l_1$ is a subset of $l_2$ (denoted $l_1 \subseteq l_2$). In other words, every element of $l_1$ appears in $l_2$.
List.Sublist.mem theorem
(hx : a ∈ l₁) (hl : l₁ <+ l₂) : a ∈ l₂
Full source 
protected theorem Sublist.mem (hx : a ∈ l₁) (hl : l₁ <+ l₂) : a ∈ l₂ :=
  hl.subset hx
Membership Preservation under Sublist Relation
Informal description
For any element $a$ of type $\alpha$ and lists $l₁$ and $l₂$ of type $\text{List } \alpha$, if $a$ is a member of $l₁$ and $l₁$ is a sublist of $l₂$, then $a$ is also a member of $l₂$.
List.Sublist.head_mem theorem
(s : ys <+ xs) (h) : ys.head h ∈ xs
Full source 
theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
  s.mem (List.head_mem h)
Head of Sublist is Member of Original List
Informal description
For any non-empty list `ys` that is a sublist of `xs`, the head element of `ys` is a member of `xs`.
List.Sublist.getLast_mem theorem
(s : ys <+ xs) (h) : ys.getLast h ∈ xs
Full source 
theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
  s.mem (List.getLast_mem h)
Last Element of Sublist Belongs to Original List
Informal description
For any nonempty list $ys$ and any list $xs$ of type $\text{List } \alpha$, if $ys$ is a sublist of $xs$ (denoted $ys <+ xs$), then the last element of $ys$ (obtained via $\text{getLast}(ys, h)$ where $h$ is a proof that $ys \neq []$) is an element of $xs$.
List.instTransSublistSubset instance
: Trans (@Sublist α) Subset Subset
Full source 
instance : Trans (@Sublist α) Subset Subset :=
  ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
Transitivity of Sublist and Subset Relations on Lists
Informal description
For any type $\alpha$, the sublist relation on lists is transitive with respect to the subset relation. That is, if $l_1$ is a sublist of $l_2$ and $l_2$ is a subset of $l_3$, then $l_1$ is a subset of $l_3$.
List.instTransSubsetSublist instance
: Trans Subset (@Sublist α) Subset
Full source 
instance : Trans Subset (@Sublist α) Subset :=
  ⟨fun h₁ h₂ => trans h₁ h₂.subset⟩
Transitivity of Subset and Sublist Relations on Lists
Informal description
For any type $\alpha$, the subset relation on lists is transitive with respect to the sublist relation. That is, if $l_1 \subseteq l_2$ and $l_2$ is a sublist of $l_3$, then $l_1 \subseteq l_3$.
List.instTransSublistMem instance
: Trans (fun l₁ l₂ => Sublist l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem
Full source 
instance : Trans (fun l₁ l₂ => Sublist l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem :=
  ⟨fun h₁ h₂ => h₁.subset h₂⟩
Transitivity of Sublist Reversal and Membership for Lists
Informal description
For any type $\alpha$, the relation that reverses the sublist order on lists of $\alpha$ is transitive with respect to the membership relation. That is, if $l_2$ is a sublist of $l_1$ and $a$ is a member of $l_2$, then $a$ is also a member of $l_1$.
List.mem_of_cons_sublist theorem
{a : α} {l₁ l₂ : List α} (s : a :: l₁ <+ l₂) : a ∈ l₂
Full source 
theorem mem_of_cons_sublist {a : α} {l₁ l₂ : List α} (s : a :: l₁a :: l₁ <+ l₂) : a ∈ l₂ :=
  (cons_subset.1 s.subset).1
Element Membership from Sublist Construction: $a \in l_2$ if $a :: l_1 <+ l_2$
Informal description
For any element $a$ of type $\alpha$ and lists $l_1, l_2$ of elements of type $\alpha$, if the list $a :: l_1$ is a sublist of $l_2$ (denoted $a :: l_1 <+ l_2$), then $a$ is an element of $l_2$ (denoted $a \in l_2$).
List.Sublist.length_le theorem
: l₁ <+ l₂ → length l₁ ≤ length l₂
Full source 
theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂
  | .slnil => Nat.le_refl 0
  | .cons _l s => le_succ_of_le (length_le s)
  | .cons₂ _ s => succ_le_succ (length_le s)
Sublist Implies Shorter or Equal Length
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₁$ is a sublist of $l₂$ (denoted $l₁ <+ l₂$), then the length of $l₁$ is less than or equal to the length of $l₂$, i.e., $\text{length}(l₁) \leq \text{length}(l₂)$.
List.Sublist.length_eq theorem
(s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂
Full source 
theorem Sublist.length_eq (s : l₁ <+ l₂) : lengthlength l₁ = length l₂ ↔ l₁ = l₂ :=
  ⟨s.eq_of_length, congrArg _⟩
Sublist Length Equality Criterion: $\text{length}(l₁) = \text{length}(l₂) \leftrightarrow l₁ = l₂$ for Sublists
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₁$ is a sublist of $l₂$ (denoted $l₁ <+ l₂$), then the lengths of $l₁$ and $l₂$ are equal if and only if $l₁$ is equal to $l₂$.
List.tail_sublist theorem
: ∀ l : List α, tail l <+ l
Full source 
theorem tail_sublist : ∀ l : List α, tailtail l <+ l
  | [] => .slnil
  | a::l => sublist_cons_self a l
Tail Sublist Property: $\text{tail}(l) <+ l$
Informal description
For any list $l$ of elements of type $\alpha$, the tail of $l$ is a sublist of $l$ itself.
List.Sublist.tail theorem
: ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → tail l₁ <+ tail l₂
Full source 
protected theorem Sublist.tail : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → tailtail l₁ <+ tail l₂
  | _, _, slnil => .slnil
  | _, _, Sublist.cons _ h => (tail_sublist _).trans h
  | _, _, Sublist.cons₂ _ h => h
Sublist Relation Preserved Under Taking Tails: $\text{tail}(l_1) <+ \text{tail}(l_2)$ if $l_1 <+ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the tail of $l_1$ is a sublist of the tail of $l_2$ (denoted $\text{tail}(l_1) <+ \text{tail}(l_2)$).
List.Sublist.of_cons_cons theorem
{l₁ l₂ : List α} {a b : α} (h : a :: l₁ <+ b :: l₂) : l₁ <+ l₂
Full source 
theorem Sublist.of_cons_cons {l₁ l₂ : List α} {a b : α} (h : a :: l₁a :: l₁ <+ b :: l₂) : l₁ <+ l₂ :=
  h.tail
Sublist Preservation Under Cons Removal: $l_1 <+ l_2$ if $a :: l_1 <+ b :: l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$ and any two elements $a$ and $b$ of type $\alpha$, if the list $a :: l_1$ is a sublist of $b :: l_2$, then $l_1$ is a sublist of $l_2$.
List.Sublist.map theorem
(f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂
Full source 
protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : mapmap f l₁ <+ map f l₂ := by
  induction s with
  | slnil => simp
  | cons a s ih =>
    simpa using cons (f a) ih
  | cons₂ a s ih =>
    simpa using cons₂ (f a) ih
Mapping Preserves Sublist Relation: $\text{map}\ f\ l_1 <+ \text{map}\ f\ l_2$ if $l_1 <+ l_2$
Informal description
For any function $f : \alpha \to \beta$ and lists $l_1, l_2$ of type $\text{List}\ \alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the mapped list $\text{map}\ f\ l_1$ is a sublist of $\text{map}\ f\ l_2$.
List.Sublist.filterMap theorem
(f : α → Option β) (s : l₁ <+ l₂) : filterMap f l₁ <+ filterMap f l₂
Full source 
protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
    filterMapfilterMap f l₁ <+ filterMap f l₂ := by
  induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons, cons₂]
Sublist Preservation under `filterMap`
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the result of applying `filterMap f` to $l_1$ is a sublist of the result of applying `filterMap f` to $l_2$.
List.Sublist.filter theorem
(p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂
Full source 
protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filterfilter p l₁ <+ filter p l₂ := by
  rw [← filterMap_eq_filter]; apply s.filterMap
Sublist Preservation under Filtering: $\text{filter}\ p\ l_1 <+ \text{filter}\ p\ l_2$ if $l_1 <+ l_2$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and lists $l_1, l_2 : \text{List}\ \alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the filtered list $\text{filter}\ p\ l_1$ is a sublist of $\text{filter}\ p\ l_2$.
List.head_filter_mem theorem
(xs : List α) (p : α → Bool) (h) : (xs.filter p).head h ∈ xs
Full source 
theorem head_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).head h ∈ xs :=
  filter_sublist.head_mem h
Head of Filtered List Belongs to Original List
Informal description
For any list $xs$ of elements of type $\alpha$, any predicate $p : \alpha \to \text{Bool}$, and any proof $h$ that the filtered list $xs.\text{filter } p$ is non-empty, the head element of $xs.\text{filter } p$ is a member of the original list $xs$.
List.getLast_filter_mem theorem
(xs : List α) (p : α → Bool) (h) : (xs.filter p).getLast h ∈ xs
Full source 
theorem getLast_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).getLast h ∈ xs :=
  filter_sublist.getLast_mem h
Last Element of Filtered List Belongs to Original List
Informal description
For any list $xs$ of type $\text{List}\ \alpha$, any predicate $p : \alpha \to \text{Bool}$, and any proof $h$ that the filtered list $\text{filter}\ p\ xs$ is non-empty, the last element of $\text{filter}\ p\ xs$ is an element of $xs$.
List.sublist_filterMap_iff theorem
{l₁ : List β} {f : α → Option β} : l₁ <+ l₂.filterMap f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filterMap f
Full source 
theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} :
    l₁ <+ l₂.filterMap fl₁ <+ l₂.filterMap f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filterMap f := by
  induction l₂ generalizing l₁ with
  | nil => simp
  | cons a l₂ ih =>
    simp only [filterMap_cons]
    split
    · simp only [ih]
      constructor
      · rintro ⟨l', h, rfl⟩
        exact ⟨l', Sublist.cons a h, rfl⟩
      · rintro ⟨l', h, rfl⟩
        cases h with
        | cons _ h =>
          exact ⟨l', h, rfl⟩
        | cons₂ _ h =>
          rename_i l'
          exact ⟨l', h, by simp_all⟩
    · constructor
      · intro w
        cases w with
        | cons _ h =>
          obtain ⟨l', s, rfl⟩ := ih.1 h
          exact ⟨l', Sublist.cons a s, rfl⟩
        | cons₂ _ h =>
          rename_i l'
          obtain ⟨l', s, rfl⟩ := ih.1 h
          refine ⟨a :: l', Sublist.cons₂ a s, ?_⟩
          rwa [filterMap_cons_some]
      · rintro ⟨l', h, rfl⟩
        replace h := h.filterMap f
        rwa [filterMap_cons_some] at h
        assumption
Sublist-FilterMap Equivalence: $l_1 <+ \text{filterMap}\ f\ l_2 \leftrightarrow \exists l', l' <+ l_2 \land l_1 = \text{filterMap}\ f\ l'$
Informal description
For any list $l_1$ of type $\text{List}\ \beta$ and function $f : \alpha \to \text{Option}\ \beta$, the following are equivalent: 1. $l_1$ is a sublist of $\text{filterMap}\ f\ l_2$ (i.e., $l_1 <+ \text{filterMap}\ f\ l_2$) 2. There exists a list $l'$ such that $l'$ is a sublist of $l_2$ and $l_1 = \text{filterMap}\ f\ l'$ In other words, a list $l_1$ is a sublist of the filtered and mapped version of $l_2$ if and only if $l_1$ itself is the filtered and mapped version of some sublist of $l_2$.
List.sublist_map_iff theorem
{l₁ : List β} {f : α → β} : l₁ <+ l₂.map f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.map f
Full source 
theorem sublist_map_iff {l₁ : List β} {f : α → β} :
    l₁ <+ l₂.map fl₁ <+ l₂.map f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.map f := by
  simp only [← filterMap_eq_map, sublist_filterMap_iff]
Sublist-Map Equivalence: $l_1 <+ \text{map}\ f\ l_2 \leftrightarrow \exists l', l' <+ l_2 \land l_1 = \text{map}\ f\ l'$
Informal description
For any list $l_1$ of type $\text{List}\ \beta$ and function $f : \alpha \to \beta$, the following are equivalent: 1. $l_1$ is a sublist of $l_2.\text{map}\ f$ (i.e., $l_1 <+ l_2.\text{map}\ f$) 2. There exists a list $l'$ such that $l'$ is a sublist of $l_2$ and $l_1 = l'.\text{map}\ f$ In other words, a list $l_1$ is a sublist of the mapped version of $l_2$ if and only if $l_1$ itself is the mapped version of some sublist of $l_2$.
List.sublist_filter_iff theorem
{l₁ : List α} {p : α → Bool} : l₁ <+ l₂.filter p ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filter p
Full source 
theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} :
    l₁ <+ l₂.filter pl₁ <+ l₂.filter p ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filter p := by
  simp only [← filterMap_eq_filter, sublist_filterMap_iff]
Sublist-Filter Equivalence: $l_1 <+ \text{filter}\ p\ l_2 \leftrightarrow \exists l', l' <+ l_2 \land l_1 = \text{filter}\ p\ l'$
Informal description
For any list $l_1$ of type $\text{List}\ \alpha$ and predicate $p : \alpha \to \text{Bool}$, the following are equivalent: 1. $l_1$ is a sublist of the filtered list $\text{filter}\ p\ l_2$ (i.e., $l_1 <+ \text{filter}\ p\ l_2$) 2. There exists a list $l'$ such that $l'$ is a sublist of $l_2$ and $l_1 = \text{filter}\ p\ l'$ In other words, a list $l_1$ is a sublist of the filtered version of $l_2$ if and only if $l_1$ itself is the filtered version of some sublist of $l_2$.
List.sublist_append_left theorem
: ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂
Full source 
theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂
  | [], _ => nil_sublist _
  | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons₂ _
Left Sublist Property of List Concatenation
Informal description
For any two lists $l_1$ and $l_2$ of type $\text{List} \alpha$, the list $l_1$ is a sublist of the concatenation $l_1 ++ l_2$.
List.sublist_append_right theorem
: ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
Full source 
theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
  | [], _ => Sublist.refl _
  | _ :: l₁, l₂ => (sublist_append_right l₁ l₂).cons _
Right Sublist Property of List Concatenation
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the list $l₂$ is a sublist of the concatenation $l₁ ++ l₂$.
List.singleton_sublist theorem
{a : α} {l} : [a] <+ l ↔ a ∈ l
Full source 
@[simp] theorem singleton_sublist {a : α} {l} : [a][a] <+ l[a] <+ l ↔ a ∈ l := by
  refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩
  obtain ⟨_, _, rfl⟩ := append_of_mem h
  exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)
Sublist Characterization of Singleton Membership: $[a] <+ l \leftrightarrow a \in l$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of type $\text{List} \alpha$, the singleton list $[a]$ is a sublist of $l$ if and only if $a$ is a member of $l$. In other words, $[a] <+ l \leftrightarrow a \in l$.
List.sublist_append_of_sublist_left theorem
(s : l <+ l₁) : l <+ l₁ ++ l₂
Full source 
@[simp] theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ :=
  s.trans <| sublist_append_left ..
Left Sublist Preservation Under Concatenation: $l <+ l_1 \to l <+ l_1 ++ l_2$
Informal description
For any lists $l$, $l_1$, and $l_2$ of elements of type $\alpha$, if $l$ is a sublist of $l_1$ (denoted $l <+ l_1$), then $l$ is also a sublist of the concatenation $l_1 ++ l_2$.
List.sublist_append_of_sublist_right theorem
(s : l <+ l₂) : l <+ l₁ ++ l₂
Full source 
@[simp] theorem sublist_append_of_sublist_right (s : l <+ l₂) : l <+ l₁ ++ l₂ :=
  s.trans <| sublist_append_right ..
Right Sublist Preservation under List Concatenation
Informal description
For any lists $l$, $l₁$, and $l₂$ of elements of type $\alpha$, if $l$ is a sublist of $l₂$ (denoted $l <+ l₂$), then $l$ is also a sublist of the concatenation $l₁ ++ l₂$.
List.append_sublist_append_left theorem
: ∀ l, l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂
Full source 
@[simp] theorem append_sublist_append_left : ∀ l, l ++ l₁ <+ l ++ l₂l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂
  | [] => Iff.rfl
  | _ :: l => cons_sublist_cons.trans (append_sublist_append_left l)
Left Concatenation Preserves Sublist Relation: $l ++ l_1 <+ l ++ l_2 \leftrightarrow l_1 <+ l_2$
Informal description
For any lists $l$, $l_1$, and $l_2$ of elements of type $\alpha$, the concatenation $l ++ l_1$ is a sublist of $l ++ l_2$ if and only if $l_1$ is a sublist of $l_2$.
List.Sublist.append_left theorem
: l₁ <+ l₂ → ∀ l, l ++ l₁ <+ l ++ l₂
Full source 
theorem Sublist.append_left : l₁ <+ l₂ → ∀ l, l ++ l₁ <+ l ++ l₂ :=
  fun h l => (append_sublist_append_left l).mpr h
Left Concatenation Preserves Sublist Relation
Informal description
For any lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then for any list $l$ of elements of type $\alpha$, the concatenation $l ++ l_1$ is a sublist of $l ++ l_2$.
List.Sublist.append_right theorem
: l₁ <+ l₂ → ∀ l, l₁ ++ l <+ l₂ ++ l
Full source 
theorem Sublist.append_right : l₁ <+ l₂ → ∀ l, l₁ ++ l <+ l₂ ++ l
  | .slnil, _ => Sublist.refl _
  | .cons _ h, _ => (h.append_right _).cons _
  | .cons₂ _ h, _ => (h.append_right _).cons₂ _
Right Concatenation Preserves Sublist Relation
Informal description
For any lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₁$ is a sublist of $l₂$, then for any list $l$ of elements of type $\alpha$, the concatenation $l₁ ++ l$ is a sublist of the concatenation $l₂ ++ l$.
List.Sublist.append theorem
(hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂
Full source 
theorem Sublist.append (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ :=
  (hl.append_right _).trans ((append_sublist_append_left _).2 hr)
Concatenation Preserves Sublist Relation: $l_1 <+ l_2 \land r_1 <+ r_2 \Rightarrow l_1 ++ r_1 <+ l_2 ++ r_2$
Informal description
For any lists $l_1, l_2, r_1, r_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$ and $r_1$ is a sublist of $r_2$, then the concatenation $l_1 ++ r_1$ is a sublist of the concatenation $l_2 ++ r_2$.
List.sublist_cons_iff theorem
{a : α} {l l'} : l <+ a :: l' ↔ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'
Full source 
theorem sublist_cons_iff {a : α} {l l'} :
    l <+ a :: l'l <+ a :: l' ↔ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l' := by
  constructor
  · intro h
    cases h with
    | cons _ h => exact Or.inl h
    | cons₂ _ h => exact Or.inr ⟨_, rfl, h⟩
  · rintro (h | ⟨r, rfl, h⟩)
    · exact h.cons _
    · exact h.cons₂ _
Sublist Condition for Cons: $l <+ a :: l' \leftrightarrow l <+ l' \lor (\exists r, l = a :: r \land r <+ l')$
Informal description
For any element $a$ of type $\alpha$ and lists $l, l'$ of type $\text{List }\alpha$, the sublist relation $l <+ a :: l'$ holds if and only if either $l$ is a sublist of $l'$ or there exists a list $r$ such that $l = a :: r$ and $r$ is a sublist of $l'$.
List.cons_sublist_iff theorem
{a : α} {l l'} : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
Full source 
theorem cons_sublist_iff {a : α} {l l'} :
    a :: la :: l <+ l'a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂ := by
  induction l' with
  | nil => simp
  | cons a' l' ih =>
    constructor
    · intro w
      cases w with
      | cons _ w =>
        obtain ⟨r₁, r₂, rfl, h₁, h₂⟩ := ih.1 w
        exact ⟨a' :: r₁, r₂, by simp, mem_cons_of_mem a' h₁, h₂⟩
      | cons₂ _ w =>
        exact ⟨[a], l', by simp, mem_singleton_self _, w⟩
    · rintro ⟨r₁, r₂, w, h₁, h₂⟩
      rw [w, ← singleton_append]
      exact Sublist.append (by simpa) h₂
Sublist Condition for Cons: $a :: l <+ l' \leftrightarrow \exists r_1 r_2, l' = r_1 ++ r_2 \land a \in r_1 \land l <+ r_2$
Informal description
For any element $a$ of type $\alpha$ and lists $l, l'$ of elements of type $\alpha$, the list $a :: l$ is a sublist of $l'$ if and only if there exist lists $r_1$ and $r_2$ such that $l' = r_1 ++ r_2$, $a$ is an element of $r_1$, and $l$ is a sublist of $r_2$.
List.sublist_append_iff theorem
{l : List α} : l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
Full source 
theorem sublist_append_iff {l : List α} :
    l <+ r₁ ++ r₂l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂ := by
  induction r₁ generalizing l with
  | nil =>
    constructor
    · intro w
      refine ⟨[], l, by simp_all⟩
    · rintro ⟨l₁, l₂, rfl, w₁, w₂⟩
      simp_all
  | cons r r₁ ih =>
    constructor
    · intro w
      simp only [cons_append] at w
      cases w with
      | cons _ w =>
        obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
        exact ⟨l₁, l₂, rfl, Sublist.cons r w₁, w₂⟩
      | cons₂ _ w =>
        rename_i l
        obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
        refine ⟨r :: l₁, l₂, by simp, cons_sublist_cons.mpr w₁, w₂⟩
    · rintro ⟨l₁, l₂, rfl, w₁, w₂⟩
      cases w₁ with
      | cons _ w₁ =>
        exact Sublist.cons _ (Sublist.append w₁ w₂)
      | cons₂ _ w₁ =>
        rename_i l
        exact Sublist.cons₂ _ (Sublist.append w₁ w₂)
Sublist Characterization via Concatenation: $l <+ r_1 ++ r_2 \leftrightarrow \exists l_1 l_2, l = l_1 ++ l_2 \land l_1 <+ r_1 \land l_2 <+ r_2$
Informal description
For any list $l$ of elements of type $\alpha$, $l$ is a sublist of the concatenation $r_1 ++ r_2$ if and only if there exist lists $l_1$ and $l_2$ such that $l = l_1 ++ l_2$, $l_1$ is a sublist of $r_1$, and $l_2$ is a sublist of $r_2$.
List.append_sublist_iff theorem
{l₁ l₂ : List α} : l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
Full source 
theorem append_sublist_iff {l₁ l₂ : List α} :
    l₁ ++ l₂ <+ rl₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂ := by
  induction l₁ generalizing r with
  | nil =>
    constructor
    · intro w
      refine ⟨[], r, by simp_all⟩
    · rintro ⟨r₁, r₂, rfl, -, w₂⟩
      simp only [nil_append]
      exact sublist_append_of_sublist_right w₂
  | cons a l₁ ih =>
    constructor
    · rw [cons_append, cons_sublist_iff]
      rintro ⟨r₁, r₂, rfl, h₁, h₂⟩
      obtain ⟨s₁, s₂, rfl, t₁, t₂⟩ := ih.1 h₂
      refine ⟨r₁ ++ s₁, s₂, by simp, ?_, t₂⟩
      rw [← singleton_append]
      exact Sublist.append (by simpa) t₁
    · rintro ⟨r₁, r₂, rfl, h₁, h₂⟩
      exact Sublist.append h₁ h₂
Concatenation Sublist Characterization: $l_1 ++ l_2 <+ r \leftrightarrow \exists r_1 r_2, r = r_1 ++ r_2 \land l_1 <+ r_1 \land l_2 <+ r_2$
Informal description
For any lists $l_1, l_2$ of elements of type $\alpha$, the concatenation $l_1 ++ l_2$ is a sublist of $r$ if and only if there exist lists $r_1, r_2$ such that $r = r_1 ++ r_2$, $l_1$ is a sublist of $r_1$, and $l_2$ is a sublist of $r_2$.
List.Sublist.of_sublist_append_left theorem
(w : ∀ a, a ∈ l → a ∉ l₂) (h : l <+ l₁ ++ l₂) : l <+ l₁
Full source 
theorem Sublist.of_sublist_append_left (w : ∀ a, a ∈ l → a ∉ l₂) (h : l <+ l₁ ++ l₂) : l <+ l₁ := by
  rw [sublist_append_iff] at h
  obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
  have : l₂' = [] := by
    rw [eq_nil_iff_forall_not_mem]
    exact fun x m => w x (mem_append_right l₁' m) (h₂.mem m)
  simp_all
Sublist Extraction from Left Append: $(\forall a \in l, a \notin l_2) \land l <+ l_1 \mathbin{+\kern-0.5em+} l_2 \implies l <+ l_1$
Informal description
For any lists $l, l_1, l_2$ of elements of type $\alpha$, if no element of $l$ appears in $l_2$ and $l$ is a sublist of the concatenation $l_1 \mathbin{+\kern-0.5em+} l_2$, then $l$ is a sublist of $l_1$.
List.Sublist.of_sublist_append_right theorem
(w : ∀ a, a ∈ l → a ∉ l₁) (h : l <+ l₁ ++ l₂) : l <+ l₂
Full source 
theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h : l <+ l₁ ++ l₂) : l <+ l₂ := by
  rw [sublist_append_iff] at h
  obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
  have : l₁' = [] := by
    rw [eq_nil_iff_forall_not_mem]
    exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)
  simp_all
Sublist Extraction from Right Append: $(\forall a \in l, a \notin l_1) \land l <+ l_1 \mathbin{+\kern-0.5em+} l_2 \implies l <+ l_2$
Informal description
For any list $l$ of elements of type $\alpha$, if every element in $l$ does not belong to $l_1$ and $l$ is a sublist of the concatenation $l_1 \mathbin{+\kern-0.5em+} l_2$, then $l$ is a sublist of $l_2$.
List.Sublist.middle theorem
{l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂
Full source 
theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂ := by
  rw [sublist_append_iff] at h
  obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
  exact Sublist.append h₁ (h₂.cons a)
Sublist Preservation Under Middle Insertion: $l <+ l_1 ++ l_2 \Rightarrow l <+ l_1 ++ (a :: l_2)$
Informal description
For any list $l$ of elements of type $\alpha$, if $l$ is a sublist of the concatenation $l_1 ++ l_2$, then for any element $a \in \alpha$, $l$ is also a sublist of $l_1 ++ (a :: l_2)$ (where $a :: l_2$ denotes the list obtained by prepending $a$ to $l_2$).
List.Sublist.reverse theorem
: l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
Full source 
theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
  | .slnil => Sublist.refl _
  | .cons _ h => by rw [reverse_cons]; exact sublist_append_of_sublist_left h.reverse
  | .cons₂ _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _
Reversal Preserves Sublist Relation: $l_1 <+ l_2 \to l_1^{\text{rev}} <+ l_2^{\text{rev}}$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$, then the reverse of $l_1$ is a sublist of the reverse of $l_2$.
List.reverse_sublist theorem
: l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂
Full source 
@[simp] theorem reverse_sublist : l₁.reverse <+ l₂.reversel₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ :=
  ⟨fun h => l₁.reverse_reverse ▸ l₂.reverse_reverse ▸ h.reverse, Sublist.reverse⟩
Sublist Relation is Preserved Under Reversal: $l_1^{\text{rev}} <+ l_2^{\text{rev}} \leftrightarrow l_1 <+ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the reverse of $l_1$ is a sublist of the reverse of $l_2$ if and only if $l_1$ is a sublist of $l_2$.
List.sublist_reverse_iff theorem
: l₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂
Full source 
theorem sublist_reverse_iff : l₁ <+ l₂.reversel₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂ :=
  by rw [← reverse_sublist, reverse_reverse]
Sublist Relation Under List Reversal: $l_1 <+ l_2^{\text{rev}} \leftrightarrow l_1^{\text{rev}} <+ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $l_1$ is a sublist of the reverse of $l_2$ if and only if the reverse of $l_1$ is a sublist of $l_2$. In symbols: $$ l_1 <+ l_2^{\text{rev}} \leftrightarrow l_1^{\text{rev}} <+ l_2 $$
List.append_sublist_append_right theorem
(l) : l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂
Full source 
@[simp] theorem append_sublist_append_right (l) : l₁ ++ l <+ l₂ ++ ll₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂ :=
  ⟨fun h => by
    have := h.reverse
    simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this
    exact this,
   fun h => h.append_right l⟩
Right Concatenation Preserves Sublist Relation: $l_1 \mathbin{+\!\!+} l <+ l_2 \mathbin{+\!\!+} l \leftrightarrow l_1 <+ l_2$
Informal description
For any lists $l_1$ and $l_2$ of elements of type $\alpha$, and any list $l$ of elements of type $\alpha$, the concatenation $l_1 \mathbin{+\!\!+} l$ is a sublist of $l_2 \mathbin{+\!\!+} l$ if and only if $l_1$ is a sublist of $l_2$.
List.replicate_sublist_replicate theorem
{m n} (a : α) : replicate m a <+ replicate n a ↔ m ≤ n
Full source 
@[simp] theorem replicate_sublist_replicate {m n} (a : α) :
    replicatereplicate m a <+ replicate n areplicate m a <+ replicate n a ↔ m ≤ n := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · have := h.length_le; simp only [length_replicate] at this ⊢; exact this
  · induction h with
    | refl => apply Sublist.refl
    | step => simp [*, replicate, Sublist.cons]
Sublist Condition for Replicated Lists: $\text{replicate}\,m\,a <+ \text{replicate}\,n\,a \leftrightarrow m \leq n$
Informal description
For any natural numbers $m$ and $n$, and any element $a$ of type $\alpha$, the list obtained by replicating $a$ $m$ times is a sublist of the list obtained by replicating $a$ $n$ times if and only if $m \leq n$. In other words, $\text{replicate}\,m\,a <+ \text{replicate}\,n\,a \leftrightarrow m \leq n$.
List.sublist_replicate_iff theorem
: l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
Full source 
theorem sublist_replicate_iff : l <+ replicate m al <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a := by
  induction l generalizing m with
  | nil =>
    simp only [nil_sublist, true_iff]
    exact ⟨0, zero_le m, by simp⟩
  | cons b l ih =>
    constructor
    · intro w
      cases m with
      | zero => simp at w
      | succ m =>
        simp [replicate_succ] at w
        cases w with
        | cons _ w =>
          obtain ⟨n, le, rfl⟩ := ih.1 (sublist_of_cons_sublist w)
          obtain rfl := (mem_replicate.1 (mem_of_cons_sublist w)).2
          exact ⟨n+1, Nat.add_le_add_right le 1, rfl⟩
        | cons₂ _ w =>
          obtain ⟨n, le, rfl⟩ := ih.1 w
          refine ⟨n+1, Nat.add_le_add_right le 1, by simp [replicate_succ]⟩
    · rintro ⟨n, le, w⟩
      rw [w]
      exact (replicate_sublist_replicate a).2 le
Sublist Characterization for Replicated Lists: $l <+ \text{replicate}\,m\,a \leftrightarrow \exists n \leq m, l = \text{replicate}\,n\,a$
Informal description
For any list $l$ of elements of type $\alpha$, natural number $m$, and element $a$ of type $\alpha$, the list $l$ is a sublist of the list obtained by replicating $a$ $m$ times if and only if there exists a natural number $n$ such that $n \leq m$ and $l$ is equal to the list obtained by replicating $a$ $n$ times. In other words: $$ l <+ \text{replicate}\,m\,a \leftrightarrow \exists n, n \leq m \land l = \text{replicate}\,n\,a $$
List.sublist_flatten_of_mem theorem
{L : List (List α)} {l} (h : l ∈ L) : l <+ L.flatten
Full source 
theorem sublist_flatten_of_mem {L : List (List α)} {l} (h : l ∈ L) : l <+ L.flatten := by
  induction L with
  | nil => cases h
  | cons l' L ih =>
    rcases mem_cons.1 h with (rfl | h)
    · simp [h]
    · simp [ih h, flatten_cons, sublist_append_of_sublist_right]
Sublist Property of List Flattening: $l \in L \implies l <+ \text{flatten}(L)$
Informal description
For any list of lists $L$ of type $\alpha$ and any list $l$ in $L$, the list $l$ is a sublist of the concatenation (flattening) of $L$.
List.sublist_flatten_iff theorem
{L : List (List α)} {l} : l <+ L.flatten ↔ ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L'.length), L'[i] <+ L[i]?.getD []
Full source 
theorem sublist_flatten_iff {L : List (List α)} {l} :
    l <+ L.flattenl <+ L.flatten ↔
      ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L'.length), L'[i] <+ L[i]?.getD [] := by
  induction L generalizing l with
  | nil =>
    constructor
    · intro w
      simp only [flatten_nil, sublist_nil] at w
      subst w
      exact ⟨[], by simp, fun i x => by cases x⟩
    · rintro ⟨L', rfl, h⟩
      simp only [flatten_nil, sublist_nil, flatten_eq_nil_iff]
      simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
      exact (forall_getElem (p := (· = []))).1 h
  | cons l' L ih =>
    simp only [flatten_cons, sublist_append_iff, ih]
    constructor
    · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
      refine ⟨l₁ :: L', by simp, ?_⟩
      intro i lt
      cases i <;> simp_all
    · rintro ⟨L', rfl, h⟩
      cases L' with
      | nil =>
        exact ⟨[], [], by simp, by simp, [], by simp, fun i x => by cases x⟩
      | cons l₁ L' =>
        exact ⟨l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
          fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
Sublist Characterization via Flattening: $l <+ \text{flatten}(L) \leftrightarrow \exists L', l = \text{flatten}(L') \land \forall i < \text{length}(L'), L'[i] <+ L[i]?.\text{getD}\ []$
Informal description
For any list of lists $L$ of type $\alpha$ and any list $l$, the list $l$ is a sublist of the concatenation (flattening) of $L$ if and only if there exists a list of lists $L'$ such that: 1. $l$ is equal to the concatenation of $L'$, and 2. For every index $i$ with $i < \text{length}(L')$, the $i$-th element of $L'$ is a sublist of the $i$-th element of $L$ (or the empty list if $L$ has no such element). In other words: $$ l <+ \text{flatten}(L) \leftrightarrow \exists L',\ l = \text{flatten}(L') \land \forall i < \text{length}(L'),\ L'[i] <+ L[i]?.\text{getD}\ [] $$
List.flatten_sublist_iff theorem
{L : List (List α)} {l} : L.flatten <+ l ↔ ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L.length), L[i] <+ L'[i]?.getD []
Full source 
theorem flatten_sublist_iff {L : List (List α)} {l} :
    L.flatten <+ lL.flatten <+ l ↔
      ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L.length), L[i] <+ L'[i]?.getD [] := by
  induction L generalizing l with
  | nil =>
    constructor
    · intro _
      exact ⟨[l], by simp, fun i x => by cases x⟩
    · rintro ⟨L', rfl, _⟩
      simp only [flatten_nil, nil_sublist]
  | cons l' L ih =>
    simp only [flatten_cons, append_sublist_iff, ih]
    constructor
    · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
      refine ⟨l₁ :: L', by simp, ?_⟩
      intro i lt
      cases i <;> simp_all
    · rintro ⟨L', rfl, h⟩
      cases L' with
      | nil =>
        exact ⟨[], [], by simp, by simpa using h 0 (by simp), [], by simp,
          fun i x => by simpa using h (i+1) (Nat.add_lt_add_right x 1)⟩
      | cons l₁ L' =>
        exact ⟨l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
          fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
Sublist Condition for Flattened Lists: $L.\text{flatten} <+ l \leftrightarrow \exists L', l = L'.\text{flatten} \land \forall i < \text{length}\,L, L[i] <+ L'[i]?.\text{getD}\ []$
Informal description
For any list of lists $L$ and any list $l$, the concatenation (flattening) of $L$ is a sublist of $l$ if and only if there exists a list of lists $L'$ such that $l$ is the concatenation of $L'$ and for every index $i$ less than the length of $L$, the $i$-th element of $L$ is a sublist of the $i$-th element of $L'$ (or the empty list if $L'$ has no such element).
List.isSublist_iff_sublist theorem
[BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.isSublist l₂ ↔ l₁ <+ l₂
Full source 
@[simp] theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
    l₁.isSublist l₂ ↔ l₁ <+ l₂ := by
  cases l₁ <;> cases l₂ <;> simp [isSublist]
  case cons.cons hd₁ tl₁ hd₂ tl₂ =>
    if h_eq : hd₁ = hd₂ then
      simp [h_eq, cons_sublist_cons, isSublist_iff_sublist]
    else
      simp only [beq_iff_eq, h_eq]
      constructor
      · intro h_sub
        apply Sublist.cons
        exact isSublist_iff_sublist.mp h_sub
      · intro h_sub
        cases h_sub
        case cons h_sub =>
          exact isSublist_iff_sublist.mpr h_sub
        case cons₂ =>
          contradiction
Equivalence of Boolean Sublist Check and Sublist Relation: $l_1.\text{isSublist}\ l_2 \leftrightarrow l_1 <+ l_2$
Informal description
For any type $\alpha$ with a decidable boolean equality relation that coincides with propositional equality, and for any two lists $l_1$ and $l_2$ of type $\alpha$, the boolean function `isSublist` returns `true` if and only if $l_1$ is a sublist of $l_2$ (i.e., $l_1$ can be obtained from $l_2$ by deleting some elements).
List.instDecidableSublistOfDecidableEq instance
[DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂)
Full source 
instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
  decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
Decidability of Sublist Relation for Lists with Decidable Equality
Informal description
For any type $\alpha$ with decidable equality and any two lists $l_1, l_2$ of elements of $\alpha$, the proposition that $l_1$ is a sublist of $l_2$ is decidable.
List.Sublist.drop theorem
: ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ i, l₁.drop i <+ l₂.drop i
Full source 
protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ i, l₁.drop i <+ l₂.drop i
  | _, _, h, 0 => h
  | _, _, h, i + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop i
Sublist Relation Preserved Under Dropping Elements: $\text{drop}\ i\ l_1 <+ \text{drop}\ i\ l_2$ if $l_1 <+ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then for any natural number $i$, the list obtained by dropping the first $i$ elements of $l_1$ is a sublist of the list obtained by dropping the first $i$ elements of $l_2$ (denoted $\text{drop}\ i\ l_1 <+ \text{drop}\ i\ l_2$).
List.prefix_append theorem
(l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂
Full source 
@[simp] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
$l_1$ is a prefix of $l_1 ++ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $l_1$ is a prefix of the concatenated list $l_1 ++ l_2$.
List.suffix_append theorem
(l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂
Full source 
@[simp] theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩
Concatenation Preserves Suffix Relation: $l_2 <:+ l_1 ++ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $l_2$ is a suffix of the concatenated list $l_1 ++ l_2$.
List.infix_append theorem
(l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃
Full source 
theorem infix_append (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃ := ⟨l₁, l₃, rfl⟩
Infix Property of List Concatenation: $l_2 \subseteq l_1 \cdot l_2 \cdot l_3$
Informal description
For any lists $l_1, l_2, l_3$ of elements of type $\alpha$, the list $l_2$ is an infix of the concatenated list $l_1 ++ l_2 ++ l_3$.
List.infix_append' theorem
(l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃)
Full source 
@[simp] theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by
  rw [← List.append_assoc]; apply infix_append
Infix Property of Concatenated Lists: $l_2 \subseteq l_1 \cdot (l_2 \cdot l_3)$
Informal description
For any lists $l_1, l_2, l_3$ of elements of type $\alpha$, the list $l_2$ is an infix of the concatenated list $l_1 \mathbin{+\kern-1.5ex+} (l_2 \mathbin{+\kern-1.5ex+} l_3)$.
List.IsPrefix.isInfix theorem
: l₁ <+: l₂ → l₁ <:+: l₂
Full source 
theorem IsPrefix.isInfix : l₁ <+: l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨[], t, h⟩
Prefix Implies Infix for Lists
Informal description
If a list $l_1$ is a prefix of another list $l_2$ (i.e., $l_2 = l_1 ++ t$ for some list $t$), then $l_1$ is also an infix of $l_2$ (i.e., $l_1$ appears as a contiguous subsequence within $l_2$).
List.IsSuffix.isInfix theorem
: l₁ <:+ l₂ → l₁ <:+: l₂
Full source 
theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩
Suffix Implies Infix for Lists
Informal description
For any two lists $l_1$ and $l_2$ of type $\alpha$, if $l_1$ is a suffix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = t \mathbin{+\kern-0.5em+} l_1$), then $l_1$ is also an infix of $l_2$ (i.e., there exist lists $s$ and $t'$ such that $l_2 = s \mathbin{+\kern-0.5em+} l_1 \mathbin{+\kern-0.5em+} t'$).
List.nil_prefix theorem
{l : List α} : [] <+: l
Full source 
@[simp] theorem nil_prefix {l : List α} : [][] <+: l := ⟨l, rfl⟩
Empty List is Prefix of Any List
Informal description
For any list $l$ of elements of type $\alpha$, the empty list $[]$ is a prefix of $l$.
List.nil_suffix theorem
{l : List α} : [] <:+ l
Full source 
@[simp] theorem nil_suffix {l : List α} : [][] <:+ l := ⟨l, append_nil _⟩
Empty List is a Suffix of Any List
Informal description
For any list $l$ of type $\alpha$, the empty list $[]$ is a suffix of $l$.
List.nil_infix theorem
{l : List α} : [] <:+: l
Full source 
@[simp] theorem nil_infix {l : List α} : [][] <:+: l := nil_prefix.isInfix
Empty List is Infix of Any List
Informal description
For any list $l$ of elements of type $\alpha$, the empty list $[]$ is an infix of $l$.
List.prefix_refl theorem
(l : List α) : l <+: l
Full source 
theorem prefix_refl (l : List α) : l <+: l := ⟨[], append_nil _⟩
Reflexivity of List Prefix Relation
Informal description
For any list $l$ of elements of type $\alpha$, $l$ is a prefix of itself, i.e., $l <+: l$.
List.prefix_rfl theorem
{l : List α} : l <+: l
Full source 
@[simp] theorem prefix_rfl {l : List α} : l <+: l := prefix_refl l
Reflexivity of List Prefix Relation
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is a prefix of itself, i.e., $l <+: l$.
List.suffix_refl theorem
(l : List α) : l <:+ l
Full source 
theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩
Reflexivity of List Suffix Relation
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is a suffix of itself, i.e., $l <:+ l$.
List.suffix_rfl theorem
{l : List α} : l <:+ l
Full source 
@[simp] theorem suffix_rfl {l : List α} : l <:+ l := suffix_refl l
Reflexivity of List Suffix Relation
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is a suffix of itself, i.e., $l$ appears at the end of $l$.
List.infix_refl theorem
(l : List α) : l <:+: l
Full source 
theorem infix_refl (l : List α) : l <:+: l := prefix_rfl.isInfix
Reflexivity of List Infix Relation
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is an infix of itself, i.e., $l$ appears as a contiguous subsequence within itself.
List.infix_rfl theorem
{l : List α} : l <:+: l
Full source 
@[simp] theorem infix_rfl {l : List α} : l <:+: l := infix_refl l
Reflexivity of List Infix Relation
Informal description
For any list $l$ of elements of type $\alpha$, the list $l$ is an infix of itself, i.e., $l$ appears as a contiguous subsequence within itself.
List.suffix_cons theorem
(a : α) : ∀ l, l <:+ a :: l
Full source 
@[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
Suffix Preservation Under List Cons: $l <:+ a :: l$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ is a suffix of the list obtained by prepending $a$ to $l$ (i.e., $a :: l$).
List.infix_cons theorem
: l₁ <:+: l₂ → l₁ <:+: a :: l₂
Full source 
theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨l₁', l₂', h⟩ => ⟨a :: l₁', l₂', h ▸ rfl⟩
Infix Preservation Under List Cons
Informal description
For any lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₁$ is an infix of $l₂$, then $l₁$ is also an infix of the list obtained by prepending an element $a$ to $l₂$ (i.e., $a :: l₂$).
List.infix_concat theorem
: l₁ <:+: l₂ → l₁ <:+: concat l₂ a
Full source 
theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨l₁', l₂', h⟩ =>
  ⟨l₁', concat l₂' a, by simp [← h, concat_eq_append, append_assoc]⟩
Infix Preservation Under List Concatenation: $l₁ \trianglelefteq l₂ \implies l₁ \trianglelefteq l₂ \cdot [a]$
Informal description
For any lists $l₁$ and $l₂$ of elements of type $\alpha$ and any element $a$ of type $\alpha$, if $l₁$ is an infix of $l₂$, then $l₁$ is also an infix of the list obtained by appending $a$ to the end of $l₂$.
List.IsPrefix.trans theorem
: ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
Full source 
theorem IsPrefix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
  | _, _, _, ⟨r₁, rfl⟩, ⟨r₂, rfl⟩ => ⟨r₁ ++ r₂, (append_assoc _ _ _).symm⟩
Transitivity of List Prefix Relation: $l_1 <+: l_2$ and $l_2 <+: l_3$ implies $l_1 <+: l_3$
Informal description
For any three lists $l_1, l_2, l_3$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$ and $l_2$ is a prefix of $l_3$, then $l_1$ is a prefix of $l_3$. Here, $l_1 <+: l_2$ means there exists a list $t$ such that $l_2 = l_1 ++ t$.
List.IsSuffix.trans theorem
: ∀ {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
Full source 
theorem IsSuffix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
  | _, _, _, ⟨l₁, rfl⟩, ⟨l₂, rfl⟩ => ⟨l₂ ++ l₁, append_assoc _ _ _⟩
Transitivity of List Suffix Relation
Informal description
For any three lists $l_1, l_2, l_3$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$) and $l_2$ is a suffix of $l_3$ (denoted $l_2 <:+ l_3$), then $l_1$ is a suffix of $l_3$ (i.e., $l_1 <:+ l_3$).
List.IsInfix.trans theorem
: ∀ {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
Full source 
theorem IsInfix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
  | l, _, _, ⟨l₁, r₁, rfl⟩, ⟨l₂, r₂, rfl⟩ => ⟨l₂ ++ l₁, r₁ ++ r₂, by simp only [append_assoc]⟩
Transitivity of List Infix Relation: $l₁ \triangleleft l₂ \land l₂ \triangleleft l₃ \to l₁ \triangleleft l₃$
Informal description
For any three lists $l₁$, $l₂$, and $l₃$ of elements of type $\alpha$, if $l₁$ is an infix of $l₂$ and $l₂$ is an infix of $l₃$, then $l₁$ is an infix of $l₃$.
List.IsInfix.sublist theorem
: l₁ <:+: l₂ → l₁ <+ l₂
Full source 
protected theorem IsInfix.sublist : l₁ <:+: l₂ → l₁ <+ l₂
  | ⟨_, _, h⟩ => h ▸ (sublist_append_right ..).trans (sublist_append_left ..)
Infix Implies Sublist for Lists
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is an infix of $l_2$ (denoted $l_1 <:+: l_2$), then $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$).
List.IsInfix.subset theorem
(hl : l₁ <:+: l₂) : l₁ ⊆ l₂
Full source 
protected theorem IsInfix.subset (hl : l₁ <:+: l₂) : l₁ ⊆ l₂ :=
  hl.sublist.subset
Infix Implies Subset for Lists: $l_1 \triangleleft l_2 \to l_1 \subseteq l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is an infix of $l_2$ (denoted $l_1 \triangleleft l_2$), then $l_1$ is a subset of $l_2$ (denoted $l_1 \subseteq l_2$). In other words, every element of $l_1$ appears in $l_2$.
List.IsPrefix.sublist theorem
(h : l₁ <+: l₂) : l₁ <+ l₂
Full source 
protected theorem IsPrefix.sublist (h : l₁ <+: l₂) : l₁ <+ l₂ :=
  h.isInfix.sublist
Prefix Implies Sublist for Lists
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), then $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$).
List.IsPrefix.subset theorem
(hl : l₁ <+: l₂) : l₁ ⊆ l₂
Full source 
protected theorem IsPrefix.subset (hl : l₁ <+: l₂) : l₁ ⊆ l₂ :=
  hl.sublist.subset
Prefix Implies Subset for Lists: $l_1 <+: l_2 \to l_1 \subseteq l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), then $l_1$ is a subset of $l_2$ (denoted $l_1 \subseteq l_2$). In other words, every element of $l_1$ appears in $l_2$.
List.IsSuffix.sublist theorem
(h : l₁ <:+ l₂) : l₁ <+ l₂
Full source 
protected theorem IsSuffix.sublist (h : l₁ <:+ l₂) : l₁ <+ l₂ :=
  h.isInfix.sublist
Suffix Implies Sublist for Lists
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$), then $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$).
List.IsSuffix.subset theorem
(hl : l₁ <:+ l₂) : l₁ ⊆ l₂
Full source 
protected theorem IsSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ :=
  hl.sublist.subset
Suffix Implies Subset for Lists
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$ (written $l_1 <:+ l_2$), then $l_1$ is a subset of $l_2$ (written $l_1 \subseteq l_2$). This means every element of $l_1$ appears in $l_2$.
List.IsPrefix.ne_nil theorem
{xs ys : List α} (h : xs <+: ys) (hx : xs ≠ []) : ys ≠ []
Full source 
theorem IsPrefix.ne_nil {xs ys : List α} (h : xs <+: ys) (hx : xs ≠ []) : ys ≠ [] := by
  rintro rfl; exact hx <| List.prefix_nil.mp h
Non-empty Prefix Implies Non-empty List
Informal description
For any lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is a prefix of $ys$ (i.e., $xs <+: ys$) and $xs$ is not the empty list (i.e., $xs \neq []$), then $ys$ is also not the empty list (i.e., $ys \neq []$).
List.IsSuffix.ne_nil theorem
{xs ys : List α} (h : xs <:+ ys) (hx : xs ≠ []) : ys ≠ []
Full source 
theorem IsSuffix.ne_nil {xs ys : List α} (h : xs <:+ ys) (hx : xs ≠ []) : ys ≠ [] := by
  rintro rfl; exact hx <| List.suffix_nil.mp h
Nonempty Suffix Implies Nonempty List
Informal description
For any two lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is a suffix of $ys$ (denoted $xs <:+ ys$) and $xs$ is not the empty list (i.e., $xs \neq []$), then $ys$ is also not the empty list (i.e., $ys \neq []$).
List.IsInfix.ne_nil theorem
{xs ys : List α} (h : xs <:+: ys) (hx : xs ≠ []) : ys ≠ []
Full source 
theorem IsInfix.ne_nil {xs ys : List α} (h : xs <:+: ys) (hx : xs ≠ []) : ys ≠ [] := by
  rintro rfl; exact hx <| List.infix_nil.mp h
Nonempty Infix Implies Nonempty List
Informal description
For any lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is an infix of $ys$ (denoted $xs <:+: ys$) and $xs$ is not the empty list (i.e., $xs \neq []$), then $ys$ is also not the empty list (i.e., $ys \neq []$).
List.IsInfix.length_le theorem
(h : l₁ <:+: l₂) : l₁.length ≤ l₂.length
Full source 
theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length :=
  h.sublist.length_le
Infix Lists Have Shorter or Equal Length
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is an infix of $l_2$ (denoted $l_1 <:+: l_2$), then the length of $l_1$ is less than or equal to the length of $l_2$, i.e., $\text{length}(l_1) \leq \text{length}(l_2)$.
List.IsPrefix.length_le theorem
(h : l₁ <+: l₂) : l₁.length ≤ l₂.length
Full source 
theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length :=
  h.sublist.length_le
Prefix Lists Have Shorter or Equal Length
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), then the length of $l_1$ is less than or equal to the length of $l_2$, i.e., $\text{length}(l_1) \leq \text{length}(l_2)$.
List.IsSuffix.length_le theorem
(h : l₁ <:+ l₂) : l₁.length ≤ l₂.length
Full source 
theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length :=
  h.sublist.length_le
Suffix Lists Have Shorter or Equal Length
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$), then the length of $l_1$ is less than or equal to the length of $l_2$, i.e., $\text{length}(l_1) \leq \text{length}(l_2)$.
List.IsPrefix.getElem theorem
{xs ys : List α} (h : xs <+: ys) {i} (hi : i < xs.length) : xs[i] = ys[i]'(Nat.le_trans hi h.length_le)
Full source 
theorem IsPrefix.getElem {xs ys : List α} (h : xs <+: ys) {i} (hi : i < xs.length) :
    xs[i] = ys[i]'(Nat.le_trans hi h.length_le) := by
  obtain ⟨_, rfl⟩ := h
  exact (List.getElem_append_left hi).symm
Prefix Lists Have Equal Elements at Common Indices
Informal description
For any two lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is a prefix of $ys$ (denoted $xs <+: ys$), then for any index $i$ such that $i < \text{length}(xs)$, the element at position $i$ in $xs$ is equal to the element at position $i$ in $ys$, i.e., $xs[i] = ys[i]$.
List.IsPrefix.mem theorem
(hx : a ∈ l₁) (hl : l₁ <+: l₂) : a ∈ l₂
Full source 
theorem IsPrefix.mem (hx : a ∈ l₁) (hl : l₁ <+: l₂) : a ∈ l₂ :=
  hl.subset hx
Element Preservation under Prefix Relation: $a \in l_1 \land l_1 <+: l_2 \to a \in l_2$
Informal description
For any element $a$ in a list $l_1$ and any list $l_2$, if $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), then $a$ is also an element of $l_2$.
List.IsSuffix.mem theorem
(hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂
Full source 
theorem IsSuffix.mem (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂ :=
  hl.subset hx
Element Preservation under Suffix Relation: $a \in l_1 \land l_1 <:+ l_2 \to a \in l_2$
Informal description
For any element $a$ in a list $l_1$ and any list $l_2$, if $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$), then $a$ is also an element of $l_2$.
List.IsInfix.mem theorem
(hx : a ∈ l₁) (hl : l₁ <:+: l₂) : a ∈ l₂
Full source 
theorem IsInfix.mem (hx : a ∈ l₁) (hl : l₁ <:+: l₂) : a ∈ l₂ :=
  hl.subset hx
Element Preservation under Infix Relation: $a \in l_1 \land l_1 \triangleleft l_2 \to a \in l_2$
Informal description
For any element $a$ in a list $l_1$ and any list $l_2$, if $l_1$ is an infix of $l_2$ (denoted $l_1 \triangleleft l_2$), then $a$ is also an element of $l_2$.
List.reverse_suffix theorem
: reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂
Full source 
@[simp] theorem reverse_suffix : reversereverse l₁ <:+ reverse l₂reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ :=
  ⟨fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]⟩,
   fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_append, e]⟩⟩
Reversed Suffix-Prefix Duality: $l_1^{\mathrm{reverse}} <:+ l_2^{\mathrm{reverse}} \leftrightarrow l_1 <+: l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the reversed list of $l_1$ is a suffix of the reversed list of $l_2$ if and only if $l_1$ is a prefix of $l_2$. In other words, $l_1^{\mathrm{reverse}} <:+ l_2^{\mathrm{reverse}} \leftrightarrow l_1 <+: l_2$.
List.reverse_prefix theorem
: reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂
Full source 
@[simp] theorem reverse_prefix : reversereverse l₁ <+: reverse l₂reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂ := by
  rw [← reverse_suffix]; simp only [reverse_reverse]
Reversed Prefix-Suffix Duality: $l_1^{\mathrm{reverse}} <+: l_2^{\mathrm{reverse}} \leftrightarrow l_1 <:+ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the reversed list of $l_1$ is a prefix of the reversed list of $l_2$ if and only if $l_1$ is a suffix of $l_2$. In other words, $l_1^{\mathrm{reverse}} <+: l_2^{\mathrm{reverse}} \leftrightarrow l_1 <:+ l_2$.
List.reverse_infix theorem
: reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂
Full source 
@[simp] theorem reverse_infix : reversereverse l₁ <:+: reverse l₂reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂ := by
  refine ⟨fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩, fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩⟩
  · rw [← reverse_reverse l₁, append_assoc, ← reverse_append, ← reverse_append, e,
      reverse_reverse]
  · rw [append_assoc, ← reverse_append, ← reverse_append, e]
Reversed List Infix Relation: $l_1^{\text{reverse}} \trianglelefteq l_2^{\text{reverse}} \leftrightarrow l_1 \trianglelefteq l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the reverse of $l_1$ is an infix of the reverse of $l_2$ if and only if $l_1$ is an infix of $l_2$. In other words, $l_1^{\text{reverse}}$ appears as a contiguous subsequence within $l_2^{\text{reverse}}$ precisely when $l_1$ appears as a contiguous subsequence within $l_2$.
List.IsInfix.reverse theorem
: l₁ <:+: l₂ → reverse l₁ <:+: reverse l₂
Full source 
theorem IsInfix.reverse : l₁ <:+: l₂ → reversereverse l₁ <:+: reverse l₂ :=
  reverse_infix.2
Reversed List Infix Preservation
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is an infix of $l_2$, then the reverse of $l_1$ is an infix of the reverse of $l_2$.
List.IsSuffix.reverse theorem
: l₁ <:+ l₂ → reverse l₁ <+: reverse l₂
Full source 
theorem IsSuffix.reverse : l₁ <:+ l₂ → reversereverse l₁ <+: reverse l₂ :=
  reverse_prefix.2
Suffix Reversal Implies Prefix Relation: $l_1 <:+ l_2 \to \text{reverse}(l_1) <:+ \text{reverse}(l_2)$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$, then the reverse of $l_1$ is a prefix of the reverse of $l_2$. In other words, $l_1 <:+ l_2$ implies $\text{reverse}(l_1) <:+ \text{reverse}(l_2)$.
List.IsPrefix.reverse theorem
: l₁ <+: l₂ → reverse l₁ <:+ reverse l₂
Full source 
theorem IsPrefix.reverse : l₁ <+: l₂ → reversereverse l₁ <:+ reverse l₂ :=
  reverse_suffix.2
Prefix Reversal Implies Suffix Relation: $l_1 <+: l_2 \to \text{reverse}(l_1) <:+ \text{reverse}(l_2)$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$, then the reverse of $l_1$ is a suffix of the reverse of $l_2$. In other words, $l_1 <+: l_2$ implies $\text{reverse}(l_1) <:+ \text{reverse}(l_2)$.
List.IsPrefix.head theorem
{l₁ l₂ : List α} (h : l₁ <+: l₂) (hx : l₁ ≠ []) : l₁.head hx = l₂.head (h.ne_nil hx)
Full source 
theorem IsPrefix.head {l₁ l₂ : List α} (h : l₁ <+: l₂) (hx : l₁ ≠ []) :
    l₁.head hx = l₂.head (h.ne_nil hx) := by
  cases l₁ <;> cases l₂ <;> simp only [head_cons, ne_eq, not_true_eq_false] at hx ⊢
  all_goals (obtain ⟨_, h⟩ := h; injection h)
First Elements of Non-empty Prefixes are Equal
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$ (i.e., $l_1 <+: l_2$) and $l_1$ is non-empty (i.e., $l_1 \neq []$), then the first element of $l_1$ is equal to the first element of $l_2$.
List.IsSuffix.getLast theorem
{l₁ l₂ : List α} (h : l₁ <:+ l₂) (hx : l₁ ≠ []) : l₁.getLast hx = l₂.getLast (h.ne_nil hx)
Full source 
theorem IsSuffix.getLast {l₁ l₂ : List α} (h : l₁ <:+ l₂) (hx : l₁ ≠ []) :
    l₁.getLast hx = l₂.getLast (h.ne_nil hx) := by
  rw [← head_reverse (by simpa), h.reverse.head,
    head_reverse (by rintro h; simp only [reverse_eq_nil_iff] at h; simp_all)]
Last Elements of Non-empty Suffixes are Equal
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$ (i.e., $l_1 <:+ l_2$) and $l_1$ is non-empty (i.e., $l_1 \neq []$), then the last element of $l_1$ is equal to the last element of $l_2$.
List.prefix_concat theorem
(a : α) (l) : l <+: concat l a
Full source 
theorem prefix_concat (a : α) (l) : l <+: concat l a := by simp
List Prefix Property: $l$ is a prefix of $\text{concat}(l, a)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ is a prefix of the list obtained by appending $a$ to the end of $l$, i.e., $l <+: \text{concat}(l, a)$.
List.infix_iff_prefix_suffix theorem
{l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂
Full source 
theorem infix_iff_prefix_suffix {l₁ l₂ : List α} : l₁ <:+: l₂l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ :=
  ⟨fun ⟨_, t, e⟩ => ⟨l₁ ++ t, ⟨_, rfl⟩, e ▸ append_assoc .. ▸ ⟨_, rfl⟩⟩,
    fun ⟨_, ⟨t, rfl⟩, s, e⟩ => ⟨s, t, append_assoc .. ▸ e⟩⟩
Infix Characterization via Prefix and Suffix: $l_1 <:+: l_2 \iff \exists t, l_1 <+: t \land t <:+ l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $l_1$ is an infix of $l_2$ (denoted $l_1 <:+: l_2$) if and only if there exists a list $t$ such that $l_1$ is a prefix of $t$ and $t$ is a suffix of $l_2$. In other words, $l_1$ appears as a contiguous subsequence in $l_2$ if and only if there exists an intermediate list $t$ that starts with $l_1$ and ends with $l_2$.
List.infix_iff_suffix_prefix theorem
{l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ t, l₁ <:+ t ∧ t <+: l₂
Full source 
theorem infix_iff_suffix_prefix {l₁ l₂ : List α} : l₁ <:+: l₂l₁ <:+: l₂ ↔ ∃ t, l₁ <:+ t ∧ t <+: l₂ :=
  ⟨fun ⟨s, t, e⟩ => ⟨s ++ l₁, ⟨_, rfl⟩, ⟨t, e⟩⟩,
    fun ⟨_, ⟨s, rfl⟩, t, e⟩ => ⟨s, t, append_assoc .. ▸ e⟩⟩
Characterization of List Infix via Suffix and Prefix: $l_1 <:+: l_2 \iff \exists t, (l_1 <:+ t) \land (t <+: l_2)$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the following are equivalent: 1. $l_1$ is an infix of $l_2$ (denoted $l_1 <:+: l_2$), meaning $l_1$ appears as a contiguous subsequence in $l_2$. 2. There exists a list $t$ such that $l_1$ is a suffix of $t$ and $t$ is a prefix of $l_2$. In other words: $$l_1 <:+: l_2 \iff \exists t, (l_1 <:+ t) \land (t <+: l_2)$$
List.prefix_of_prefix_length_le theorem
: ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
Full source 
theorem prefix_of_prefix_length_le :
    ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
  | [], _, _, _, _, _ => nil_prefix
  | _ :: _, b :: _, _, ⟨_, rfl⟩, ⟨_, e⟩, ll => by
    injection e with _ e'; subst b
    rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩
    exact ⟨r₃, rfl⟩
Shorter Prefix of Common List is Prefix of Longer Prefix
Informal description
For any three lists $l_1, l_2, l_3$ of elements of type $\alpha$, if both $l_1$ and $l_2$ are prefixes of $l_3$ and the length of $l_1$ is less than or equal to the length of $l_2$, then $l_1$ is a prefix of $l_2$.
List.prefix_or_prefix_of_prefix theorem
(h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂ ∨ l₂ <+: l₁
Full source 
theorem prefix_or_prefix_of_prefix (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂l₁ <+: l₂ ∨ l₂ <+: l₁ :=
  (Nat.le_total (length l₁) (length l₂)).imp (prefix_of_prefix_length_le h₁ h₂)
    (prefix_of_prefix_length_le h₂ h₁)
Prefix Antisymmetry for Lists: $l_1 <+: l_3$ and $l_2 <+: l_3$ implies $l_1 <+: l_2$ or $l_2 <+: l_1$
Informal description
For any three lists $l_1, l_2, l_3$ of elements of type $\alpha$, if both $l_1$ and $l_2$ are prefixes of $l_3$, then either $l_1$ is a prefix of $l_2$ or $l_2$ is a prefix of $l_1$.
List.suffix_of_suffix_length_le theorem
(h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : length l₁ ≤ length l₂) : l₁ <:+ l₂
Full source 
theorem suffix_of_suffix_length_le
    (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : length l₁ ≤ length l₂) : l₁ <:+ l₂ :=
  reverse_prefix.1 <|
    prefix_of_prefix_length_le (reverse_prefix.2 h₁) (reverse_prefix.2 h₂) (by simp [ll])
Shorter Suffix of Common List is Suffix of Longer Suffix
Informal description
For any three lists $l_1, l_2, l_3$ of elements of type $\alpha$, if both $l_1$ and $l_2$ are suffixes of $l_3$ and the length of $l_1$ is less than or equal to the length of $l_2$, then $l_1$ is a suffix of $l_2$.
List.suffix_or_suffix_of_suffix theorem
(h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) : l₁ <:+ l₂ ∨ l₂ <:+ l₁
Full source 
theorem suffix_or_suffix_of_suffix (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) : l₁ <:+ l₂l₁ <:+ l₂ ∨ l₂ <:+ l₁ :=
  (prefix_or_prefix_of_prefix (reverse_prefix.2 h₁) (reverse_prefix.2 h₂)).imp reverse_prefix.1
    reverse_prefix.1
Suffix Antisymmetry for Lists: $l_1 <:+ l_3$ and $l_2 <:+ l_3$ implies $l_1 <:+ l_2$ or $l_2 <:+ l_1$
Informal description
For any three lists $l_1$, $l_2$, and $l_3$ of elements of type $\alpha$, if both $l_1$ and $l_2$ are suffixes of $l_3$, then either $l_1$ is a suffix of $l_2$ or $l_2$ is a suffix of $l_1$.
List.prefix_cons_iff theorem
: l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :: t ∧ t <+: l₂
Full source 
theorem prefix_cons_iff : l₁ <+: a :: l₂l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :: t ∧ t <+: l₂ := by
  cases l₁ with
  | nil => simp
  | cons a' l₁ =>
    constructor
    · rintro ⟨t, h⟩
      simp at h
      obtain ⟨rfl, rfl⟩ := h
      exact Or.inr ⟨l₁, rfl, prefix_append l₁ t⟩
    · rintro (h | ⟨t, w, ⟨s, h'⟩⟩)
      · simp [h]
      · simp only [w]
        refine ⟨s, by simp [h']⟩
Characterization of Prefixes for Non-Empty Lists: $l_1 <^+ (a :: l_2) \leftrightarrow l_1 = [] \lor (\exists t, l_1 = a :: t \land t <^+ l_2)$
Informal description
For any element $a$ of type $\alpha$ and lists $l_1, l_2$ of type $\text{List } \alpha$, the list $l_1$ is a prefix of $a :: l_2$ if and only if either: 1. $l_1$ is the empty list, or 2. There exists a list $t$ such that $l_1 = a :: t$ and $t$ is a prefix of $l_2$.
List.cons_prefix_cons theorem
: a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
Full source 
@[simp] theorem cons_prefix_cons : a :: l₁a :: l₁ <+: b :: l₂a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
  simp only [prefix_cons_iff, cons.injEq, false_or, List.cons_ne_nil]
  constructor
  · rintro ⟨t, ⟨rfl, rfl⟩, h⟩
    exact ⟨rfl, h⟩
  · rintro ⟨rfl, h⟩
    exact ⟨l₁, ⟨rfl, rfl⟩, h⟩
Prefix Condition for Cons Lists: $(a :: l_1) <^+ (b :: l_2) \leftrightarrow a = b \land l_1 <^+ l_2$
Informal description
For any elements $a$ and $b$ of type $\alpha$ and any lists $l_1$ and $l_2$ of type $\text{List } \alpha$, the list $a :: l_1$ is a prefix of $b :: l_2$ if and only if $a = b$ and $l_1$ is a prefix of $l_2$.
List.suffix_cons_iff theorem
: l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂
Full source 
theorem suffix_cons_iff : l₁ <:+ a :: l₂l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂ := by
  constructor
  · rintro ⟨⟨hd, tl⟩, hl₃⟩
    · exact Or.inl hl₃
    · simp only [cons_append] at hl₃
      injection hl₃ with _ hl₄
      exact Or.inr ⟨_, hl₄⟩
  · rintro (rfl | hl₁)
    · exact (a :: l₂).suffix_refl
    · exact hl₁.trans (l₂.suffix_cons _)
Characterization of Suffixes for Non-Empty Lists: $l_1 <:+ (a :: l_2) \leftrightarrow l_1 = a :: l_2 \lor l_1 <:+ l_2$
Informal description
For any element $a$ of type $\alpha$ and lists $l_1, l_2$ of type $\text{List } \alpha$, the list $l_1$ is a suffix of $a :: l_2$ if and only if either: 1. $l_1$ equals $a :: l_2$, or 2. $l_1$ is a suffix of $l_2$.
List.infix_cons_iff theorem
: l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
Full source 
theorem infix_cons_iff : l₁ <:+: a :: l₂l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ := by
  constructor
  · rintro ⟨⟨hd, tl⟩, t, hl₃⟩
    · exact Or.inl ⟨t, hl₃⟩
    · simp only [cons_append] at hl₃
      injection hl₃ with _ hl₄
      exact Or.inr ⟨_, t, hl₄⟩
  · rintro (h | hl₁)
    · exact h.isInfix
    · exact infix_cons hl₁
Infix Characterization for Cons Lists: $l_1 \triangleleft a :: l_2 \leftrightarrow l_1 \prec a :: l_2 \lor l_1 \triangleleft l_2$
Informal description
For any lists $l_1$ and $l_2$ of elements of type $\alpha$ and any element $a \in \alpha$, the list $l_1$ is an infix of $a :: l_2$ if and only if either $l_1$ is a prefix of $a :: l_2$ or $l_1$ is an infix of $l_2$.
List.prefix_concat_iff theorem
{l₁ l₂ : List α} {a : α} : l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂
Full source 
theorem prefix_concat_iff {l₁ l₂ : List α} {a : α} :
    l₁ <+: l₂ ++ [a]l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂ := by
  simp only [← reverse_suffix, reverse_concat, suffix_cons_iff]
  simp only [concat_eq_append, ← reverse_concat, reverse_eq_iff, reverse_reverse]
Prefix Characterization for List Concatenation with Singleton: $l_1 <+: l_2 \mathbin{+\!\!+} [a] \leftrightarrow l_1 = l_2 \mathbin{+\!\!+} [a] \lor l_1 <+: l_2$
Informal description
For any lists $l_1, l_2$ of elements of type $\alpha$ and any element $a \in \alpha$, the list $l_1$ is a prefix of $l_2 \mathbin{+\!\!+} [a]$ if and only if either $l_1$ equals $l_2 \mathbin{+\!\!+} [a]$ or $l_1$ is a prefix of $l_2$.
List.suffix_concat_iff theorem
{l₁ l₂ : List α} {a : α} : l₁ <:+ l₂ ++ [a] ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂
Full source 
theorem suffix_concat_iff {l₁ l₂ : List α} {a : α} :
    l₁ <:+ l₂ ++ [a]l₁ <:+ l₂ ++ [a] ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂ := by
  rw [← reverse_prefix, reverse_concat, prefix_cons_iff]
  simp only [reverse_eq_nil_iff]
  apply or_congr_right
  constructor
  · rintro ⟨t, w, h⟩
    exact ⟨t.reverse, by simpa using congrArg reverse w, by simpa using h.reverse⟩
  · rintro ⟨t, rfl, h⟩
    exact ⟨t.reverse, by simp, by simpa using h.reverse⟩
Suffix Characterization for List Concatenation with Singleton: $l_1 <:+ l_2 \mathbin{+\!\!+} [a] \leftrightarrow l_1 = [] \lor (\exists t, l_1 = t \mathbin{+\!\!+} [a] \land t <:+ l_2)$
Informal description
For any lists $l_1, l_2$ of elements of type $\alpha$ and any element $a \in \alpha$, the list $l_1$ is a suffix of $l_2 \mathbin{+\!\!+} [a]$ if and only if either: 1. $l_1$ is the empty list, or 2. There exists a list $t$ such that $l_1 = t \mathbin{+\!\!+} [a]$ and $t$ is a suffix of $l_2$.
List.infix_concat_iff theorem
{l₁ l₂ : List α} {a : α} : l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂
Full source 
theorem infix_concat_iff {l₁ l₂ : List α} {a : α} :
    l₁ <:+: l₂ ++ [a]l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂ := by
  rw [← reverse_infix, reverse_concat, infix_cons_iff, reverse_infix,
    ← reverse_prefix, reverse_concat]
Infix Characterization for List Concatenation with Singleton: $l_1 \triangleleft l_2 \mathbin{+\!\!+} [a] \leftrightarrow l_1 \trianglelefteq l_2 \mathbin{+\!\!+} [a] \lor l_1 \triangleleft l_2$
Informal description
For any lists $l_1, l_2$ of elements of type $\alpha$ and any element $a \in \alpha$, the list $l_1$ is an infix of $l_2 \mathbin{+\!\!+} [a]$ if and only if either $l_1$ is a suffix of $l_2 \mathbin{+\!\!+} [a]$ or $l_1$ is an infix of $l_2$.
List.isPrefix_iff theorem
: l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i]
Full source 
theorem isPrefix_iff : l₁ <+: l₂l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
  induction l₁ generalizing l₂ with
  | nil => simp
  | cons a l₁ ih =>
    cases l₂ with
    | nil =>
      simpa using ⟨0, by simp⟩
    | cons b l₂ =>
      simp only [cons_append, cons_prefix_cons, ih]
      rw (occs := [2]) [← Nat.and_forall_add_one]
      simp [Nat.succ_lt_succ_iff, eq_comm]
Characterization of List Prefix via Element-wise Equality
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, $l_1$ is a prefix of $l_2$ if and only if for every index $i$ with $i < \text{length}(l_1)$, the $i$-th element of $l_2$ (when it exists) is equal to the $i$-th element of $l_1$.
List.isPrefix_iff_getElem theorem
{l₁ l₂ : List α} : l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ i (hx : i < l₁.length), l₁[i] = l₂[i]'(Nat.lt_of_lt_of_le hx h)
Full source 
theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
    l₁ <+: l₂l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ i (hx : i < l₁.length),
      l₁[i] = l₂[i]'(Nat.lt_of_lt_of_le hx h) where
  mp h := ⟨h.length_le, fun _ h' ↦ h.getElem h'⟩
  mpr h := by
    obtain ⟨hl, h⟩ := h
    induction l₂ generalizing l₁ with
    | nil =>
      simpa using hl
    | cons _ _ tail_ih =>
      cases l₁ with
      | nil =>
        exact nil_prefix
      | cons _ _ =>
        simp only [length_cons, Nat.add_le_add_iff_right, Fin.getElem_fin] at hl h
        simp only [cons_prefix_cons]
        exact ⟨h 0 (zero_lt_succ _), tail_ih hl fun a ha ↦ h a.succ (succ_lt_succ ha)⟩
Prefix Characterization via Length and Element-wise Equality
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, $l_1$ is a prefix of $l_2$ if and only if the length of $l_1$ is less than or equal to the length of $l_2$ and for every index $i < \text{length}(l_1)$, the $i$-th elements of $l_1$ and $l_2$ are equal.
List.isPrefix_filterMap_iff theorem
{β} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <+: filterMap f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = filterMap f l
Full source 
theorem isPrefix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
    l₂ <+: filterMap f l₁l₂ <+: filterMap f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = filterMap f l := by
  simp only [IsPrefix, append_eq_filterMap_iff]
  constructor
  · rintro ⟨_, l₁, l₂, rfl, rfl, rfl⟩
    exact ⟨l₁, ⟨l₂, rfl⟩, rfl⟩
  · rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩
    exact ⟨_, l₁, l₂, rfl, rfl, rfl⟩
Prefix Characterization for Filter-Mapped Lists: $l_2 \prec^+ \text{filterMap } f\ l_1 \leftrightarrow \exists l \prec^+ l_1, l_2 = \text{filterMap } f\ l$
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and lists $l_1 : \text{List } \alpha$, $l_2 : \text{List } \beta$, the list $l_2$ is a prefix of $\text{filterMap } f\ l_1$ if and only if there exists a list $l$ such that $l$ is a prefix of $l_1$ and $l_2 = \text{filterMap } f\ l$.
List.isSuffix_filterMap_iff theorem
{β} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <:+ filterMap f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = filterMap f l
Full source 
theorem isSuffix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+ filterMap f l₁l₂ <:+ filterMap f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = filterMap f l := by
  simp only [IsSuffix, append_eq_filterMap_iff]
  constructor
  · rintro ⟨_, l₁, l₂, rfl, rfl, rfl⟩
    exact ⟨l₂, ⟨l₁, rfl⟩, rfl⟩
  · rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩
    exact ⟨_, l₂, l₁, rfl, rfl, rfl⟩
Characterization of Suffixes under `filterMap`: $l_2 <:+ \text{filterMap } f\ l_1 \leftrightarrow \exists l <:+ l_1, l_2 = \text{filterMap } f\ l$
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and lists $l_1 : \text{List } \alpha$, $l_2 : \text{List } \beta$, the list $l_2$ is a suffix of $\text{filterMap } f\ l_1$ if and only if there exists a list $l$ that is a suffix of $l_1$ such that $l_2 = \text{filterMap } f\ l$. Here, $\text{filterMap } f\ l$ denotes the list obtained by applying $f$ to each element of $l$ and collecting all results of the form $\text{some } b$, discarding any $\text{none}$ values.
List.isInfix_filterMap_iff theorem
{β} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <:+: filterMap f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = filterMap f l
Full source 
theorem isInfix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+: filterMap f l₁l₂ <:+: filterMap f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = filterMap f l := by
  simp only [IsInfix, append_eq_filterMap_iff, filterMap_eq_append_iff]
  constructor
  · rintro ⟨_, _, _, l₁, rfl, ⟨⟨l₂, l₃, rfl, rfl, rfl⟩, rfl⟩⟩
    exact ⟨l₃, ⟨l₂, l₁, rfl⟩, rfl⟩
  · rintro ⟨l₃, ⟨l₂, l₁, rfl⟩, rfl⟩
    exact ⟨_, _, _, l₁, rfl, ⟨⟨l₂, l₃, rfl, rfl, rfl⟩, rfl⟩⟩
Characterization of Infixes under `filterMap`: $l_2 \subseteq_{\text{inf}} \text{filterMap } f \ l_1 \leftrightarrow \exists l \subseteq_{\text{inf}} l_1, l_2 = \text{filterMap } f \ l$
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and lists $l_1 : \text{List } \alpha$, $l_2 : \text{List } \beta$, the list $l_2$ is an infix of $\text{filterMap } f \ l_1$ if and only if there exists a list $l$ such that $l$ is an infix of $l_1$ and $l_2 = \text{filterMap } f \ l$.
List.isPrefix_filter_iff theorem
{p : α → Bool} {l₁ l₂ : List α} : l₂ <+: l₁.filter p ↔ ∃ l, l <+: l₁ ∧ l₂ = l.filter p
Full source 
theorem isPrefix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
    l₂ <+: l₁.filter pl₂ <+: l₁.filter p ↔ ∃ l, l <+: l₁ ∧ l₂ = l.filter p := by
  rw [← filterMap_eq_filter, isPrefix_filterMap_iff]
Prefix Characterization for Filtered Lists: $l_2 \prec^+ \text{filter } p\ l_1 \leftrightarrow \exists l \prec^+ l_1, l_2 = \text{filter } p\ l$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and lists $l_1, l_2 : \text{List } \alpha$, the filtered list $l_2$ is a prefix of $l_1.\text{filter } p$ if and only if there exists a list $l$ that is a prefix of $l_1$ such that $l_2 = l.\text{filter } p$.
List.isSuffix_filter_iff theorem
{p : α → Bool} {l₁ l₂ : List α} : l₂ <:+ l₁.filter p ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.filter p
Full source 
theorem isSuffix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
    l₂ <:+ l₁.filter pl₂ <:+ l₁.filter p ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.filter p := by
  rw [← filterMap_eq_filter, isSuffix_filterMap_iff]
Characterization of Suffixes under Filtering: $l_2 <:+ \text{filter } p\ l_1 \leftrightarrow \exists l <:+ l_1, l_2 = \text{filter } p\ l$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and lists $l_1, l_2 : \text{List } \alpha$, the list $l_2$ is a suffix of the filtered list $\text{filter } p\ l_1$ if and only if there exists a list $l$ that is a suffix of $l_1$ such that $l_2 = \text{filter } p\ l$.
List.isInfix_filter_iff theorem
{p : α → Bool} {l₁ l₂ : List α} : l₂ <:+: l₁.filter p ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.filter p
Full source 
theorem isInfix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
    l₂ <:+: l₁.filter pl₂ <:+: l₁.filter p ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.filter p := by
  rw [← filterMap_eq_filter, isInfix_filterMap_iff]
Characterization of Infixes under Filtering: $l_2 \subseteq_{\text{inf}} \text{filter } p \ l_1 \leftrightarrow \exists l \subseteq_{\text{inf}} l_1, l_2 = \text{filter } p \ l$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and lists $l_1, l_2 : \text{List } \alpha$, the list $l_2$ is an infix of the filtered list $\text{filter } p \ l_1$ if and only if there exists a list $l$ such that $l$ is an infix of $l_1$ and $l_2 = \text{filter } p \ l$.
List.isPrefix_map_iff theorem
{β} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <+: l₁.map f ↔ ∃ l, l <+: l₁ ∧ l₂ = l.map f
Full source 
theorem isPrefix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
    l₂ <+: l₁.map fl₂ <+: l₁.map f ↔ ∃ l, l <+: l₁ ∧ l₂ = l.map f := by
  rw [← filterMap_eq_map, isPrefix_filterMap_iff]
Prefix Characterization for Mapped Lists: $l_2 \prec^+ \text{map}\ f\ l_1 \leftrightarrow \exists l \prec^+ l_1, l_2 = \text{map}\ f\ l$
Informal description
For any function $f : \alpha \to \beta$ and lists $l_1$ of type $\text{List}\ \alpha$ and $l_2$ of type $\text{List}\ \beta$, the list $l_2$ is a prefix of the mapped list $l_1.\text{map}\ f$ if and only if there exists a list $l$ that is a prefix of $l_1$ such that $l_2 = l.\text{map}\ f$.
List.isSuffix_map_iff theorem
{β} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <:+ l₁.map f ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.map f
Full source 
theorem isSuffix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+ l₁.map fl₂ <:+ l₁.map f ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.map f := by
  rw [← filterMap_eq_map, isSuffix_filterMap_iff]
Suffix Characterization under List Mapping: $l_2 <:+ \text{map } f\ l_1 \leftrightarrow \exists l <:+ l_1, l_2 = \text{map } f\ l$
Informal description
For any function $f : \alpha \to \beta$ and lists $l_1 : \text{List } \alpha$, $l_2 : \text{List } \beta$, the list $l_2$ is a suffix of the mapped list $\text{map } f\ l_1$ if and only if there exists a list $l$ that is a suffix of $l_1$ such that $l_2 = \text{map } f\ l$.
List.isInfix_map_iff theorem
{β} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <:+: l₁.map f ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.map f
Full source 
theorem isInfix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+: l₁.map fl₂ <:+: l₁.map f ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.map f := by
  rw [← filterMap_eq_map, isInfix_filterMap_iff]
Characterization of Infixes under List Mapping: $l_2 \subseteq_{\text{inf}} \text{map } f \ l_1 \leftrightarrow \exists l \subseteq_{\text{inf}} l_1, l_2 = \text{map } f \ l$
Informal description
For any function $f : \alpha \to \beta$ and lists $l_1 : \text{List } \alpha$, $l_2 : \text{List } \beta$, the list $l_2$ is an infix of the mapped list $\text{map } f \ l_1$ if and only if there exists a list $l$ such that $l$ is an infix of $l_1$ and $l_2 = \text{map } f \ l$.
List.isPrefix_replicate_iff theorem
{n} {a : α} {l : List α} : l <+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a
Full source 
theorem isPrefix_replicate_iff {n} {a : α} {l : List α} :
    l <+: List.replicate n al <+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a := by
  rw [IsPrefix]
  simp only [append_eq_replicate_iff]
  constructor
  · rintro ⟨_, rfl, _, _⟩
    exact ⟨le_add_right .., ‹_›⟩
  · rintro ⟨h, w⟩
    refine ⟨replicate (n - l.length) a, ?_, ?_⟩
    · simpa using add_sub_of_le h
    · simpa using w
Characterization of Prefixes of Replicated Lists: $l <+: \text{replicate } n a \leftrightarrow \text{length } l \leq n \land l = \text{replicate } (\text{length } l) a$
Informal description
For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of type $\text{List } \alpha$, the list $l$ is a prefix of the replicated list $\text{replicate } n a$ if and only if the length of $l$ is less than or equal to $n$ and $l$ is equal to $\text{replicate } (\text{length } l) a$.
List.isSuffix_replicate_iff theorem
{n} {a : α} {l : List α} : l <:+ List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a
Full source 
theorem isSuffix_replicate_iff {n} {a : α} {l : List α} :
    l <:+ List.replicate n al <:+ List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a := by
  rw [← reverse_prefix, reverse_replicate, isPrefix_replicate_iff]
  simp [reverse_eq_iff]
Characterization of Suffixes of Replicated Lists: $l <:+ \text{replicate } n a \leftrightarrow \text{length } l \leq n \land l = \text{replicate } (\text{length } l) a$
Informal description
For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of type $\text{List } \alpha$, the list $l$ is a suffix of the replicated list $\text{replicate } n a$ if and only if the length of $l$ is less than or equal to $n$ and $l$ is equal to $\text{replicate } (\text{length } l) a$.
List.isInfix_replicate_iff theorem
{n} {a : α} {l : List α} : l <:+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a
Full source 
theorem isInfix_replicate_iff {n} {a : α} {l : List α} :
    l <:+: List.replicate n al <:+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a := by
  rw [IsInfix]
  simp only [append_eq_replicate_iff, length_append]
  constructor
  · rintro ⟨_, _, rfl, ⟨-, _, _⟩, _⟩
    exact ⟨le_add_right_of_le (le_add_left ..), ‹_›⟩
  · rintro ⟨h, w⟩
    refine ⟨replicate (n - l.length) a, [], ?_, ?_⟩
    · simpa using Nat.sub_add_cancel h
    · simpa using w
Characterization of Infixes in Replicated Lists: $l \text{ is infix of } \text{replicate } n a \leftrightarrow \text{length } l \leq n \land l = \text{replicate } (\text{length } l) a$
Informal description
For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of type $\text{List } \alpha$, the list $l$ is an infix of the replicated list $\text{replicate } n a$ if and only if the length of $l$ is less than or equal to $n$ and $l$ is equal to $\text{replicate } (\text{length } l) a$.
List.infix_of_mem_flatten theorem
: ∀ {L : List (List α)}, l ∈ L → l <:+: flatten L
Full source 
theorem infix_of_mem_flatten : ∀ {L : List (List α)}, l ∈ L → l <:+: flatten L
  | l' :: _, h =>
    match h with
    | List.Mem.head .. => infix_append [] _ _
    | List.Mem.tail _ hlMemL =>
      IsInfix.trans (infix_of_mem_flatten hlMemL) <| (suffix_append _ _).isInfix
Membership in List of Lists Implies Infix in Flattened List
Informal description
For any list of lists $L$ of elements of type $\alpha$, if a list $l$ is a member of $L$, then $l$ is an infix of the flattened list obtained by concatenating all lists in $L$.
List.prefix_append_right_inj theorem
(l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂
Full source 
@[simp] theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂ :=
  exists_congr fun r => by rw [append_assoc, append_right_inj]
Prefix Preservation under Right Concatenation: $l \mathbin{+\kern-1.5ex+} l_1 <+: l \mathbin{+\kern-1.5ex+} l_2 \leftrightarrow l_1 <+: l_2$
Informal description
For any list $l$ and any two lists $l_1, l_2$ of elements of type $\alpha$, the concatenation $l \mathbin{+\kern-1.5ex+} l_1$ is a prefix of $l \mathbin{+\kern-1.5ex+} l_2$ if and only if $l_1$ is a prefix of $l_2$.
List.prefix_cons_inj theorem
(a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂
Full source 
theorem prefix_cons_inj (a) : a :: l₁a :: l₁ <+: a :: l₂a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
  prefix_append_right_inj [a]
Prefix Preservation under Cons Operation: $a :: l_1 <+: a :: l_2 \leftrightarrow l_1 <+: l_2$
Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $a :: l_1$ is a prefix of $a :: l_2$ if and only if $l_1$ is a prefix of $l_2$.
List.take_prefix theorem
(i) (l : List α) : take i l <+: l
Full source 
theorem take_prefix (i) (l : List α) : taketake i l <+: l :=
  ⟨_, take_append_drop _ _⟩
Prefix Property of List Take Operation: $\text{take}(i, l) <+: l$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, the list obtained by taking the first $i$ elements of $l$ (denoted $\text{take}(i, l)$) is a prefix of $l$. That is, $\text{take}(i, l) <+: l$.
List.drop_suffix theorem
(i) (l : List α) : drop i l <:+ l
Full source 
theorem drop_suffix (i) (l : List α) : dropdrop i l <:+ l :=
  ⟨_, take_append_drop _ _⟩
Dropping Elements Yields a Suffix: $\text{drop}(i, l) <:+ l$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, the list obtained by dropping the first $i$ elements of $l$ is a suffix of $l$. In other words, $\text{drop}(i, l) <:+ l$.
List.take_sublist theorem
(i) (l : List α) : take i l <+ l
Full source 
theorem take_sublist (i) (l : List α) : taketake i l <+ l :=
  (take_prefix i l).sublist
Sublist Property of List Take Operation: $\text{take}(i, l) <+ l$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, the list obtained by taking the first $i$ elements of $l$ (denoted $\text{take}(i, l)$) is a sublist of $l$. That is, $\text{take}(i, l) <+ l$.
List.drop_sublist theorem
(i) (l : List α) : drop i l <+ l
Full source 
theorem drop_sublist (i) (l : List α) : dropdrop i l <+ l :=
  (drop_suffix i l).sublist
Dropping Elements Yields a Sublist: $\text{drop}(i, l) <+ l$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, the list obtained by dropping the first $i$ elements of $l$ is a sublist of $l$. In other words, $\text{drop}(i, l) <+ l$.
List.take_subset theorem
(i) (l : List α) : take i l ⊆ l
Full source 
theorem take_subset (i) (l : List α) : taketake i l ⊆ l :=
  (take_sublist i l).subset
Subset Property of List Take Operation: $\text{take}(i, l) \subseteq l$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, the list obtained by taking the first $i$ elements of $l$ (denoted $\text{take}(i, l)$) is a subset of $l$. That is, $\text{take}(i, l) \subseteq l$.
List.drop_subset theorem
(i) (l : List α) : drop i l ⊆ l
Full source 
theorem drop_subset (i) (l : List α) : dropdrop i l ⊆ l :=
  (drop_sublist i l).subset
Subset Property of Dropped List: $\text{drop}(i, l) \subseteq l$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, the list obtained by dropping the first $i$ elements of $l$ is a subset of $l$. In other words, $\text{drop}(i, l) \subseteq l$.
List.mem_of_mem_take theorem
{l : List α} (h : a ∈ l.take i) : a ∈ l
Full source 
theorem mem_of_mem_take {l : List α} (h : a ∈ l.take i) : a ∈ l :=
  take_subset _ _ h
Membership Preservation under List Take: $a \in \text{take}(i, l) \implies a \in l$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$, if an element $a$ belongs to the first $i$ elements of $l$ (i.e., $a \in \text{take}(i, l)$), then $a$ also belongs to $l$ (i.e., $a \in l$).
List.mem_of_mem_drop theorem
{i} {l : List α} (h : a ∈ l.drop i) : a ∈ l
Full source 
theorem mem_of_mem_drop {i} {l : List α} (h : a ∈ l.drop i) : a ∈ l :=
  drop_subset _ _ h
Membership Preservation under List Drop: $a \in \text{drop}(i, l) \implies a \in l$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, if an element $a$ is in the list obtained by dropping the first $i$ elements of $l$, then $a$ is also in the original list $l$. In other words, if $a \in \text{drop}(i, l)$, then $a \in l$.
List.drop_suffix_drop_left theorem
(l : List α) {i j : Nat} (h : i ≤ j) : drop j l <:+ drop i l
Full source 
theorem drop_suffix_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : dropdrop j l <:+ drop i l := by
  rw [← Nat.sub_add_cancel h, Nat.add_comm, ← drop_drop]
  apply drop_suffix
Suffix Relation Between Dropped Lists: $\text{drop}(j, l) <:+ \text{drop}(i, l)$ for $i \leq j$
Informal description
For any list $l$ of elements of type $\alpha$ and natural numbers $i, j$ with $i \leq j$, the list obtained by dropping the first $j$ elements of $l$ is a suffix of the list obtained by dropping the first $i$ elements of $l$. In other words: $$\text{drop}(j, l) <:+ \text{drop}(i, l)$$
List.drop_sublist_drop_left theorem
(l : List α) {i j : Nat} (h : i ≤ j) : drop j l <+ drop i l
Full source 
theorem drop_sublist_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : dropdrop j l <+ drop i l :=
  (drop_suffix_drop_left l h).sublist
Sublist Relation Between Dropped Lists: $\text{drop}(j, l) <+ \text{drop}(i, l)$ for $i \leq j$
Informal description
For any list $l$ of elements of type $\alpha$ and natural numbers $i, j$ with $i \leq j$, the list obtained by dropping the first $j$ elements of $l$ is a sublist of the list obtained by dropping the first $i$ elements of $l$. In other words: $$\text{drop}(j, l) <+ \text{drop}(i, l)$$
List.drop_subset_drop_left theorem
(l : List α) {i j : Nat} (h : i ≤ j) : drop j l ⊆ drop i l
Full source 
theorem drop_subset_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : dropdrop j l ⊆ drop i l :=
  (drop_sublist_drop_left l h).subset
Subset Relation for Dropped Lists: $\text{drop}(j, l) \subseteq \text{drop}(i, l)$ when $i \leq j$
Informal description
For any list $l$ of elements of type $\alpha$ and natural numbers $i, j$ with $i \leq j$, the list obtained by dropping the first $j$ elements of $l$ is a subset of the list obtained by dropping the first $i$ elements of $l$. In other words: $$\text{drop}(j, l) \subseteq \text{drop}(i, l)$$
List.takeWhile_prefix theorem
(p : α → Bool) : l.takeWhile p <+: l
Full source 
theorem takeWhile_prefix (p : α → Bool) : l.takeWhile p <+: l :=
  ⟨l.dropWhile p, takeWhile_append_dropWhile⟩
$\text{takeWhile } p \, l$ is a prefix of $l$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, the list $\text{takeWhile } p \, l$ is a prefix of $l$. That is, there exists a list $t$ such that $l = (\text{takeWhile } p \, l) \mathbin{+\!\!+} t$.
List.dropWhile_suffix theorem
(p : α → Bool) : l.dropWhile p <:+ l
Full source 
theorem dropWhile_suffix (p : α → Bool) : l.dropWhile p <:+ l :=
  ⟨l.takeWhile p, takeWhile_append_dropWhile⟩
`dropWhile` yields a suffix of the original list
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, the result of `dropWhile p l` is a suffix of $l$. In other words, $l.\text{dropWhile } p <:+ l$.
List.takeWhile_sublist theorem
(p : α → Bool) : l.takeWhile p <+ l
Full source 
theorem takeWhile_sublist (p : α → Bool) : l.takeWhile p <+ l :=
  (takeWhile_prefix p).sublist
$\text{takeWhile } p \, l$ is a sublist of $l$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, the list $\text{takeWhile } p \, l$ is a sublist of $l$.
List.dropWhile_sublist theorem
(p : α → Bool) : l.dropWhile p <+ l
Full source 
theorem dropWhile_sublist (p : α → Bool) : l.dropWhile p <+ l :=
  (dropWhile_suffix p).sublist
`dropWhile` yields a sublist of the original list
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, the result of `dropWhile p l` is a sublist of $l$. In other words, $l.\text{dropWhile } p <+ l$.
List.takeWhile_subset theorem
{l : List α} (p : α → Bool) : l.takeWhile p ⊆ l
Full source 
theorem takeWhile_subset {l : List α} (p : α → Bool) : l.takeWhile p ⊆ l :=
  (takeWhile_sublist p).subset
Subset Property of $\text{takeWhile}$: $\text{takeWhile } p \, l \subseteq l$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, the list $\text{takeWhile } p \, l$ is a subset of $l$, i.e., every element of $\text{takeWhile } p \, l$ appears in $l$.
List.dropWhile_subset theorem
{l : List α} (p : α → Bool) : l.dropWhile p ⊆ l
Full source 
theorem dropWhile_subset {l : List α} (p : α → Bool) : l.dropWhile p ⊆ l :=
  (dropWhile_sublist p).subset
Subset Property of `dropWhile`: $\text{dropWhile } p l \subseteq l$
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, the list obtained by dropping the longest prefix of $l$ for which $p$ holds is a subset of $l$. In other words, $\text{dropWhile } p l \subseteq l$.
List.dropLast_prefix theorem
: ∀ l : List α, l.dropLast <+: l
Full source 
theorem dropLast_prefix : ∀ l : List α, l.dropLast <+: l
  | [] => ⟨nil, by rw [dropLast, List.append_nil]⟩
  | a :: l => ⟨_, dropLast_concat_getLast (cons_ne_nil a l)⟩
Prefix Property of List DropLast Operation: $\text{dropLast } l <+: l$
Informal description
For any list $l$ of elements of type $\alpha$, the list obtained by removing the last element of $l$ is a prefix of $l$.
List.dropLast_sublist theorem
(l : List α) : l.dropLast <+ l
Full source 
theorem dropLast_sublist (l : List α) : l.dropLast <+ l :=
  (dropLast_prefix l).sublist
Sublist Property of List DropLast Operation: $\text{dropLast } l <+ l$
Informal description
For any list $l$ of elements of type $\alpha$, the list obtained by removing the last element of $l$ is a sublist of $l$. In other words, $l.\text{dropLast} <+ l$.
List.dropLast_subset theorem
(l : List α) : l.dropLast ⊆ l
Full source 
theorem dropLast_subset (l : List α) : l.dropLast ⊆ l :=
  (dropLast_sublist l).subset
Subset Property of List DropLast Operation: $\text{dropLast } l \subseteq l$
Informal description
For any list $l$ of elements of type $\alpha$, the list obtained by removing the last element of $l$ is a subset of $l$. In other words, $l.\text{dropLast} \subseteq l$.
List.tail_suffix theorem
(l : List α) : tail l <:+ l
Full source 
theorem tail_suffix (l : List α) : tailtail l <:+ l := by rw [← drop_one]; apply drop_suffix
Tail of a List is a Suffix
Informal description
For any list $l$ of elements of type $\alpha$, the tail of $l$ is a suffix of $l$. In other words, if $l$ is non-empty, then removing its first element yields a list that appears at the end of $l$.
List.IsPrefix.map theorem
{β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f
Full source 
theorem IsPrefix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f := by
  obtain ⟨r, rfl⟩ := h
  rw [map_append]; apply prefix_append
Mapping Preserves Prefix Relation: $\text{map } f l_1 <+: \text{map } f l_2$ if $l_1 <+: l_2$
Informal description
For any function $f : \alpha \to \beta$ and any two lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$, then the mapped list $\text{map } f l_1$ is a prefix of the mapped list $\text{map } f l_2$.
List.IsSuffix.map theorem
{β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f
Full source 
theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f := by
  obtain ⟨r, rfl⟩ := h
  rw [map_append]; apply suffix_append
Mapping Preserves Suffix Relation: $\text{map } f l_1 <:+ \text{map } f l_2$ when $l_1 <:+ l_2$
Informal description
For any function $f : \alpha \to \beta$ and any two lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = t ++ l_1$), then the mapped list $\text{map } f l_1$ is a suffix of $\text{map } f l_2$.
List.IsInfix.map theorem
{β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f
Full source 
theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f := by
  obtain ⟨r₁, r₂, rfl⟩ := h
  rw [map_append, map_append]; apply infix_append
Preservation of Infix Relation Under List Mapping: $l_1 \subseteq l_2 \implies f \circ l_1 \subseteq f \circ l_2$
Informal description
For any function $f : \alpha \to \beta$ and any lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is an infix of $l_2$, then the mapped list $f \circ l_1$ is an infix of the mapped list $f \circ l_2$. Here, $f \circ l$ denotes the list obtained by applying $f$ to each element of $l$.
List.IsPrefix.filter theorem
(p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.filter p <+: l₂.filter p
Full source 
theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
    l₁.filter p <+: l₂.filter p := by
  obtain ⟨xs, rfl⟩ := h
  rw [filter_append]; apply prefix_append
Filter Preserves Prefix Relation: $\text{filter } p \ l_1 <+: \text{filter } p \ l_2$ when $l_1 <+: l_2$
Informal description
For any predicate $p \colon \alpha \to \text{Bool}$ and any two lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$, then the filtered list $\text{filter } p \ l_1$ is a prefix of the filtered list $\text{filter } p \ l_2$. In symbols: \[ l_1 <+: l_2 \implies \text{filter } p \ l_1 <+: \text{filter } p \ l_2 \]
List.IsSuffix.filter theorem
(p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.filter p <:+ l₂.filter p
Full source 
theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
    l₁.filter p <:+ l₂.filter p := by
  obtain ⟨xs, rfl⟩ := h
  rw [filter_append]; apply suffix_append
Filter Preserves Suffix Relation: $\text{filter } p \ l_1 <:+ \text{filter } p \ l_2$ when $l_1 <:+ l_2$
Informal description
For any predicate $p \colon \alpha \to \text{Bool}$ and any two lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is a suffix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = t ++ l_1$), then the filtered list $\text{filter } p \ l_1$ is a suffix of the filtered list $\text{filter } p \ l_2$. In symbols: \[ l_1 <:+ l_2 \implies \text{filter } p \ l_1 <:+ \text{filter } p \ l_2 \]
List.IsInfix.filter theorem
(p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.filter p <:+: l₂.filter p
Full source 
theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
    l₁.filter p <:+: l₂.filter p := by
  obtain ⟨xs, ys, rfl⟩ := h
  rw [filter_append, filter_append]; apply infix_append _
Filter Preserves Infix Relation on Lists
Informal description
For any predicate $p \colon \alpha \to \text{Bool}$ and any two lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is an infix of $l_2$ (i.e., there exist lists $s$ and $t$ such that $l_2 = s ++ l_1 ++ t$), then the filtered list $\text{filter } p \ l_1$ is an infix of $\text{filter } p \ l_2$. In symbols: \[ l_1 \subseteq_{\text{infix}} l_2 \implies \text{filter } p \ l_1 \subseteq_{\text{infix}} \text{filter } p \ l_2 \]
List.IsPrefix.filterMap theorem
{β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : filterMap f l₁ <+: filterMap f l₂
Full source 
theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
    filterMapfilterMap f l₁ <+: filterMap f l₂ := by
  obtain ⟨xs, rfl⟩ := h
  rw [filterMap_append]; apply prefix_append
Preservation of Prefix Relation under `filterMap`
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and any two lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is a prefix of $l_2$, then the result of applying $\text{filterMap } f$ to $l_1$ is a prefix of the result of applying $\text{filterMap } f$ to $l_2$. In other words, the $\text{filterMap}$ operation preserves the prefix relation between lists.
List.IsSuffix.filterMap theorem
{β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : filterMap f l₁ <:+ filterMap f l₂
Full source 
theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
    filterMapfilterMap f l₁ <:+ filterMap f l₂ := by
  obtain ⟨xs, rfl⟩ := h
  rw [filterMap_append]; apply suffix_append
Preservation of Suffix Relation under `filterMap`
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and any two lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is a suffix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = t \mathbin{+\kern-1.5ex+} l_1$), then the result of applying `filterMap f` to $l_1$ is a suffix of the result of applying `filterMap f` to $l_2$. In other words, the `filterMap` operation preserves the suffix relation between lists.
List.IsInfix.filterMap theorem
{β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : filterMap f l₁ <:+: filterMap f l₂
Full source 
theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
    filterMapfilterMap f l₁ <:+: filterMap f l₂ := by
  obtain ⟨xs, ys, rfl⟩ := h
  rw [filterMap_append, filterMap_append]; apply infix_append
`filterMap` Preserves Infix Relation on Lists
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and any two lists $l_1, l_2 : \text{List } \alpha$, if $l_1$ is an infix of $l_2$, then the result of applying `filterMap f` to $l_1$ is an infix of the result of applying `filterMap f` to $l_2$. In other words, if there exist lists $s, t$ such that $l_2 = s \mathbin{+\kern-1.5ex+} l_1 \mathbin{+\kern-1.5ex+} t$, then there exist lists $s', t'$ such that $\text{filterMap } f l_2 = s' \mathbin{+\kern-1.5ex+} \text{filterMap } f l_1 \mathbin{+\kern-1.5ex+} t'$.
List.isPrefixOf_iff_prefix theorem
[BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.isPrefixOf l₂ ↔ l₁ <+: l₂
Full source 
@[simp] theorem isPrefixOf_iff_prefix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
    l₁.isPrefixOf l₂ ↔ l₁ <+: l₂ := by
  induction l₁ generalizing l₂ with
  | nil => simp
  | cons a l₁ ih =>
    cases l₂ with
    | nil => simp
    | cons a' l₂ => simp [isPrefixOf, ih]
Boolean Prefix Check Equivalence: $\text{isPrefixOf}\,l_1\,l_2 \leftrightarrow l_1 <+: l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$ with a boolean equality relation `==` that coincides with propositional equality, the boolean function `isPrefixOf l₁ l₂` returns `true` if and only if $l_1$ is a prefix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = l_1 ++ t$).
List.instDecidableIsPrefixOfDecidableEq instance
[DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+: l₂)
Full source 
instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+: l₂) :=
  decidable_of_iff (l₁.isPrefixOf l₂) isPrefixOf_iff_prefix
Decidability of List Prefix Relation
Informal description
For any type $\alpha$ with decidable equality and any two lists $l_1, l_2$ of elements of $\alpha$, the proposition that $l_1$ is a prefix of $l_2$ is decidable.
List.isSuffixOf_iff_suffix theorem
[BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.isSuffixOf l₂ ↔ l₁ <:+ l₂
Full source 
@[simp] theorem isSuffixOf_iff_suffix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
    l₁.isSuffixOf l₂ ↔ l₁ <:+ l₂ := by
  simp [isSuffixOf]
Boolean Suffix Check Equivalence: `isSuffixOf l₁ l₂ ↔ l₁ <:+ l₂`
Informal description
For any two lists $l_1$ and $l_2$ of type $\alpha$ with a boolean equality relation `==` that coincides with propositional equality, the boolean function `isSuffixOf l₁ l₂` returns `true` if and only if $l_1$ is a suffix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = t ++ l_1$).
List.instDecidableIsSuffixOfDecidableEq instance
[DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+ l₂)
Full source 
instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+ l₂) :=
  decidable_of_iff (l₁.isSuffixOf l₂) isSuffixOf_iff_suffix
Decidability of List Suffix Relation for Types with Decidable Equality
Informal description
For any type $\alpha$ with decidable equality and any two lists $l_1, l_2$ of elements of $\alpha$, the proposition that $l_1$ is a suffix of $l_2$ (written $l_1 <:+ l_2$) is decidable.
List.prefix_iff_eq_append theorem
: l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂
Full source 
theorem prefix_iff_eq_append : l₁ <+: l₂l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
  ⟨by rintro ⟨r, rfl⟩; rw [drop_left], fun e => ⟨_, e⟩⟩
Prefix Characterization via Concatenation and Drop: $l_1 <+: l_2 \leftrightarrow l_1 ++ \text{drop}(|l_1|, l_2) = l_2$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, $l_1$ is a prefix of $l_2$ if and only if the concatenation of $l_1$ with the list obtained by dropping the first $|l_1|$ elements of $l_2$ equals $l_2$, where $|l_1|$ denotes the length of $l_1$.
List.prefix_iff_eq_take theorem
: l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂
Full source 
theorem prefix_iff_eq_take : l₁ <+: l₂l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
  ⟨fun h => append_cancel_right <| (prefix_iff_eq_append.1 h).trans (take_append_drop _ _).symm,
    fun e => e.symm ▸ take_prefix _ _⟩
Prefix Characterization via Take Operation: $l_1 <+: l_2 \leftrightarrow l_1 = \text{take}(|l_1|, l_2)$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, $l_1$ is a prefix of $l_2$ if and only if $l_1$ equals the list obtained by taking the first $|l_1|$ elements of $l_2$, where $|l_1|$ denotes the length of $l_1$.
List.sublist_join_of_mem abbrev
Full source 
@[deprecated sublist_flatten_of_mem (since := "2024-10-14")] abbrev sublist_join_of_mem := @sublist_flatten_of_mem
Sublist Property of List Joining: Membership Implies Sublist of Join
Informal description
For any list of lists $L : \text{List}(\text{List} \alpha)$ and any list $l \in L$, the list $l$ is a sublist of the concatenation (join) of all lists in $L$.
List.sublist_join_iff abbrev
Full source 
@[deprecated sublist_flatten_iff (since := "2024-10-14")] abbrev sublist_join_iff := @sublist_flatten_iff
Sublist Characterization via List Joining: $l <+ \text{join}(L) \leftrightarrow \exists L', l = \text{join}(L') \land \forall i < |L'|, L'[i] <+ L[i]?.\text{getD}\ []$
Informal description
For any list of lists $L : \text{List}(\text{List} \alpha)$ and any list $l : \text{List} \alpha$, the list $l$ is a sublist of the concatenation (join) of $L$ if and only if there exists a list of lists $L'$ such that: 1. $l$ is equal to the concatenation of $L'$, and 2. For every index $i$ with $i < \text{length}(L')$, the $i$-th element of $L'$ is a sublist of the $i$-th element of $L$ (or the empty list if $L$ has no such element). In symbols: $$ l <+ \text{join}(L) \leftrightarrow \exists L',\ l = \text{join}(L') \land \forall i < \text{length}(L'),\ L'[i] <+ L[i]?.\text{getD}\ [] $$
List.flatten_join_iff abbrev
Full source 
@[deprecated flatten_sublist_iff (since := "2024-10-14")] abbrev flatten_join_iff := @flatten_sublist_iff
Sublist Condition for Flattened Lists: $L.\text{flatten} <+ l \leftrightarrow \exists L', l = L'.\text{flatten} \land \forall i < \text{length}\,L, L[i] <+ L'[i]?.\text{getD}\ []$
Informal description
For any list of lists $L : \text{List}(\text{List} \alpha)$ and any list $l : \text{List} \alpha$, the concatenation (flattening) of $L$ is a sublist of $l$ if and only if there exists a list of lists $L'$ such that: 1. $l$ is the concatenation of $L'$, and 2. For every index $i$ less than the length of $L$, the $i$-th element of $L$ is a sublist of the $i$-th element of $L'$ (or the empty list if $L'$ has no such element). In symbols: $$L.\text{flatten} <+ l \leftrightarrow \exists L', l = L'.\text{flatten} \land \forall i < \text{length}\,L, L[i] <+ L'[i]?.\text{getD}\ []$$
List.infix_of_mem_join abbrev
Full source 
@[deprecated infix_of_mem_flatten (since := "2024-10-14")] abbrev infix_of_mem_join := @infix_of_mem_flatten
Membership in Joined List Implies Infix in Flattened List
Informal description
For any list of lists $L$ of elements of type $\alpha$, if a list $l$ is a member of the join (flattened concatenation) of $L$, then $l$ is an infix of the flattened list obtained by concatenating all lists in $L$.