theorem Option.default_eq_none {α : Type u_1} : default = none

@[deprecated Option.mem_def (since := "2025-04-07")]

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_iff {α : 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.eq_none_or_eq_some {α : Type u_1} (a : Option α) : a = none ∨ ∃ (x : α), a = 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.get_of_eq_some {α : Type u_1} {a : α} {o : Option α} (h : o.isSome = true) : o = some a → o.get h = a

@[simp]

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

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 {α : Type u_1} [Inhabited α] (o : Option α) : o.get! = o.getD default

theorem Option.get_congr {α : Type u_1} {o o' : Option α} {ho : o.isSome = true} (h : o = o') : o.get ho = o'.get ⋯

theorem Option.get_inj {α : Type u_1} {o1 o2 : Option α} {h1 : o1.isSome = true} {h2 : o2.isSome = true} : o1.get h1 = o2.get h2 ↔ o1 = o2

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

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

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

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

theorem Option.eq_none_iff_forall_ne_some {α✝ : Type u_1} {o : Option α✝} : o = none ↔ ∀ (a : α✝), o ≠ some a

theorem Option.eq_none_iff_forall_some_ne {α✝ : Type u_1} {o : Option α✝} : o = none ↔ ∀ (a : α✝), some a ≠ o

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

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

theorem Option.isSome_eq_isSome {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {y : Option α✝¹} : x.isSome = y.isSome ↔ (x = none ↔ y = none)

theorem Option.isSome_of_mem {α : Type u_1} {x : Option α} {y : α} (h : y ∈ x) : x.isSome = true

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

@[simp]

theorem Option.isSome_eq_false_iff {α✝ : Type u_1} {a : Option α✝} : a.isSome = false ↔ a.isNone = true

@[simp]

theorem Option.isNone_eq_false_iff {α✝ : Type u_1} {a : Option α✝} : a.isNone = false ↔ a.isSome = true

@[simp]

theorem Option.not_isSome {α : Type u_1} (a : Option α) : (!a.isSome) = a.isNone

@[simp]

theorem Option.not_comp_isSome {α : Type u_1} : (fun (x : Bool) => !x) ∘ isSome = isNone

@[simp]

theorem Option.not_isNone {α : Type u_1} (a : Option α) : (!a.isNone) = a.isSome

@[simp]

theorem Option.not_comp_isNone {α : Type u_1} : (fun (x : Bool) => !x) ∘ isNone = isSome

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

@[simp]

theorem Option.any_true {α : Type u_1} {o : Option α} : Option.any (fun (x : α) => true) o = o.isSome

@[simp]

theorem Option.any_false {α : Type u_1} {o : Option α} : Option.any (fun (x : α) => false) o = false

@[simp]

theorem Option.all_true {α : Type u_1} {o : Option α} : Option.all (fun (x : α) => true) o = true

@[simp]

theorem Option.all_false {α : Type u_1} {o : Option α} : Option.all (fun (x : α) => false) o = o.isNone

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.exists_ne_none {α : Type u_1} {p : Option α → Prop} : (∃ (x : Option α), x ≠ none ∧ p x) ↔ ∃ (x : α), p (some x)

@[deprecated Option.exists_ne_none (since := "2025-04-04")]

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.forall_ne_none {α : Type u_1} {p : Option α → Prop} : (∀ (x : Option α), x ≠ none → p x) ↔ ∀ (x : α), p (some x)

@[reducible, inline, deprecated Option.forall_ne_none (since := "2025-04-04")]

abbrev 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} : bind = Option.bind

@[simp]

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

@[simp]

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

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

@[reducible, inline, deprecated Option.bind_eq_some_iff (since := "2025-04-10")]

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

@[simp]

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

@[reducible, inline, deprecated Option.bind_eq_none_iff (since := "2025-04-10")]

abbrev 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 : α), o = some a → f a ≠ some b

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.bind_congr {α : Type u_1} {β : Type u_2} {o : Option α} {f g : α → Option β} (h : ∀ (a : α), o = some a → f a = g a) : o.bind f = o.bind g

theorem Option.isSome_bind {α : Type u_1} {β : Type u_2} (x : Option α) (f : α → Option β) : (x.bind f).isSome = Option.any (fun (x : α) => (f x).isSome) x

theorem Option.isNone_bind {α : Type u_1} {β : Type u_2} (x : Option α) (f : α → Option β) : (x.bind f).isNone = Option.all (fun (x : α) => (f x).isNone) x

theorem Option.isSome_of_isSome_bind {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome = true) : x.isSome = true

theorem Option.isSome_apply_of_isSome_bind {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome = true) : (f (x.get ⋯)).isSome = true

@[simp]

theorem Option.get_bind {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome = true) : (x.bind f).get h = (f (x.get ⋯)).get ⋯

theorem Option.any_bind {β : Type u_1} {α : Type u_2} {p : β → Bool} {f : α → Option β} {o : Option α} : Option.any p (o.bind f) = Option.any (Option.any p ∘ f) o

theorem Option.all_bind {β : Type u_1} {α : Type u_2} {p : β → Bool} {f : α → Option β} {o : Option α} : Option.all p (o.bind f) = Option.all (Option.all p ∘ f) o

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

theorem Option.join_eq_some_iff {α✝ : Type u_1} {a : α✝} {x : Option (Option α✝)} : x.join = some a ↔ x = some (some a)

@[reducible, inline, deprecated Option.join_eq_some_iff (since := "2025-04-10")]

abbrev 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_iff {α✝ : Type u_1} {o : Option (Option α✝)} : o.join = none ↔ o = none ∨ o = some none

@[reducible, inline, deprecated Option.join_eq_none_iff (since := "2025-04-10")]

abbrev Option.join_eq_none {α✝ : Type u_1} {o : Option (Option α✝)} : o.join = none ↔ o = none ∨ o = some none

theorem Option.bind_join {α : Type u_1} {β : Type u_2} {f : α → Option β} {o : Option (Option α)} : o.join.bind f = o.bind fun (x : Option α) => x.bind f

@[simp]

theorem Option.map_eq_map {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} : Functor.map f = Option.map f

@[reducible, inline, deprecated Option.map_none (since := "2025-04-10")]

abbrev Option.map_none' {α : Type u_1} {β : Type u_2} (f : α → β) : Option.map f none = none

@[reducible, inline, deprecated Option.map_some (since := "2025-04-10")]

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

@[simp]

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

@[reducible, inline, deprecated Option.map_eq_some_iff (since := "2025-04-10")]

abbrev Option.map_eq_some {α✝ : Type u_1} {b : α✝} {α✝¹ : Type u_2} {x : Option α✝¹} {f : α✝¹ → α✝} : Option.map f x = some b ↔ ∃ (a : α✝¹), x = some a ∧ f a = b

@[reducible, inline, deprecated Option.map_eq_some_iff (since := "2025-04-10")]

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

@[simp]

