doc-next-gen

Init.Data.List.BasicAux

Module docstring

{"The following functions can't be defined at Init.Data.List.Basic, because they depend on Init.Util, and Init.Util depends on Init.Data.List.Basic. ","## Alternative getters ","### get? ","### get! ","### getD ","### getLast! ","## Head and tail ","### head! ","### tail! ","### partitionM ","### partitionMap ","### mapMono

This is a performance optimization for List.mapM that avoids allocating a new list when the result of each f a is a pointer equal value a.

For verification purposes, List.mapMono = List.map. ","## Additional lemmas required for bootstrapping Array. "}

List.get? definition
: (as : List α) → (i : Nat) → Option α
Full source 
/--
Returns the `i`-th element in the list (zero-based).

If the index is out of bounds (`i ≥ as.length`), this function returns `none`.
Also see `get`, `getD` and `get!`.
-/
@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
def get? : (as : List α) → (i : Nat) → Option α
  | a::_,  0   => some a
  | _::as, n+1 => get? as n
  | _,     _   => none
List element access with optional result
Informal description
The function `List.get?` takes a list `as` of type `List α` and a natural number index `i`, and returns the `i`-th element of the list (0-based) as an optional value (`Option α`). If the index is out of bounds (i.e., `i ≥ as.length`), it returns `none`. Specifically: - For a non-empty list `a :: as` and index `0`, it returns `some a`. - For a non-empty list `a :: as` and index `n+1`, it recursively calls `get? as n`. - For an empty list or any invalid index, it returns `none`.
List.get?_nil theorem
: @get? α [] n = none
Full source 
@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
theorem get?_nil : @get? α [] n = none := rfl
Empty List Access Yields None
Informal description
For any type $\alpha$ and any natural number index $n$, accessing the $n$-th element of the empty list `[]` using `List.get?` returns `none`.
List.get?_cons_zero theorem
: @get? α (a :: l) 0 = some a
Full source 
@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
theorem get?_cons_zero : @get? α (a::l) 0 = some a := rfl
First Element Access in List via `get?`
Informal description
For any list `a :: l` of type `List α` and index `0`, the `get?` function returns `some a`, i.e., the first element of the list.
List.get?_cons_succ theorem
: @get? α (a :: l) (n + 1) = get? l n
Full source 
@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
theorem get?_cons_succ : @get? α (a::l) (n+1) = get? l n := rfl
Recursive List Access via `get?` on Successor Index
Informal description
For any list `a :: l` of type `List α` and natural number index `n`, accessing the element at index `n + 1` via `List.get?` is equivalent to accessing the element at index `n` in the tail `l` of the list. In other words, $\text{get?}(a :: l, n + 1) = \text{get?}(l, n)$.
List.ext_get? theorem
: ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
Full source 
@[deprecated "Use `List.ext_getElem?`." (since := "2025-02-12")]
theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
  | [], [], _ => rfl
  | _ :: _, [], h => nomatch h 0
  | [], _ :: _, h => nomatch h 0
  | a :: l₁, a' :: l₂, h => by
    have h0 : some a = some a' := h 0
    injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
List Equality via Element-wise Access: $\forall n, l_1.\text{get?}\,n = l_2.\text{get?}\,n \to l_1 = l_2$
Informal description
For any two lists $l_1$ and $l_2$ of type $\text{List}\,\alpha$, if for every natural number index $n$, the result of accessing the $n$-th element via $\text{get?}$ is the same for both lists (i.e., $l_1.\text{get?}\,n = l_2.\text{get?}\,n$), then $l_1 = l_2$.
List.get! definition
[Inhabited α] : (as : List α) → (i : Nat) → α
Full source 
/--
Returns the `i`-th element in the list (zero-based).

If the index is out of bounds (`i ≥ as.length`), this function panics when executed, and returns
`default`. See `get?` and `getD` for safer alternatives.
-/
@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
def get! [Inhabited α] : (as : List α) → (i : Nat) → α
  | a::_,  0   => a
  | _::as, n+1 => get! as n
  | _,     _   => panic! "invalid index"
List element access with panic on out-of-bounds
Informal description
Given a list `as` of elements of type `α` (which must have a default value) and a natural number index `i`, this function returns the `i`-th element of the list (0-based). If the index is out of bounds (i.e., `i ≥ as.length`), the function raises a runtime panic with the message "invalid index" and returns the default value of type `α`. The function is defined recursively: - For a non-empty list `a::as` and index `0`, it returns the head `a`. - For a non-empty list `a::as` and index `n+1`, it recursively calls `get!` on the tail `as` with index `n`. - For any other case (empty list or invalid index), it panics.
List.get!_nil theorem
[Inhabited α] (n : Nat) : [].get! n = (default : α)
Full source 
@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
theorem get!_nil [Inhabited α] (n : Nat) : [].get! n = (default : α) := rfl
Empty List Access Yields Default Value: $[\,].\text{get!}\, n = \text{default}$
Informal description
For any natural number $n$ and any inhabited type $\alpha$, accessing the $n$-th element of an empty list using the `get!` function returns the default value of type $\alpha$. That is, $[\,].\text{get!}\, n = \text{default}$.
List.get!_cons_succ theorem
[Inhabited α] (l : List α) (a : α) (n : Nat) : (a :: l).get! (n + 1) = get! l n
Full source 
@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
theorem get!_cons_succ [Inhabited α] (l : List α) (a : α) (n : Nat) :
    (a::l).get! (n+1) = get! l n := rfl
Tail Access via `get!` at Successor Index: $(a :: l).\text{get!}(n + 1) = l.\text{get!}(n)$
Informal description
For any inhabited type $\alpha$, list $l$ of elements in $\alpha$, element $a \in \alpha$, and natural number $n$, accessing the $(n+1)$-th element of the list $a :: l$ via `get!` is equal to accessing the $n$-th element of $l$ via `get!$. That is, $(a :: l).\text{get!}(n + 1) = l.\text{get!}(n)$.
List.get!_cons_zero theorem
[Inhabited α] (l : List α) (a : α) : (a :: l).get! 0 = a
Full source 
@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
Head Access via `get!` at Index Zero
Informal description
For any inhabited type $\alpha$, list $l$ of elements in $\alpha$, and element $a \in \alpha$, the head of the list $a :: l$ accessed via `get!` at index $0$ equals $a$, i.e., $(a :: l).\text{get!}(0) = a$.
List.getD definition
(as : List α) (i : Nat) (fallback : α) : α
Full source 
/--
Returns the element at the provided index, counting from `0`. Returns `fallback` if the index is out
of bounds.

To return an `Option` depending on whether the index is in bounds, use `as[i]?`. To panic if the
index is out of bounds, use `as[i]!`.

Examples:
 * `["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"`
 * `["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"`
 * `["spring", "summer", "fall", "winter"].getD 4 "never" = "never"`
-/
def getD (as : List α) (i : Nat) (fallback : α) : α :=
  as[i]?.getD fallback
Default list element accessor
Informal description
Given a list `as` of type `List α`, a natural number index `i`, and a default value `fallback` of type `α`, the function returns the element at position `i` in `as` if `i` is a valid index (i.e., `i < as.length`), otherwise it returns `fallback`.
List.getD_nil theorem
: getD [] n d = d
Full source 
@[simp] theorem getD_nil : getD [] n d = d := rfl
Default Access on Empty List: $\text{getD}(\text{[]}, n, d) = d$
Informal description
For any natural number index $n$ and default value $d$ of type $\alpha$, accessing an element in the empty list `[]` using `getD` with index $n$ and default $d$ returns $d$.
List.getLast! definition
[Inhabited α] : List α → α
Full source 
/--
Returns the last element in the list. Panics and returns `default` if the list is empty.

Safer alternatives include:
 * `getLast?`, which returns an `Option`,
 * `getLastD`, which takes a fallback value for empty lists, and
 * `getLast`, which requires a proof that the list is non-empty.

Examples:
 * `["circle", "rectangle"].getLast! = "rectangle"`
 * `["circle"].getLast! = "circle"`
-/
def getLast! [Inhabited α] : List α → α
  | []    => panic! "empty list"
  | a::as => getLast (a::as) (fun h => List.noConfusion h)
Last element of a list (with panic on empty list)
Informal description
The function takes a list of elements of type $\alpha$ (which must have a default value) and returns its last element. If the list is empty, it raises a panic with the message "empty list" and returns the default value of $\alpha$.
List.head! definition
[Inhabited α] : List α → α
Full source 
/--
Returns the first element in the list. If the list is empty, panics and returns `default`.

Safer alternatives include:
  * `List.head`, which requires a proof that the list is non-empty,
  * `List.head?`, which returns an `Option`, and
  * `List.headD`, which returns an explicitly-provided fallback value on empty lists.
-/
def head! [Inhabited α] : List α → α
  | []   => panic! "empty list"
  | a::_ => a
Head of a list (with panic on empty list)
Informal description
The function `List.head!` takes a list of elements of type `α` (which must have a default value) and returns its first element. If the list is empty, it raises a panic with the message "empty list" and returns the default value of `α`.
List.tail! definition
: List α → List α
Full source 
/--
Drops the first element of a nonempty list, returning the tail. If the list is empty, this function
panics when executed and returns the empty list.

Safer alternatives include
 * `tail`, which returns the empty list without panicking,
 * `tail?`, which returns an `Option`, and
 * `tailD`, which returns a fallback value when passed the empty list.

Examples:
 * `["apple", "banana", "grape"].tail! = ["banana", "grape"]`
 * `["banana", "grape"].tail! = ["grape"]`
-/
def tail! : List α → List α
  | []    => panic! "empty list"
  | _::as => as
Tail of a list (with panic on empty list)
Informal description
The function `List.tail!` takes a list of elements of type `α` and returns the tail of the list (i.e., the list without its first element). If the input list is empty, the function panics with the message "empty list".
List.tail!_cons theorem
: @tail! α (a :: l) = l
Full source 
@[simp] theorem tail!_cons : @tail! α (a::l) = l := rfl
Tail of Cons List Equals Original List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of type $\text{List}\,\alpha$, the tail of the list $a :: l$ is equal to $l$.
List.partitionM definition
[Monad m] (p : α → m Bool) (l : List α) : m (List α × List α)
Full source 
/--
Returns a pair of lists that together contain all the elements of `as`. The first list contains
those elements for which the monadic predicate `p` returns `true`, and the second contains those for
which `p` returns `false`. The list's elements are examined in order, from left to right.

This is a monadic version of `List.partition`.

Example:
```lean example
def posOrNeg (x : Int) : Except String Bool :=
  if x > 0 then pure true
  else if x < 0 then pure false
  else throw "Zero is not positive or negative"
```
```lean example
#eval [-1, 2, 3].partitionM posOrNeg
```
```output
Except.ok ([2, 3], [-1])
```
```lean example
#eval [0, 2, 3].partitionM posOrNeg
```
```output
Except.error "Zero is not positive or negative"
```
-/
@[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (ListList α × List α) :=
  go l #[] #[]
where
  /-- Auxiliary for `partitionM`:
  `partitionM.go p l acc₁ acc₂` returns `(acc₁.toList ++ left, acc₂.toList ++ right)`
  if `partitionM p l` returns `(left, right)`. -/
  @[specialize] go : List α → Array α → Array α → m (ListList α × List α)
  | [], acc₁, acc₂ => pure (acc₁.toList, acc₂.toList)
  | x :: xs, acc₁, acc₂ => do
    if ← p x then
      go xs (acc₁.push x) acc₂
    else
      go xs acc₁ (acc₂.push x)
Monadic partition of a list
Informal description
Given a monadic predicate `p : α → m Bool` and a list `l : List α`, the function `List.partitionM` partitions the elements of `l` into two lists based on the result of applying `p` to each element. The first list contains elements for which `p` returns `true`, and the second list contains elements for which `p` returns `false`. The operation is performed in the monadic context `m`, and the order of elements in the input list is preserved in the output lists.
List.partitionMap definition
(f : α → β ⊕ γ) (l : List α) : List β × List γ
Full source 
/--
Applies a function that returns a disjoint union to each element of a list, collecting the `Sum.inl`
and `Sum.inr` results into separate lists.

Examples:
 * `[0, 1, 2, 3].partitionMap (fun x => if x % 2 = 0 then .inl x else .inr x) = ([0, 2], [1, 3])`
 * `[0, 1, 2, 3].partitionMap (fun x => if x = 0 then .inl x else .inr x) = ([0], [1, 2, 3])`
-/
@[inline] def partitionMap (f : α → β ⊕ γ) (l : List α) : ListList β × List γ := go l #[] #[] where
  /-- Auxiliary for `partitionMap`:
  `partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)`
  if `partitionMap f l = (left, right)`. -/
  @[specialize] go : List α → Array β → Array γ → ListList β × List γ
  | [], acc₁, acc₂ => (acc₁.toList, acc₂.toList)
  | x :: xs, acc₁, acc₂ =>
    match f x with
    | .inl a => go xs (acc₁.push a) acc₂
    | .inr b => go xs acc₁ (acc₂.push b)
Partition a list based on a function returning a disjoint union
Informal description
Given a function $f : \alpha \to \beta \oplus \gamma$ and a list $l$ of elements of type $\alpha$, the function `List.partitionMap` applies $f$ to each element of $l$ and collects the results into two separate lists: one for the `inl` results (of type $\beta$) and one for the `inr` results (of type $\gamma$). For example: - Applying `partitionMap` with $f(x) = \text{inl}\,x$ if $x$ is even and $\text{inr}\,x$ otherwise to the list $[0, 1, 2, 3]$ yields $([0, 2], [1, 3])$. - Applying `partitionMap` with $f(x) = \text{inl}\,x$ if $x = 0$ and $\text{inr}\,x$ otherwise to the list $[0, 1, 2, 3]$ yields $([0], [1, 2, 3])$.
List.mapMonoM definition
[Monad m] (as : List α) (f : α → m α) : m (List α)
Full source 
/--
Applies a monadic function to each element of a list, returning the list of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new list if the result of each function call is
pointer-equal to its argument.
-/
@[implemented_by mapMonoMImp] def mapMonoM [Monad m] (as : List α) (f : α → m α) : m (List α) :=
  match as with
  | [] => return []
  | a :: as => return (← f a) :: (← mapMonoM as f)
Monadic map preserving pointer equality
Informal description
Given a monad `m`, a list `as` of elements of type `α`, and a monadic function `f : α → m α`, the function `List.mapMonoM` applies `f` to each element of `as` and returns the list of results in the monadic context. The implementation ensures that if each application of `f` returns a value that is pointer-equal to its input, no new list is allocated.
List.mapMono definition
(as : List α) (f : α → α) : List α
Full source 
/--
Applies a function to each element of a list, returning the list of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new list if the result of each function call is
pointer-equal to its argument.

For verification purposes, `List.mapMono = List.map`.
-/
def mapMono (as : List α) (f : α → α) : List α :=
  Id.run <| as.mapMonoM f
Pointer-preserving map on lists
Informal description
Given a list `as` of elements of type `α` and a function `f : α → α`, the function `List.mapMono` applies `f` to each element of `as` and returns the list of results. The implementation is optimized to avoid allocating a new list if each application of `f` returns a value that is pointer-equal to its input. For verification purposes, this function is equivalent to `List.map`.
List.getElem_append_left theorem
{as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} : (as ++ bs)[i] = as[i]
Full source 
@[simp]
theorem getElem_append_left {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} :
    (as ++ bs)[i] = as[i] := by
  induction as generalizing i with
  | nil => trivial
  | cons a as ih =>
    cases i with
    | zero => rfl
    | succ i => apply ih
Element Access in Concatenated List Preserves Left Operand
Informal description
For any lists `as` and `bs` of elements of type `α`, and any natural number index `i` such that `i < as.length` and `i < (as ++ bs).length`, the element at index `i` in the concatenated list `as ++ bs` is equal to the element at index `i` in `as`. In other words, $(as \mathbin{+\kern-1.5ex+} bs)[i] = as[i]$.
List.getElem_append_right theorem
{as bs : List α} {i : Nat} (h₁ : as.length ≤ i) {h₂} : (as ++ bs)[i]'h₂ = bs[i - as.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂)
Full source 
@[simp]
theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i) {h₂} :
    (as ++ bs)[i]'h₂ =
      bs[i - as.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) := by
  induction as generalizing i with
  | nil => trivial
  | cons a as ih =>
    cases i with simp [Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h₁
    | succ i => apply ih; simp [h₁]
Element Access in Concatenated List's Right Operand: $(\text{as} \mathbin{+\kern-1.5ex+} \text{bs})[i] = \text{bs}[i - |\text{as}|]$ when $|\text{as}| \leq i$
Informal description
For any lists `as` and `bs` of elements of type $\alpha$, and any natural number index `i` such that the length of `as` is less than or equal to `i` (i.e., $|\text{as}| \leq i$), the element at index `i` in the concatenated list $\text{as} \mathbin{+\kern-1.5ex+} \text{bs}$ is equal to the element at index $i - |\text{as}|$ in `bs`. More formally, under the assumption $|\text{as}| \leq i$ and the validity condition $i < |\text{as} \mathbin{+\kern-1.5ex+} \text{bs}|$, we have: $$(\text{as} \mathbin{+\kern-1.5ex+} \text{bs})[i] = \text{bs}[i - |\text{as}|]$$
List.get_last theorem
{as : List α} {i : Fin (length (as ++ [a]))} (h : ¬i.1 < as.length) : (as ++ [a] : List _).get i = a
Full source 
@[deprecated "Deprecated without replacement." (since := "2025-02-13")]
theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a := by
  cases i; rename_i i h'
  induction as generalizing i with
  | nil => cases i with
    | zero => simp [List.get]
    | succ => simp +arith at h'
  | cons a as ih =>
    cases i with simp at h
    | succ i => apply ih; simp [h]
Last Element Access in Concatenated List: $(as \mathbin{+\kern-1.5ex+} [a])[i] = a$ when $i \geq \text{length}(as)$
Informal description
For any list `as` of elements of type `alpha`, any element `a` of type `alpha`, and any index `i` of type `Fin (length (as ++ [a]))` (i.e., a natural number less than the length of the concatenated list `as ++ [a]`), if the value of `i` is not less than the length of `as`, then the element at position `i` in the concatenated list `as ++ [a]` is equal to `a`. In other words, if $i \geq \text{length}(as)$, then $(as \mathbin{+\kern-1.5ex+} [a])[i] = a$.
List.sizeOf_lt_of_mem theorem
[SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as
Full source 
theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as := by
  induction h with
  | head => simp +arith
  | tail _ _ ih => exact Nat.lt_trans ih (by simp +arith)
Size Comparison for List Elements: $\text{sizeOf}(a) < \text{sizeOf}(as)$ when $a \in as$
Informal description
For any type $\alpha$ with a size function and any list $as$ of elements of type $\alpha$, if an element $a$ is a member of $as$, then the size of $a$ is strictly less than the size of $as$.
List.tacticSizeOf_list_dec definition
: Lean.ParserDescr✝
Full source 
macromacro "sizeOf_list_dec" : tactic =>
  `(tactic| first
    | with_reducible apply sizeOf_lt_of_mem; assumption; done
    | with_reducible
        apply Nat.lt_of_lt_of_le (sizeOf_lt_of_mem ?h)
        case' h => assumption
      simp +arith)
Size comparison tactic for list elements
Informal description
The tactic `sizeOf_list_dec` is added to the `decreasing_trivial` toolbox to automatically prove that `sizeOf a < sizeOf as` when `a` is a member of the list `as`. This is particularly useful for well-founded recursions over nested inductive types like `inductive T | mk : List T → T`.
List.append_cancel_left theorem
{as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs
Full source 
theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs := by
  induction as with
  | nil => assumption
  | cons a as ih =>
    injection h with _ h
    exact ih h
Left Cancellation Property of List Concatenation
Informal description
For any lists $as$, $bs$, and $cs$ of elements of type $\alpha$, if the concatenation $as ++ bs$ is equal to the concatenation $as ++ cs$, then $bs$ is equal to $cs$.
List.append_cancel_right theorem
{as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs
Full source 
theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs := by
  match as, cs with
  | [], []       => rfl
  | [], c::cs    => have aux := congrArg length h; simp +arith at aux
  | a::as, []    => have aux := congrArg length h; simp +arith at aux
  | a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]
Right Cancellation Property of List Concatenation
Informal description
For any lists $as$, $bs$, and $cs$ of elements of type $\alpha$, if the concatenation $as ++ bs$ is equal to the concatenation $cs ++ bs$, then $as$ is equal to $cs$.
List.append_cancel_left_eq theorem
(as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs)
Full source 
@[simp] theorem append_cancel_left_eq (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs) := by
  apply propext; apply Iff.intro
  next => apply append_cancel_left
  next => intro h; simp [h]
Left Cancellation Property of List Concatenation: $(as ++ bs = as ++ cs) ↔ (bs = cs)$
Informal description
For any lists $as$, $bs$, and $cs$ of elements of type $\alpha$, the equality $as ++ bs = as ++ cs$ holds if and only if $bs = cs$.
List.append_cancel_right_eq theorem
(as bs cs : List α) : (as ++ bs = cs ++ bs) = (as = cs)
Full source 
@[simp] theorem append_cancel_right_eq (as bs cs : List α) : (as ++ bs = cs ++ bs) = (as = cs) := by
  apply propext; apply Iff.intro
  next => apply append_cancel_right
  next => intro h; simp [h]
Right Cancellation Property of List Concatenation: $(as ++ bs = cs ++ bs) ↔ (as = cs)$
Informal description
For any lists $as$, $bs$, and $cs$ of elements of type $\alpha$, the equality $as ++ bs = cs ++ bs$ holds if and only if $as = cs$.
List.sizeOf_get theorem
[SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as
Full source 
theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
  match as, i with
  | a::as, ⟨0, _⟩  => simp +arith [get]
  | a::as, ⟨i+1, h⟩ =>
    have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
    apply Nat.lt_trans ih
    simp +arith
Element Size Bound in List: $\text{sizeOf}(as.get\ i) < \text{sizeOf}(as)$
Informal description
For any list `as` of elements of type `α` equipped with a size function `sizeOf`, and for any valid index `i` of type `Fin as.length` (a natural number less than the length of `as`), the size of the element `as.get i` is strictly less than the size of the entire list `as`. That is, $\text{sizeOf}(as.get\ i) < \text{sizeOf}(as)$.
List.not_lex_antisymm theorem
[DecidableEq α] {r : α → α → Prop} [DecidableRel r] (antisymm : ∀ x y : α, ¬r x y → ¬r y x → x = y) {as bs : List α} (h₁ : ¬Lex r bs as) (h₂ : ¬Lex r as bs) : as = bs
Full source 
theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
    {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
  match as, bs with
  | [],    []    => rfl
  | [],    _::_ => False.elim <| h₂ (List.Lex.nil ..)
  | _::_, []    => False.elim <| h₁ (List.Lex.nil ..)
  | a::as, b::bs => by
    by_cases hab : r a b
    · exact False.elim <| h₂ (List.Lex.rel hab)
    · by_cases eq : a = b
      · subst eq
        have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)
        have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)
        simp [not_lex_antisymm antisymm h₁ h₂]
      · exfalso
        by_cases hba : r b a
        · exact h₁ (Lex.rel hba)
        · exact eq (antisymm _ _ hab hba)
Antisymmetry of List Lexicographic Order under Negated Relations
Informal description
Let $\alpha$ be a type with decidable equality and $r$ be a decidable binary relation on $\alpha$. Suppose that for any $x, y \in \alpha$, if neither $r(x,y)$ nor $r(y,x)$ holds, then $x = y$. Then for any two lists $as, bs$ of elements of $\alpha$, if neither $as$ is lexicographically less than $bs$ with respect to $r$ nor $bs$ is lexicographically less than $as$ with respect to $r$, then $as = bs$.
List.le_antisymm theorem
[DecidableEq α] [LT α] [DecidableLT α] [i : Std.Antisymm (¬· < · : α → α → Prop)] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs
Full source 
protected theorem le_antisymm [DecidableEq α] [LT α] [DecidableLT α]
    [i : Std.Antisymm (¬ · < · : α → α → Prop)]
    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
  not_lex_antisymm i.antisymm h₁ h₂
Antisymmetry of Lexicographic Order on Lists
Informal description
Let $\alpha$ be a type with decidable equality and a decidable "less than" relation $<$, such that the relation $\neg(x < y)$ is antisymmetric (i.e., if $\neg(x < y)$ and $\neg(y < x)$ both hold, then $x = y$). Then for any two lists $as$ and $bs$ of elements of $\alpha$, if $as \leq bs$ and $bs \leq as$ with respect to the lexicographic order, it follows that $as = bs$.
List.instAntisymmLeOfDecidableEqOfDecidableLTOfNotLt instance
[DecidableEq α] [LT α] [DecidableLT α] [s : Std.Antisymm (¬· < · : α → α → Prop)] : Std.Antisymm (· ≤ · : List α → List α → Prop)
Full source 
instance [DecidableEq α] [LT α] [DecidableLT α]
    [s : Std.Antisymm (¬ · < · : α → α → Prop)] :
    Std.Antisymm (· ≤ · : List α → List α → Prop) where
  antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂
Antisymmetry of Lexicographic Order on Lists with Decidable Relations
Informal description
For any type $\alpha$ with decidable equality and a decidable "less than" relation $<$, if the relation $\neg(x < y)$ is antisymmetric, then the lexicographic order $\leq$ on lists of elements of $\alpha$ is also antisymmetric.