doc-next-gen

Mathlib.Data.Option.Basic

Module docstring

{"# 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.

"}

Option.coe_def theorem
: (fun a ↦ ↑a : α → Option α) = some
Full source 
theorem coe_def : (fun a ↦ ↑a : α → Option α) = some :=
  rfl
Coercion to Option Type as `some` Constructor
Informal description
The canonical embedding from a type $\alpha$ to $\text{Option }\alpha$ is equal to the `some` constructor, i.e., the function $\lambda a \mapsto \text{some }a$ is identical to the coercion function $\uparrow : \alpha \to \text{Option }\alpha$.
Option.mem_map theorem
{f : α → β} {y : β} {o : Option α} : y ∈ o.map f ↔ ∃ x ∈ o, f x = y
Full source 
theorem mem_map {f : α → β} {y : β} {o : Option α} : y ∈ o.map fy ∈ o.map f ↔ ∃ x ∈ o, f x = y := by simp
Membership in Mapped Option Characterization
Informal description
For any function $f : \alpha \to \beta$, element $y \in \beta$, and option $o : \text{Option }\alpha$, the element $y$ is in the image of $o$ under $f$ if and only if there exists an element $x \in o$ such that $f(x) = y$.
Option.mem_map_of_injective theorem
{f : α → β} (H : Function.Injective f) {a : α} {o : Option α} : f a ∈ o.map f ↔ a ∈ o
Full source 
@[simp 1100, nolint simpNF]
theorem mem_map_of_injective {f : α → β} (H : Function.Injective f) {a : α} {o : Option α} :
    f a ∈ o.map ff a ∈ o.map f ↔ a ∈ o := by
  aesop
Injectivity Preserves Membership under Option Mapping
Informal description
Let $f : \alpha \to \beta$ be an injective function. For any element $a \in \alpha$ and any option $o \in \text{Option }\alpha$, the image $f(a)$ is in the mapped option $o.\text{map }f$ if and only if $a$ is in $o$.
Option.forall_mem_map theorem
{f : α → β} {o : Option α} {p : β → Prop} : (∀ y ∈ o.map f, p y) ↔ ∀ x ∈ o, p (f x)
Full source 
theorem forall_mem_map {f : α → β} {o : Option α} {p : β → Prop} :
    (∀ y ∈ o.map f, p y) ↔ ∀ x ∈ o, p (f x) := by simp
Universal Quantification over Mapped Option
Informal description
For any function $f : \alpha \to \beta$, any option $o : \text{Option }\alpha$, and any predicate $p : \beta \to \text{Prop}$, the following are equivalent: 1. For every $y$ in the image of $o$ under $f$, $p(y)$ holds. 2. For every $x$ in $o$, $p(f(x))$ holds. In other words, $(\forall y \in \text{map }f\, o, p(y)) \leftrightarrow (\forall x \in o, p(f(x)))$.
Option.exists_mem_map theorem
{f : α → β} {o : Option α} {p : β → Prop} : (∃ y ∈ o.map f, p y) ↔ ∃ x ∈ o, p (f x)
Full source 
theorem exists_mem_map {f : α → β} {o : Option α} {p : β → Prop} :
    (∃ y ∈ o.map f, p y) ↔ ∃ x ∈ o, p (f x) := by simp
Existence in Mapped Option Type
Informal description
For any function $f \colon \alpha \to \beta$, any option type $o$ of $\alpha$, and any predicate $p$ on $\beta$, there exists an element $y$ in the image of $o$ under $f$ such that $p(y)$ holds if and only if there exists an element $x$ in $o$ such that $p(f(x))$ holds.
Option.coe_get theorem
{o : Option α} (h : o.isSome) : ((Option.get _ h : α) : Option α) = o
Full source 
theorem coe_get {o : Option α} (h : o.isSome) : ((Option.get _ h : α) : Option α) = o :=
  Option.some_get h
Embedding of Extracted Value from Nonempty Option Equals Original Option
Informal description
For any option type `o : Option α` with a proof `h` that `o` is nonempty (i.e., `o.isSome` holds), the canonical embedding of the extracted value `Option.get o h` back into `Option α` equals `o` itself. In other words, if `o` is of the form `some a`, then `some (get o h) = o`.
Option.Mem.leftUnique theorem
: Relator.LeftUnique ((· ∈ ·) : α → Option α → Prop)
Full source 
theorem Mem.leftUnique : Relator.LeftUnique ((· ∈ ·) : α → Option α → Prop) :=
  fun _ _ _=> mem_unique
Left-Uniqueness of Membership in Option Type
Informal description
The membership relation `(· ∈ ·) : α → Option α → Prop` is left-unique, meaning that for any element `a : α`, there is at most one option `o : Option α` such that `a ∈ o`.
Option.some_injective theorem
(α : Type*) : Function.Injective (@some α)
Full source 
theorem some_injective (α : Type*) : Function.Injective (@some α) := fun _ _ ↦ some_inj.mp
Injectivity of the `some` Constructor in Option Types
Informal description
For any type $\alpha$, the function $\operatorname{some} : \alpha \to \operatorname{Option} \alpha$ is injective. That is, for any $x, y \in \alpha$, if $\operatorname{some}(x) = \operatorname{some}(y)$, then $x = y$.
Option.map_injective theorem
{f : α → β} (Hf : Function.Injective f) : Function.Injective (Option.map f)
Full source 
/-- `Option.map f` is injective if `f` is injective. -/
theorem map_injective {f : α → β} (Hf : Function.Injective f) : Function.Injective (Option.map f)
  | none, none, _ => rfl
  | some a₁, some a₂, H => by rw [Hf (Option.some.inj H)]
Injectivity of Option.map for Injective Functions
Informal description
For any function $f \colon \alpha \to \beta$, if $f$ is injective, then the lifted function $\mathrm{Option.map}\, f \colon \mathrm{Option}\, \alpha \to \mathrm{Option}\, \beta$ is also injective.
Option.map_comp_some theorem
(f : α → β) : Option.map f ∘ some = some ∘ f
Full source 
@[simp]
theorem map_comp_some (f : α → β) : Option.mapOption.map f ∘ some = somesome ∘ f :=
  rfl
Commutativity of Option Map with Some Constructor
Informal description
For any function $f : \alpha \to \beta$, the composition of the option map of $f$ with the `some` constructor equals the composition of the `some` constructor with $f$. In other words, the following diagram commutes: $$\text{Option.map } f \circ \text{some} = \text{some} \circ f$$
Option.none_bind' theorem
(f : α → Option β) : none.bind f = none
Full source 
@[simp]
theorem none_bind' (f : α → Option β) : none.bind f = none :=
  rfl
Bind Operation on `none` Yields `none`
Informal description
For any function $f : \alpha \to \text{Option}\ \beta$, the bind operation applied to `none` and $f$ yields `none`, i.e., $\text{none.bind}\ f = \text{none}$.
Option.some_bind' theorem
(a : α) (f : α → Option β) : (some a).bind f = f a
Full source 
@[simp]
theorem some_bind' (a : α) (f : α → Option β) : (some a).bind f = f a :=
  rfl
Bind Operation on Some Element Equals Function Application
Informal description
For any element $a$ of type $\alpha$ and any function $f \colon \alpha \to \text{Option}\ \beta$, the bind operation applied to $\text{some}\ a$ and $f$ equals $f(a)$. In other words, $(\text{some}\ a) \mathbin{\text{bind}} f = f(a)$.
Option.bind_eq_some' theorem
{x : Option α} {f : α → Option β} {b : β} : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b
Full source 
theorem bind_eq_some' {x : Option α} {f : α → Option β} {b : β} :
    x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by
  cases x <;> simp
Characterization of Option Binding: $x \bind f = \text{some }b \leftrightarrow \exists a, x = \text{some }a \land f a = \text{some }b$
Informal description
For an option type `x : Option α`, a function `f : α → Option β`, and an element `b : β`, the binding operation `x.bind f` evaluates to `some b` if and only if there exists an element `a : α` such that `x = some a` and `f a = some b`.
Option.bind_congr' theorem
{f g : α → Option β} {x y : Option α} (hx : x = y) (hf : ∀ a ∈ y, f a = g a) : x.bind f = y.bind g
Full source 
@[congr]
theorem bind_congr' {f g : α → Option β} {x y : Option α} (hx : x = y)
    (hf : ∀ a ∈ y, f a = g a) : x.bind f = y.bind g :=
  hx.symm ▸ bind_congr hf
Congruence of Bind Operation on Option Types
Informal description
Let $f, g : \alpha \to \text{Option } \beta$ be functions and $x, y : \text{Option } \alpha$ be optional values. If $x = y$ and for every $a \in y$ we have $f(a) = g(a)$, then the bind operations satisfy $x.\text{bind } f = y.\text{bind } g$.
Option.bind_congr'' theorem
{f g : α → Option β} {x : Option α} (h : ∀ a ∈ x, f a = g a) : x.bind f = x.bind g
Full source 
@[deprecated bind_congr (since := "2025-03-20")]
-- This was renamed from `bind_congr` after https://github.com/leanprover/lean4/pull/7529
-- upstreamed it with a slightly different statement.
theorem bind_congr'' {f g : α → Option β} {x : Option α}
    (h : ∀ a ∈ x, f a = g a) : x.bind f = x.bind g := by
  cases x <;> simp only [some_bind, none_bind, mem_def, h]
Equality of Option Binds under Pointwise Function Equality
Informal description
For any functions $f, g : \alpha \to \text{Option } \beta$ and any option $x : \text{Option } \alpha$, if for every $a \in x$ we have $f(a) = g(a)$, then the bind operations $x.\text{bind } f$ and $x.\text{bind } g$ are equal.
Option.joinM_eq_join theorem
: joinM = @join α
Full source 
theorem joinM_eq_join : joinM = @join α :=
  funext fun _ ↦ rfl
Monadic Join Equals Standard Join for Option Type
Informal description
The monadic join operation `joinM` on the option type is equal to the standard join operation `join` for the type `α`.
Option.bind_eq_bind' theorem
{α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f
Full source 
theorem bind_eq_bind' {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=
  rfl
Monadic Bind Equals Option Bind
Informal description
For any types $\alpha$ and $\beta$, a function $f \colon \alpha \to \text{Option } \beta$, and an element $x \colon \text{Option } \alpha$, the monadic bind operation `x >>= f` is equal to the `bind` method `x.bind f`.
Option.map_coe theorem
{α β} {a : α} {f : α → β} : f <$> (a : Option α) = ↑(f a)
Full source 
theorem map_coe {α β} {a : α} {f : α → β} : f <$> (a : Option α) = ↑(f a) :=
  rfl
Mapping Function Preserves Option Construction: $f <$> \text{some } a = \text{some } (f a)$
Informal description
For any types $\alpha$ and $\beta$, any element $a \in \alpha$, and any function $f : \alpha \to \beta$, the map operation applied to the option type with value $a$ satisfies $(f <$> (a : \text{Option } \alpha)) = \text{some } (f a)$.
Option.map_coe' theorem
{a : α} {f : α → β} : Option.map f (a : Option α) = ↑(f a)
Full source 
@[simp]
theorem map_coe' {a : α} {f : α → β} : Option.map f (a : Option α) = ↑(f a) :=
  rfl
Mapping Function Preserves Option Construction
Informal description
For any element $a$ of type $\alpha$ and any function $f : \alpha \to \beta$, the mapping of $f$ over the option type containing $a$ (denoted as `some a`) equals the option type containing $f(a)$ (denoted as `some (f a)`). In other words, $\text{Option.map}\, f\, (\text{some}\, a) = \text{some}\, (f a)$.
Option.map_injective' theorem
: Function.Injective (@Option.map α β)
Full source 
/-- `Option.map` as a function between functions is injective. -/
theorem map_injective' : Function.Injective (@Option.map α β) := fun f g h ↦
  funext fun x ↦ some_injective _ <| by simp only [← map_some', h]
Injectivity of the Option Mapping Function
Informal description
For any types $\alpha$ and $\beta$, the function $\operatorname{Option.map} : (\alpha \to \beta) \to (\operatorname{Option} \alpha \to \operatorname{Option} \beta)$ is injective. That is, for any functions $f, g : \alpha \to \beta$, if $\operatorname{Option.map}\, f = \operatorname{Option.map}\, g$, then $f = g$.
Option.map_inj theorem
{f g : α → β} : Option.map f = Option.map g ↔ f = g
Full source 
@[simp]
theorem map_inj {f g : α → β} : Option.mapOption.map f = Option.map g ↔ f = g :=
  map_injective'.eq_iff
Equality of Option Maps Reflects Equality of Functions
Informal description
For any functions $f, g : \alpha \to \beta$, the mapping functions $\operatorname{Option.map}\, f$ and $\operatorname{Option.map}\, g$ on the option type are equal if and only if $f = g$. That is, \[ \operatorname{Option.map}\, f = \operatorname{Option.map}\, g \leftrightarrow f = g. \]
Option.map_eq_id theorem
{f : α → α} : Option.map f = id ↔ f = id
Full source 
@[simp]
theorem map_eq_id {f : α → α} : Option.mapOption.map f = id ↔ f = id :=
  map_injective'.eq_iff' map_id
Option Map Equals Identity if and only if Function Equals Identity
Informal description
For any function $f : \alpha \to \alpha$, the option map of $f$ is equal to the identity function if and only if $f$ itself is equal to the identity function. That is, \[ \text{Option.map}\, f = \text{id} \leftrightarrow f = \text{id}. \]
Option.map_comm theorem
{f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) : (Option.map f₁ a).map g₁ = (Option.map f₂ a).map g₂
Full source 
theorem map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂)
    (a : α) :
    (Option.map f₁ a).map g₁ = (Option.map f₂ a).map g₂ := by rw [map_map, h, ← map_map]
Commutativity of Option Maps under Function Composition
Informal description
For any functions $f_1: \alpha \to \beta$, $f_2: \alpha \to \gamma$, $g_1: \beta \to \delta$, and $g_2: \gamma \to \delta$, if $g_1 \circ f_1 = g_2 \circ f_2$, then for any $a \in \alpha$, the composition of option maps satisfies $(f_1(a)).\text{map}\, g_1 = (f_2(a)).\text{map}\, g_2$.
Option.pbind_eq_bind theorem
(f : α → Option β) (x : Option α) : (x.pbind fun a _ ↦ f a) = x.bind f
Full source 
@[simp]
theorem pbind_eq_bind (f : α → Option β) (x : Option α) : (x.pbind fun a _ ↦ f a) = x.bind f := by
  cases x <;> simp only [pbind, none_bind', some_bind']
Partial Bind Equals Bind for Option Types
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and any optional value $x : \text{Option } \alpha$, the partial bind operation $\text{pbind}$ with $f$ is equal to the bind operation $\text{bind}$ with $f$. That is, \[ \text{pbind } x \, (\lambda a \, \_. f a) = \text{bind } x \, f. \]
Option.map_bind' theorem
(f : β → γ) (x : Option α) (g : α → Option β) : Option.map f (x.bind g) = x.bind fun a ↦ Option.map f (g a)
Full source 
theorem map_bind' (f : β → γ) (x : Option α) (g : α → Option β) :
    Option.map f (x.bind g) = x.bind fun a ↦ Option.map f (g a) := by cases x <;> simp
Commutativity of Map and Bind for Option Types: $\text{map } f \circ \text{bind } g = \text{bind } (\text{map } f \circ g)$
Informal description
For any function $f : \beta \to \gamma$, any optional value $x : \text{Option } \alpha$, and any function $g : \alpha \to \text{Option } \beta$, the following equality holds: $$\text{map } f (\text{bind } x \, g) = \text{bind } x \left( \lambda a, \text{map } f (g \, a) \right)$$ Here, $\text{map}$ applies $f$ to the value inside an $\text{Option}$ (if present), and $\text{bind}$ chains operations that may produce optional values.
Option.pbind_map theorem
(f : α → β) (x : Option α) (g : ∀ b : β, b ∈ x.map f → Option γ) : pbind (Option.map f x) g = x.pbind fun a h ↦ g (f a) (mem_map_of_mem _ h)
Full source 
theorem pbind_map (f : α → β) (x : Option α) (g : ∀ b : β, b ∈ x.map f → Option γ) :
    pbind (Option.map f x) g = x.pbind fun a h ↦ g (f a) (mem_map_of_mem _ h) := by cases x <;> rfl
Partial Bind Commutes with Map for Option Types: $\text{pbind } (\text{map } f \, x) \, g = \text{pbind } x \, (\lambda a \, h, g (f a) (\text{mem\_map\_of\_mem } f \, h))$
Informal description
For any function $f : \alpha \to \beta$, any optional value $x : \text{Option } \alpha$, and any dependent function $g : (\forall b : \beta, b \in \text{map } f \, x) \to \text{Option } \gamma$, the following equality holds: \[ \text{pbind } (\text{map } f \, x) \, g = \text{pbind } x \, (\lambda a \, h, g (f a) (\text{mem\_map\_of\_mem } f \, h)) \] Here, $\text{pbind}$ is the partial bind operation that chains operations producing optional values while preserving the proof that the value is in the mapped option, and $\text{mem\_map\_of\_mem}$ is a proof that if $a \in x$, then $f a \in \text{map } f \, x$.
Option.mem_pmem theorem
{a : α} (h : ∀ a ∈ x, p a) (ha : a ∈ x) : f a (h a ha) ∈ pmap f x h
Full source 
theorem mem_pmem {a : α} (h : ∀ a ∈ x, p a) (ha : a ∈ x) : f a (h a ha) ∈ pmap f x h := by
  rw [mem_def] at ha ⊢
  subst ha
  rfl
Membership Preservation in Partial Map of Option Types
Informal description
Let $x$ be an optional value of type $\text{Option } \alpha$, $p$ a predicate on $\alpha$, and $f$ a function that takes an element $a \in \alpha$ with proof that $p(a)$ holds and returns some value. If for every $a \in x$ we have $p(a)$, and $a$ is actually in $x$, then $f(a, h(a))$ is in the partial map $\text{pmap } f x h$, where $h$ is the proof that all elements of $x$ satisfy $p$.
Option.pmap_bind theorem
{α β γ} {x : Option α} {g : α → Option β} {p : β → Prop} {f : ∀ b, p b → γ} (H) (H' : ∀ (a : α), ∀ b ∈ g a, b ∈ x >>= g) : pmap f (x >>= g) H = x >>= fun a ↦ pmap f (g a) fun _ h ↦ H _ (H' a _ h)
Full source 
theorem pmap_bind {α β γ} {x : Option α} {g : α → Option β} {p : β → Prop} {f : ∀ b, p b → γ} (H)
    (H' : ∀ (a : α), ∀ b ∈ g a, b ∈ x >>= g) :
    pmap f (x >>= g) H = x >>= fun a ↦ pmap f (g a) fun _ h ↦ H _ (H' a _ h) := by
  cases x <;> simp only [pmap, bind_eq_bind, none_bind, some_bind]
Partial Map-Bind Commutation for Option Types
Informal description
Let $\alpha$, $\beta$, $\gamma$ be types, $x$ be an option of type $\alpha$, $g : \alpha \to \text{Option}\ \beta$ be a function, $p : \beta \to \text{Prop}$ be a predicate, and $f : \forall b, p\ b \to \gamma$ be a function. Given: 1. A proof $H$ that for all $b$ in $x \gg= g$, $p\ b$ holds 2. A proof $H'$ that for all $a \in \alpha$ and $b \in g\ a$, $b$ is in $x \gg= g$ Then the partial map of $f$ over the bind of $x$ and $g$ equals the bind of $x$ with a function that partially maps $f$ over $g\ a$ for each $a$. In symbols: $$\text{pmap}\ f\ (x \gg= g)\ H = x \gg= \lambda a.\ \text{pmap}\ f\ (g\ a)\ (\lambda \_ h.\ H\ \_\ (H'\ a\ \_\ h))$$
Option.bind_pmap theorem
{α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) : pmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h))
Full source 
theorem bind_pmap {α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) :
    pmappmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h)) := by
  cases x <;> simp only [pmap, bind_eq_bind, none_bind, some_bind, pbind]