theorem Option.map_eq_none_iff {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f x = none ↔ x = none

@[reducible, inline, deprecated Option.map_eq_none_iff (since := "2025-04-10")]

abbrev Option.map_eq_none {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f x = none ↔ x = none

@[reducible, inline, deprecated Option.map_eq_none_iff (since := "2025-04-10")]

abbrev Option.map_eq_none' {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f x = none ↔ x = none

@[simp]

theorem Option.isSome_map {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} : (Option.map f x).isSome = x.isSome

@[reducible, inline, deprecated Option.isSome_map (since := "2025-04-10")]

abbrev Option.isSome_map' {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} : (Option.map f x).isSome = x.isSome

@[simp]

theorem Option.isNone_map {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} : (Option.map f x).isNone = x.isNone

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

theorem Option.map_congr {α : Type u_1} {α✝ : Type u_2} {f g : α → α✝} {x : Option α} (h : ∀ (a : α), x = some a → 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

@[simp]

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

theorem Option.map_inj_right {α : Type u_1} {β : Type u_2} {f : α → β} {o o' : Option α} (w : ∀ (x y : α), f x = f y → x = y) : Option.map f o = Option.map f o' ↔ o = o'

@[simp]

theorem Option.map_if {α : Type u_1} {β : Type u_2} {c : Prop} {a : α} {f : α → β} {x✝ : 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 : α → β} {x✝ : 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.filter_some_pos {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (h : p a = true) : Option.filter p (some a) = some a

theorem Option.filter_some_neg {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (h : p a = false) : Option.filter p (some a) = none

theorem Option.isSome_of_isSome_filter {α : Type u_1} (p : α → Bool) (o : Option α) (h : (Option.filter p o).isSome = true) : o.isSome = true

@[reducible, inline, deprecated Option.isSome_of_isSome_filter (since := "2025-03-18")]

abbrev 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_iff {α : Type u_1} {o : Option α} {p : α → Bool} : Option.filter p o = none ↔ ∀ (a : α), o = some a → ¬p a = true

@[reducible, inline, deprecated Option.filter_eq_none_iff (since := "2025-04-10")]

abbrev Option.filter_eq_none {α : Type u_1} {o : Option α} {p : α → Bool} : Option.filter p o = none ↔ ∀ (a : α), o = some a → ¬p a = true

@[simp]

theorem Option.filter_eq_some_iff {α : Type u_1} {a : α} {o : Option α} {p : α → Bool} : Option.filter p o = some a ↔ o = some a ∧ p a = true

@[reducible, inline, deprecated Option.filter_eq_some_iff (since := "2025-04-10")]

abbrev Option.filter_eq_some {α : Type u_1} {a : α} {o : Option α} {p : α → Bool} : Option.filter p o = some a ↔ o = some a ∧ p a = true

theorem Option.filter_some_eq_some {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} : Option.filter p (some a) = some a ↔ p a = true

theorem Option.filter_some_eq_none {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} : Option.filter p (some a) = none ↔ ¬p a = true

theorem Option.mem_filter_iff {α : Type u_1} {p : α → Bool} {a : α} {o : Option α} : a ∈ Option.filter p o ↔ a ∈ o ∧ p a = true

theorem Option.bind_guard {α : Type u_1} (x : Option α) (p : α → Bool) : x.bind (guard p) = Option.filter p x

@[deprecated Option.bind_guard (since := "2025-05-15")]

theorem Option.filter_eq_bind {α : Type u_1} (x : Option α) (p : α → Bool) : Option.filter p x = x.bind (guard p)

@[simp]

theorem Option.any_filter {α : Type u_1} {p q : α → Bool} (o : Option α) : Option.any q (Option.filter p o) = Option.any (fun (a : α) => p a && q a) o

@[simp]

theorem Option.all_filter {α : Type u_1} {p q : α → Bool} (o : Option α) : Option.all q (Option.filter p o) = Option.all (fun (a : α) => !p a || q a) o

@[simp]

theorem Option.isNone_filter {α✝ : Type u_1} {p : α✝ → Bool} {o : Option α✝} : (Option.filter p o).isNone = Option.all (fun (a : α✝) => !p a) o

@[simp]

theorem Option.isSome_filter {α✝ : Type u_1} {p : α✝ → Bool} {o : Option α✝} : (Option.filter p o).isSome = Option.any p o

@[simp]

theorem Option.filter_filter {α✝ : Type u_1} {q p : α✝ → Bool} {o : Option α✝} : Option.filter q (Option.filter p o) = Option.filter (fun (x : α✝) => p x && q x) o

theorem Option.filter_bind {α : Type u_1} {β : Type u_2} {x : Option α} {p : β → Bool} {f : α → Option β} : Option.filter p (x.bind f) = (Option.filter (fun (a : α) => Option.any p (f a)) x).bind f

theorem Option.eq_some_of_filter_eq_some {α : Type u_1} {p : α → Bool} {o : Option α} {a : α} (h : Option.filter p o = some a) : o = some a

theorem Option.filter_map {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} {p : β → Bool} : Option.filter p (Option.map f x) = Option.map f (Option.filter (p ∘ f) x)

@[simp]

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

@[simp]

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

theorem Option.all_eq_true {α : Type u_1} (p : α → Bool) (x : Option α) : Option.all p x = true ↔ ∀ (y : α), x = some y → p y = true

theorem Option.all_eq_true_iff_get {α : Type u_1} (p : α → Bool) (x : Option α) : Option.all p x = true ↔ ∀ (h : x.isSome = true), p (x.get h) = true

theorem Option.all_eq_false {α : Type u_1} (p : α → Bool) (x : Option α) : Option.all p x = false ↔ ∃ (y : α), x = some y ∧ p y = false

theorem Option.all_eq_false_iff_get {α : Type u_1} (p : α → Bool) (x : Option α) : Option.all p x = false ↔ ∃ (h : x.isSome = true), p (x.get h) = false

theorem Option.any_eq_true {α : Type u_1} (p : α → Bool) (x : Option α) : Option.any p x = true ↔ ∃ (y : α), x = some y ∧ p y = true

theorem Option.any_eq_true_iff_get {α : Type u_1} (p : α → Bool) (x : Option α) : Option.any p x = true ↔ ∃ (h : x.isSome = true), p (x.get h) = true

theorem Option.any_eq_false {α : Type u_1} (p : α → Bool) (x : Option α) : Option.any p x = false ↔ ∀ (y : α), x = some y → p y = false

theorem Option.any_eq_false_iff_get {α : Type u_1} (p : α → Bool) (x : Option α) : Option.any p x = false ↔ ∀ (h : x.isSome = true), p (x.get h) = false

theorem Option.isSome_of_any {α : Type u_1} {x : Option α} {p : α → Bool} (h : Option.any p x = true) : x.isSome = true

theorem Option.get_of_any_eq_true {α : Type u_1} (p : α → Bool) (x : Option α) (h : Option.any p x = true) : p (x.get ⋯) = true

theorem Option.any_map {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} {p : β → Bool} : Option.any p (Option.map f x) = Option.any (fun (a : α) => p (f a)) x

theorem Option.all_map {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} {p : β → Bool} : Option.all p (Option.map f x) = Option.all (fun (a : α) => p (f a)) x

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 join x).join

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

theorem Option.any_join {α : Type u_1} {p : α → Bool} {x : Option (Option α)} : Option.any p x.join = Option.any (Option.any p) x

theorem Option.all_join {α : Type u_1} {p : α → Bool} {x : Option (Option α)} : Option.all p x.join = Option.all (Option.all p) x

theorem Option.isNone_join {α : Type u_1} {x : Option (Option α)} : x.join.isNone = Option.all isNone x

theorem Option.isSome_join {α : Type u_1} {x : Option (Option α)} : x.join.isSome = Option.any isSome x

theorem Option.get_join {α : Type u_1} {x : Option (Option α)} {h : x.join.isSome = true} : x.join.get h = (x.get ⋯).get ⋯

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

theorem Option.getD_join {α : Type u_1} {x : Option (Option α)} {default : α} : x.join.getD default = (x.getD (some default)).getD default

theorem Option.get!_join {α : Type u_1} [Inhabited α] {x : Option (Option α)} : x.join.get! = x.get!.get!

@[simp]

theorem Option.guard_eq_some_iff {α✝ : Type u_1} {p : α✝ → Bool} {a b : α✝} : guard p a = some b ↔ a = b ∧ p a = true

@[reducible, inline, deprecated Option.guard_eq_some_iff (since := "2025-04-10")]

abbrev Option.guard_eq_some {α✝ : Type u_1} {p : α✝ → Bool} {a b : α✝} : guard p a = some b ↔ a = b ∧ p a = true

@[simp]

theorem Option.isSome_guard {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} : (guard p a).isSome = p a

@[reducible, inline, deprecated Option.isSome_guard (since := "2025-03-18")]

abbrev Option.guard_isSome {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} : (guard p a).isSome = p a

@[simp]

theorem Option.isNone_guard {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} : (guard p a).isNone = !p a

@[simp]

theorem Option.guard_eq_none_iff {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} : guard p a = none ↔ p a = false

@[simp]

theorem Option.guard_pos {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (h : p a = true) : guard p a = some a

theorem Option.guard_congr {α : Type u_1} {f g : α → Bool} (h : ∀ (a : α), f a = g a) : guard f = guard g

@[simp]

theorem Option.guard_false {α : Type u_1} : (guard fun (x : α) => false) = fun (x : α) => none

@[simp]

theorem Option.guard_true {α : Type u_1} : (guard fun (x : α) => true) = some

theorem Option.guard_comp {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : β → α} : guard p ∘ f = Option.map f ∘ guard (p ∘ f)

theorem Option.get_none {α : Type u_1} (a : α) {h : none.isSome = true} : none.get h = a

@[simp]

theorem Option.get_none_eq_iff_true {α : Type u_1} {a : α} {h : none.isSome = true} : none.get h = a ↔ True

@[simp]

theorem Option.get_guard {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {h : (guard p a).isSome = true} : (guard p a).get h = a

theorem Option.guard_def {α : Type u_1} (p : α → Bool) : guard p = fun (x : α) => if p x = true then some x else none

@[deprecated Option.guard_def (since := "2025-05-15")]

theorem Option.guard_eq_map {α : Type u_1} (p : α → Bool) : guard p = fun (x : α) => Option.map (fun (x_1 : α) => x) (if p x = true then some x else none)

theorem Option.guard_eq_ite {α : Type u_1} {p : α → Bool} {x : α} : guard p x = if p x = true then some x else none

theorem Option.guard_eq_filter {α : Type u_1} {p : α → Bool} {x : α} : guard p x = Option.filter p (some x)

@[simp]

theorem Option.filter_guard {α : Type u_1} {p q : α → Bool} {x : α} : Option.filter q (guard p x) = guard (fun (y : α) => p y && q y) x

theorem Option.map_guard {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → β} {x : α} : Option.map f (guard p x) = if p x = true then some (f x) else none

theorem Option.join_filter {α : Type u_1} {p : Option α → Bool} {o : Option (Option α)} : (Option.filter p o).join = Option.filter (fun (a : α) => p (some a)) o.join

theorem Option.filter_join {α : Type u_1} {p : α → Bool} {o : Option (Option α)} : Option.filter p o.join = (Option.filter (Option.any p) o).join

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

@[simp]

theorem Option.merge_none_left {α : Type u_1} {f : α → α → α} {b : Option α} : merge f none b = b

@[simp]

theorem Option.merge_none_right {α : Type u_1} {f : α → α → α} {a : Option α} : merge f a none = a

@[simp]

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

@[deprecated Option.merge_eq_or_eq (since := "2025-04-04")]

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

@[deprecated Option.merge_none_left (since := "2025-04-04")]

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

@[deprecated Option.merge_none_right (since := "2025-04-04")]

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

@[deprecated Option.merge_some_some (since := "2025-04-04")]

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

instance Option.commutative_merge {α : Type u_1} (f : α → α → α) [Std.Commutative f] : Std.Commutative (merge f)

instance Option.associative_merge {α : Type u_1} (f : α → α → α) [Std.Associative f] : Std.Associative (merge f)

instance Option.idempotentOp_merge {α : Type u_1} (f : α → α → α) [Std.IdempotentOp f] : Std.IdempotentOp (merge f)

instance Option.lawfulIdentity_merge {α : Type u_1} (f : α → α → α) : Std.LawfulIdentity (merge f) none

theorem Option.merge_join {α : Type u_1} {o o' : Option (Option α)} {f : α → α → α} : merge f o.join o'.join = (merge (merge f) o o').join

theorem Option.merge_eq_some_iff {α : Type u_1} {o o' : Option α} {f : α → α → α} {a : α} : merge f o o' = some a ↔ o = some a ∧ o' = none ∨ o = none ∧ o' = some a ∨ ∃ (b : α), ∃ (c : α), o = some b ∧ o' = some c ∧ f b c = a

@[simp]

theorem Option.merge_eq_none_iff {α : Type u_1} {f : α → α → α} {o o' : Option α} : merge f o o' = none ↔ o = none ∧ o' = none

@[simp]

theorem Option.any_merge {α : Type u_1} {p : α → Bool} {f : α → α → α} (hpf : ∀ (a b : α), p (f a b) = (p a || p b)) {o o' : Option α} : Option.any p (merge f o o') = (Option.any p o || Option.any p o')

@[simp]

theorem Option.all_merge {α : Type u_1} {p : α → Bool} {f : α → α → α} (hpf : ∀ (a b : α), p (f a b) = (p a && p b)) {o o' : Option α} : Option.all p (merge f o o') = (Option.all p o && Option.all p o')

@[simp]

theorem Option.isSome_merge {α : Type u_1} {o o' : Option α} {f : α → α → α} : (merge f o o').isSome = (o.isSome || o'.isSome)

@[simp]

theorem Option.isNone_merge {α : Type u_1} {o o' : Option α} {f : α → α → α} : (merge f o o').isNone = (o.isNone && o'.isNone)

@[simp]

theorem Option.get_merge {α : Type u_1} {o o' : Option α} {f : α → α → α} {i : α} [Std.LawfulIdentity f i] {h : (merge f o o').isSome = true} : (merge f o o').get h = f (o.getD i) (o'.getD i)

@[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

theorem Option.elim_filter {α : Type u_1} {β : Sort u_2} {p : α → Bool} {f : α → β} {o : Option α} {b : β} : (Option.filter p o).elim b f = o.elim b fun (a : α) => if p a = true then f a else b

theorem Option.elim_join {α : Type u_1} {β : Sort u_2} {o : Option (Option α)} {b : β} {f : α → β} : o.join.elim b f = o.elim b fun (x : Option α) => x.elim b f

theorem Option.elim_guard {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : α✝ → α✝¹} : (guard p a).elim b f = if p a = true then f a else b

@[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 optional arbitrary element of a given type.

If α is non-empty, then there exists some v : α and this arbitrary element is some v. Otherwise, it is none.

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

@[reducible, inline, deprecated Option.choice_eq_some (since := "2025-05-12")]

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

@[simp]

theorem Option.choice_eq_default {α : Type u_1} [Subsingleton α] [Inhabited α] : choice α = some default

theorem Option.choice_eq_none_iff_not_nonempty {α : Type u_1} : choice α = none ↔ ¬Nonempty α

theorem Option.isNone_choice_iff_not_nonempty {α : Type u_1} : (choice α).isNone = true ↔ ¬Nonempty α

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

@[simp]

theorem Option.isSome_choice {α : Type u_1} [Nonempty α] : (choice α).isSome = true

@[reducible, inline, deprecated Option.isSome_choice_iff_nonempty (since := "2025-03-18")]

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

@[simp]

theorem Option.isNone_choice_eq_false {α : Type u_1} [Nonempty α] : (choice α).isNone = false

@[simp]

theorem Option.getD_choice {α : Type u_1} {a : α} : (choice α).getD a = (choice α).get ⋯

@[simp]

theorem Option.get!_choice {α : Type u_1} [Inhabited α] : (choice α).get! = (choice α).get ⋯

@[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.toArray_some {α : Type u_1} (a : α) : (some a).toArray = #[a]

@[simp]

theorem Option.toArray_none (α : Type u_1) : none.toArray = #[]

@[simp]

theorem Option.some_or {α✝ : 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_right_of_none {α : Type u_1} {o o' : Option α} (h : o = none) : o.or o' = o'

@[simp]

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

@[reducible, inline, deprecated Option.or_some (since := "2025-05-03")]

abbrev Option.or_some' {α : Type u_1} {a : α} {o : Option α} : o.or (some a) = some (o.getD a)

@[simp]

theorem Option.or_none {α✝ : Type u_1} {o : Option α✝} : o.or none = 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_iff {α✝ : Type u_1} {o o' : Option α✝} : o.or o' = none ↔ o = none ∧ o' = none

@[reducible, inline, deprecated Option.or_eq_none_iff (since := "2025-04-10")]

abbrev Option.or_eq_none {α✝ : Type u_1} {o o' : Option α✝} : o.or o' = none ↔ o = none ∧ o' = none

@[simp]

theorem Option.or_eq_some_iff {α✝ : Type u_1} {o o' : Option α✝} {a : α✝} : o.or o' = some a ↔ o = some a ∨ o = none ∧ o' = some a

@[reducible, inline, deprecated Option.or_eq_some_iff (since := "2025-04-10")]

abbrev 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 or

theorem Option.or_eq_left_of_none {α : Type u_1} {o o' : Option α} (h : o' = none) : o.or o' = o

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

@[simp]

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

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

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

@[reducible, inline, deprecated Option.map_or (since := "2025-04-10")]

abbrev Option.map_or' {α✝ : Type u_1} {o o' : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f (o.or o') = (Option.map f o).or (Option.map f o')

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

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

@[simp]

theorem Option.getD_or {α : Type u_1} {o o' : Option α} {fallback : α} : (o.or o').getD fallback = o.getD (o'.getD fallback)

@[simp]

theorem Option.get!_or {α : Type u_1} {o o' : Option α} [Inhabited α] : (o.or o').get! = o.getD o'.get!

@[simp]

theorem Option.filter_or_filter {α : Type u_1} {o o' : Option α} {f : α → Bool} : Option.filter f (o.or (Option.filter f o')) = Option.filter f (o.or o')

theorem Option.guard_or_guard {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {q : α✝ → Bool} : (guard p a).or (guard q a) = guard (fun (x : α✝) => p x || q x) a

orElse

@[simp]

theorem Option.orElse_eq_orElse {α : Type u_1} : HOrElse.hOrElse = Option.orElse

The simp normal form of o <|> o' is o.or o' via orElse_eq_orElse and orElse_eq_or.

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

@[simp]

theorem Option.orElse_eq_or {α : Type u_1} {o : Option α} {f : Unit → Option α} : o.orElse f = o.or (f ())

The simp normal form of o.orElse f is o.or (f ())`.

@[deprecated Option.or_some (since := "2025-05-03")]

theorem Option.some_orElse {α : Type u_1} (a : α) (f : Unit → Option α) : (some a).orElse f = some a

@[deprecated Option.or_none (since := "2025-05-03")]

theorem Option.none_orElse {α : Type u_1} (f : Unit → Option α) : none.orElse f = f ()

@[deprecated Option.or_none (since := "2025-05-13")]

theorem Option.orElse_fun_none {α : Type u_1} (x : Option α) : (x.orElse fun (x : Unit) => none) = x

@[deprecated Option.or_some (since := "2025-05-13")]

theorem Option.orElse_fun_some {α : Type u_1} (x : Option α) (a : α) : (x.orElse fun (x : Unit) => some a) = some (x.getD a)

@[deprecated Option.or_eq_some_iff (since := "2025-05-13")]

theorem Option.orElse_eq_some_iff {α : Type u_1} (o : Option α) (f : Unit → Option α) (x : α) : o.orElse f = some x ↔ o = some x ∨ o = none ∧ f () = some x

@[deprecated Option.or_eq_none_iff (since := "2025-05-13")]

theorem Option.orElse_eq_none_iff {α : Type u_1} (o : Option α) (f : Unit → Option α) : o.orElse f = none ↔ o = none ∧ f () = none

@[deprecated Option.map_or (since := "2025-05-13")]

theorem Option.map_orElse {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} {y : Unit → Option α} : Option.map f (x.orElse y) = (Option.map f x).orElse fun (x : Unit) => Option.map f (y ())

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.isEqSome_eq_beq_some {α : Type u_1} [BEq α] {y : α} {o : Option α} : o.isEqSome y = (o == some y)

We simplify away isEqSome in terms of ==.

@[simp]

theorem Option.reflBEq_iff {α : Type u_1} [BEq α] : ReflBEq (Option α) ↔ ReflBEq α

@[simp]

theorem Option.lawfulBEq_iff {α : Type u_1} [BEq α] : LawfulBEq (Option α) ↔ LawfulBEq α

@[simp]

theorem Option.beq_none {α : Type u_1} [BEq α] {o : Option α} : (o == none) = o.isNone

@[simp]

theorem Option.filter_beq_self {α : Type u_1} [BEq α] [ReflBEq α] {p : α → Bool} {o : Option α} : (Option.filter p o == o) = Option.all p o

@[simp]

theorem Option.self_beq_filter {α : Type u_1} [BEq α] [ReflBEq α] {p : α → Bool} {o : Option α} : (o == Option.filter p o) = Option.all p o

theorem Option.join_beq_some {α : Type u_1} [BEq α] {o : Option (Option α)} {a : α} : (o.join == some a) = (o == some (some a))

theorem Option.join_beq_none {α : Type u_1} [BEq α] {o : Option (Option α)} : (o.join == none) = (o == none || o == some none)

@[simp]

theorem Option.guard_beq_some {α : Type u_1} [BEq α] [ReflBEq α] {x : α} {p : α → Bool} : (guard p x == some x) = p x

theorem Option.guard_beq_none {α : Type u_1} [BEq α] {x : α} {p : α → Bool} : (guard p x == none) = !p x

theorem Option.merge_beq_none {α : Type u_1} [BEq α] {o o' : Option α} {f : α → α → α} : (merge f o o' == none) = (o == none && o' == none)

ite

@[simp]

theorem Option.dite_none_left_eq_some {β : Type u_1} {a : β} {p : Prop} {x✝ : Decidable p} {b : ¬p → Option β} : (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} {x✝ : Decidable p} {b : p → Option α} : (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} {x✝ : Decidable p} {b : ¬p → Option β} : (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} {x✝ : Decidable p} {b : p → Option α} : (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} {x✝ : 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} {x✝ : 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} {x✝ : 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} {x✝ : Decidable p} {b : Option α} : (some a = if p then b else none) ↔ p ∧ some a = b

theorem Option.ite_some_none_eq_some {α : Type u_1} {p : Prop} {x✝ : Decidable p} {a b : α} : (if p then some a else none) = some b ↔ p ∧ a = b

theorem Option.mem_dite_none_left {α : Type u_1} {p : Prop} {x : α} {x✝ : Decidable p} {l : ¬p → Option α} : (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 : α} {x✝ : Decidable p} {l : p → Option α} : (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 : α} {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 : α} {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} {x✝ : 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} {x✝ : Decidable p} : (if p then some b else none).isSome = true ↔ p

@[simp]

theorem Option.isSome_dite' {β : Type u_1} {p : Prop} {x✝ : 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} {x✝ : Decidable p} : (if p then none else some b).isSome = true ↔ ¬p

@[simp]

theorem Option.get_dite {β : Type u_1} {p : Prop} {x✝ : 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} {x✝ : 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} {x✝ : 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} {x✝ : Decidable p} (h : (if p then none else some b).isSome = true) : (if p then none else some b).get h = b

@[simp]

theorem Option.get_filter {α : Type u_1} {x : Option α} {f : α → Bool} (h : (Option.filter f x).isSome = true) : (Option.filter f x).get h = x.get ⋯

pbind

@[simp]

theorem Option.pbind_none {α✝ : Type u_1} {α✝¹ : Type u_2} {f : (a : α✝) → none = some a → Option α✝¹} : none.pbind f = none

@[simp]

theorem Option.pbind_some {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : (a_1 : α✝) → some a = some a_1 → Option α✝¹} : (some a).pbind f = f a ⋯

theorem Option.pbind_none' {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : (a : α✝) → x = some a → Option α✝¹} (h : x = none) : x.pbind f = none

theorem Option.pbind_some' {α✝ : Type u_1} {x : Option α✝} {a : α✝} {α✝¹ : Type u_2} {f : (a : α✝) → x = some a → Option α✝¹} (h : x = some a) : x.pbind f = f a h

@[simp]

theorem Option.map_pbind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {o : Option α} {f : (a : α) → o = some a → Option β} {g : β → γ} : Option.map g (o.pbind f) = o.pbind fun (a : α) (h : o = some a) => Option.map g (f a h)

@[simp]

theorem Option.pbind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (o : Option α) (f : α → β) (g : (x : β) → Option.map f o = some x → Option γ) : (Option.map f o).pbind g = o.pbind fun (x : α) (h : o = some x) => g (f x) ⋯

@[simp]

theorem Option.pbind_eq_bind {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → Option β) : (o.pbind fun (x : α) (x_1 : o = some x) => f x) = o.bind f

theorem Option.pbind_congr {α : Type u_1} {β : Type u_2} {o o' : Option α} (ho : o = o') {f : (a : α) → o = some a → Option β} {g : (a : α) → o' = some a → Option β} (hf : ∀ (a : α) (h : o' = some a), 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 : α) → o = some a → Option β} : o.pbind f = none ↔ o = none ∨ ∃ (a : α), ∃ (h : o = some a), f a h = none

theorem Option.isSome_pbind_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} : (o.pbind f).isSome = true ↔ ∃ (a : α), ∃ (h : o = some a), (f a h).isSome = true

theorem Option.isNone_pbind_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} : (o.pbind f).isNone = true ↔ o = none ∨ ∃ (a : α), ∃ (h : o = some a), f a h = none

@[deprecated "isSome_pbind_iff" (since := "2025-04-01")]

theorem Option.pbind_isSome {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} : ((o.pbind f).isSome = true) = ∃ (a : α), ∃ (h : o = some a), (f a h).isSome = true

theorem Option.pbind_eq_some_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} {b : β} : o.pbind f = some b ↔ ∃ (a : α), ∃ (h : o = some a), f a h = some b

theorem Option.pbind_join {α : Type u_1} {β : Type u_2} {o : Option (Option α)} {f : (a : α) → o.join = some a → Option β} : o.join.pbind f = o.pbind fun (o' : Option α) (ho' : o = some o') => o'.pbind fun (a : α) (ha : o' = some a) => f a ⋯

theorem Option.isSome_of_isSome_pbind {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} : (o.pbind f).isSome = true → o.isSome = true

theorem Option.isSome_get_of_isSome_pbind {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} (h : (o.pbind f).isSome = true) : (f (o.get ⋯) ⋯).isSome = true

@[simp]

theorem Option.get_pbind {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} {h : (o.pbind f).isSome = true} : (o.pbind f).get h = (f (o.get ⋯) ⋯).get ⋯

pmap

@[simp]

theorem Option.pmap_none {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), none = some a → p a} : 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 : α), some a = some a_1 → p a_1} : pmap f (some a) h = some (f a ⋯)

theorem Option.pmap_none' {α : Type u_1} {β : Type u_2} {x : Option α} {p : α → Prop} {f : (a : α) → p a → β} (he : x = none) {h : ∀ (a : α), x = some a → p a} : pmap f x h = none

theorem Option.pmap_some' {α : Type u_1} {β : Type u_2} {x : Option α} {a : α} {p : α → Prop} {f : (a : α) → p a → β} (he : x = some a) {h : ∀ (a : α), x = some a → p a} : pmap f x 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 : α), o = some a → p a} : pmap f o h = none ↔ o = none

@[simp]

theorem Option.isSome_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} : (pmap f o h).isSome = o.isSome

@[simp]

theorem Option.isNone_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} : (pmap f o h).isNone = o.isNone

@[reducible, inline, deprecated Option.isSome_pmap (since := "2025-04-01")]

abbrev Option.pmap_isSome {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} : (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 : α), o = some a → p a} : pmap f o h = some b ↔ ∃ (a : α), ∃ (h : p a), o = some a ∧ b = f a h

@[simp]

theorem Option.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) : pmap (fun (a : α) (x : p a) => f a) o H = Option.map f o

theorem Option.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) : Option.map g (pmap f o H) = pmap (fun (a : α) (h : p a) => g (f a h)) o H

theorem Option.pmap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (o : Option α) (f : α → β) {p : β → Prop} (g : (b : β) → p b → γ) (H : ∀ (a : β), Option.map f o = some a → p a) : pmap g (Option.map f o) H = pmap (fun (a : α) (h : p (f a)) => g (f a) h) o ⋯

theorem Option.pmap_or {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o o' : Option α} {h : ∀ (a : α), o.or o' = some a → p a} : pmap f (o.or o') h = match o, h with | none, h => pmap f o' ⋯ | some a, h => some (f a ⋯)

theorem Option.pmap_pred_congr {α : Type u} {p p' : α → Prop} (hp : ∀ (x : α), p x ↔ p' x) {o o' : Option α} (ho : o = o') (h : ∀ (x : α), o = some x → p x) (x : α) : o' = some x → p' x

theorem Option.pmap_congr {α : Type u} {β : Type v} {p p' : α → Prop} (hp : ∀ (x : α), p x ↔ p' x) {f : (x : α) → p x → β} {f' : (x : α) → p' x → β} (hf : ∀ (x : α) (h : p' x), f x ⋯ = f' x h) {o o' : Option α} (ho : o = o') {h : ∀ (x : α), o = some x → p x} : pmap f o h = pmap f' o' ⋯

theorem Option.pmap_guard {α : Type u_1} {β : Type u_2} {q : α → Bool} {p : α → Prop} (f : (x : α) → p x → β) {x : α} (h : ∀ (a : α), guard q x = some a → p a) : pmap f (guard q x) h = if h' : q x = true then some (f x ⋯) else none

@[simp]

theorem Option.get_pmap {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : (x : α) → p x = true → β} {o : Option α} {h : ∀ (a : α), o = some a → p a = true} {h' : (pmap f o h).isSome = true} : (pmap f o h).get h' = f (o.get ⋯) ⋯

pelim

@[simp]

theorem Option.pelim_none {α✝ : Sort u_1} {b : α✝} {α✝¹ : Type u_2} {f : (a : α✝¹) → none = some a → α✝} : none.pelim b f = b

@[simp]

theorem Option.pelim_some {α✝ : Type u_1} {a : α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : (a_1 : α✝) → some a = some a_1 → α✝¹} : (some a).pelim b f = f a ⋯

theorem Option.pelim_none' {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : (a : α✝) → x = some a → α✝¹} (h : x = none) : x.pelim b f = b

theorem Option.pelim_some' {α✝ : Type u_1} {x : Option α✝} {a : α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : (a : α✝) → x = some a → α✝¹} (h : x = some a) : x.pelim b f = f a h

@[simp]

theorem Option.pelim_eq_elim {α✝ : Type u_1} {o : Option α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : α✝ → α✝¹} : (o.pelim b fun (a : α✝) (x : o = some a) => f a) = o.elim b f

@[simp]

theorem Option.elim_pmap {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) (g : γ) (g' : β → γ) : (pmap f o H).elim g g' = o.pelim g fun (a : α) (h : o = some a) => g' (f a ⋯)

theorem Option.pelim_congr_left {α : Type u_1} {β : Sort u_2} {o o' : Option α} {b : β} {f : (a : α) → a ∈ o → β} (h : o = o') : o.pelim b f = o'.pelim b fun (a : α) (ha : o' = some a) => f a ⋯

theorem Option.pelim_filter {α : Type u_1} {β : Sort u_2} {p : α → Bool} {o : Option α} {b : β} {f : (a : α) → a ∈ Option.filter p o → β} : (Option.filter p o).pelim b f = o.pelim b fun (a : α) (h : o = some a) => if hp : p a = true then f a ⋯ else b

theorem Option.pelim_join {α : Type u_1} {β : Sort u_2} {o : Option (Option α)} {b : β} {f : (a : α) → a ∈ o.join → β} : o.join.pelim b f = o.pelim b fun (o' : Option α) (ho' : o = some o') => o'.pelim b fun (a : α) (ha : o' = some a) => f a ⋯

theorem Option.pelim_congr {α : Type u_1} {β : Sort u_2} {o o' : Option α} {b b' : β} {f : (a : α) → o = some a → β} {g : (a : α) → o' = some a → β} (ho : o = o') (hb : b = b') (hf : ∀ (a : α) (ha : o' = some a), f a ⋯ = g a ha) : o.pelim b f = o'.pelim b' g

theorem Option.pelim_guard {α : Type u_1} {p : α → Bool} {β : Sort u_2} {b : β} {a : α} {f : (a' : α) → guard p a = some a' → β} : (guard p a).pelim b f = if h : p a = true then f a ⋯ else b

pfilter

theorem Option.pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o') {f : (a : α) → o = some a → Bool} {g : (a : α) → o' = some a → Bool} (hf : ∀ (a : α) (ha : o' = some a), f a ⋯ = g a ha) : o.pfilter f = o'.pfilter g

@[simp]

theorem Option.pfilter_none {α : Type u_1} {p : (a : α) → none = some a → Bool} : none.pfilter p = none

@[simp]

theorem Option.pfilter_some {α : Type u_1} {x : α} {p : (a : α) → some x = some a → Bool} : (some x).pfilter p = if p x ⋯ = true then some x else none

theorem Option.isSome_pfilter_iff {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} : (o.pfilter p).isSome = true ↔ ∃ (a : α), ∃ (ha : o = some a), p a ha = true

theorem Option.isSome_pfilter_iff_get {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} : (o.pfilter p).isSome = true ↔ ∃ (h : o.isSome = true), p (o.get h) ⋯ = true

theorem Option.isSome_of_isSome_pfilter {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} (h : (o.pfilter p).isSome = true) : o.isSome = true

theorem Option.isNone_pfilter_iff {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} : (o.pfilter p).isNone = true ↔ ∀ (a : α) (ha : o = some a), p a ha = false

@[simp]

theorem Option.get_pfilter {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} (h : (o.pfilter p).isSome = true) : (o.pfilter p).get h = o.get ⋯

theorem Option.pfilter_eq_none_iff {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} : o.pfilter p = none ↔ o = none ∨ ∃ (a : α), ∃ (ha : o = some a), p a ha = false

theorem Option.pfilter_eq_some_iff {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {a : α} : o.pfilter p = some a ↔ ∃ (ha : o = some a), p a ha = true

theorem Option.eq_some_of_pfilter_eq_some {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {a : α} (h : o.pfilter p = some a) : o = some a

theorem Option.filter_pbind {α : Type u_1} {o : Option α} {β : Type u_2} {p : β → Bool} {f : (a : α) → o = some a → Option β} : Option.filter p (o.pbind f) = (o.pfilter fun (a : α) (h : o = some a) => Option.any p (f a h)).pbind fun (a : α) (h : (o.pfilter fun (a : α) (h : o = some a) => Option.any p (f a h)) = some a) => f a ⋯

@[simp]

theorem Option.pfilter_eq_filter {α : Type u_1} {o : Option α} {p : α → Bool} : (o.pfilter fun (a : α) (x : o = some a) => p a) = Option.filter p o

@[simp]

theorem Option.pfilter_filter {α : Type u_1} {o : Option α} {p : α → Bool} {q : (a : α) → Option.filter p o = some a → Bool} : (Option.filter p o).pfilter q = o.pfilter fun (a : α) (h : o = some a) => if h' : p a = true then q a ⋯ else false

@[simp]

theorem Option.filter_pfilter {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {q : α → Bool} : Option.filter q (o.pfilter p) = o.pfilter fun (a : α) (h : o = some a) => p a h && q a

@[simp]

theorem Option.pfilter_pfilter {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {q : (a : α) → o.pfilter p = some a → Bool} : (o.pfilter p).pfilter q = o.pfilter fun (a : α) (h : o = some a) => if h' : p a h = true then q a ⋯ else false

theorem Option.pfilter_eq_pbind_ite {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} : o.pfilter p = o.pbind fun (a : α) (h : o = some a) => if p a h = true then some a else none

theorem Option.filter_pmap {α : Type u_1} {β : Type u_2} {o : Option α} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), o = some a → p a} {q : β → Bool} : Option.filter q (pmap f o h) = pmap f (o.pfilter fun (a : α) (h' : o = some a) => q (f a ⋯)) ⋯

theorem Option.pfilter_join {α : Type u_1} {o : Option (Option α)} {p : (a : α) → o.join = some a → Bool} : o.join.pfilter p = (o.pfilter fun (o' : Option α) (h : o = some o') => o'.pelim false fun (a : α) (ha : o' = some a) => p a ⋯).join

theorem Option.join_pfilter {α : Type u_1} {o : Option (Option α)} {p : (o' : Option α) → o = some o' → Bool} : (o.pfilter p).join = o.pbind fun (o' : Option α) (ho' : o = some o') => if p o' ho' = true then o' else none

theorem Option.elim_pfilter {α : Type u_1} {β : Sort u_2} {o : Option α} {b : β} {f : α → β} {p : (a : α) → o = some a → Bool} : (o.pfilter p).elim b f = o.pelim b fun (a : α) (ha : o = some a) => if p a ha = true then f a else b

theorem Option.pelim_pfilter {α : Type u_1} {β : Sort u_2} {o : Option α} {b : β} {p : (a : α) → o = some a → Bool} {f : (a : α) → o.pfilter p = some a → β} : (o.pfilter p).pelim b f = o.pelim b fun (a : α) (ha : o = some a) => if hp : p a ha = true then f a ⋯ else b

theorem Option.pfilter_guard {α : Type u_1} {a : α} {p : α → Bool} {q : (a' : α) → guard p a = some a' → Bool} : (guard p a).pfilter q = if ∃ (h : p a = true), q a ⋯ = true then some a else none

LT and LE

@[simp]

theorem Option.not_lt_none {α : Type u_1} [LT α] {a : Option α} : ¬a < none

theorem Option.none_lt_some {α : Type u_1} [LT α] {a : α} : none < some a

@[simp]

theorem Option.none_lt {α : Type u_1} [LT α] {a : Option α} : none < a ↔ a.isSome = true

@[simp]

theorem Option.some_lt_some {α : Type u_1} [LT α] {a b : α} : some a < some b ↔ a < b

@[simp]

theorem Option.none_le {α : Type u_1} [LE α] {a : Option α} : none ≤ a

theorem Option.not_some_le_none {α : Type u_1} [LE α] {a : α} : ¬some a ≤ none

@[simp]

theorem Option.le_none {α : Type u_1} [LE α] {a : Option α} : a ≤ none ↔ a = none

@[simp]

theorem Option.some_le_some {α : Type u_1} [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b

@[simp]

theorem Option.filter_le {α : Type u_1} [LE α] (le_refl : ∀ (x : α), x ≤ x) {o : Option α} {p : α → Bool} : Option.filter p o ≤ o

@[simp]

theorem Option.filter_lt {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) {o : Option α} {p : α → Bool} : Option.filter p o < o ↔ Option.any (fun (a : α) => !p a) o = true

@[simp]

theorem Option.le_filter {α : Type u_1} [LE α] (le_refl : ∀ (x : α), x ≤ x) {o : Option α} {p : α → Bool} : o ≤ Option.filter p o ↔ Option.all p o = true

@[simp]

theorem Option.not_lt_filter {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) {o : Option α} {p : α → Bool} : ¬o < Option.filter p o

@[simp]

theorem Option.pfilter_le {α : Type u_1} [LE α] (le_refl : ∀ (x : α), x ≤ x) {o : Option α} {p : (a : α) → o = some a → Bool} : o.pfilter p ≤ o

@[simp]

theorem Option.not_lt_pfilter {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) {o : Option α} {p : (a : α) → o = some a → Bool} : ¬o < o.pfilter p

theorem Option.join_le {α : Type u_1} [LE α] {o : Option (Option α)} {o' : Option α} : o.join ≤ o' ↔ o ≤ some o'

@[simp]

theorem Option.guard_le_some {α : Type u_1} [LE α] (le_refl : ∀ (x : α), x ≤ x) {x : α} {p : α → Bool} : guard p x ≤ some x

@[simp]

theorem Option.guard_lt_some {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) {x : α} {p : α → Bool} : guard p x < some x ↔ p x = false

theorem Option.left_le_of_merge_le {α : Type u_1} [LE α] {f : α → α → α} (hf : ∀ (a b c : α), f a b ≤ c → a ≤ c) {o₁ o₂ o₃ : Option α} : merge f o₁ o₂ ≤ o₃ → o₁ ≤ o₃

theorem Option.right_le_of_merge_le {α : Type u_1} [LE α] {f : α → α → α} (hf : ∀ (a b c : α), f a b ≤ c → b ≤ c) {o₁ o₂ o₃ : Option α} : merge f o₁ o₂ ≤ o₃ → o₂ ≤ o₃

theorem Option.merge_le {α : Type u_1} [LE α] {f : α → α → α} {o₁ o₂ o₃ : Option α} (hf : ∀ (a b c : α), a ≤ c → b ≤ c → f a b ≤ c) : o₁ ≤ o₃ → o₂ ≤ o₃ → merge f o₁ o₂ ≤ o₃

@[simp]

theorem Option.merge_le_iff {α : Type u_1} [LE α] {f : α → α → α} {o₁ o₂ o₃ : Option α} (hf : ∀ (a b c : α), f a b ≤ c ↔ a ≤ c ∧ b ≤ c) : merge f o₁ o₂ ≤ o₃ ↔ o₁ ≤ o₃ ∧ o₂ ≤ o₃

theorem Option.left_lt_of_merge_lt {α : Type u_1} [LT α] {f : α → α → α} (hf : ∀ (a b c : α), f a b < c → a < c) {o₁ o₂ o₃ : Option α} : merge f o₁ o₂ < o₃ → o₁ < o₃

theorem Option.right_lt_of_merge_lt {α : Type u_1} [LT α] {f : α → α → α} (hf : ∀ (a b c : α), f a b < c → b < c) {o₁ o₂ o₃ : Option α} : merge f o₁ o₂ < o₃ → o₂ < o₃

theorem Option.merge_lt {α : Type u_1} [LT α] {f : α → α → α} {o₁ o₂ o₃ : Option α} (hf : ∀ (a b c : α), a < c → b < c → f a b < c) : o₁ < o₃ → o₂ < o₃ → merge f o₁ o₂ < o₃

@[simp]

theorem Option.merge_lt_iff {α : Type u_1} [LT α] {f : α → α → α} {o₁ o₂ o₃ : Option α} (hf : ∀ (a b c : α), f a b < c ↔ a < c ∧ b < c) : merge f o₁ o₂ < o₃ ↔ o₁ < o₃ ∧ o₂ < o₃

Rel

@[simp]

theorem Option.rel_some_some {α : Type u_1} {β : Type u_2} {a : α} {b : β} {r : α → β → Prop} : Rel r (some a) (some b) ↔ r a b

@[simp]

theorem Option.not_rel_some_none {α : Type u_1} {β : Type u_2} {a : α} {r : α → β → Prop} : ¬Rel r (some a) none

@[simp]

theorem Option.not_rel_none_some {α : Type u_1} {β : Type u_2} {a : β} {r : α → β → Prop} : ¬Rel r none (some a)

@[simp]

theorem Option.rel_none_none {α : Type u_1} {β : Type u_2} {r : α → β → Prop} : Rel r none none

min and max

theorem Option.min_eq_left {α : Type u_1} [LE α] [Min α] (min_eq_left : ∀ (x y : α), x ≤ y → min x y = x) {a b : Option α} (h : a ≤ b) : min a b = a

theorem Option.min_eq_right {α : Type u_1} [LE α] [Min α] (min_eq_right : ∀ (x y : α), y ≤ x → min x y = y) {a b : Option α} (h : b ≤ a) : min a b = b

theorem Option.min_eq_left_of_lt {α : Type u_1} [LT α] [Min α] (min_eq_left : ∀ (x y : α), x < y → min x y = x) {a b : Option α} (h : a < b) : min a b = a

theorem Option.min_eq_right_of_lt {α : Type u_1} [LT α] [Min α] (min_eq_right : ∀ (x y : α), y < x → min x y = y) {a b : Option α} (h : b < a) : min a b = b

theorem Option.min_eq_or {α : Type u_1} [LE α] [Min α] (min_eq_or : ∀ (x y : α), min x y = x ∨ min x y = y) {a b : Option α} : min a b = a ∨ min a b = b

theorem Option.min_le_left {α : Type u_1} [LE α] [Min α] (min_le_left : ∀ (x y : α), min x y ≤ x) {a b : Option α} : min a b ≤ a

theorem Option.min_le_right {α : Type u_1} [LE α] [Min α] (min_le_right : ∀ (x y : α), min x y ≤ y) {a b : Option α} : min a b ≤ b

theorem Option.le_min {α : Type u_1} [LE α] [Min α] (le_min : ∀ (x y z : α), x ≤ min y z ↔ x ≤ y ∧ x ≤ z) {a b c : Option α} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

theorem Option.max_eq_left {α : Type u_1} [LE α] [Max α] (max_eq_left : ∀ (x y : α), x ≤ y → max x y = y) {a b : Option α} (h : a ≤ b) : max a b = b

theorem Option.max_eq_right {α : Type u_1} [LE α] [Max α] (max_eq_right : ∀ (x y : α), y ≤ x → max x y = x) {a b : Option α} (h : b ≤ a) : max a b = a

theorem Option.max_eq_left_of_lt {α : Type u_1} [LT α] [Max α] (max_eq_left : ∀ (x y : α), x < y → max x y = y) {a b : Option α} (h : a < b) : max a b = b

theorem Option.max_eq_right_of_lt {α : Type u_1} [LT α] [Max α] (max_eq_right : ∀ (x y : α), y < x → max x y = x) {a b : Option α} (h : b < a) : max a b = a

theorem Option.max_eq_or {α : Type u_1} [LE α] [Max α] (max_eq_or : ∀ (x y : α), max x y = x ∨ max x y = y) {a b : Option α} : max a b = a ∨ max a b = b

theorem Option.left_le_max {α : Type u_1} [LE α] [Max α] (le_refl : ∀ (x : α), x ≤ x) (left_le_max : ∀ (x y : α), x ≤ max x y) {a b : Option α} : a ≤ max a b

theorem Option.right_le_max {α : Type u_1} [LE α] [Max α] (le_refl : ∀ (x : α), x ≤ x) (right_le_max : ∀ (x y : α), y ≤ max x y) {a b : Option α} : b ≤ max a b

theorem Option.max_le {α : Type u_1} [LE α] [Max α] (max_le : ∀ (x y z : α), max x y ≤ z ↔ x ≤ z ∧ y ≤ z) {a b c : Option α} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

@[simp]

theorem Option.merge_max {α : Type u_1} [Max α] : merge max = max

instance Option.instLawfulIdentityMaxNone {α : Type u_1} [Max α] : Std.LawfulIdentity max none

instance Option.instIdempotentOpMax {α : Type u_1} [Max α] [Std.IdempotentOp max] : Std.IdempotentOp max

@[simp]

theorem Option.max_filter_left {α : Type u_1} [Max α] [Std.IdempotentOp max] {p : α → Bool} {o : Option α} : max (Option.filter p o) o = o

@[simp]

theorem Option.max_filter_right {α : Type u_1} [Max α] [Std.IdempotentOp max] {p : α → Bool} {o : Option α} : max o (Option.filter p o) = o

@[simp]

theorem Option.min_filter_left {α : Type u_1} [Min α] [Std.IdempotentOp min] {p : α → Bool} {o : Option α} : min (Option.filter p o) o = Option.filter p o

@[simp]

theorem Option.min_filter_right {α : Type u_1} [Min α] [Std.IdempotentOp min] {p : α → Bool} {o : Option α} : min o (Option.filter p o) = Option.filter p o

@[simp]

theorem Option.max_pfilter_left {α : Type u_1} [Max α] [Std.IdempotentOp max] {o : Option α} {p : (a : α) → o = some a → Bool} : max (o.pfilter p) o = o

@[simp]

theorem Option.max_pfilter_right {α : Type u_1} [Max α] [Std.IdempotentOp max] {o : Option α} {p : (a : α) → o = some a → Bool} : max o (o.pfilter p) = o

@[simp]

theorem Option.min_pfilter_left {α : Type u_1} [Min α] [Std.IdempotentOp min] {o : Option α} {p : (a : α) → o = some a → Bool} : min (o.pfilter p) o = o.pfilter p

@[simp]

theorem Option.min_pfilter_right {α : Type u_1} [Min α] [Std.IdempotentOp min] {o : Option α} {p : (a : α) → o = some a → Bool} : min o (o.pfilter p) = o.pfilter p

@[simp]

theorem Option.isSome_max {α : Type u_1} [Max α] {o o' : Option α} : (max o o').isSome = (o.isSome || o'.isSome)

@[simp]

theorem Option.isNone_max {α : Type u_1} [Max α] {o o' : Option α} : (max o o').isNone = (o.isNone && o'.isNone)

@[simp]

theorem Option.isSome_min {α : Type u_1} [Min α] {o o' : Option α} : (min o o').isSome = (o.isSome && o'.isSome)

@[simp]

theorem Option.isNone_min {α : Type u_1} [Min α] {o o' : Option α} : (min o o').isNone = (o.isNone || o'.isNone)

theorem Option.max_join_left {α : Type u_1} [Max α] {o : Option (Option α)} {o' : Option α} : max o.join o' = (max o (some o')).get ⋯

theorem Option.max_join_right {α : Type u_1} [Max α] {o : Option α} {o' : Option (Option α)} : max o o'.join = (max (some o) o').get ⋯

theorem Option.join_max {α : Type u_1} [Max α] {o o' : Option (Option α)} : (max o o').join = max o.join o'.join

theorem Option.min_join_left {α : Type u_1} [Min α] {o : Option (Option α)} {o' : Option α} : min o.join o' = (min o (some o')).join

theorem Option.min_join_right {α : Type u_1} [Min α] {o : Option α} {o' : Option (Option α)} : min o o'.join = (min (some o) o').join

theorem Option.join_min {α : Type u_1} [Min α] {o o' : Option (Option α)} : (min o o').join = min o.join o'.join

@[simp]

theorem Option.min_guard_some {α : Type u_1} [Min α] [Std.IdempotentOp min] {x : α} {p : α → Bool} : min (guard p x) (some x) = guard p x

@[simp]

theorem Option.min_some_guard {α : Type u_1} [Min α] [Std.IdempotentOp min] {x : α} {p : α → Bool} : min (some x) (guard p x) = guard p x

@[simp]

theorem Option.max_guard_some {α : Type u_1} [Max α] [Std.IdempotentOp max] {x : α} {p : α → Bool} : max (guard p x) (some x) = some x

@[simp]

theorem Option.max_some_guard {α : Type u_1} [Max α] [Std.IdempotentOp max] {x : α} {p : α → Bool} : max (some x) (guard p x) = some x

theorem Option.max_eq_some_iff {α : Type u_1} [Max α] {o o' : Option α} {a : α} : max o o' = some a ↔ o = some a ∧ o' = none ∨ o = none ∧ o' = some a ∨ ∃ (b : α), ∃ (c : α), o = some b ∧ o' = some c ∧ max b c = a

@[simp]

theorem Option.max_eq_none_iff {α : Type u_1} [Max α] {o o' : Option α} : max o o' = none ↔ o = none ∧ o' = none

@[simp]

theorem Option.min_eq_some_iff {α : Type u_1} [Min α] {o o' : Option α} {a : α} : min o o' = some a ↔ ∃ (b : α), ∃ (c : α), o = some b ∧ o' = some c ∧ min b c = a

@[simp]

theorem Option.min_eq_none_iff {α : Type u_1} [Min α] {o o' : Option α} : min o o' = none ↔ o = none ∨ o' = none

@[simp]

theorem Option.any_max {α : Type u_1} [Max α] {o o' : Option α} {p : α → Bool} (hp : ∀ (a b : α), p (max a b) = (p a || p b)) : Option.any p (max o o') = (Option.any p o || Option.any p o')

@[simp]

theorem Option.all_min {α : Type u_1} [Min α] {o o' : Option α} {p : α → Bool} (hp : ∀ (a b : α), p (min a b) = (p a || p b)) : Option.all p (min o o') = (Option.all p o || Option.all p o')

theorem Option.isSome_left_of_isSome_min {α : Type u_1} [Min α] {o o' : Option α} : (min o o').isSome = true → o.isSome = true

theorem Option.isSome_right_of_isSome_min {α : Type u_1} [Min α] {o o' : Option α} : (min o o').isSome = true → o'.isSome = true

@[simp]

theorem Option.get_min {α : Type u_1} [Min α] {o o' : Option α} {h : (min o o').isSome = true} : (min o o').get h = min (o.get ⋯) (o'.get ⋯)

theorem Option.map_max {α : Type u_1} {β : Type u_2} [Max α] [Max β] {o o' : Option α} {f : α → β} (hf : ∀ (x y : α), f (max x y) = max (f x) (f y)) : Option.map f (max o o') = max (Option.map f o) (Option.map f o')

theorem Option.map_min {α : Type u_1} {β : Type u_2} [Min α] [Min β] {o o' : Option α} {f : α → β} (hf : ∀ (x y : α), f (min x y) = min (f x) (f y)) : Option.map f (min o o') = min (Option.map f o) (Option.map f o')