doc-next-gen

Init.Data.List.Range

Module docstring

{"# Lemmas about List.range and List.zipIdx

Most of the results are deferred to Data.Init.List.Nat.Range, where more results about natural arithmetic are available. ","## Ranges and enumeration ","### range' ","### range ","### zipIdx ","### enumFrom ","### enum "}

List.range'_succ theorem
{s n step} : range' s (n + 1) step = s :: range' (s + step) n step
Full source 
theorem range'_succ {s n step} : range' s (n + 1) step = s :: range' (s + step) n step := by
  simp [range', Nat.add_succ, Nat.mul_succ]
Recursive Definition of Arithmetic Sequence with Successor Length
Informal description
For any natural numbers $s$, $n$, and $step$, the arithmetic sequence starting at $s$ with length $n+1$ and step size $step$ is equal to the list obtained by prepending $s$ to the arithmetic sequence starting at $s + step$ with length $n$ and the same step size. In other words: \[ \text{range'}\, s\, (n + 1)\, step = s :: \text{range'}\, (s + step)\, n\, step \]
List.length_range' theorem
{s step} : ∀ {n : Nat}, length (range' s n step) = n
Full source 
@[simp] theorem length_range' {s step} : ∀ {n : Nat}, length (range' s n step) = n
  | 0 => rfl
  | _ + 1 => congrArg succ length_range'
Length of Arithmetic Sequence List Equals Input Length
Informal description
For any natural numbers $s$, $n$, and $step$, the length of the list `range' s n step` is equal to $n$. That is, $\text{length}(\text{range'}\ s\ n\ step) = n$.
List.range'_eq_nil abbrev
Full source 
@[deprecated range'_eq_nil_iff (since := "2025-01-29")] abbrev range'_eq_nil := @range'_eq_nil_iff
Empty Arithmetic Sequence Condition: $\operatorname{range'}(s, n, step) = [] \leftrightarrow n = 0$
Informal description
For any natural numbers $s$, $n$, and $step$, the arithmetic sequence $\operatorname{range'}(s, n, step)$ is equal to the empty list if and only if $n = 0$.
List.range'_ne_nil_iff theorem
(s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0
Full source 
theorem range'_ne_nil_iff (s : Nat) {n step : Nat} : range'range' s n step ≠ []range' s n step ≠ [] ↔ n ≠ 0 := by
  cases n <;> simp
Non-emptiness of Arithmetic Sequence $\operatorname{range'}(s, n, \mathit{step})$ iff $n \neq 0$
Informal description
For any natural numbers $s$, $n$, and $\mathit{step}$, the arithmetic sequence $\operatorname{range'}(s, n, \mathit{step})$ is non-empty if and only if $n \neq 0$.
List.range'_ne_nil abbrev
Full source 
@[deprecated range'_ne_nil_iff (since := "2025-01-29")] abbrev range'_ne_nil := @range'_ne_nil_iff
Non-emptiness of Arithmetic Sequence $\operatorname{range'}(s, n, \mathit{step})$ iff $n \neq 0$
Informal description
For any natural numbers $s$, $n$, and $\mathit{step}$, the arithmetic sequence $\operatorname{range'}(s, n, \mathit{step})$ is non-empty if and only if $n \neq 0$.
List.range'_zero theorem
: range' s 0 step = []
Full source 
@[simp] theorem range'_zero : range' s 0 step = [] := by
  simp
Empty Arithmetic Sequence for Zero Length
Informal description
For any natural numbers $s$ and $\mathit{step}$, the arithmetic sequence generated by `List.range'` with starting value $s$, length $0$, and step size $\mathit{step}$ is the empty list, i.e., $\mathtt{range'}\,s\,0\,\mathit{step} = []$.
List.range'_one theorem
{s step : Nat} : range' s 1 step = [s]
Full source 
@[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
Singleton Arithmetic Sequence Property: $\mathit{range'}(s, 1, \mathit{step}) = [s]$
Informal description
For any natural numbers $s$ and $\mathit{step}$, the arithmetic sequence `List.range'` starting at $s$ with length $1$ and step size $\mathit{step}$ is equal to the singleton list $[s]$.
List.tail_range' theorem
: (range' s n step).tail = range' (s + step) (n - 1) step
Full source 
@[simp] theorem tail_range' : (range' s n step).tail = range' (s + step) (n - 1) step := by
  cases n with
  | zero => simp
  | succ n => simp [range'_succ]
Tail of Arithmetic Sequence Equals Shifted Sequence
Informal description
For any natural numbers $s$, $n$, and $step$, the tail of the arithmetic sequence $\text{range'}\,s\,n\,step$ is equal to the arithmetic sequence starting at $s + step$ with length $n - 1$ and the same step size. In other words: \[ \text{tail}(\text{range'}\,s\,n\,step) = \text{range'}\,(s + step)\,(n - 1)\,step \]
List.range'_inj theorem
: range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')
Full source 
@[simp] theorem range'_inj : range'range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
  constructor
  · intro h
    have h' := congrArg List.length h
    simp at h'
    subst h'
    cases n with
    | zero => simp
    | succ n =>
      simp only [range'_succ] at h
      simp_all
  · rintro ⟨rfl, rfl | rfl⟩ <;> simp
Equality of Arithmetic Sequences: $\text{range'}\,s\,n = \text{range'}\,s'\,n' \iff n = n' \land (n = 0 \lor s = s')$
Informal description
For any natural numbers $s, s', n, n'$, the arithmetic sequences `range' s n` and `range' s' n'` are equal if and only if $n = n'$ and either $n = 0$ or $s = s'$. In other words: \[ \text{range'}\,s\,n = \text{range'}\,s'\,n' \iff n = n' \land (n = 0 \lor s = s') \]
List.mem_range' theorem
: ∀ {n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step * i
Full source 
theorem mem_range' : ∀ {n}, m ∈ range' s n stepm ∈ range' s n step ↔ ∃ i < n, m = s + step * i
  | 0 => by simp [range', Nat.not_lt_zero]
  | n + 1 => by
    have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n := by
      cases i <;> simp [Nat.succ_le, Nat.succ_inj']
    simp [range', mem_range', Nat.lt_succ, h]; simp only [← exists_and_right, and_assoc]
    rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
Membership Condition for Arithmetic Sequence: $m \in \text{range'}\ s\ n\ step \leftrightarrow \exists i < n, m = s + step \cdot i$
Informal description
For any natural numbers $m$, $s$, $n$, and $step$, the element $m$ belongs to the list $\text{range'}\ s\ n\ step$ if and only if there exists a natural number $i < n$ such that $m = s + step \cdot i$.
List.getElem?_range' theorem
{s step} : ∀ {i n : Nat}, i < n → (range' s n step)[i]? = some (s + step * i)
Full source 
theorem getElem?_range' {s step} :
    ∀ {i n : Nat}, i < n → (range' s n step)[i]? = some (s + step * i)
  | 0, n + 1, _ => by simp [range'_succ]
  | m + 1, n + 1, h => by
    simp only [range'_succ, getElem?_cons_succ]
    exact (getElem?_range' (s := s + step) (by exact succ_lt_succ_iff.mp h)).trans <| by
      simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
Optional Indexing of Arithmetic Sequence Yields Correct Element for Valid Indices
Informal description
For any natural numbers $s$, $step$, $i$, and $n$, if $i < n$, then the optional indexing operation on the arithmetic sequence $\text{range'}\,s\,n\,step$ at position $i$ returns $\text{some}\,(s + step \cdot i)$. That is: \[ (\text{range'}\,s\,n\,step)[i]? = \text{some}\,(s + step \cdot i) \]
List.getElem_range' theorem
{n m step} {i} (H : i < (range' n m step).length) : (range' n m step)[i] = n + step * i
Full source 
@[simp] theorem getElem_range' {n m step} {i} (H : i < (range' n m step).length) :
    (range' n m step)[i] = n + step * i :=
  (getElem?_eq_some_iff.1 <| getElem?_range' (by simpa using H)).2
Indexing Formula for Arithmetic Sequence: $(\text{range'}\,n\,m\,step)[i] = n + step \cdot i$ for Valid Indices
Informal description
For any natural numbers $n$, $m$, $step$, and $i$, if $i$ is a valid index for the list $\text{range'}\,n\,m\,step$ (i.e., $i < \text{length}(\text{range'}\,n\,m\,step)$), then the element at index $i$ in the list is equal to $n + step \cdot i$. In symbols: $$(\text{range'}\,n\,m\,step)[i] = n + step \cdot i$$
List.head?_range' theorem
: (range' s n).head? = if n = 0 then none else some s
Full source 
theorem head?_range' : (range' s n).head? = if n = 0 then none else some s := by
  induction n <;> simp_all [range'_succ, head?_append]
First Element of Arithmetic Sequence: $\text{head?}(\text{range'}\,s\,n) = \text{if } n=0 \text{ then none else some }s$
Informal description
For any natural numbers $s$ and $n$, the first element of the arithmetic sequence `range' s n` (with default step size 1) is: - `none` if $n = 0$ (i.e., the sequence is empty) - `some s` otherwise (i.e., the first element is $s$)
List.head_range' theorem
(h) : (range' s n).head h = s
Full source 
@[simp] theorem head_range' (h) : (range' s n).head h = s := by
  repeat simp_all [head?_range', head_eq_iff_head?_eq_some]
First Element of Arithmetic Sequence: $\text{head}(\text{range'}\,s\,n) = s$ when $n > 0$
Informal description
For any natural numbers $s$ and $n$, if the list $\text{range'}\,s\,n$ is non-empty (i.e., $n > 0$), then its first element is $s$.
List.map_add_range' theorem
{a} : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step
Full source 
theorem map_add_range' {a} : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step
  | _, 0, _ => rfl
  | s, n + 1, step => by simp [range', map_add_range' (s + step), Nat.add_assoc]
Mapping Addition over Arithmetic Sequence Yields Shifted Sequence
Informal description
For any natural numbers $a$, $s$, $n$, and $step$, the list obtained by mapping the function $x \mapsto a + x$ over the arithmetic sequence `range' s n step` is equal to the arithmetic sequence `range' (a + s) n step`. In other words, adding a constant $a$ to each element of the sequence $[s, s + step, \ldots, s + (n-1) \cdot step]$ yields the sequence $[a + s, a + s + step, \ldots, a + s + (n-1) \cdot step]$.
List.range'_succ_left theorem
: range' (s + 1) n step = (range' s n step).map (· + 1)
Full source 
theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1) := by
  apply ext_getElem
  · simp
  · simp [Nat.add_right_comm]
Shifted Arithmetic Sequence via Element-wise Increment
Informal description
For any natural numbers $s$, $n$, and $step$, the arithmetic sequence starting at $s + 1$ with length $n$ and step size $step$ is equal to the sequence obtained by adding $1$ to each element of the arithmetic sequence starting at $s$ with the same length and step size. In symbols: $$\text{range'}\,(s + 1)\,n\,step = \text{map}\,(x \mapsto x + 1)\,(\text{range'}\,s\,n\,step)$$
List.range'_append theorem
: ∀ {s m n step : Nat}, range' s m step ++ range' (s + step * m) n step = range' s (m + n) step
Full source 
theorem range'_append : ∀ {s m n step : Nat},
    range' s m step ++ range' (s + step * m) n step = range' s (m + n) step
  | _, 0, _, _ => by simp
  | s, m + 1, n, step => by
    simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
      using range'_append (s := s + step)
Concatenation of Arithmetic Sequences: $\mathtt{range'}\,s\,m\,\mathit{step} \mathbin{+\!\!+} \mathtt{range'}\,(s + \mathit{step} \cdot m)\,n\,\mathit{step} = \mathtt{range'}\,s\,(m + n)\,\mathit{step}$
Informal description
For any natural numbers $s$, $m$, $n$, and $\mathit{step}$, the concatenation of the arithmetic sequences $\mathtt{range'}\,s\,m\,\mathit{step}$ and $\mathtt{range'}\,(s + \mathit{step} \cdot m)\,n\,\mathit{step}$ is equal to the arithmetic sequence $\mathtt{range'}\,s\,(m + n)\,\mathit{step}$. In other words, the list $[s, s + \mathit{step}, \ldots, s + (m-1) \cdot \mathit{step}]$ concatenated with $[s + \mathit{step} \cdot m, s + \mathit{step} \cdot (m + 1), \ldots, s + \mathit{step} \cdot (m + n - 1)]$ equals $[s, s + \mathit{step}, \ldots, s + \mathit{step} \cdot (m + n - 1)]$.
List.range'_append_1 theorem
{s m n : Nat} : range' s m ++ range' (s + m) n = range' s (m + n)
Full source 
@[simp] theorem range'_append_1 {s m n : Nat} :
    range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
Concatenation of Consecutive Arithmetic Sequences: $\mathtt{range'}\,s\,m \mathbin{+\!\!+} \mathtt{range'}\,(s + m)\,n = \mathtt{range'}\,s\,(m + n)$
Informal description
For any natural numbers $s$, $m$, and $n$, the concatenation of the arithmetic sequences $\mathtt{range'}\,s\,m$ and $\mathtt{range'}\,(s + m)\,n$ is equal to the arithmetic sequence $\mathtt{range'}\,s\,(m + n)$. In other words, the list $[s, s + 1, \ldots, s + m - 1]$ concatenated with $[s + m, s + m + 1, \ldots, s + m + n - 1]$ equals $[s, s + 1, \ldots, s + m + n - 1]$.
List.range'_sublist_right theorem
{s m n : Nat} : range' s m step <+ range' s n step ↔ m ≤ n
Full source 
theorem range'_sublist_right {s m n : Nat} : range'range' s m step <+ range' s n steprange' s m step <+ range' s n step ↔ m ≤ n :=
  ⟨fun h => by simpa only [length_range'] using h.length_le,
   fun h => by rw [← add_sub_of_le h, ← range'_append]; apply sublist_append_left⟩
Sublist Condition for Arithmetic Sequences: $\mathtt{range'}\,s\,m\,\mathit{step} <+ \mathtt{range'}\,s\,n\,\mathit{step} \leftrightarrow m \leq n$
Informal description
For any natural numbers $s$, $m$, $n$, and $\mathit{step}$, the arithmetic sequence $\mathtt{range'}\,s\,m\,\mathit{step}$ is a sublist of $\mathtt{range'}\,s\,n\,\mathit{step}$ if and only if $m \leq n$.
List.range'_subset_right theorem
{s m n : Nat} (step0 : 0 < step) : range' s m step ⊆ range' s n step ↔ m ≤ n
Full source 
theorem range'_subset_right {s m n : Nat} (step0 : 0 < step) :
    range'range' s m step ⊆ range' s n steprange' s m step ⊆ range' s n step ↔ m ≤ n := by
  refine ⟨fun h => Nat.le_of_not_lt fun hn => ?_, fun h => (range'_sublist_right.2 h).subset⟩
  have ⟨i, h', e⟩ := mem_range'.1 <| h <| mem_range'.2 ⟨_, hn, rfl⟩
  exact Nat.ne_of_gt h' (Nat.eq_of_mul_eq_mul_left step0 (Nat.add_left_cancel e))
Subset Condition for Arithmetic Sequences with Positive Step: $\mathtt{range'}\,s\,m\,\mathit{step} \subseteq \mathtt{range'}\,s\,n\,\mathit{step} \leftrightarrow m \leq n$
Informal description
For any natural numbers $s$, $m$, $n$, and a positive step size $\mathit{step} > 0$, the arithmetic sequence $\mathtt{range'}\,s\,m\,\mathit{step}$ is a subset of $\mathtt{range'}\,s\,n\,\mathit{step}$ if and only if $m \leq n$.
List.range'_subset_right_1 theorem
{s m n : Nat} : range' s m ⊆ range' s n ↔ m ≤ n
Full source 
theorem range'_subset_right_1 {s m n : Nat} : range'range' s m ⊆ range' s nrange' s m ⊆ range' s n ↔ m ≤ n :=
  range'_subset_right (by decide)
Subset Condition for Arithmetic Sequences: $\mathtt{range'}\,s\,m \subseteq \mathtt{range'}\,s\,n \leftrightarrow m \leq n$
Informal description
For any natural numbers $s$, $m$, and $n$, the arithmetic sequence $\mathtt{range'}\,s\,m$ is a subset of $\mathtt{range'}\,s\,n$ if and only if $m \leq n$.
List.range'_concat theorem
{s n : Nat} : range' s (n + 1) step = range' s n step ++ [s + step * n]
Full source 
theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ [s + step * n] := by
  exact range'_append.symm
Concatenation Property of Arithmetic Sequences: $\mathtt{range'}\,s\,(n + 1)\,\mathit{step} = \mathtt{range'}\,s\,n\,\mathit{step} \mathbin{+\!\!+} [s + \mathit{step} \cdot n]$
Informal description
For any natural numbers $s$, $n$, and $\mathit{step}$, the arithmetic sequence $\mathtt{range'}\,s\,(n + 1)\,\mathit{step}$ is equal to the concatenation of the arithmetic sequence $\mathtt{range'}\,s\,n\,\mathit{step}$ with the singleton list $[s + \mathit{step} \cdot n]$. In other words, the list $[s, s + \mathit{step}, \ldots, s + \mathit{step} \cdot n]$ can be constructed by appending the element $s + \mathit{step} \cdot n$ to the list $[s, s + \mathit{step}, \ldots, s + \mathit{step} \cdot (n - 1)]$.
List.range'_1_concat theorem
{s n : Nat} : range' s (n + 1) = range' s n ++ [s + n]
Full source 
theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ [s + n] := by
  simp [range'_concat]
Concatenation Property of Arithmetic Sequences with Step 1: $\mathtt{range'}\,s\,(n + 1) = \mathtt{range'}\,s\,n \mathbin{+\!\!+} [s + n]$
Informal description
For any natural numbers $s$ and $n$, the arithmetic sequence $\mathtt{range'}\,s\,(n + 1)$ is equal to the concatenation of the arithmetic sequence $\mathtt{range'}\,s\,n$ with the singleton list $[s + n]$. In other words, the list $[s, s+1, \ldots, s+n]$ can be constructed by appending the element $s + n$ to the list $[s, s+1, \ldots, s+n-1]$.
List.range'_eq_cons_iff theorem
: range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)
Full source 
theorem range'_eq_cons_iff : range'range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1) := by
  induction n generalizing s with
  | zero => simp
  | succ n ih =>
    simp only [range'_succ]
    simp only [cons.injEq, and_congr_right_iff]
    rintro rfl
    simp [eq_comm]
Characterization of Arithmetic Sequence as Cons List
Informal description
For any natural numbers $s$ and $n$, and any list element $a$ and list $xs$, the arithmetic sequence $\mathtt{range'}\,s\,n$ equals $a :: xs$ if and only if the following three conditions hold: 1. The starting value $s$ equals $a$, 2. The length $n$ is positive ($0 < n$), and 3. The tail $xs$ equals the arithmetic sequence starting at $a + 1$ with length $n - 1$. In other words: \[ \mathtt{range'}\,s\,n = a :: xs \leftrightarrow s = a \land 0 < n \land xs = \mathtt{range'}\,(a + 1)\,(n - 1) \]
List.range_loop_range' theorem
: ∀ s n, range.loop s (range' s n) = range' 0 (n + s)
Full source 
theorem range_loop_range' : ∀ s n, range.loop s (range' s n) = range' 0 (n + s)
  | 0, _ => rfl
  | s + 1, n => by rw [← Nat.add_assoc, Nat.add_right_comm n s 1]; exact range_loop_range' s (n + 1)
Range Loop Transformation: `range.loop s (range' s n) = range' 0 (n + s)`
Informal description
For any natural numbers $s$ and $n$, the result of applying `range.loop` with starting value $s$ to the list `range' s n` is equal to the list `range' 0 (n + s)`. In other words, if `range' s n` generates the list $[s, s+1, \dots, s+n-1]$, then `range.loop s (range' s n)` produces the list $[0, 1, \dots, n+s-1]$.
List.range_eq_range' theorem
{n : Nat} : range n = range' 0 n
Full source 
theorem range_eq_range' {n : Nat} : range n = range' 0 n :=
  (range_loop_range' n 0).trans <| by rw [Nat.zero_add]
Equality of `range n` and `range' 0 n`: $\mathtt{range}\,n = [0, 1, \dots, n-1]$
Informal description
For any natural number $n$, the list `range n` is equal to the arithmetic sequence `range' 0 n`, which is the list $[0, 1, \dots, n-1]$.
List.getElem?_range theorem
{i n : Nat} (h : i < n) : (range n)[i]? = some i
Full source 
theorem getElem?_range {i n : Nat} (h : i < n) : (range n)[i]? = some i := by
  simp [range_eq_range', getElem?_range' h]
Optional Indexing of Range List Yields Correct Element for Valid Indices
Informal description
For any natural numbers $i$ and $n$ such that $i < n$, the optional indexing operation on the list $\text{range}\,n$ at position $i$ returns $\text{some}\,i$. That is: \[ (\text{range}\,n)[i]? = \text{some}\,i \]
List.getElem_range theorem
(h : j < (range n).length) : (range n)[j] = j
Full source 
@[simp] theorem getElem_range (h : j < (range n).length) : (range n)[j] = j := by
  simp [range_eq_range']
Indexing Property of Range List: $(\mathtt{range}\,n)[j] = j$ for Valid Indices
Informal description
For any natural numbers $j$ and $n$, if $j$ is a valid index for the list $\mathtt{range}\,n$ (i.e., $j < \mathtt{length}(\mathtt{range}\,n)$), then the element at index $j$ in $\mathtt{range}\,n$ is equal to $j$. In symbols: $$(\mathtt{range}\,n)[j] = j$$
List.range_succ_eq_map theorem
{n : Nat} : range (n + 1) = 0 :: map succ (range n)
Full source 
theorem range_succ_eq_map {n : Nat} : range (n + 1) = 0 :: map succ (range n) := by
  rw [range_eq_range', range_eq_range', range', Nat.add_comm, ← map_add_range']
  congr; exact funext (Nat.add_comm 1)
Recursive Definition of Range via Successor Mapping: $\mathtt{range}\,(n+1) = 0 :: \mathtt{map}\,(\mathtt{succ})\,(\mathtt{range}\,n)$
Informal description
For any natural number $n$, the list $\mathtt{range}\,(n + 1)$ is equal to the list obtained by prepending $0$ to the list $\mathtt{map}\,(\lambda x.x + 1)\,(\mathtt{range}\,n)$. In other words, $[0, 1, \dots, n] = 0 :: [1, 2, \dots, n]$.
List.range'_eq_map_range theorem
{s n : Nat} : range' s n = map (s + ·) (range n)
Full source 
theorem range'_eq_map_range {s n : Nat} : range' s n = map (s + ·) (range n) := by
  rw [range_eq_range', map_add_range']; rfl
Arithmetic Sequence as Shifted Range: $\mathtt{range'}\,s\,n = \mathtt{map}\,(s + \cdot)\,(\mathtt{range}\,n)$
Informal description
For any natural numbers $s$ and $n$, the arithmetic sequence `range' s n` (which generates the list $[s, s+1, \dots, s+(n-1)]$) is equal to the list obtained by mapping the function $x \mapsto s + x$ over the standard range `range n` (which is $[0, 1, \dots, n-1]$). In other words, $[s, s+1, \dots, s+(n-1)] = [s+0, s+1, \dots, s+(n-1)]$.
List.length_range theorem
{n : Nat} : (range n).length = n
Full source 
@[simp] theorem length_range {n : Nat} : (range n).length = n := by
  simp only [range_eq_range', length_range']
Length of Range List: $\text{length}(\text{range}\,n) = n$
Informal description
For any natural number $n$, the length of the list `range n` (which contains the numbers from $0$ to $n-1$) is equal to $n$.
List.range_ne_nil theorem
{n : Nat} : range n ≠ [] ↔ n ≠ 0
Full source 
theorem range_ne_nil {n : Nat} : rangerange n ≠ []range n ≠ [] ↔ n ≠ 0 := by
  cases n <;> simp
Non-emptiness of `range n` is equivalent to $n \neq 0$
Informal description
For any natural number $n$, the list `range n` is non-empty if and only if $n$ is non-zero. In other words, the list $[0, 1, \dots, n-1]$ is not empty precisely when $n \neq 0$.
List.tail_range theorem
: (range n).tail = range' 1 (n - 1)
Full source 
@[simp] theorem tail_range : (range n).tail = range' 1 (n - 1) := by
  rw [range_eq_range', tail_range']
Tail of Range List Equals Shifted Arithmetic Sequence
Informal description
For any natural number $n$, the tail of the list $\mathtt{range}\,n = [0, 1, \dots, n-1]$ is equal to the arithmetic sequence starting at $1$ with length $n-1$, i.e., $\mathtt{range'}\,1\,(n-1) = [1, 2, \dots, n-1]$.
List.range_sublist theorem
{m n : Nat} : range m <+ range n ↔ m ≤ n
Full source 
@[simp]
theorem range_sublist {m n : Nat} : rangerange m <+ range nrange m <+ range n ↔ m ≤ n := by
  simp only [range_eq_range', range'_sublist_right]
Sublist Condition for Range Lists: $\mathtt{range}\,m <+ \mathtt{range}\,n \leftrightarrow m \leq n$
Informal description
For any natural numbers $m$ and $n$, the list $\mathtt{range}\,m = [0, 1, \dots, m-1]$ is a sublist of $\mathtt{range}\,n = [0, 1, \dots, n-1]$ if and only if $m \leq n$.
List.range_subset theorem
{m n : Nat} : range m ⊆ range n ↔ m ≤ n
Full source 
@[simp]
theorem range_subset {m n : Nat} : rangerange m ⊆ range nrange m ⊆ range n ↔ m ≤ n := by
  simp only [range_eq_range', range'_subset_right, lt_succ_self]
Subset Relation for Range Lists: $\mathtt{range}\,m \subseteq \mathtt{range}\,n \leftrightarrow m \leq n$
Informal description
For any natural numbers $m$ and $n$, the list $\mathtt{range}\,m = [0, 1, \dots, m-1]$ is a subset of the list $\mathtt{range}\,n = [0, 1, \dots, n-1]$ if and only if $m \leq n$.
List.range_succ theorem
{n : Nat} : range (succ n) = range n ++ [n]
Full source 
theorem range_succ {n : Nat} : range (succ n) = range n ++ [n] := by
  simp only [range_eq_range', range'_1_concat, Nat.zero_add]
Range of Successor: $\mathtt{range}\,(n+1) = \mathtt{range}\,n \mathbin{+\!\!+} [n]$
Informal description
For any natural number $n$, the list $\mathtt{range}\,(\mathtt{succ}\,n) = [0, 1, \dots, n]$ is equal to the concatenation of the list $\mathtt{range}\,n = [0, 1, \dots, n-1]$ with the singleton list $[n]$.
List.range_add theorem
{n m : Nat} : range (n + m) = range n ++ (range m).map (n + ·)
Full source 
theorem range_add {n m : Nat} : range (n + m) = range n ++ (range m).map (n + ·) := by
  rw [← range'_eq_map_range]
  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 (s := 0)).symm
Range Addition Formula: $\mathtt{range}\,(n + m) = \mathtt{range}\,n \mathbin{+\!\!+} \mathtt{map}\,(n + \cdot)\,(\mathtt{range}\,m)$
Informal description
For any natural numbers $n$ and $m$, the list $\mathtt{range}\,(n + m) = [0, 1, \dots, n + m - 1]$ is equal to the concatenation of the list $\mathtt{range}\,n = [0, 1, \dots, n - 1]$ with the list obtained by mapping the function $x \mapsto n + x$ over $\mathtt{range}\,m = [0, 1, \dots, m - 1]$. In other words, $[0, 1, \dots, n + m - 1] = [0, 1, \dots, n - 1] \mathbin{+\!\!+} [n, n + 1, \dots, n + m - 1]$.
List.head?_range theorem
{n : Nat} : (range n).head? = if n = 0 then none else some 0
Full source 
theorem head?_range {n : Nat} : (range n).head? = if n = 0 then none else some 0 := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [range_succ, head?_append, ih]
    split <;> simp_all
Head of Range List: $\mathtt{head?}(\mathtt{range}\,n) = \mathtt{if}\,n=0\,\mathtt{then}\,\mathtt{none}\,\mathtt{else}\,\mathtt{some}\,0$
Informal description
For any natural number $n$, the first element of the list $\mathtt{range}\,n = [0, 1, \dots, n-1]$ (as an optional value) is $\mathtt{none}$ if $n = 0$, and $\mathtt{some}\,0$ otherwise.
List.head_range theorem
{n : Nat} (h) : (range n).head h = 0
Full source 
@[simp] theorem head_range {n : Nat} (h) : (range n).head h = 0 := by
  cases n with
  | zero => simp at h
  | succ n => simp [head?_range, head_eq_iff_head?_eq_some]
First Element of Range List is Zero: $\mathtt{head}(\mathtt{range}\,n) = 0$ for non-empty lists
Informal description
For any natural number $n$ and a proof $h$ that the list $\mathtt{range}\,n$ is non-empty, the first element of $\mathtt{range}\,n = [0, 1, \dots, n-1]$ is $0$.
List.getLast?_range theorem
{n : Nat} : (range n).getLast? = if n = 0 then none else some (n - 1)
Full source 
theorem getLast?_range {n : Nat} : (range n).getLast? = if n = 0 then none else some (n - 1) := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [range_succ, getLast?_append, ih]
    split <;> simp_all
Last Element of Range List: $\text{getLast?}(\text{range}\,n) = \text{if } n = 0 \text{ then none else some }(n-1)$
Informal description
For any natural number $n$, the last element of the list `range n` (which contains the numbers from $0$ to $n-1$) is `none` if $n = 0$ (i.e., the list is empty), and `some (n - 1)` otherwise (i.e., the last element is $n-1$).
List.getLast_range theorem
{n : Nat} (h) : (range n).getLast h = n - 1
Full source 
@[simp] theorem getLast_range {n : Nat} (h) : (range n).getLast h = n - 1 := by
  cases n with
  | zero => simp at h
  | succ n => simp [getLast?_range, getLast_eq_iff_getLast?_eq_some]
Last Element of Range List: $\mathrm{last}(\mathrm{range}\,n) = n - 1$ for $n > 0$
Informal description
For any natural number $n$ and a proof $h$ that the list $\mathrm{range}\,n$ is non-empty, the last element of $\mathrm{range}\,n$ is equal to $n - 1$.
List.zipIdx_eq_nil_iff theorem
{l : List α} {i : Nat} : List.zipIdx l i = [] ↔ l = []
Full source 
@[simp]
theorem zipIdx_eq_nil_iff {l : List α} {i : Nat} : List.zipIdxList.zipIdx l i = [] ↔ l = [] := by
  cases l <;> simp
Empty List Condition for Indexed Zipping: $\mathrm{zipIdx}(l, i) = [] \leftrightarrow l = []$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$, the list obtained by pairing each element of $l$ with its index starting from $i$ is empty if and only if $l$ itself is empty. In other words, $\mathrm{zipIdx}(l, i) = [] \leftrightarrow l = []$.
List.length_zipIdx theorem
: ∀ {l : List α} {i}, (zipIdx l i).length = l.length
Full source 
@[simp] theorem length_zipIdx : ∀ {l : List α} {i}, (zipIdx l i).length = l.length
  | [], _ => rfl
  | _ :: _, _ => congrArg Nat.succ length_zipIdx
Length Preservation of Indexed Pairing: $\mathrm{length}(\mathrm{zipIdx}(l, i)) = \mathrm{length}(l)$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$, the length of the list obtained by pairing each element of $l$ with its index (starting from $i$) is equal to the length of $l$. That is, $\mathrm{length}(\mathrm{zipIdx}(l, i)) = \mathrm{length}(l)$.
List.getElem?_zipIdx theorem
: ∀ {l : List α} {i j}, (zipIdx l i)[j]? = l[j]?.map fun a => (a, i + j)
Full source 
@[simp]
theorem getElem?_zipIdx :
    ∀ {l : List α} {i j}, (zipIdx l i)[j]? = l[j]?.map fun a => (a, i + j)
  | [], _, _ => rfl
  | _ :: _, _, 0 => by simp
  | _ :: l, n, m + 1 => by
    simp only [zipIdx_cons, getElem?_cons_succ]
    exact getElem?_zipIdx.trans <| by rw [Nat.add_right_comm]; rfl
Optional Indexing of Indexed List: $(l.\mathrm{zipIdx}\ i)[j]? = l[j]?.map (a \mapsto (a, i + j))$
Informal description
For any list $l$ of elements of type $\alpha$ and natural numbers $i$ and $j$, the optional indexing operation on the list obtained by pairing each element of $l$ with its index starting from $i$ satisfies $(l.\mathrm{zipIdx}\ i)[j]? = l[j]?.map (a \mapsto (a, i + j))$. In other words, if $j$ is a valid index for $l$, then $(l.\mathrm{zipIdx}\ i)[j]?$ returns $\mathrm{some}\ (a, i + j)$ where $a$ is the $j$-th element of $l$; otherwise, it returns $\mathrm{none}$.
List.getElem_zipIdx theorem
{l : List α} (h : i < (l.zipIdx j).length) : (l.zipIdx j)[i] = (l[i]'(by simpa [length_zipIdx] using h), j + i)
Full source 
@[simp]
theorem getElem_zipIdx {l : List α} (h : i < (l.zipIdx j).length) :
    (l.zipIdx j)[i] = (l[i]'(by simpa [length_zipIdx] using h), j + i) := by
  simp only [length_zipIdx] at h
  rw [getElem_eq_getElem?_get]
  simp only [getElem?_zipIdx, getElem?_eq_getElem h]
  simp
Element Access in Indexed List: $(l.\mathrm{zipIdx}\ j)[i] = (l[i], j + i)$ for Valid Index $i$
Informal description
For any list $l$ of elements of type $\alpha$, natural numbers $i$ and $j$, and proof $h$ that $i$ is a valid index for the list $\mathrm{zipIdx}(l, j)$, the $i$-th element of $\mathrm{zipIdx}(l, j)$ is equal to the pair $(l[i], j + i)$, where $l[i]$ is the $i$-th element of $l$.
List.tail_zipIdx theorem
{l : List α} {i : Nat} : (zipIdx l i).tail = zipIdx l.tail (i + 1)
Full source 
@[simp]
theorem tail_zipIdx {l : List α} {i : Nat} : (zipIdx l i).tail = zipIdx l.tail (i + 1) := by
  induction l generalizing i with
  | nil => simp
  | cons _ l ih => simp [ih, zipIdx_cons]
Tail of Indexed List Equals Indexed Tail with Offset
Informal description
For any list $L$ of elements of type $\alpha$ and any natural number $i$, the tail of the list obtained by pairing each element of $L$ with its index starting from $i$ is equal to the list obtained by pairing each element of the tail of $L$ with its index starting from $i + 1$. In other words, $\mathrm{tail}(\mathrm{zipIdx}(L, i)) = \mathrm{zipIdx}(\mathrm{tail}(L), i + 1)$.
List.map_snd_add_zipIdx_eq_zipIdx theorem
{l : List α} {n k : Nat} : map (Prod.map id (· + n)) (zipIdx l k) = zipIdx l (n + k)
Full source 
theorem map_snd_add_zipIdx_eq_zipIdx {l : List α} {n k : Nat} :
    map (Prod.map id (· + n)) (zipIdx l k) = zipIdx l (n + k) :=
  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl
Index Shift in `zipIdx`: $\mathrm{map} (x, i \mapsto (x, i + n)) \circ \mathrm{zipIdx}(l, k) = \mathrm{zipIdx}(l, n + k)$
Informal description
For any list $l$ of elements of type $\alpha$ and natural numbers $n$ and $k$, the list obtained by mapping the function $(x, i) \mapsto (x, i + n)$ over the list $\mathrm{zipIdx}(l, k)$ is equal to the list $\mathrm{zipIdx}(l, n + k)$. In other words, adding a constant $n$ to all indices in $\mathrm{zipIdx}(l, k)$ is equivalent to starting the indexing at $n + k$ in the first place.
List.zipIdx_cons' theorem
{i : Nat} {x : α} {xs : List α} : zipIdx (x :: xs) i = (x, i) :: (zipIdx xs i).map (Prod.map id (· + 1))
Full source 
theorem zipIdx_cons' {i : Nat} {x : α} {xs : List α} :
    zipIdx (x :: xs) i = (x, i)(x, i) :: (zipIdx xs i).map (Prod.map id (· + 1)) := by
  rw [zipIdx_cons, Nat.add_comm, ← map_snd_add_zipIdx_eq_zipIdx]
Recursive decomposition of indexed list with increment: $\mathrm{zipIdx}(x::xs, i) = (x,i) :: \mathrm{map}\ (+1)_2\ (\mathrm{zipIdx}(xs, i))$
Informal description
For any natural number $i$, element $x$ of type $\alpha$, and list $xs$ of elements of type $\alpha$, the indexed list $\mathrm{zipIdx}(x :: xs, i)$ is equal to $(x, i)$ followed by the list obtained by incrementing all indices in $\mathrm{zipIdx}(xs, i)$ by 1. That is, $$\mathrm{zipIdx}(x :: xs, i) = (x, i) :: \mathrm{map}\ (y, j \mapsto (y, j + 1))\ (\mathrm{zipIdx}(xs, i))$$
List.zipIdx_map_snd theorem
(i : Nat) : ∀ (l : List α), map Prod.snd (zipIdx l i) = range' i l.length
Full source 
@[simp]
theorem zipIdx_map_snd (i : Nat) :
    ∀ (l : List α), map Prod.snd (zipIdx l i) = range' i l.length
  | [] => rfl
  | _ :: _ => congrArg (cons _) (zipIdx_map_snd ..)
Indices in `zipIdx` form an arithmetic sequence: $\mathrm{map}\ \pi_2 \circ \mathrm{zipIdx}\ l\ i = \mathrm{range'}\ i\ (\mathrm{length}\ l)$
Informal description
For any natural number $i$ and any list $l$ of elements of type $\alpha$, the list obtained by mapping the second component (the index) of each pair in $\mathrm{zipIdx}(l, i)$ is equal to the arithmetic sequence $\mathrm{range'}(i, \mathrm{length}(l))$. In other words, if we pair each element of $l$ with its index starting from $i$ and then extract just the indices, we get the list $[i, i+1, \dots, i + \mathrm{length}(l) - 1]$.
List.zipIdx_map_fst theorem
: ∀ i (l : List α), map Prod.fst (zipIdx l i) = l
Full source 
@[simp]
theorem zipIdx_map_fst : ∀ i (l : List α), map Prod.fst (zipIdx l i) = l
  | _, [] => rfl
  | _, _ :: _ => congrArg (cons _) (zipIdx_map_fst ..)
First Projection of Indexed List Equals Original List
Informal description
For any natural number $i$ and any list $L$ of elements of type $\alpha$, the list obtained by applying the first projection (extracting the $\alpha$ component) to each element of $\mathrm{zipIdx}(L, i)$ is equal to $L$ itself. In other words, $\mathrm{map}\ \pi_1\ (\mathrm{zipIdx}(L, i)) = L$, where $\pi_1$ denotes the first projection function.
List.zipIdx_eq_zip_range' theorem
{l : List α} {i : Nat} : l.zipIdx i = l.zip (range' i l.length)
Full source 
theorem zipIdx_eq_zip_range' {l : List α} {i : Nat} : l.zipIdx i = l.zip (range' i l.length) :=
  zip_of_prod (zipIdx_map_fst ..) (zipIdx_map_snd ..)
$\mathrm{zipIdx}(l, i) = \mathrm{zip}(l, \mathrm{range'}(i, |l|))$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$, the list obtained by pairing each element of $l$ with its index starting from $i$ is equal to the zip of $l$ with the arithmetic sequence $[i, i+1, \dots, i + \mathrm{length}(l) - 1]$. In other words, $\mathrm{zipIdx}(l, i) = \mathrm{zip}(l, \mathrm{range'}(i, \mathrm{length}(l)))$.
List.unzip_zipIdx_eq_prod theorem
{l : List α} {i : Nat} : (l.zipIdx i).unzip = (l, range' i l.length)
Full source 
@[simp]
theorem unzip_zipIdx_eq_prod {l : List α} {i : Nat} :
    (l.zipIdx i).unzip = (l, range' i l.length) := by
  simp only [zipIdx_eq_zip_range', unzip_zip, length_range']
Unzipping Indexed List Yields Original List and Index Range
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$, the unzipping of the list obtained by pairing each element of $l$ with its index starting from $i$ equals the pair $(l, [i, i+1, \dots, i + \mathrm{length}(l) - 1])$. In other words, $\mathrm{unzip}(\mathrm{zipIdx}(l, i)) = (l, \mathrm{range'}(i, \mathrm{length}(l)))$.
List.zipIdx_succ theorem
{l : List α} {i : Nat} : l.zipIdx (i + 1) = (l.zipIdx i).map (fun ⟨a, i⟩ => (a, i + 1))
Full source 
/-- Replace `zipIdx` with a starting index `n+1` with `zipIdx` starting from `n`,
followed by a `map` increasing the indices by one. -/
theorem zipIdx_succ {l : List α} {i : Nat} :
    l.zipIdx (i + 1) = (l.zipIdx i).map (fun ⟨a, i⟩ => (a, i + 1)) := by
  induction l generalizing i with
  | nil => rfl
  | cons _ _ ih => simp only [zipIdx_cons, ih, map_cons]
Index Shift in List Pairing: $\mathrm{zipIdx}(l, i+1) = \mathrm{map}(\lambda (a, j). (a, j+1), \mathrm{zipIdx}(l, i))$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$, the operation of pairing each element of $l$ with its index starting from $i+1$ is equivalent to first pairing the elements with indices starting from $i$ and then incrementing each index by $1$. In other words, $\mathrm{zipIdx}(l, i+1) = \mathrm{map}(\lambda (a, j). (a, j+1), \mathrm{zipIdx}(l, i))$.
List.zipIdx_eq_map_add theorem
{l : List α} {i : Nat} : l.zipIdx i = l.zipIdx.map (fun ⟨a, j⟩ => (a, i + j))
Full source 
/-- Replace `zipIdx` with a starting index with `zipIdx` starting from 0,
followed by a `map` increasing the indices. -/
theorem zipIdx_eq_map_add {l : List α} {i : Nat} :
    l.zipIdx i = l.zipIdx.map (fun ⟨a, j⟩ => (a, i + j)) := by
  induction l generalizing i with
  | nil => rfl
  | cons _ _ ih => simp [ih (i := i + 1), zipIdx_succ, Nat.add_assoc, Nat.add_comm 1]
Index Shift via Addition in List Pairing: $\mathrm{zipIdx}(l, i) = \mathrm{map}(\lambda (a, j). (a, i + j), \mathrm{zipIdx}(l, 0))$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$, the operation of pairing each element of $l$ with its index starting from $i$ is equivalent to pairing the elements with indices starting from $0$ and then adding $i$ to each index. In other words, $\mathrm{zipIdx}(l, i) = \mathrm{map}(\lambda (a, j). (a, i + j), \mathrm{zipIdx}(l, 0))$.
List.enumFrom_eq_nil theorem
{n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = []
Full source 
@[deprecated zipIdx_eq_nil_iff (since := "2025-01-21"), simp]
theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFromList.enumFrom n l = [] ↔ l = [] := by
  cases l <;> simp
Empty Enumeration from Index $n$ iff List is Empty
Informal description
For any natural number $n$ and any list $l$ of elements of type $\alpha$, the enumeration of $l$ starting from index $n$ is the empty list if and only if $l$ itself is the empty list. In other words, $\text{enumFrom}(n, l) = [] \leftrightarrow l = []$.
List.enumFrom_length theorem
: ∀ {n} {l : List α}, (enumFrom n l).length = l.length
Full source 
@[deprecated length_zipIdx (since := "2025-01-21"), simp]
theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
  | _, [] => rfl
  | _, _ :: _ => congrArg Nat.succ enumFrom_length
Length Preservation in List Enumeration from Index $n$
Informal description
For any natural number $n$ and any list $l$ of elements of type $\alpha$, the length of the list obtained by enumerating $l$ starting from index $n$ is equal to the length of $l$. That is, $\text{length}(\text{enumFrom}(n, l)) = \text{length}(l)$.
List.getElem?_enumFrom theorem
: ∀ i (l : List α) j, (enumFrom i l)[j]? = l[j]?.map fun a => (i + j, a)
Full source 
@[deprecated getElem?_zipIdx (since := "2025-01-21"), simp]
theorem getElem?_enumFrom :
    ∀ i (l : List α) j, (enumFrom i l)[j]? = l[j]?.map fun a => (i + j, a)
  | _, [], _ => rfl
  | _, _ :: _, 0 => by simp
  | n, _ :: l, m + 1 => by
    simp only [enumFrom_cons, getElem?_cons_succ]
    exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl
Optional Indexing of Enumerated List via Shifted Index
Informal description
For any natural number $i$, any list $l$ of elements of type $\alpha$, and any natural number $j$, the optional indexing operation on the enumerated list starting from index $i$ satisfies: $$(\text{enumFrom}\ i\ l)[j]? = \text{Option.map}\ (\lambda a \mapsto (i + j, a))\ (l[j]?)$$ where $\text{enumFrom}\ i\ l$ is the list of pairs $(k, x)$ where $k$ ranges from $i$ to $i + \text{length}\ l - 1$ and $x$ is the corresponding element of $l$, and $l[j]?$ is the optional $j$-th element of $l$ (returning $\text{none}$ if $j$ is out of bounds).
List.getElem_enumFrom theorem
(l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) : (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h))
Full source 
@[deprecated getElem_zipIdx (since := "2025-01-21"), simp]
theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) :
    (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h)) := by
  simp only [enumFrom_length] at h
  rw [getElem_eq_getElem?_get]
  simp only [getElem?_enumFrom, getElem?_eq_getElem h]
  simp
Indexed Element of Enumerated List: $(\text{enumFrom}\ n\ l)[i] = (n + i, l[i])$ for Valid Indices
Informal description
For any list $l$ of elements of type $\alpha$, natural number $n$, and index $i$ such that $i < \text{length}(\text{enumFrom}(n, l))$, the $i$-th element of the enumerated list starting from index $n$ is equal to the pair $(n + i, l[i])$, where $l[i]$ is the $i$-th element of $l$.
List.tail_enumFrom theorem
(l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail
Full source 
@[deprecated tail_zipIdx (since := "2025-01-21"), simp]
theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail := by
  induction l generalizing n with
  | nil => simp
  | cons _ l ih => simp [ih, enumFrom_cons]
Tail of Enumerated List Starting from Index $n$ Equals Enumeration of Tail Starting from $n+1$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $n$, the tail of the list obtained by enumerating $l$ starting from index $n$ is equal to the enumeration of the tail of $l$ starting from index $n+1$. In other words, $\text{tail}(\text{enumFrom}(n, l)) = \text{enumFrom}(n+1, \text{tail}(l))$.
List.map_fst_add_enumFrom_eq_enumFrom theorem
(l : List α) (n k : Nat) : map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l
Full source 
@[deprecated map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21"), simp]
theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
    map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl
Shifted Enumeration via Index Addition: $\text{map}\ (+n)\ \text{fst}\ \circ\ \text{enumFrom}\ k = \text{enumFrom}\ (n + k)$
Informal description
For any list $l$ of elements of type $\alpha$ and natural numbers $n$ and $k$, mapping the function $(m, x) \mapsto (m + n, x)$ over the list obtained by enumerating $l$ starting from index $k$ is equal to enumerating $l$ starting from index $n + k$. In other words: $$\text{map}\ (\lambda (m, x) \mapsto (m + n, x))\ (\text{enumFrom}\ k\ l) = \text{enumFrom}\ (n + k)\ l$$ where $\text{enumFrom}\ k\ l$ is the list of pairs $(i, x_i)$ for each element $x_i$ in $l$ with indices $i$ starting from $k$.
List.map_fst_add_enum_eq_enumFrom theorem
(l : List α) (n : Nat) : map (Prod.map (· + n) id) (enum l) = enumFrom n l
Full source 
@[deprecated map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21"), simp]
theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
    map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
  map_fst_add_enumFrom_eq_enumFrom l _ _
Shifted Enumeration via Index Addition: $\text{map}\ (m \mapsto m + n)\ \text{fst}\ \circ\ \text{enum} = \text{enumFrom}\ n$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $n$, mapping the function $(m, x) \mapsto (m + n, x)$ over the enumerated list $\text{enum}\ l$ (which pairs elements with indices starting from 0) yields the same result as enumerating $l$ starting from index $n$. In other words: $$\text{map}\ (\lambda (m, x) \mapsto (m + n, x))\ (\text{enum}\ l) = \text{enumFrom}\ n\ l$$ where $\text{enum}\ l = [(0, x_0), (1, x_1), \dots]$ and $\text{enumFrom}\ n\ l = [(n, x_0), (n+1, x_1), \dots]$.
List.enumFrom_cons' theorem
(n : Nat) (x : α) (xs : List α) : enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id)
Full source 
@[deprecated zipIdx_cons' (since := "2025-01-21"), simp]
theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
    enumFrom n (x :: xs) = (n, x)(n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
Recursive Enumeration of List with Index Shift: $\text{enumFrom } n (x :: xs) = (n, x) :: \text{map } (+1) \text{fst } (\text{enumFrom } n xs)$
Informal description
For any natural number $n$, element $x$ of type $\alpha$, and list $xs$ of type $\text{List }\alpha$, the enumeration of the list $x :: xs$ starting from index $n$ is equal to the pair $(n, x)$ followed by the enumeration of $xs$ starting from index $n$ where each index is incremented by 1. That is, \[ \text{enumFrom } n (x :: xs) = (n, x) :: \text{map } (\lambda (m, y) \mapsto (m + 1, y)) (\text{enumFrom } n xs). \]
List.enumFrom_map_fst theorem
(n) : ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
Full source 
@[deprecated zipIdx_map_snd (since := "2025-01-21"), simp]
theorem enumFrom_map_fst (n) :
    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
  | [] => rfl
  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
First Projection of Enumerated List Equals Arithmetic Sequence
Informal description
For any natural number $n$ and any list $l$ of elements of type $\alpha$, the list obtained by mapping the first projection (index) over the enumerated list starting from $n$ is equal to the arithmetic sequence starting at $n$ with length equal to the length of $l$. More precisely, if we enumerate $l$ starting from index $n$ to get pairs $(i, x_i)$ where $i$ ranges from $n$ to $n + \text{length}(l) - 1$, then extracting just the indices $i$ gives the list $[n, n+1, ..., n + \text{length}(l) - 1]$.
List.enumFrom_map_snd theorem
: ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
Full source 
@[deprecated zipIdx_map_fst (since := "2025-01-21"), simp]
theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
  | _, [] => rfl
  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
Mapping Second Component of Enumerated List Recovers Original List
Informal description
For any natural number $n$ and any list $l$ of elements of type $\alpha$, mapping the second projection function $\text{snd}$ over the enumerated list $\text{enumFrom}\ n\ l$ yields the original list $l$. In other words, $\text{map}\ \text{snd}\ (\text{enumFrom}\ n\ l) = l$.
List.enumFrom_eq_zip_range' theorem
(l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l
Full source 
@[deprecated zipIdx_eq_zip_range' (since := "2025-01-21")]
theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
Enumeration as Zip with Arithmetic Sequence: $\text{enumFrom}\ n\ l = \text{zip}\ (\text{range'}\ n\ (\text{length}\ l))\ l$
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $n$, the enumerated list starting from index $n$ is equal to the zip of the arithmetic sequence starting at $n$ with length equal to the length of $l$ and the list $l$ itself. More precisely, $\text{enumFrom}\ n\ l = \text{zip}\ (\text{range'}\ n\ (\text{length}\ l))\ l$, where $\text{range'}\ n\ k$ generates the list $[n, n+1, \dots, n+k-1]$.
List.unzip_enumFrom_eq_prod theorem
(l : List α) {n : Nat} : (l.enumFrom n).unzip = (range' n l.length, l)
Full source 
@[deprecated unzip_zipIdx_eq_prod (since := "2025-01-21"), simp]
theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
    (l.enumFrom n).unzip = (range' n l.length, l) := by
  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
Unzipping Enumerated List Yields Arithmetic Sequence and Original List
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $n$, the unzipping of the enumerated list starting from index $n$ equals the pair consisting of the arithmetic sequence starting at $n$ with length equal to the length of $l$ and the list $l$ itself. More precisely, $\text{unzip}(\text{enumFrom}\ n\ l) = (\text{range'}\ n\ (\text{length}\ l),\ l)$, where $\text{range'}\ n\ k$ generates the list $[n, n+1, \dots, n+k-1]$.
List.enum_cons theorem
: (a :: as).enum = (0, a) :: as.enumFrom 1
Full source 
@[deprecated zipIdx_cons (since := "2025-01-21")]
theorem enum_cons : (a::as).enum = (0, a)(0, a) :: as.enumFrom 1 := rfl
Enumeration of Cons List: $\text{enum}(a :: as) = (0, a) :: \text{enumFrom}(1, as)$
Informal description
For any element $a$ of type $\alpha$ and any list $as$ of elements of type $\alpha$, the enumeration of the list $a :: as$ is equal to the pair $(0, a)$ followed by the enumeration of $as$ starting from index $1$. In other words, $\text{enum}(a :: as) = (0, a) :: \text{enumFrom}(1, as)$.
List.enum_cons' theorem
(x : α) (xs : List α) : enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id)
Full source 
@[deprecated zipIdx_cons (since := "2025-01-21")]
theorem enum_cons' (x : α) (xs : List α) :
    enum (x :: xs) = (0, x)(0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
  enumFrom_cons' _ _ _
Recursive Enumeration of Cons List with Index Shift: $\text{enum}(x :: xs) = (0, x) :: \text{map}\ (+1)\ \text{fst}\ (\text{enum}\ xs)$
Informal description
For any element $x$ of type $\alpha$ and any list $xs$ of elements of type $\alpha$, the enumeration of the list $x :: xs$ is equal to the pair $(0, x)$ followed by the enumeration of $xs$ where each index is incremented by 1. That is, \[ \text{enum}(x :: xs) = (0, x) :: \text{map}\ (\lambda (i, y) \mapsto (i + 1, y))\ (\text{enum}\ xs). \]
List.enum_eq_enumFrom theorem
{l : List α} : l.enum = l.enumFrom 0
Full source 
@[deprecated "These are now both `l.zipIdx 0`" (since := "2025-01-21")]
theorem enum_eq_enumFrom {l : List α} : l.enum = l.enumFrom 0 := rfl
Equality of List Enumeration Starting from Zero
Informal description
For any list $l$ of elements of type $\alpha$, the enumeration of $l$ starting from index $0$ is equal to the enumeration of $l$ with a custom starting index of $0$. In other words, $\text{enum}(l) = \text{enumFrom}(0, l)$.
List.enumFrom_eq_map_enum theorem
(l : List α) (n : Nat) : enumFrom n l = (enum l).map (Prod.map (· + n) id)
Full source 
@[deprecated "Use the reverse direction of `map_snd_add_zipIdx_eq_zipIdx` instead" (since := "2025-01-21")]
theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
    enumFrom n l = (enum l).map (Prod.map (· + n) id) := by
  induction l generalizing n with
  | nil => simp
  | cons x xs ih =>
    simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
      cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]
    intro a b _
    exact (succ_add a n).symm
Enumeration from Index $n$ as Shifted Enumeration from Zero
Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $n$, the enumeration of $l$ starting from index $n$ is equal to the enumeration of $l$ starting from index $0$ with each index incremented by $n$. That is, \[ \text{enumFrom}\ n\ l = \text{map}\ (\lambda (i, x) \mapsto (i + n, x))\ (\text{enum}\ l). \]