lookmap

@[simp]

theorem List.lookmap_nil {α : Type u_1} (f : α → Option α) : lookmap f [] = []

@[simp]

theorem List.lookmap_cons_none {α : Type u_1} (f : α → Option α) {a : α} (l : List α) (h : f a = none) : lookmap f (a :: l) = a :: lookmap f l

@[simp]

theorem List.lookmap_cons_some {α : Type u_1} (f : α → Option α) {a b : α} (l : List α) (h : f a = some b) : lookmap f (a :: l) = b :: l

theorem List.lookmap_some {α : Type u_1} (l : List α) : lookmap some l = l

theorem List.lookmap_none {α : Type u_1} (l : List α) : lookmap (fun (x : α) => none) l = l

theorem List.lookmap_congr {α : Type u_1} {f g : α → Option α} {l : List α} : (∀ (a : α), a ∈ l → f a = g a) → lookmap f l = lookmap g l

theorem List.lookmap_of_forall_not {α : Type u_1} (f : α → Option α) {l : List α} (H : ∀ (a : α), a ∈ l → f a = none) : lookmap f l = l

theorem List.lookmap_map_eq {α : Type u_1} {β : Type u_2} (f : α → Option α) (g : α → β) (h : ∀ (a b : α), b ∈ f a → g a = g b) (l : List α) : map g (lookmap f l) = map g l

theorem List.lookmap_id' {α : Type u_1} (f : α → Option α) (h : ∀ (a b : α), b ∈ f a → a = b) (l : List α) : lookmap f l = l

theorem List.length_lookmap {α : Type u_1} (f : α → Option α) (l : List α) : (lookmap f l).length = l.length

theorem List.perm_lookmap {α : Type u_1} (f : α → Option α) {l₁ l₂ : List α} (H : Pairwise (fun (a b : α) => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁) (p : l₁.Perm l₂) : (lookmap f l₁).Perm (lookmap f l₂)