Documentation

Init.Data.Option.Lemmas

theorem Option.mem_iff {α : Type u_1} {a : α} {b : Option α} :
a b b = some a
theorem Option.mem_some {α : Type u_1} {a : α} {b : α} :
a some b b = a
theorem Option.mem_some_self {α : Type u_1} (a : α) :
a 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 oo.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 = truesome 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.isSome_eq_isSome :
∀ {α : Type u_1} {x : Option α} {α_1 : Type u_2} {y : Option α_1}, x.isSome = y.isSome (x = none y = none)
@[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 nonep 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 : α_1Option α}, 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 af 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.mem_bind_iff {α : Type u_1} {β : Type u_2} {b : β} {o : Option α} {f : αOption β} :
b o.bind f ∃ (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 xf a = g a)Option.map f x = Option.map g x
@[simp]
theorem Option.map_id_fun {α : Type u} :
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 α) :
theorem Option.comp_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : βγ) (g : αβ) (x : Option α) :
@[simp]
theorem Option.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : βγ) :
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
theorem Option.isSome_filter_of_isSome {α : Type u_1} (p : αBool) (o : Option α) (h : (Option.filter p o).isSome = true) :
o.isSome = true
@[simp]
theorem Option.filter_eq_none {α : Type u_1} {o : Option α} {p : αBool} :
Option.filter p o = none o = none ∀ (a : α), a o¬p a = true
@[simp]
theorem Option.filter_eq_some {α : Type u_1} {a : α} {o : Option α} {p : αBool} :
theorem Option.mem_filter_iff {α : Type u_1} {p : αBool} {a : α} {o : Option α} :
a Option.filter p o a o p a = true
@[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.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βOption γ} {x : Option α} :
(Option.map f x).bind g = x.bind (g f)
@[simp]
theorem Option.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αOption β} {g : βγ} {x : Option α} :
Option.map g (x.bind f) = x.bind (Option.map g f)
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 aOption.guard p a = some a
theorem Option.guard_congr {α : Type u_1} {f : αProp} {g : αProp} [DecidablePred f] [DecidablePred g] (h : ∀ (a : α), f a g a) :
@[simp]
theorem Option.guard_false {α : Type u_1} :
(Option.guard fun (x : α) => False) = fun (x : α) => none
@[simp]
theorem Option.guard_true {α : Type u_1} :
(Option.guard fun (x : α) => True) = some
theorem Option.guard_comp {α : Type u_1} {β : Type u_2} {p : αProp} [DecidablePred p] {f : βα} :
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) :

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

