theorem Option.mem_iff {α : Type u_1} {a : α} {b : Option α} : a ∈ b ↔ b = some a

theorem Option.some_ne_none {α : Type u_1} (x : α) : some x ≠ none

theorem Option.forall {α : Type u_1} {p : Option α → Prop} : (∀ (x : Option α), p x) ↔ p none ∧ ∀ (x : α), p (some x)

theorem Option.exists {α : Type u_1} {p : Option α → Prop} : (∃ (x : Option α), p x) ↔ p none ∨ ∃ (x : α), p (some x)

theorem Option.get_mem {α : Type u_1} {o : Option α} (h : o.isSome = true) : o.get h ∈ o

theorem Option.get_of_mem {α : Type u_1} {a : α} {o : Option α} (h : o.isSome = true) : a ∈ o → o.get h = a

theorem Option.not_mem_none {α : Type u_1} (a : α) : ¬a ∈ none

@[simp]

theorem Option.some_get {α : Type u_1} {x : Option α} (h : x.isSome = true) : some (x.get h) = x

@[simp]

theorem Option.get_some {α : Type u_1} (x : α) (h : (some x).isSome = true) : (some x).get h = x

theorem Option.getD_of_ne_none {α : Type u_1} {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x

theorem Option.getD_eq_iff {α : Type u_1} {o : Option α} {a : α} {b : α} : o.getD a = b ↔ o = some b ∨ o = none ∧ a = b

@[simp]

theorem Option.get!_none {α : Type u_1} [Inhabited α] : none.get! = default

@[simp]

theorem Option.get!_some {α : Type u_1} [Inhabited α] {a : α} : (some a).get! = a

theorem Option.get_eq_get! {α : Type u_1} [Inhabited α] (o : Option α) {h : o.isSome = true} : o.get h = o.get!

theorem Option.get_eq_getD {α : Type u_1} {fallback : α} (o : Option α) {h : o.isSome = true} : o.get h = o.getD fallback

theorem Option.some_get! {α : Type u_1} [Inhabited α] (o : Option α) : o.isSome = true → some o.get! = o

theorem Option.get!_eq_getD_default {α : Type u_1} [Inhabited α] (o : Option α) : o.get! = o.getD default

theorem Option.mem_unique {α : Type u_1} {o : Option α} {a : α} {b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b

theorem Option.ext_iff {α : Type u_1} {o₁ : Option α} {o₂ : Option α} : o₁ = o₂ ↔ ∀ (a : α), a ∈ o₁ ↔ a ∈ o₂

theorem Option.ext {α : Type u_1} {o₁ : Option α} {o₂ : Option α} : (∀ (a : α), a ∈ o₁ ↔ a ∈ o₂) → o₁ = o₂

theorem Option.eq_none_iff_forall_not_mem : ∀ {α : Type u_1} {o : Option α}, o = none ↔ ∀ (a : α), ¬a ∈ o

@[simp]

theorem Option.isSome_none {α : Type u_1} : none.isSome = false

@[simp]

theorem Option.isSome_some : ∀ {α : Type u_1} {a : α}, (some a).isSome = true

theorem Option.isSome_iff_exists : ∀ {α : Type u_1} {x : Option α}, x.isSome = true ↔ ∃ (a : α), x = some a

@[simp]

theorem Option.isNone_none {α : Type u_1} : none.isNone = true

@[simp]

theorem Option.isNone_some : ∀ {α : Type u_1} {a : α}, (some a).isNone = false

@[simp]

theorem Option.not_isSome : ∀ {α : Type u_1} {a : Option α}, a.isSome = false ↔ a.isNone = true

theorem Option.eq_some_iff_get_eq : ∀ {α : Type u_1} {o : Option α} {a : α}, o = some a ↔ ∃ (h : o.isSome = true), o.get h = a

theorem Option.eq_some_of_isSome {α : Type u_1} {o : Option α} (h : o.isSome = true) : o = some (o.get h)

theorem Option.isSome_iff_ne_none : ∀ {α : Type u_1} {o : Option α}, o.isSome = true ↔ o ≠ none

theorem Option.not_isSome_iff_eq_none : ∀ {α : Type u_1} {o : Option α}, ¬o.isSome = true ↔ o = none

theorem Option.ne_none_iff_isSome : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ o.isSome = true

theorem Option.ne_none_iff_exists : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ (x : α), some x = o

theorem Option.ne_none_iff_exists' : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ (x : α), o = some x

theorem Option.bex_ne_none {α : Type u_1} {p : Option α → Prop} : (∃ (x : Option α), ∃ (x_1 : x ≠ none), p x) ↔ ∃ (x : α), p (some x)

theorem Option.ball_ne_none {α : Type u_1} {p : Option α → Prop} : (∀ (x : Option α), x ≠ none → p x) ↔ ∀ (x : α), p (some x)

@[simp]

theorem Option.pure_def {α : Type u_1} : pure = some

@[simp]

theorem Option.bind_eq_bind {α : Type u_1} {β : Type u_1} : bind = Option.bind

@[simp]

theorem Option.bind_some {α : Type u_1} (x : Option α) : x.bind some = x

@[simp]

theorem Option.bind_none {α : Type u_1} {β : Type u_2} (x : Option α) : (x.bind fun (x : α) => none) = none

theorem Option.bind_eq_some : ∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1 → Option α}, x.bind f = some b ↔ ∃ (a : α_1), x = some a ∧ f a = some b

@[simp]

theorem Option.bind_eq_none {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} : o.bind f = none ↔ ∀ (a : α), o = some a → f a = none

theorem Option.bind_eq_none' {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} : o.bind f = none ↔ ∀ (b : β) (a : α), a ∈ o → ¬b ∈ f a

theorem Option.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → Option γ} (a : Option α) (b : Option β) : (a.bind fun (x : α) => b.bind (f x)) = b.bind fun (y : β) => a.bind fun (x : α) => f x y

