Option of a type

This file develops the basic theory of option types.

If α is a type, then Option α can be understood as the type with one more element than α. Option α has terms some a, where a : α, and none, which is the added element. This is useful in multiple ways:

• It is the prototype of addition of terms to a type. See for example WithBot α which uses none as an element smaller than all others.
• It can be used to define failsafe partial functions, which return some the_result_we_expect if we can find the_result_we_expect, and none if there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it return none.
• Option is a monad. We love monads.

Part is an alternative to Option that can be seen as the type of True/False values along with a term a : α if the value is True.

theorem Option.coe_def {α : Type u_1} : (fun (a : α) => some a) = some

theorem Option.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} {o : Option α} : y ∈ Option.map f o ↔ ∃ x ∈ o, f x = y

@[simp]

theorem Option.mem_map_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (H : Function.Injective f) {a : α} {o : Option α} : f a ∈ Option.map f o ↔ a ∈ o

theorem Option.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {p : β → Prop} : (∀ y ∈ Option.map f o, p y) ↔ ∀ x ∈ o, p (f x)

theorem Option.exists_mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {p : β → Prop} : (∃ y ∈ Option.map f o, p y) ↔ ∃ x ∈ o, p (f x)

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

theorem Option.eq_of_mem_of_mem {α : Type u_1} {a : α} {o1 o2 : Option α} (h1 : a ∈ o1) (h2 : a ∈ o2) : o1 = o2

theorem Option.Mem.leftUnique {α : Type u_1} : Relator.LeftUnique fun (x1 : α) (x2 : Option α) => x1 ∈ x2

theorem Option.some_injective (α : Type u_5) : Function.Injective some

@[simp]

theorem Option.map_comp_some {α : Type u_1} {β : Type u_2} (f : α → β) : Option.map f ∘ some = some ∘ f

theorem Option.bind_congr' {α : Type u_1} {β : Type u_2} {f g : α → Option β} {x y : Option α} (hx : x = y) (hf : ∀ a ∈ y, f a = g a) : x.bind f = y.bind g

theorem Option.joinM_eq_join {α : Type u_1} : joinM = join

theorem Option.bind_eq_bind' {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f

theorem Option.map_coe {α β : Type u_5} {a : α} {f : α → β} : f <$> some a = some (f a)

@[simp]

theorem Option.map_coe' {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} : Option.map f (some a) = some (f a)

theorem Option.map_injective' {α : Type u_1} {β : Type u_2} : Function.Injective Option.map

Option.map as a function between functions is injective.

@[simp]

theorem Option.map_inj {α : Type u_1} {β : Type u_2} {f g : α → β} : Option.map f = Option.map g ↔ f = g

@[simp]

theorem Option.map_eq_id {α : Type u_1} {f : α → α} : Option.map f = id ↔ f = id

theorem Option.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) : Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))

