@[simp]

theorem Option.mem_toArray {α : Type u_1} {a : α} {o : Option α} : a ∈ o.toArray ↔ o = some a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Option.foldl_toArray {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : α → β → α) : Array.foldl f a o.toArray = o.elim a fun (b : β) => f a b

@[simp]

theorem Option.foldr_toArray {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : β → α → α) : Array.foldr f a o.toArray = o.elim a fun (b : β) => f b a

@[simp]

theorem Option.toList_toArray {α : Type u_1} {o : Option α} : o.toArray.toList = o.toList

@[simp]

theorem Option.toArray_toList {α : Type u_1} {o : Option α} : o.toList.toArray = o.toArray

theorem Option.toArray_filter {α : Type u_1} {o : Option α} {p : α → Bool} : (Option.filter p o).toArray = Array.filter p o.toArray

theorem Option.toArray_bind {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} : (o.bind f).toArray = Array.flatMap (toArray ∘ f) o.toArray

theorem Option.toArray_join {α : Type u_1} {o : Option (Option α)} : o.join.toArray = Array.flatMap toArray o.toArray

theorem Option.toArray_map {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → β} : (Option.map f o).toArray = Array.map f o.toArray

theorem Option.toArray_min {α : Type u_1} [Min α] {o o' : Option α} : (min o o').toArray = Array.zipWith min o.toArray o'.toArray

@[simp]

theorem Option.size_toArray_le {α : Type u_1} {o : Option α} : o.toArray.size ≤ 1

theorem Option.size_toArray {α : Type u_1} {o : Option α} : o.toArray.size = if o.isSome = true then 1 else 0

@[simp]

theorem Option.toArray_eq_empty_iff {α : Type u_1} {o : Option α} : o.toArray = #[] ↔ o = none

@[simp]

theorem Option.toArray_eq_singleton_iff {α : Type u_1} {a : α} {o : Option α} : o.toArray = #[a] ↔ o = some a

theorem Option.size_toArray_eq_zero_iff {α : Type u_1} {o : Option α} : o.toArray.size = 0 ↔ o = none

@[simp]

theorem Option.size_toArray_eq_one_iff {α : Type u_1} {o : Option α} : o.toArray.size = 1 ↔ o.isSome = true

theorem Option.size_toArray_choice_eq_one {α : Type u_1} [Nonempty α] : (choice α).toArray.size = 1