theorem Option.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Option α) (f : α → Option β) (g : β → Option γ) : (x.bind f).bind g = x.bind fun (y : α) => (f y).bind g

theorem Option.join_eq_some : ∀ {α : Type u_1} {a : α} {x : Option (Option α)}, x.join = some a ↔ x = some (some a)

theorem Option.join_ne_none : ∀ {α : Type u_1} {x : Option (Option α)}, x.join ≠ none ↔ ∃ (z : α), x = some (some z)

theorem Option.join_ne_none' : ∀ {α : Type u_1} {x : Option (Option α)}, ¬x.join = none ↔ ∃ (z : α), x = some (some z)

theorem Option.join_eq_none : ∀ {α : Type u_1} {o : Option (Option α)}, o.join = none ↔ o = none ∨ o = some none

theorem Option.bind_id_eq_join {α : Type u_1} {x : Option (Option α)} : x.bind id = x.join

@[simp]

theorem Option.map_eq_map : ∀ {α α_1 : Type u_1} {f : α → α_1}, Functor.map f = Option.map f

theorem Option.map_none : ∀ {α α_1 : Type u_1} {f : α → α_1}, f <$> none = none

theorem Option.map_some : ∀ {α α_1 : Type u_1} {f : α → α_1} {a : α}, f <$> some a = some (f a)

@[simp]

theorem Option.map_eq_some' : ∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1 → α}, Option.map f x = some b ↔ ∃ (a : α_1), x = some a ∧ f a = b

theorem Option.map_eq_some : ∀ {α α_1 : Type u_1} {f : α → α_1} {x : Option α} {b : α_1}, f <$> x = some b ↔ ∃ (a : α), x = some a ∧ f a = b

@[simp]

theorem Option.map_eq_none' : ∀ {α : Type u_1} {x : Option α} {α_1 : Type u_2} {f : α → α_1}, Option.map f x = none ↔ x = none