Equations
Instances For
    theorem Option.choice_eq {α : Type u_1} [Subsingleton α] (a : α) :
    @[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} :
    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'

    beq #

    @[simp]
    theorem Option.none_beq_none {α : Type u_1} [BEq α] :
    (none == none) = true
    @[simp]
    theorem Option.none_beq_some {α : Type u_1} [BEq α] (a : α) :
    (none == some a) = false
    @[simp]
    theorem Option.some_beq_none {α : Type u_1} [BEq α] (a : α) :
    (some a == none) = false
    @[simp]
    theorem Option.some_beq_some {α : Type u_1} [BEq α] {a : α} {b : α} :
    (some a == some b) = (a == b)
    @[simp]
    theorem Option.reflBEq_iff {α : Type u_1} [BEq α] :
    @[simp]
    theorem Option.lawfulBEq_iff {α : Type u_1} [BEq α] :

    ite #

    @[simp]
    theorem Option.dite_none_left_eq_some {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : ¬pOption β} :
    (if h : p then none else b h) = some a ∃ (h : ¬p), b h = some a
    @[simp]
    theorem Option.dite_none_right_eq_some {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : pOption α} :
    (if h : p then b h else none) = some a ∃ (h : p), b h = some a
    @[simp]
    theorem Option.some_eq_dite_none_left {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : ¬pOption β} :
    (some a = if h : p then none else b h) ∃ (h : ¬p), some a = b h
    @[simp]
    theorem Option.some_eq_dite_none_right {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : pOption α} :
    (some a = if h : p then b h else none) ∃ (h : p), some a = b h
    @[simp]
    theorem Option.ite_none_left_eq_some {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : Option β} :
    (if p then none else b) = some a ¬p b = some a
    @[simp]
    theorem Option.ite_none_right_eq_some {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : Option α} :
    (if p then b else none) = some a p b = some a
    @[simp]
    theorem Option.some_eq_ite_none_left {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : Option β} :
    (some a = if p then none else b) ¬p some a = b
    @[simp]
    theorem Option.some_eq_ite_none_right {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : Option α} :
    (some a = if p then b else none) p some a = b
    theorem Option.mem_dite_none_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : ¬pOption α} :
    (x if h : p then none else l h) ∃ (h : ¬p), x l h
    theorem Option.mem_dite_none_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : pOption α} :
    (x if h : p then l h else none) ∃ (h : p), x l h
    theorem Option.mem_ite_none_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Option α} :
    (x if p then none else l) ¬p x l
    theorem Option.mem_ite_none_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Option α} :
    (x if p then l else none) p x l
    @[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

    pbind #

    @[simp]
    theorem Option.pbind_none :
    ∀ {α : Type u_1} {α_1 : Type u_2} {f : (a : α) → a noneOption α_1}, none.pbind f = none
    @[simp]
    theorem Option.pbind_some :
    ∀ {α : Type u_1} {a : α} {α_1 : Type u_2} {f : (a_1 : α) → a_1 some aOption α_1}, (some a).pbind f = f a
    @[simp]
    theorem Option.map_pbind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {o : Option α} {f : (a : α) → a oOption β} {g : βγ} :
    Option.map g (o.pbind f) = o.pbind fun (a : α) (h : a o) => Option.map g (f a h)
    theorem Option.pbind_congr {α : Type u_1} {β : Type u_2} {o : Option α} {o' : Option α} (ho : o = o') {f : (a : α) → a oOption β} {g : (a : α) → a o'Option β} (hf : ∀ (a : α) (h : a o'), f a = g a h) :
    o.pbind f = o'.pbind g
    theorem Option.pbind_eq_none_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a oOption β} :
    o.pbind f = none o = none ∃ (a : α), ∃ (h : a o), f a h = none
    theorem Option.pbind_isSome {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a oOption β} :
    ((o.pbind f).isSome = true) = ∃ (a : α), ∃ (h : a o), (f a h).isSome = true
    theorem Option.pbind_eq_some_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a oOption β} {b : β} :
    o.pbind f = some b ∃ (a : α), ∃ (h : a o), f a h = some b

    pmap #

    @[simp]
    theorem Option.pmap_none {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {h : ∀ (a : α), a nonep a} :
    Option.pmap f none h = none
    @[simp]
    theorem Option.pmap_some {α : Type u_1} {β : Type u_2} {a : α} {p : αProp} {f : (a : α) → p aβ} {h : ∀ (a_1 : α), a_1 some ap a_1} :
    Option.pmap f (some a) h = some (f a )
    @[simp]
    theorem Option.pmap_eq_none_iff {α : Type u_1} {β : Type u_2} {o : Option α} {p : αProp} {f : (a : α) → p aβ} {h : ∀ (a : α), a op a} :
    Option.pmap f o h = none o = none
    @[simp]
    theorem Option.pmap_isSome {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {o : Option α} {h : ∀ (a : α), a op a} :
    (Option.pmap f o h).isSome = o.isSome
    @[simp]
    theorem Option.pmap_eq_some_iff {α : Type u_1} {β : Type u_2} {b : β} {p : αProp} {f : (a : α) → p aβ} {o : Option α} {h : ∀ (a : α), a op a} :
    Option.pmap f o h = some b ∃ (a : α), ∃ (h : p a), o = some a b = f a h