Bootstrapping properties of Lists

theorem List.ext {α : Type u_1} {l₁ : List α} {l₂ : List α} : (∀ (n : Nat), List.get? l₁ n = List.get? l₂ n) → l₁ = l₂

theorem List.ext_get {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : List.length l₁ = List.length l₂) (h : ∀ (n : Nat) (h₁ : n < List.length l₁) (h₂ : n < List.length l₂), List.get l₁ { val := n, isLt := h₁ } = List.get l₂ { val := n, isLt := h₂ }) : l₁ = l₂

@[simp]

theorem List.get_map {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Fin (List.length (List.map f l))} : List.get (List.map f l) n = f (List.get l { val := ↑n, isLt := ⋯ })

foldl / foldr

theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) : List.foldl g init (List.map f l) = List.foldl (fun (x : α) (y : β₁) => g x (f y)) init l

theorem List.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) : List.foldr g init (List.map f l) = List.foldr (fun (x : α₁) (y : β) => g (f x) y) init l