theorem Option.isSome_map {α : Type u_1} : ∀ {α_1 : Type u_1} {f : α → α_1} {x : Option α}, (f <$> x).isSome = x.isSome

@[simp]

theorem Option.isSome_map' {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α_1} {x : Option α}, (Option.map f x).isSome = x.isSome

@[simp]

theorem Option.isNone_map' {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α_1} {x : Option α}, (Option.map f x).isNone = x.isNone

theorem Option.map_eq_none : ∀ {α α_1 : Type u_1} {f : α → α_1} {x : Option α}, f <$> x = none ↔ x = none

theorem Option.map_eq_bind {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α_1} {x : Option α}, Option.map f x = x.bind (some ∘ f)

theorem Option.map_congr {α : Type u_1} : ∀ {α_1 : Type u_2} {f g : α → α_1} {x : Option α}, (∀ (a : α), a ∈ x → f a = g a) → Option.map f x = Option.map g x

@[simp]

theorem Option.map_id_fun {α : Type u} : Option.map id = id

theorem Option.map_id' {α : Type u_1} {x : Option α} : Option.map (fun (a : α) => a) x = x

@[simp]

theorem Option.map_id_fun' {α : Type u} : (Option.map fun (a : α) => a) = id

theorem Option.get_map {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {h : (Option.map f o).isSome = true} : (Option.map f o).get h = f (o.get ⋯)

@[simp]

theorem Option.map_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : β → γ) (g : α → β) (x : Option α) : Option.map h (Option.map g x) = Option.map (h ∘ g) x

theorem Option.comp_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : β → γ) (g : α → β) (x : Option α) : Option.map (h ∘ g) x = Option.map h (Option.map g x)

@[simp]

theorem Option.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) : Option.map g ∘ Option.map f = Option.map (g ∘ f)

