Properties of List.enum

@[simp]

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

@[deprecated List.get?_enumFrom]

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

Alias of List.get?_enumFrom.

@[simp]

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

@[deprecated List.get?_enum]

theorem List.enum_get? {α : Type u_1} (l : List α) (n : ℕ) : List.get? (List.enum l) n = Option.map (fun (a : α) => (n, a)) (List.get? l 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 (List.enum l) = l

@[simp]

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

@[simp]

theorem List.get_enum {α : Type u_1} (l : List α) (i : Fin (List.length (List.enum l))) : List.get (List.enum l) i = (↑i, List.get l (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 ↔ List.get? l 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 ∧ List.get? l (i - n) = some x

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

theorem List.mem_enum_iff_get? {α : Type u_1} {x : ℕ × α} {l : List α} : x ∈ List.enum l ↔ List.get? l 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 + List.length l

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

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 ∈ List.enum l) : 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 + List.length xs ∧ x ∈ xs

@[simp]

theorem List.enum_nil {α : Type u_1} : List.enum [] = []

@[simp]

theorem List.enum_cons {α : Type u_1} (x : α) (xs : List α) : List.enum (x :: xs) = (0, x) :: List.enumFrom 1 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 : α) : List.enum [x] = [(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 + List.length xs) ys

theorem List.enum_append {α : Type u_1} (xs : List α) (ys : List α) : List.enum (xs ++ ys) = List.enum xs ++ List.enumFrom (List.length xs) 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) (List.enum l) = 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 α) : List.enum (x :: xs) = (0, x) :: List.map (Prod.map Nat.succ id) (List.enum xs)

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.enum (List.map f l) = List.map (Prod.map id f) (List.enum l)

@[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 α} : List.enum l = [] ↔ l = []