theorem Option.mem_pmem {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (x : Option α) {a : α} (h : ∀ a ∈ x, p a) (ha : a ∈ x) : f a ⋯ ∈ pmap f x h

theorem Option.pmap_bind {α β γ : Type u_5} {x : Option α} {g : α → Option β} {p : β → Prop} {f : (b : β) → p b → γ} (H : ∀ (a : β), x >>= g = some a → p a) (H' : ∀ (a : α), ∀ b ∈ g a, b ∈ x >>= g) : pmap f (x >>= g) H = do let a ← x pmap f (g a) ⋯

theorem Option.bind_pmap {α : Type u_5} {β γ : Type u_6} {p : α → Prop} (f : (a : α) → p a → β) (x : Option α) (g : β → Option γ) (H : ∀ (a : α), x = some a → p a) : pmap f x H >>= g = x.pbind fun (a : α) (h : x = some a) => g (f a ⋯)

theorem Option.pbind_eq_none {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → a ∈ x → Option β} (h' : ∀ (a : α) (H : a ∈ x), f a H = none → x = none) : x.pbind f = none ↔ x = none

theorem Option.join_pmap_eq_pmap_join {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {x : Option (Option α)} (H : ∀ (a : Option α), x = some a → ∀ (a_2 : α), a = some a_2 → p a_2) : (pmap (pmap f) x H).join = pmap f x.join ⋯

theorem Option.pmap_bind_id_eq_pmap_join {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {x : Option (Option α)} (H : ∀ (a : Option α), x = some a → ∀ (a_2 : α), a = some a_2 → p a_2) : ((pmap (pmap f) x H).bind fun (a : Option β) => a) = pmap f x.join ⋯

@[simp]

theorem Option.seq_some {α β : Type u_5} {a : α} {f : α → β} : some f <*> some a = some (f a)

@[deprecated "Use `Option.get` with proof of `isSome`." (since := "2026-01-05")]

theorem Option.iget_mem {α : Type u_1} [Inhabited α] {o : Option α} : o.isSome = true → o.iget ∈ o

@[deprecated "Use `Option.getD`." (since := "2026-01-05")]

theorem Option.iget_of_mem {α : Type u_1} [Inhabited α] {a : α} {o : Option α} : a ∈ o → o.iget = a

@[deprecated "Use `Option.getD` directly." (since := "2026-01-05")]

theorem Option.getD_default_eq_iget {α : Type u_1} [Inhabited α] (o : Option α) : o.getD default = o.iget

@[simp]

theorem Option.failure_eq_none {α : Type u_5} : failure = none

@[simp]

theorem Option.guard_eq_some' {p : Prop} [Decidable p] (u : Unit) : _root_.guard p = some u ↔ p

def Option.casesOn' {α : Type u_1} {β : Type u_2} : Option α → β → (α → β) → β

Given an element of a : Option α, a default element b : β and a function α → β, apply this function to a if it comes from α, and return b otherwise.

@[simp]

theorem Option.casesOn'_none {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) : none.casesOn' x f = x

@[simp]

theorem Option.casesOn'_some {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α) : (some a).casesOn' x f = f a

@[simp]

theorem Option.casesOn'_coe {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α) : (some a).casesOn' x f = f a

@[simp]

theorem Option.casesOn'_none_coe {α : Type u_1} {β : Type u_2} (f : Option α → β) (o : Option α) : o.casesOn' (f none) (f ∘ fun (a : α) => some a) = f o

theorem Option.casesOn'_eq_elim {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) (a : Option α) : a.casesOn' b f = a.elim b f

theorem Option.orElse_eq_some {α : Type u_1} (o o' : Option α) (x : α) : (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x

theorem Option.orElse_eq_none {α : Type u_1} (o o' : Option α) : (o <|> o') = none ↔ o = none ∧ o' = none

theorem Option.choice_eq_none (α : Type u_5) [IsEmpty α] : choice α = none

@[simp]

theorem Option.elim_none_some {α : Type u_1} {β : Type u_2} (f : Option α → β) (i : Option α) : i.elim (f none) (f ∘ some) = f i

theorem Option.elim_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) {f : γ → α} {x : α} {i : Option γ} : (i.elim (h x) fun (j : γ) => h (f j)) = h (i.elim x f)

theorem Option.elim_comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β → γ) {f : γ → α} {x : α} {g : γ → β} {y : β} {i : Option γ} : (i.elim (h x y) fun (j : γ) => h (f j) (g j)) = h (i.elim x f) (i.elim y g)

theorem Option.elim_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γ → α → β} {x : α → β} {i : Option γ} {y : α} : i.elim x f y = i.elim (x y) fun (j : γ) => f j y

@[simp]

theorem Option.elim'_update {α : Type u_5} {β : Type u_6} [DecidableEq α] (f : β) (g : α → β) (a : α) (x : β) : Option.elim' f (Function.update g a x) = Function.update (Option.elim' f g) (some a) x

@[simp]

theorem Option.getD_comp_some {α : Type u_1} (d : α) : (fun (x : Option α) => x.getD d) ∘ some = id

@[simp]

theorem Option.none_eq_map_iff {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} : none = Option.map f x ↔ x = none

@[simp]

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