theorem Option.mem_map_of_mem {α : Type u_1} {β : Type u_2} {x : Option α} {a : α} (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x

@[simp]

theorem Option.map_if {α : Type u_1} {β : Type u_2} {c : Prop} {a : α} {f : α → β} [Decidable c] : Option.map f (if c then some a else none) = if c then some (f a) else none

@[simp]

theorem Option.map_dif {α : Type u_1} {β : Type u_2} {c : Prop} {f : α → β} [Decidable c] {a : c → α} : Option.map f (if h : c then some (a h) else none) = if h : c then some (f (a h)) else none

@[simp]

theorem Option.filter_none {α : Type u_1} (p : α → Bool) : Option.filter p none = none

theorem Option.filter_some : ∀ {α : Type u_1} {p : α → Bool} {a : α}, Option.filter p (some a) = if p a = true then some a else none

@[simp]

theorem Option.all_guard {α : Type u_1} {q : α → Bool} (p : α → Prop) [DecidablePred p] (a : α) : Option.all q (Option.guard p a) = (!decide (p a) || q a)

@[simp]

theorem Option.any_guard {α : Type u_1} {q : α → Bool} (p : α → Prop) [DecidablePred p] (a : α) : Option.any q (Option.guard p a) = (decide (p a) && q a)

theorem Option.bind_map_comm {α : Type u_1} {β : Type u_2} {x : Option (Option α)} {f : α → β} : x.bind (Option.map f) = (Option.map (Option.map f) x).bind id

theorem Option.join_map_eq_map_join {α : Type u_1} {β : Type u_2} {f : α → β} {x : Option (Option α)} : (Option.map (Option.map f) x).join = Option.map f x.join

theorem Option.join_join {α : Type u_1} {x : Option (Option (Option α))} : x.join.join = (Option.map Option.join x).join

theorem Option.mem_of_mem_join {α : Type u_1} {a : α} {x : Option (Option α)} (h : a ∈ x.join) : some a ∈ x

@[simp]

theorem Option.some_orElse {α : Type u_1} (a : α) (x : Option α) : (HOrElse.hOrElse (some a) fun (x_1 : Unit) => x) = some a

@[simp]

theorem Option.none_orElse {α : Type u_1} (x : Option α) : (HOrElse.hOrElse none fun (x_1 : Unit) => x) = x

@[simp]

theorem Option.orElse_none {α : Type u_1} (x : Option α) : (HOrElse.hOrElse x fun (x : Unit) => none) = x

theorem Option.map_orElse {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α_1} {x y : Option α}, Option.map f (HOrElse.hOrElse x fun (x : Unit) => y) = HOrElse.hOrElse (Option.map f x) fun (x : Unit) => Option.map f y

@[simp]

theorem Option.guard_eq_some : ∀ {α : Type u_1} {p : α → Prop} {a b : α} [inst : DecidablePred p], Option.guard p a = some b ↔ a = b ∧ p a

@[simp]

theorem Option.guard_isSome : ∀ {α : Type u_1} {p : α → Prop} {a : α} [inst : DecidablePred p], (Option.guard p a).isSome = true ↔ p a

@[simp]

theorem Option.guard_eq_none : ∀ {α : Type u_1} {p : α → Prop} {a : α} [inst : DecidablePred p], Option.guard p a = none ↔ ¬p a

@[simp]

theorem Option.guard_pos : ∀ {α : Type u_1} {p : α → Prop} {a : α} [inst : DecidablePred p], p a → Option.guard p a = some a

theorem Option.liftOrGet_eq_or_eq {α : Type u_1} {f : α → α → α} (h : ∀ (a b : α), f a b = a ∨ f a b = b) (o₁ : Option α) (o₂ : Option α) : Option.liftOrGet f o₁ o₂ = o₁ ∨ Option.liftOrGet f o₁ o₂ = o₂

@[simp]

theorem Option.liftOrGet_none_left {α : Type u_1} {f : α → α → α} {b : Option α} : Option.liftOrGet f none b = b

@[simp]

theorem Option.liftOrGet_none_right {α : Type u_1} {f : α → α → α} {a : Option α} : Option.liftOrGet f a none = a

@[simp]

theorem Option.liftOrGet_some_some {α : Type u_1} {f : α → α → α} {a : α} {b : α} : Option.liftOrGet f (some a) (some b) = some (f a b)

@[simp]

theorem Option.elim_none {β : Sort u_1} {α : Type u_2} (x : β) (f : α → β) : none.elim x f = x

@[simp]

theorem Option.elim_some {β : Sort u_1} {α : Type u_2} (x : β) (f : α → β) (a : α) : (some a).elim x f = f a

@[simp]

theorem Option.getD_map {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (o : Option α) : (Option.map f o).getD (f x) = f (o.getD x)

noncomputable def Option.choice (α : Type u_1) : Option α

An arbitrary some a with a : α if α is nonempty, and otherwise none.

Equations

• Option.choice α = if h : Nonempty α then some (Classical.choice h) else none

theorem Option.choice_eq {α : Type u_1} [Subsingleton α] (a : α) : Option.choice α = some a

theorem Option.choice_isSome_iff_nonempty {α : Type u_1} : (Option.choice α).isSome = true ↔ Nonempty α

@[simp]

theorem Option.toList_some {α : Type u_1} (a : α) : (some a).toList = [a]

@[simp]

theorem Option.toList_none (α : Type u_1) : none.toList = []

@[simp]

theorem Option.or_some : ∀ {α : Type u_1} {a : α} {o : Option α}, (some a).or o = some a

@[simp]

theorem Option.none_or : ∀ {α : Type u_1} {o : Option α}, none.or o = o

theorem Option.or_eq_bif : ∀ {α : Type u_1} {o o' : Option α}, o.or o' = bif o.isSome then o else o'

@[simp]

theorem Option.isSome_or : ∀ {α : Type u_1} {o o' : Option α}, (o.or o').isSome = (o.isSome || o'.isSome)

@[simp]

theorem Option.isNone_or : ∀ {α : Type u_1} {o o' : Option α}, (o.or o').isNone = (o.isNone && o'.isNone)

@[simp]

theorem Option.or_eq_none : ∀ {α : Type u_1} {o o' : Option α}, o.or o' = none ↔ o = none ∧ o' = none

@[simp]

theorem Option.or_eq_some : ∀ {α : Type u_1} {o o' : Option α} {a : α}, o.or o' = some a ↔ o = some a ∨ o = none ∧ o' = some a

theorem Option.or_assoc : ∀ {α : Type u_1} {o₁ o₂ o₃ : Option α}, (o₁.or o₂).or o₃ = o₁.or (o₂.or o₃)

instance Option.instAssociativeOr {α : Type u_1} : Std.Associative Option.or

Equations

• ⋯ = ⋯

@[simp]

theorem Option.or_none : ∀ {α : Type u_1} {o : Option α}, o.or none = o

instance Option.instLawfulIdentityOrNone {α : Type u_1} : Std.LawfulIdentity Option.or none

Equations

• ⋯ = ⋯

@[simp]

theorem Option.or_self : ∀ {α : Type u_1} {o : Option α}, o.or o = o

instance Option.instIdempotentOpOr {α : Type u_1} : Std.IdempotentOp Option.or

Equations

• ⋯ = ⋯

theorem Option.or_eq_orElse : ∀ {α : Type u_1} {o o' : Option α}, o.or o' = o.orElse fun (x : Unit) => o'

theorem Option.map_or : ∀ {α α_1 : Type u_1} {f : α → α_1} {o o' : Option α}, f <$> o.or o' = (f <$> o).or (f <$> o')

theorem Option.map_or' : ∀ {α : Type u_1} {o o' : Option α} {α_1 : Type u_2} {f : α → α_1}, Option.map f (o.or o') = (Option.map f o).or (Option.map f o')

theorem Option.or_of_isSome {α : Type u_1} {o : Option α} {o' : Option α} (h : o.isSome = true) : o.or o' = o

theorem Option.or_of_isNone {α : Type u_1} {o : Option α} {o' : Option α} (h : o.isNone = true) : o.or o' = o'

@[simp]

theorem Option.isSome_dite {β : Type u_1} {p : Prop} [Decidable p] {b : p → β} : (if h : p then some (b h) else none).isSome = true ↔ p

@[simp]

theorem Option.isSome_ite : ∀ {α : Type u_1} {b : α} {p : Prop} [inst : Decidable p], (if p then some b else none).isSome = true ↔ p

@[simp]

theorem Option.isSome_dite' {β : Type u_1} {p : Prop} [Decidable p] {b : ¬p → β} : (if h : p then none else some (b h)).isSome = true ↔ ¬p

@[simp]

theorem Option.isSome_ite' : ∀ {α : Type u_1} {b : α} {p : Prop} [inst : Decidable p], (if p then none else some b).isSome = true ↔ ¬p

@[simp]

theorem Option.get_dite {β : Type u_1} {p : Prop} [Decidable p] (b : p → β) (w : (if h : p then some (b h) else none).isSome = true) : (if h : p then some (b h) else none).get w = b ⋯

@[simp]

theorem Option.get_ite : ∀ {α : Type u_1} {b : α} {p : Prop} [inst : Decidable p] (h : (if p then some b else none).isSome = true), (if p then some b else none).get h = b

@[simp]

theorem Option.get_dite' {β : Type u_1} {p : Prop} [Decidable p] (b : ¬p → β) (w : (if h : p then none else some (b h)).isSome = true) : (if h : p then none else some (b h)).get w = b ⋯

@[simp]

theorem Option.get_ite' : ∀ {α : Type u_1} {b : α} {p : Prop} [inst : Decidable p] (h : (if p then none else some b).isSome = true), (if p then none else some b).get h = b