Properties of List.enum

@[simp]

theorem List.getElem?_enumFrom {α : Type u_1} (n : ℕ) (l : List α) (m : ℕ) : (List.enumFrom n l)[m]? = Option.map (fun (a : α) => (n + m, a)) l[m]?

theorem List.get?_enumFrom {α : Type u_1} (n : ℕ) (l : List α) (m : ℕ) : (List.enumFrom n l).get? m = Option.map (fun (a : α) => (n + m, a)) (l.get? m)

@[deprecated List.get?_enumFrom]

theorem List.enumFrom_get? {α : Type u_1} (n : ℕ) (l : List α) (m : ℕ) : (List.enumFrom n l).get? m = Option.map (fun (a : α) => (n + m, a)) (l.get? m)

Alias of List.get?_enumFrom.

@[simp]

theorem List.getElem?_enum {α : Type u_1} (l : List α) (n : ℕ) : l.enum[n]? = Option.map (fun (a : α) => (n, a)) l[n]?

theorem List.get?_enum {α : Type u_1} (l : List α) (n : ℕ) : l.enum.get? n = Option.map (fun (a : α) => (n, a)) (l.get? n)

@[deprecated List.get?_enum]

theorem List.enum_get? {α : Type u_1} (l : List α) (n : ℕ) : l.enum.get? n = Option.map (fun (a : α) => (n, a)) (l.get? n)

Alias of List.get?_enum.

@[simp]

theorem List.enumFrom_map_snd {α : Type u_1} (n : ℕ) (l : List α) : List.map Prod.snd (List.enumFrom n l) = l

@[simp]

theorem List.enum_map_snd {α : Type u_1} (l : List α) : List.map Prod.snd l.enum = l

@[simp]

theorem List.getElem_enumFrom {α : Type u_1} (l : List α) (n : ℕ) (i : ℕ) (h : i < (List.enumFrom n l).length) : (List.enumFrom n l)[i] = (n + i, l[i])

theorem List.get_enumFrom {α : Type u_1} (l : List α) (n : ℕ) (i : Fin (List.enumFrom n l).length) : (List.enumFrom n l).get i = (n + ↑i, l.get (Fin.cast ⋯ i))

@[simp]

theorem List.getElem_enum {α : Type u_1} (l : List α) (i : ℕ) (h : i < l.enum.length) : l.enum[i] = (i, l[i])

theorem List.get_enum {α : Type u_1} (l : List α) (i : Fin l.enum.length) : l.enum.get i = (↑i, l.get (Fin.cast ⋯ i))

theorem List.mk_add_mem_enumFrom_iff_get? {α : Type u_1} {n : ℕ} {i : ℕ} {x : α} {l : List α} : (n + i, x) ∈ List.enumFrom n l ↔ l.get? i = some x

theorem List.mk_mem_enumFrom_iff_le_and_get?_sub {α : Type u_1} {n : ℕ} {i : ℕ} {x : α} {l : List α} : (i, x) ∈ List.enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = some x

theorem List.mk_mem_enum_iff_get? {α : Type u_1} {i : ℕ} {x : α} {l : List α} : (i, x) ∈ l.enum ↔ l.get? i = some x

theorem List.mem_enum_iff_get? {α : Type u_1} {x : ℕ × α} {l : List α} : x ∈ l.enum ↔ l.get? x.1 = some x.2

theorem List.le_fst_of_mem_enumFrom {α : Type u_1} {x : ℕ × α} {n : ℕ} {l : List α} (h : x ∈ List.enumFrom n l) : n ≤ x.1

theorem List.fst_lt_add_of_mem_enumFrom {α : Type u_1} {x : ℕ × α} {n : ℕ} {l : List α} (h : x ∈ List.enumFrom n l) : x.1 < n + l.length

theorem List.fst_lt_of_mem_enum {α : Type u_1} {x : ℕ × α} {l : List α} (h : x ∈ l.enum) : x.1 < l.length

theorem List.snd_mem_of_mem_enumFrom {α : Type u_1} {x : ℕ × α} {n : ℕ} {l : List α} (h : x ∈ List.enumFrom n l) : x.2 ∈ l

theorem List.snd_mem_of_mem_enum {α : Type u_1} {x : ℕ × α} {l : List α} (h : x ∈ l.enum) : x.2 ∈ l

theorem List.mem_enumFrom {α : Type u_1} {x : α} {i : ℕ} {j : ℕ} (xs : List α) (h : (i, x) ∈ List.enumFrom j xs) : j ≤ i ∧ i < j + xs.length ∧ x ∈ xs

@[simp]

theorem List.enumFrom_singleton {α : Type u_1} (x : α) (n : ℕ) : List.enumFrom n [x] = [(n, x)]

@[simp]

theorem List.enum_singleton {α : Type u_1} (x : α) : [x].enum = [(0, x)]

theorem List.enumFrom_append {α : Type u_1} (xs : List α) (ys : List α) (n : ℕ) : List.enumFrom n (xs ++ ys) = List.enumFrom n xs ++ List.enumFrom (n + xs.length) ys

theorem List.enum_append {α : Type u_1} (xs : List α) (ys : List α) : (xs ++ ys).enum = xs.enum ++ List.enumFrom xs.length ys

theorem List.map_fst_add_enumFrom_eq_enumFrom {α : Type u_1} (l : List α) (n : ℕ) (k : ℕ) : List.map (Prod.map (fun (x : ℕ) => x + n) id) (List.enumFrom k l) = List.enumFrom (n + k) l

theorem List.map_fst_add_enum_eq_enumFrom {α : Type u_1} (l : List α) (n : ℕ) : List.map (Prod.map (fun (x : ℕ) => x + n) id) l.enum = List.enumFrom n l

theorem List.enumFrom_cons' {α : Type u_1} (n : ℕ) (x : α) (xs : List α) : List.enumFrom n (x :: xs) = (n, x) :: List.map (Prod.map Nat.succ id) (List.enumFrom n xs)

theorem List.enum_cons' {α : Type u_1} (x : α) (xs : List α) : (x :: xs).enum = (0, x) :: List.map (Prod.map Nat.succ id) xs.enum

theorem List.enumFrom_map {α : Type u_1} {β : Type u_2} (n : ℕ) (l : List α) (f : α → β) : List.enumFrom n (List.map f l) = List.map (Prod.map id f) (List.enumFrom n l)

theorem List.enum_map {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) : (List.map f l).enum = List.map (Prod.map id f) l.enum

@[simp]

theorem List.enumFrom_eq_nil {α : Type u_1} {n : ℕ} {l : List α} : List.enumFrom n l = [] ↔ l = []

@[simp]

theorem List.enum_eq_nil {α : Type u_1} {l : List α} : l.enum = [] ↔ l = []