Equality between Partial Map-Bind and Partial Bind Operations on Option Types
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be types, and let $p : \alpha \to \mathrm{Prop}$ be a predicate on $\alpha$. Given a function $f : \forall a, p(a) \to \beta$, an option type $x : \mathrm{Option}\,\alpha$, a function $g : \beta \to \mathrm{Option}\,\gamma$, and a proof $H$ that for all $a \in x$, $p(a)$ holds, then the following equality holds: \[ \mathrm{pmap}\,f\,x\,H \mathbin{>>=} g = x.\mathrm{pbind}\,(\lambda a\,h, g(f\,a\,(H\,a\,h))) \] Here, $\mathrm{pmap}$ is the partial map operation, $\mathbin{>>=}$ is the bind operation for the option monad, and $\mathrm{pbind}$ is the partial bind operation.
Option.pbind_eq_none theorem
{f : ∀ a : α, a ∈ x → Option β} (h' : ∀ a (H : a ∈ x), f a H = none → x = none) : x.pbind f = none ↔ x = none
Full source 
theorem pbind_eq_none {f : ∀ a : α, a ∈ x → Option β}
    (h' : ∀ a (H : a ∈ x), f a H = none → x = none) : x.pbind f = none ↔ x = none := by
  cases x
  · simp
  · simp only [pbind, iff_false, reduceCtorEq]
    intro h
    cases h' _ rfl h
Partial Bind Yields None iff Input is None
Informal description
Let $x$ be an option type over $\alpha$, and $f$ be a function that for any $a \in \alpha$ with proof $H$ that $a \in x$, returns an option type over $\beta$. If for all $a \in x$ and proofs $H$, $f(a,H) = \text{none}$ implies $x = \text{none}$, then the partial bind operation $x.\text{pbind}\ f$ equals $\text{none}$ if and only if $x$ itself equals $\text{none}$.
Option.pbind_eq_some theorem
{f : ∀ a : α, a ∈ x → Option β} {y : β} : x.pbind f = some y ↔ ∃ (z : α) (H : z ∈ x), f z H = some y
Full source 
theorem pbind_eq_some {f : ∀ a : α, a ∈ x → Option β} {y : β} :
    x.pbind f = some y ↔ ∃ (z : α) (H : z ∈ x), f z H = some y := by
  rcases x with (_|x)
  · simp
  · simp only [pbind]
    refine ⟨fun h ↦ ⟨x, rfl, h⟩, ?_⟩
    rintro ⟨z, H, hz⟩
    simp only [mem_def, Option.some_inj] at H
    simpa [H] using hz
Partial Bind Yields Some if and only if Function Yields Some on Some Element
Informal description
For a partial bind operation `pbind` on an option type, the result is `some y` if and only if there exists an element `z` in the option `x` such that applying the partial function `f` to `z` (with proof that `z` is in `x`) yields `some y`. In other words, given a partial function `f` that takes an element `a` of type `α` and a proof that `a` is in the option `x`, and returns an option of type `β`, we have: \[ \text{pbind } f \, x = \text{some } y \leftrightarrow \exists (z : \alpha) (H : z \in x), f \, z \, H = \text{some } y. \]
Option.join_pmap_eq_pmap_join theorem
{f : ∀ a, p a → β} {x : Option (Option α)} (H) : (pmap (pmap f) x H).join = pmap f x.join fun a h ↦ H (some a) (mem_of_mem_join h) _ rfl
Full source 
theorem join_pmap_eq_pmap_join {f : ∀ a, p a → β} {x : Option (Option α)} (H) :
    (pmap (pmap f) x H).join = pmap f x.join fun a h ↦ H (some a) (mem_of_mem_join h) _ rfl := by
  rcases x with (_ | _ | x) <;> simp
Join of Partial Map Equals Partial Map of Join for Nested Option Types
Informal description
Let $f : \forall a, p(a) \to \beta$ be a function and $x : \text{Option}(\text{Option }\alpha)$ be a nested option type. For any proof $H$ that $x$ satisfies predicate $p$, the join operation applied to the partial mapping of partial mapping of $f$ over $x$ equals the partial mapping of $f$ over the join of $x$. Specifically, for any $a \in \alpha$ and proof $h$ that $a$ is in the join of $x$, we have: \[ \text{join}(\text{pmap}(\text{pmap }f) x H) = \text{pmap }f (\text{join }x) \left(\lambda a h \mapsto H (\text{some }a) (\text{mem\_of\_mem\_join }h) \_\ \text{rfl}\right) \]
Option.pmap_bind_id_eq_pmap_join theorem
{f : ∀ a, p a → β} {x : Option (Option α)} (H) : ((pmap (pmap f) x H).bind fun a ↦ a) = pmap f x.join fun a h ↦ H (some a) (mem_of_mem_join h) _ rfl
Full source 
/-- `simp`-normal form of `join_pmap_eq_pmap_join` -/
@[simp]
theorem pmap_bind_id_eq_pmap_join {f : ∀ a, p a → β} {x : Option (Option α)} (H) :
    ((pmap (pmap f) x H).bind fun a ↦ a) =
      pmap f x.join fun a h ↦ H (some a) (mem_of_mem_join h) _ rfl := by
  rcases x with (_ | _ | x) <;> simp
Equality of Partial Map Bind Identity and Partial Map Join
Informal description
Let $f : \forall a, p(a) \to \beta$ be a function and $x : \text{Option } (\text{Option } \alpha)$ be an optional value of optional values. Given a proof $H$ that for any $a \in x.\text{join}$, $p(a)$ holds, then the following equality holds: \[ \text{bind } (\text{pmap } (\text{pmap } f) \, x \, H) \, \text{id} = \text{pmap } f \, (x.\text{join}) \, \left( \lambda a \, h, H (\text{some } a) (\text{mem\_of\_mem\_join } h) \, \_ \, \text{rfl} \right), \] where $\text{id}$ is the identity function and $\text{rfl}$ is reflexivity.
Option.seq_some theorem
{α β} {a : α} {f : α → β} : some f <*> some a = some (f a)
Full source 
@[simp]
theorem seq_some {α β} {a : α} {f : α → β} : somesome f <*> some a = some (f a) :=
  rfl
Applicative Sequencing of Some Values Yields Some Function Application
Informal description
For any types $\alpha$ and $\beta$, and any element $a \in \alpha$ and function $f : \alpha \to \beta$, the applicative sequencing operation `<*>` applied to `some f` and `some a` yields `some (f a)`.
Option.some_orElse' theorem
(a : α) (x : Option α) : (some a).orElse (fun _ ↦ x) = some a
Full source 
@[simp]
theorem some_orElse' (a : α) (x : Option α) : (some a).orElse (fun _ ↦ x) = some a :=
  rfl
Left Identity of `orElse` for `some` in Option Type
Informal description
For any element $a$ of type $\alpha$ and any optional value $x$ of type $\text{Option }\alpha$, the operation $\text{some }a \text{ orElse } x$ evaluates to $\text{some }a$.
Option.none_orElse' theorem
(x : Option α) : none.orElse (fun _ ↦ x) = x
Full source 
@[simp]
theorem none_orElse' (x : Option α) : none.orElse (fun _ ↦ x) = x := by cases x <;> rfl
Right Identity of `orElse` for `none` in Option Type
Informal description
For any optional value $x$ of type $\text{Option }\alpha$, the operation $\text{none orElse } x$ evaluates to $x$.
Option.orElse_none' theorem
(x : Option α) : x.orElse (fun _ ↦ none) = x
Full source 
@[simp]
theorem orElse_none' (x : Option α) : x.orElse (fun _ ↦ none) = x := by cases x <;> rfl
Right Identity of `orElse` with `none` in Option Type
Informal description
For any optional value $x$ of type $\text{Option }\alpha$, the operation $x \text{ orElse none}$ evaluates to $x$.
Option.exists_ne_none theorem
{p : Option α → Prop} : (∃ x ≠ none, p x) ↔ (∃ x : α, p x)
Full source 
theorem exists_ne_none {p : Option α → Prop} : (∃ x ≠ none, p x) ↔ (∃ x : α, p x) := by
  simp only [← exists_prop, bex_ne_none]
Existence of Non-None Option Satisfying Predicate is Equivalent to Existence of Underlying Element Satisfying Predicate
Informal description
For any predicate $p$ on the option type $\text{Option }\alpha$, there exists an element $x \neq \text{none}$ such that $p(x)$ holds if and only if there exists an element $x : \alpha$ such that $p(\text{some }x)$ holds.
Option.iget_mem theorem
[Inhabited α] : ∀ {o : Option α}, isSome o → o.iget ∈ o
Full source 
theorem iget_mem [Inhabited α] : ∀ {o : Option α}, isSome o → o.iget ∈ o
  | some _, _ => rfl
Default Extraction Yields Element of Non-None Option
Informal description
For any inhabited type $\alpha$ and any option $o : \text{Option }\alpha$ that is not `none` (i.e., $\text{isSome }o$ holds), the default-valued extraction $\text{iget }o$ is an element of $o$.
Option.iget_of_mem theorem
[Inhabited α] {a : α} : ∀ {o : Option α}, a ∈ o → o.iget = a
Full source 
theorem iget_of_mem [Inhabited α] {a : α} : ∀ {o : Option α}, a ∈ o → o.iget = a
  | _, rfl => rfl
Default Extraction from Option Yields Contained Element
Informal description
Given a type $\alpha$ with a distinguished default element (i.e., $\alpha$ is inhabited), for any element $a \in \alpha$ and any option $o \in \text{Option }\alpha$, if $a$ is contained in $o$ (i.e., $o = \text{some }a$), then the default-valued extraction function $\text{iget}$ applied to $o$ returns $a$.
Option.getD_default_eq_iget theorem
[Inhabited α] (o : Option α) : o.getD default = o.iget
Full source 
theorem getD_default_eq_iget [Inhabited α] (o : Option α) :
    o.getD default = o.iget := by cases o <;> rfl
Equivalence of `getD default` and `iget` for Option types
Informal description
For any inhabited type $\alpha$ and any option value $o : \text{Option } \alpha$, the result of applying `getD` with the default value is equal to applying `iget` to $o$, i.e., $o.\text{getD default} = o.\text{iget}$.
Option.guard_eq_some' theorem
{p : Prop} [Decidable p] (u) : _root_.guard p = some u ↔ p
Full source 
@[simp]
theorem guard_eq_some' {p : Prop} [Decidable p] (u) : _root_.guard_root_.guard p = some u ↔ p := by
  cases u
  by_cases h : p <;> simp [_root_.guard, h]
Guard Condition Equivalence: `guard p = some u ↔ p`
Informal description
For any proposition `p` with a decidable instance, and for any value `u`, the expression `guard p` evaluates to `some u` if and only if `p` holds.
Option.liftOrGet_choice theorem
{f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) : ∀ o₁ o₂, liftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
Full source 
theorem liftOrGet_choice {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
    ∀ o₁ o₂, liftOrGetliftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
  | none, none => Or.inl rfl
  | some _, none => Or.inl rfl
  | none, some _ => Or.inr rfl
  | some a, some b => by simpa [liftOrGet] using h a b
`liftOrGet` preserves the choice property of $f$
Informal description
For any binary function $f : \alpha \to \alpha \to \alpha$ satisfying the property that for all $a, b \in \alpha$, either $f(a, b) = a$ or $f(a, b) = b$, and for any two option values $o_1, o_2 : \text{Option } \alpha$, the result of applying the `liftOrGet` operation with $f$ to $o_1$ and $o_2$ is equal to either $o_1$ or $o_2$.
Option.casesOn' definition
: Option α → β → (α → β) → β
Full source 
/-- 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. -/
def casesOn' : Option α → β → (α → β) → β
  | none, n, _ => n
  | some a, _, s => s a
Case analysis for Option type
Informal description
Given an element `a` of type `Option α`, a default value `b` of type `β`, and a function `f : α → β`, the function `Option.casesOn'` returns `f a` if `a` is `some x` for some `x : α`, and returns `b` otherwise. In other words, it applies `f` to the value inside the `Option` if it exists, and falls back to `b` if the `Option` is `none`.
Option.casesOn'_none theorem
(x : β) (f : α → β) : casesOn' none x f = x
Full source 
@[simp]
theorem casesOn'_none (x : β) (f : α → β) : casesOn' none x f = x :=
  rfl
Case Analysis on `none` Yields Default Value
Informal description
For any default value $x$ of type $\beta$ and any function $f : \alpha \to \beta$, applying the case analysis function `casesOn'` to the `none` element of `Option $\alpha$` with default $x$ and function $f$ yields $x$. That is, $\text{casesOn'}(\text{none}, x, f) = x$.
Option.casesOn'_some theorem
(x : β) (f : α → β) (a : α) : casesOn' (some a) x f = f a
Full source 
@[simp]
theorem casesOn'_some (x : β) (f : α → β) (a : α) : casesOn' (some a) x f = f a :=
  rfl
Case Analysis on `some` Constructor Yields Function Application
Informal description
For any default value $x$ of type $\beta$, any function $f : \alpha \to \beta$, and any element $a$ of type $\alpha$, applying the case analysis function `casesOn'` to `some a` with default $x$ and function $f$ yields $f(a)$.
Option.casesOn'_coe theorem
(x : β) (f : α → β) (a : α) : casesOn' (a : Option α) x f = f a
Full source 
@[simp]
theorem casesOn'_coe (x : β) (f : α → β) (a : α) : casesOn' (a : Option α) x f = f a :=
  rfl
Case Analysis on Coerced Option Element: $\text{casesOn'}(a, x, f) = f(a)$
Informal description
For any default value $x$ of type $\beta$, any function $f : \alpha \to \beta$, and any element $a$ of type $\alpha$, the case analysis function `casesOn'` applied to the coercion of $a$ into `Option $\alpha$` with default $x$ and function $f$ equals $f(a)$. In other words, $\text{casesOn'}(a : \text{Option }\alpha, x, f) = f(a)$.
Option.casesOn'_none_coe theorem
(f : Option α → β) (o : Option α) : casesOn' o (f none) (f ∘ (fun a ↦ ↑a)) = f o
Full source 
@[simp]
theorem casesOn'_none_coe (f : Option α → β) (o : Option α) :
    casesOn' o (f none) (f ∘ (fun a ↦ ↑a)) = f o := by cases o <;> rfl
Case Analysis Equivalence for Option Types
Informal description
For any function $f : \text{Option } \alpha \to \beta$ and any option type $o : \text{Option } \alpha$, the case analysis `casesOn'` applied to $o$ with default value $f(\text{none})$ and function $f \circ (\lambda a, \text{some } a)$ equals $f(o)$. In other words, evaluating `casesOn'` on $o$ with these arguments is equivalent to directly applying $f$ to $o$.
Option.casesOn'_eq_elim theorem
(b : β) (f : α → β) (a : Option α) : Option.casesOn' a b f = Option.elim a b f
Full source 
lemma casesOn'_eq_elim (b : β) (f : α → β) (a : Option α) :
    Option.casesOn' a b f = Option.elim a b f := by cases a <;> rfl
Equivalence of Case Analysis and Elimination for Option Types
Informal description
For any default value $b$ of type $\beta$, any function $f : \alpha \to \beta$, and any optional value $a$ of type $\text{Option }\alpha$, the case analysis function $\text{casesOn'}$ applied to $a$, $b$, and $f$ is equal to the elimination function $\text{elim}$ applied to $a$, $b$, and $f$. In other words, $\text{casesOn'}\ a\ b\ f = \text{elim}\ a\ b\ f$.
Option.orElse_eq_some theorem
(o o' : Option α) (x : α) : (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
Full source 
theorem orElse_eq_some (o o' : Option α) (x : α) :
    (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x := by
  cases o
  · simp only [true_and, false_or, eq_self_iff_true, none_orElse, reduceCtorEq]
  · simp only [some_orElse, or_false, false_and, reduceCtorEq]
Characterization of `orElse` Result as `some x` in Option Types
Informal description
For any option types `o` and `o'` of type `Option α` and any element `x : α`, the expression `o <|> o'` evaluates to `some x` if and only if either `o` is `some x` or `o` is `none` and `o'` is `some x`.
Option.orElse_eq_some' theorem
(o o' : Option α) (x : α) : o.orElse (fun _ ↦ o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
Full source 
theorem orElse_eq_some' (o o' : Option α) (x : α) :
    o.orElse (fun _ ↦ o') = some x ↔ o = some x ∨ o = none ∧ o' = some x :=
  Option.orElse_eq_some o o' x
Characterization of `orElse` Result as `some x` via Lambda Function in Option Types
Informal description
For any option values $o$ and $o'$ of type $\text{Option }\alpha$ and any element $x \in \alpha$, the expression $o.\text{orElse} (\lambda \_ \Rightarrow o')$ evaluates to $\text{some }x$ if and only if either $o = \text{some }x$ or $o = \text{none}$ and $o' = \text{some }x$.
Option.orElse_eq_none theorem
(o o' : Option α) : (o <|> o') = none ↔ o = none ∧ o' = none
Full source 
@[simp]
theorem orElse_eq_none (o o' : Option α) : (o <|> o') = none ↔ o = none ∧ o' = none := by
  cases o
  · simp only [true_and, none_orElse, eq_self_iff_true]
  · simp only [some_orElse, reduceCtorEq, false_and]
"Or Else" Operation Yields None if and only if Both Operands are None
Informal description
For any two option values `o` and `o'` of type `Option α`, the result of the "or else" operation `o <|> o'` is `none` if and only if both `o` and `o'` are `none`.
Option.orElse_eq_none' theorem
(o o' : Option α) : o.orElse (fun _ ↦ o') = none ↔ o = none ∧ o' = none
Full source 
@[simp]
theorem orElse_eq_none' (o o' : Option α) : o.orElse (fun _ ↦ o') = none ↔ o = none ∧ o' = none :=
  Option.orElse_eq_none o o'
"Or Else" Operation Yields None if and only if Both Operands are None
Informal description
For any two option values $o$ and $o'$ of type $\mathrm{Option}\,\alpha$, the result of the operation $o.\mathrm{orElse}(\lambda \_ \Rightarrow o')$ is $\mathrm{none}$ if and only if both $o$ and $o'$ are $\mathrm{none}$.
Option.choice_eq_none theorem
(α : Type*) [IsEmpty α] : choice α = none
Full source 
theorem choice_eq_none (α : Type*) [IsEmpty α] : choice α = none :=
  dif_neg (not_nonempty_iff_imp_false.mpr isEmptyElim)
Choice Function on Empty Type Yields None
Informal description
For any type $\alpha$ that is empty (i.e., `IsEmpty α` holds), the choice function on $\alpha$ returns `none`. In other words, $\text{choice}(\alpha) = \text{none}$ when $\alpha$ has no elements.
Option.elim_none_some theorem
(f : Option α → β) (i : Option α) : i.elim (f none) (f ∘ some) = f i
Full source 
@[simp]
theorem elim_none_some (f : Option α → β) (i : Option α) : i.elim (f none) (f ∘ some) = f i := by
  cases i <;> rfl
Elimination of Option via Function Application
Informal description
For any function $f \colon \mathrm{Option}\,\alpha \to \beta$ and any term $i \colon \mathrm{Option}\,\alpha$, the elimination of $i$ with $f(\mathrm{none})$ and $f \circ \mathrm{some}$ equals $f(i)$. In other words, \[ i.\mathrm{elim}(f(\mathrm{none}), f \circ \mathrm{some}) = f(i). \]
Option.elim_comp theorem
(h : α → β) {f : γ → α} {x : α} {i : Option γ} : (i.elim (h x) fun j => h (f j)) = h (i.elim x f)
Full source 
theorem elim_comp (h : α → β) {f : γ → α} {x : α} {i : Option γ} :
    (i.elim (h x) fun j => h (f j)) = h (i.elim x f) := by cases i <;> rfl
Commutativity of Function Application with Option Elimination
Informal description
Let $h : \alpha \to \beta$ be a function, $f : \gamma \to \alpha$ a function, $x \in \alpha$ an element, and $i : \text{Option } \gamma$ an optional value. Then the following equality holds: \[ \text{elim}_i (h(x), \lambda j.\, h(f(j))) = h(\text{elim}_i (x, f)) \] where $\text{elim}_i$ is the elimination function for the option type, which evaluates to its first argument if $i$ is $\text{none}$ and applies its second argument to the contained value if $i$ is $\text{some } j$.
Option.elim_comp₂ theorem
(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)
Full source 
theorem elim_comp₂ (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) := by
  cases i <;> rfl
Elimination Function Commutes with Binary Operation on Option Types
Informal description
Let $h : \alpha \to \beta \to \gamma$ be a function, $f : \gamma \to \alpha$ and $g : \gamma \to \beta$ be functions, $x \in \alpha$ and $y \in \beta$ be elements, and $i$ be an option of type $\gamma$. Then the following equality holds: \[ i.\text{elim}(h(x,y), \lambda j, h(f(j), g(j))) = h(i.\text{elim}(x,f), i.\text{elim}(y,g)) \] where $i.\text{elim}(a, \phi)$ is the elimination function for the option type, which returns $a$ when $i$ is `none` and applies $\phi$ to the contained value when $i$ is `some j`.
Option.elim_apply theorem
{f : γ → α → β} {x : α → β} {i : Option γ} {y : α} : i.elim x f y = i.elim (x y) fun j => f j y
Full source 
theorem elim_apply {f : γ → α → β} {x : α → β} {i : Option γ} {y : α} :
    i.elim x f y = i.elim (x y) fun j => f j y := by rw [elim_comp fun f : α → β => f y]
Function Application Commutes with Option Elimination
Informal description
Let $f : \gamma \to \alpha \to \beta$ and $x : \alpha \to \beta$ be functions, $i : \text{Option } \gamma$ an optional value, and $y : \alpha$ an element. Then the following equality holds: \[ i.\text{elim}(x, f)(y) = i.\text{elim}(x(y), \lambda j.\, f(j)(y)) \] where $i.\text{elim}(a, \phi)$ is the elimination function for the option type, which returns $a$ when $i$ is $\text{none}$ and applies $\phi$ to the contained value when $i$ is $\text{some } j$.
Option.bnot_isSome theorem
(a : Option α) : (!a.isSome) = a.isNone
Full source 
@[simp]
lemma bnot_isSome (a : Option α) : (! a.isSome) = a.isNone := by
  cases a <;> simp
Negation of isSome is isNone in Option Types
Informal description
For any option type `Option α` and any element `a : Option α`, the negation of the proposition "`a` is `some`" is equivalent to the proposition "`a` is `none`", i.e., $\neg (\text{isSome } a) = \text{isNone } a$.
Option.bnot_comp_isSome theorem
: (!·) ∘ @Option.isSome α = Option.isNone
Full source 
@[simp]
lemma bnot_comp_isSome : (! ·) ∘ @Option.isSome α = Option.isNone := by
  funext
  simp
Negation of `isSome` Compositionally Equals `isNone` for Option Types
Informal description
The composition of the boolean negation function with the `isSome` predicate on option types is equal to the `isNone` predicate. In other words, for any type $\alpha$, we have $(\neg \cdot) \circ \text{isSome} = \text{isNone}$.
Option.bnot_isNone theorem
(a : Option α) : (!a.isNone) = a.isSome
Full source 
@[simp]
lemma bnot_isNone (a : Option α) : (! a.isNone) = a.isSome := by
  cases a <;> simp
Negation of `isNone` is `isSome` for Option Types
Informal description
For any term `a` of type `Option α`, the negation of the proposition "`a` is `none`" is equivalent to the proposition "`a` is `some`". In other words, $\neg(\text{isNone } a) = \text{isSome } a$.
Option.bnot_comp_isNone theorem
: (!·) ∘ @Option.isNone α = Option.isSome
Full source 
@[simp]
lemma bnot_comp_isNone : (! ·) ∘ @Option.isNone α = Option.isSome := by
  funext x
  simp
Negation of `isNone` Composition Equals `isSome` for Option Types
Informal description
The composition of the boolean negation function `¬·` with the `Option.isNone` predicate is equal to the `Option.isSome` predicate. In other words, for any type `α`, the function that first checks if an `Option α` is `none` and then negates the result is equivalent to checking if the option is `some`.
Option.isNone_eq_false_iff theorem
(a : Option α) : Option.isNone a = false ↔ Option.isSome a
Full source 
@[simp]
lemma isNone_eq_false_iff (a : Option α) : Option.isNoneOption.isNone a = false ↔ Option.isSome a := by
  cases a <;> simp
Equivalence of `isNone` and `isSome` for Option Types
Informal description
For any term `a` of type `Option α`, the predicate `isNone a` evaluates to `false` if and only if `isSome a` holds.
Option.elim'_update theorem
{α : Type*} {β : Type*} [DecidableEq α] (f : β) (g : α → β) (a : α) (x : β) : Option.elim' f (update g a x) = update (Option.elim' f g) (.some a) x
Full source 
@[simp]
lemma elim'_update {α : Type*} {β : Type*} [DecidableEq α]
    (f : β) (g : α → β) (a : α) (x : β) :
    Option.elim' f (update g a x) = update (Option.elim' f g) (.some a) x :=
  -- Can't reuse `Option.rec_update` as `Option.elim'` is not defeq.
  Function.rec_update (α := fun _ => β) (@Option.some.inj _) (Option.elim' f) (fun _ _ => rfl) (fun
    | _, _, .some _, h => (h _ rfl).elim
    | _, _, .none, _ => rfl) _ _ _
Update Commutes with Option Elimination
Informal description
Let $\alpha$ and $\beta$ be types with $\alpha$ having decidable equality. For any default value $f \in \beta$, function $g : \alpha \to \beta$, element $a \in \alpha$, and value $x \in \beta$, the following equality holds: \[ \text{Option.elim'}\ f\ (\text{update}\ g\ a\ x) = \text{update}\ (\text{Option.elim'}\ f\ g)\ (\text{some}\ a)\ x \] where: - $\text{Option.elim'}$ is the elimination principle for optional values, - $\text{update}\ g\ a\ x$ is the function that maps $a$ to $x$ and equals $g$ elsewhere, - $\text{some}\ a$ represents the optional value containing $a$.