@[simp]

theorem Option.mem_toList {α : Type u_1} {a : α} {o : Option α} : a ∈ o.toList ↔ o = some a

@[simp]

theorem Option.forIn'_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) : forIn' o.toList b f = forIn' o b fun (a : α) (m : a ∈ o) (b : β) => f a ⋯ b

@[simp]

theorem Option.forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) : forIn o.toList b f = forIn o b f

@[simp]

theorem Option.foldlM_toList {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) : List.foldlM f a o.toList = o.elim (pure a) fun (b : β) => f a b

@[simp]

theorem Option.foldrM_toList {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) : List.foldrM f a o.toList = o.elim (pure a) fun (b : β) => f b a

@[simp]

theorem Option.foldl_toList {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : α → β → α) : List.foldl f a o.toList = o.elim a fun (b : β) => f a b

@[simp]

theorem Option.foldr_toList {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : β → α → α) : List.foldr f a o.toList = o.elim a fun (b : β) => f b a

@[simp]

theorem Option.pairwise_toList {α : Type u_1} {P : α → α → Prop} {o : Option α} : List.Pairwise P o.toList

@[simp]

theorem Option.head?_toList {α : Type u_1} {o : Option α} : o.toList.head? = o

theorem Option.toList_filter {α : Type u_1} {o : Option α} {p : α → Bool} : (Option.filter p o).toList = List.filter p o.toList

theorem Option.toList_bind {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} : (o.bind f).toList = List.flatMap (toList ∘ f) o.toList

theorem Option.toList_join {α : Type u_1} {o : Option (Option α)} : o.join.toList = List.flatMap toList o.toList

theorem Option.toList_map {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → β} : (Option.map f o).toList = List.map f o.toList

theorem Option.toList_min {α : Type u_1} [Min α] {o o' : Option α} : (min o o').toList = List.zipWith min o.toList o'.toList

@[simp]

theorem Option.length_toList_le {α : Type u_1} {o : Option α} : o.toList.length ≤ 1

theorem Option.length_toList {α : Type u_1} {o : Option α} : o.toList.length = if o.isSome = true then 1 else 0

@[simp]

theorem Option.toList_eq_nil_iff {α : Type u_1} {o : Option α} : o.toList = [] ↔ o = none

@[simp]

theorem Option.toList_eq_singleton_iff {α : Type u_1} {a : α} {o : Option α} : o.toList = [a] ↔ o = some a

theorem Option.length_toList_eq_zero_iff {α : Type u_1} {o : Option α} : o.toList.length = 0 ↔ o = none

@[simp]

theorem Option.length_toList_eq_one_iff {α : Type u_1} {o : Option α} : o.toList.length = 1 ↔ o.isSome = true

theorem Option.length_toList_choice_eq_one {α : Type u_1} [Nonempty α] : (choice α).toList.length = 1