Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.option.defs
! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Init.Algebra.Classes

/-!
# Extra definitions on `Option`

This file defines more operations involving `Option α`. Lemmas about them are located in other
files under `Mathlib.Data.Option`.
Other basic operations on `Option` are defined in the core library.
-/

namespace Option

#align option.lift_or_get Option.liftOrGet: {α : Type u_1} → (α → α → α) → Option α → Option α → Option αOption.liftOrGet

/-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
`none ~ none`. -/
inductive rel: {α : Type ?u.21} → {β : Type ?u.24} → (α → β → Prop) → Option α → Option β → Proprel (r: α → β → Propr : α: ?m.4α → β: ?m.11β → Prop: TypeProp) : Option: Type ?u.21 → Type ?u.21Option α: ?m.4α → Option: Type ?u.24 → Type ?u.24Option β: ?m.11β → Prop: TypeProp
| /-- If `a ~ b`, then `some a ~ some b` -/
some: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β}, r a b → rel r (some a) (some b)some {a: ?m.33a b: ?m.36b} : r: α → β → Propr a: ?m.33a b: ?m.36b → rel: {α : Type ?u.21} → {β : Type ?u.24} → (α → β → Prop) → Option α → Option β → Proprel r: α → β → Propr (some: {α : Type ?u.49} → α → Option αsome a: ?m.33a) (some: {α : Type ?u.52} → α → Option αsome b: ?m.36b)
| /-- `none ~ none` -/
none: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, rel r none nonenone : rel: {α : Type ?u.21} → {β : Type ?u.24} → (α → β → Prop) → Option α → Option β → Proprel r: α → β → Propr none: {α : Type ?u.69} → Option αnone none: {α : Type ?u.71} → Option αnone
#align option.rel Option.rel: {α : Type u_1} → {β : Type u_2} → (α → β → Prop) → Option α → Option β → PropOption.rel

/-- Traverse an object of `Option α` with a function `f : α → F β` for an applicative `F`. -/
protected def traverse: {F : Type u → Type v} → [inst : Applicative F] → {α : Type u_1} → {β : Type u} → (α → F β) → Option α → F (Option β)traversetraverse.{u, v}: {F : Type u → Type v} → [inst : Applicative F] → {α : Type ?u.130} → {β : Type u} → (α → F β) → Option α → F (Option β).{u, v} {F: Type u → Type vF : Type u: Type (u+1)Type u → Type v: Type (v+1)Type v} [Applicative: (Type ?u.124 → Type ?u.123) → Type (max(?u.124+1)?u.123)Applicative F: Type u → Type vF] {α: Type ?u.130α β: Type ?u.133β : Type _: Type (?u.133+1)Type _} (f: α → F βf : α: Type ?u.130α → F: Type u → Type vF β: Type ?u.133β) :
Option: Type ?u.141 → Type ?u.141Option α: Type ?u.130α → F: Type u → Type vF (Option: Type ?u.143 → Type ?u.143Option β: Type ?u.133β)
| none: {α : Type ?u.154} → Option αnone => pure: {f : Type ?u.164 → Type ?u.163} → [self : Pure f] → {α : Type ?u.164} → α → f αpure none: {α : Type ?u.185} → Option αnone
| some: {α : Type ?u.206} → α → Option αsome x: αx => some: {α : Type ?u.236} → α → Option αsome <\$> f: α → F βf x: αx
#align option.traverse Option.traverse: {F : Type u → Type v} → [inst : Applicative F] → {α : Type u_1} → {β : Type u} → (α → F β) → Option α → F (Option β)Option.traverse

/-- If you maybe have a monadic computation in a `[Monad m]` which produces a term of type `α`,
then there is a naturally associated way to always perform a computation in `m` which maybe
produces a result. -/
def maybe: {m : Type u → Type v} → [inst : Monad m] → {α : Type u} → Option (m α) → m (Option α)maybemaybe.{u, v}: {m : Type u → Type v} → [inst : Monad m] → {α : Type u} → Option (m α) → m (Option α).{u, v} {m: Type u → Type vm : Type u: Type (u+1)Type u → Type v: Type (v+1)Type v} [Monad: (Type ?u.542 → Type ?u.541) → Type (max(?u.542+1)?u.541)Monad m: Type u → Type vm] {α: Type uα : Type u: Type (u+1)Type u} : Option: Type ?u.551 → Type ?u.551Option (m: Type u → Type vm α: Type uα) → m: Type u → Type vm (Option: Type ?u.553 → Type ?u.553Option α: Type uα)
| none: {α : Type ?u.562} → Option αnone => pure: {f : Type ?u.572 → Type ?u.571} → [self : Pure f] → {α : Type ?u.572} → α → f αpure none: {α : Type ?u.596} → Option αnone
| some: {α : Type ?u.627} → α → Option αsome fn: m αfn => some: {α : Type ?u.657} → α → Option αsome <\$> fn: m αfn
#align option.maybe Option.maybe: {m : Type u → Type v} → [inst : Monad m] → {α : Type u} → Option (m α) → m (Option α)Option.maybe

#align option.mmap Option.mapM: {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [inst : Monad m] → (α → m β) → Option α → m (Option β)Option.mapM
#align option.melim Option.elimM: {m : Type u_1 → Type u_2} → {α β : Type u_1} → [inst : Monad m] → m (Option α) → m β → (α → m β) → m βOption.elimM

@[deprecated getDM: {m : Type u_1 → Type u_2} → {α : Type u_1} → [inst : Monad m] → Option α → m α → m αgetDM]
protected def getDM': {m : Type ?u.923 → Type ?u.918} → {α : Type ?u.923} → [inst : Monad m] → m (Option α) → m α → m αgetDM' [Monad: (Type ?u.919 → Type ?u.918) → Type (max(?u.919+1)?u.918)Monad m: ?m.905m] (x: m (Option α)x : m: ?m.905m (Option: Type ?u.923 → Type ?u.923Option α: ?m.915α)) (y: m αy : m: ?m.905m α: ?m.915α) : m: ?m.905m α: ?m.915α := do
(← x): ?m.989(← x: m (Option α)x(← x): ?m.989).getDM: {m : Type ?u.992 → Type ?u.991} → {α : Type ?u.992} → [inst : Monad m] → Option α → m α → m αgetDM y: m αy
#align option.mget_or_else Option.getDM': {m : Type u_1 → Type u_2} → {α : Type u_1} → [inst : Monad m] → m (Option α) → m α → m αOption.getDM'

variable {α: Type ?u.1136α : Type _: Type (?u.1142+1)Type _} {β: Type ?u.1820β : Type _: Type (?u.1539+1)Type _}

-- Porting note: Would need to add the attribute directly in `Init.Prelude`.
-- attribute [inline] Option.isSome Option.isNone

/-- An elimination principle for `Option`. It is a nondependent version of `Option.rec`. -/
protected def elim': β → (α → β) → Option α → βelim' (b: βb : β: Type ?u.1145β) (f: α → βf : α: Type ?u.1142α → β: Type ?u.1145β) : Option: Type ?u.1155 → Type ?u.1155Option α: Type ?u.1142α → β: Type ?u.1145β
| some: {α : Type ?u.1163} → α → Option αsome a: αa => f: α → βf a: αa
| none: {α : Type ?u.1179} → Option αnone => b: βb
#align option.elim Option.elim': {α : Type u_1} → {β : Type u_2} → β → (α → β) → Option α → βOption.elim'

@[simp]
theorem elim'_none: ∀ {α : Type u_2} {β : Type u_1} (b : β) (f : α → β), Option.elim' b f none = belim'_none (b: βb : β: Type ?u.1388β) (f: α → βf : α: Type ?u.1385α → β: Type ?u.1388β) : Option.elim': {α : Type ?u.1399} → {β : Type ?u.1398} → β → (α → β) → Option α → βOption.elim' b: βb f: α → βf none: {α : Type ?u.1405} → Option αnone = b: βb := rfl: ∀ {α : Sort ?u.1412} {a : α}, a = arfl
@[simp]
theorem elim'_some: ∀ {a : α} (b : β) (f : α → β), Option.elim' b f (some a) = f aelim'_some (b: βb : β: Type ?u.1451β) (f: α → βf : α: Type ?u.1448α → β: Type ?u.1451β) : Option.elim': {α : Type ?u.1483} → {β : Type ?u.1482} → β → (α → β) → Option α → βOption.elim' b: βb f: α → βf (some: {α : Type ?u.1489} → α → Option αsome a: ?m.1472a) = f: α → βf a: ?m.1472a := rfl: ∀ {α : Sort ?u.1496} {a : α}, a = arfl

theorem mem_some_iff: ∀ {α : Type u_1} {a b : α}, a ∈ some b ↔ b = amem_some_iff {α: Type ?u.1542α : Type _: Type (?u.1542+1)Type _} {a: αa b: αb : α: Type ?u.1542α} : a: αa ∈ some: {α : Type ?u.1554} → α → Option αsome b: αb ↔ b: αb = a: αa := byGoals accomplished! 🐙 α✝: Type ?u.1536β: Type ?u.1539α: Type u_1a, b: αa ∈ some b ↔ b = asimpGoals accomplished! 🐙
#align option.mem_some_iff Option.mem_some_iff: ∀ {α : Type u_1} {a b : α}, a ∈ some b ↔ b = aOption.mem_some_iff

/-- `o = none` is decidable even if the wrapped type does not have decidable equality.
This is not an instance because it is not definitionally equal to `Option.decidableEq`.
Try to use `o.isNone` or `o.isSome` instead.
-/
@[inline]
def decidableEqNone: {o : Option α} → Decidable (o = none)decidableEqNone {o: Option αo : Option: Type ?u.1670 → Type ?u.1670Option α: Type ?u.1664α} : Decidable: Prop → TypeDecidable (o: Option αo = none: {α : Type ?u.1674} → Option αnone) :=
decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable qdecidable_of_decidable_of_iff isNone_iff_eq_none: ∀ {α : Type ?u.1748} {o : Option α}, isNone o = true ↔ o = noneisNone_iff_eq_none
#align option.decidable_eq_none Option.decidableEqNone: {α : Type u_1} → {o : Option α} → Decidable (o = none)Option.decidableEqNone

instance decidableForallMem: {p : α → Prop} → [inst : DecidablePred p] → (o : Option α) → Decidable (∀ (a : α), a ∈ o → p a)decidableForallMem {p: α → Propp : α: Type ?u.1817α → Prop: TypeProp} [DecidablePred: {α : Sort ?u.1827} → (α → Prop) → Sort (max1?u.1827)DecidablePred p: α → Propp] :
∀ o: Option αo : Option: Type ?u.1838 → Type ?u.1838Option α: Type ?u.1817α, Decidable: Prop → TypeDecidable (∀ a: ?m.1842a ∈ o: Option αo, p: α → Propp a: ?m.1842a)
| none: {α : Type ?u.1886} → Option αnone => isTrue: {p : Prop} → p → Decidable pisTrue (byGoals accomplished! 🐙 α: Type ?u.1817β: Type ?u.1820p: α → Propinst✝: DecidablePred p∀ (a : α), a ∈ none → p asimp [false_imp_iff: ∀ (a : Prop), False → a ↔ Truefalse_imp_iff]Goals accomplished! 🐙)
| some: {α : Type ?u.1904} → α → Option αsome a: αa =>
if h: ?m.1932h : p: α → Propp a: αa then isTrue: {p : Prop} → p → Decidable pisTrue fun o: ?m.1938o e: ?m.1941e ↦ some_inj: ∀ {α : Type ?u.1943} {a b : α}, some a = some b ↔ a = bsome_inj.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 e: ?m.1941e ▸ h: ?m.1932h
else isFalse: {p : Prop} → ¬p → Decidable pisFalse <| mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬amt (fun H: ?m.1981H ↦ H: ?m.1981H _: α_ rfl: ∀ {α : Sort ?u.1987} {a : α}, a = arfl) h: ?m.1969h

instance decidableExistsMem: {α : Type u_1} → {p : α → Prop} → [inst : DecidablePred p] → (o : Option α) → Decidable (∃ a, a ∈ o ∧ p a)decidableExistsMem {p: α → Propp : α: Type ?u.2426α → Prop: TypeProp} [DecidablePred: {α : Sort ?u.2436} → (α → Prop) → Sort (max1?u.2436)DecidablePred p: α → Propp] :
∀ o: Option αo : Option: Type ?u.2447 → Type ?u.2447Option α: Type ?u.2426α, Decidable: Prop → TypeDecidable (∃ a: ?m.2453a ∈ o: Option αo, p: α → Propp a: ?m.2453a)
| none: {α : Type ?u.2484} → Option αnone => isFalse: {p : Prop} → ¬p → Decidable pisFalse fun ⟨a: αa, ⟨h: a ∈ noneh, _⟩⟩ ↦ byGoals accomplished! 🐙 α: Type ?u.2426β: Type ?u.2429p: α → Propinst✝: DecidablePred px✝: ∃ a, a ∈ none ∧ p aa: αh: a ∈ noneright✝: p aFalsecases h: a ∈ nonehGoals accomplished! 🐙
| some: {α : Type ?u.2648} → α → Option αsome a: αa => if h: ?m.2676h : p: α → Propp a: αa then isTrue: {p : Prop} → p → Decidable pisTrue <| ⟨_: ?m.2684_, rfl: ∀ {α : Sort ?u.2700} {a : α}, a = arfl, h: ?m.2676h⟩ else isFalse: {p : Prop} → ¬p → Decidable pisFalse fun ⟨_: α_, ⟨rfl: ∀ {α : Sort ?u.2719} {a : α}, a = arfl, hn: p ahn⟩⟩ ↦ h: ?m.2711h hn: p ahn

/-- Inhabited `get` function. Returns `a` if the input is `some a`, otherwise returns `default`. -/
@[reducible]
def iget: [inst : Inhabited α] → Option α → αiget [Inhabited: Sort ?u.3243 → Sort (max1?u.3243)Inhabited α: Type ?u.3237α] : Option: Type ?u.3247 → Type ?u.3247Option α: Type ?u.3237α → α: Type ?u.3237α
| some: {α : Type ?u.3254} → α → Option αsome x: αx => x: αx
| none: {α : Type ?u.3270} → Option αnone => default: {α : Sort ?u.3278} → [self : Inhabited α] → αdefault
#align option.iget Option.iget: {α : Type u_1} → [inst : Inhabited α] → Option α → αOption.iget

theorem iget_some: ∀ [inst : Inhabited α] {a : α}, iget (some a) = aiget_some [Inhabited: Sort ?u.3530 → Sort (max1?u.3530)Inhabited α: Type ?u.3524α] {a: αa : α: Type ?u.3524α} : (some: {α : Type ?u.3536} → α → Option αsome a: αa).iget: {α : Type ?u.3538} → [inst : Inhabited α] → Option α → αiget = a: αa :=
rfl: ∀ {α : Sort ?u.3554} {a : α}, a = arfl
#align option.iget_some Option.iget_some: ∀ {α : Type u_1} [inst : Inhabited α] {a : α}, iget (some a) = aOption.iget_some

@[simp]
theorem mem_toList: ∀ {α : Type u_1} {a : α} {o : Option α}, a ∈ toList o ↔ a ∈ omem_toList {a: αa : α: Type ?u.3573α} {o: Option αo : Option: Type ?u.3581 → Type ?u.3581Option α: Type ?u.3573α} : a: αa ∈ toList: {α : Type ?u.3589} → Option α → List αtoList o: Option αo ↔ a: αa ∈ o: Option αo := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.3576a: αo: Option αa ∈ toList o ↔ a ∈ ocases o: Option αoα: Type u_1β: Type ?u.3576a: αnonea ∈ toList none ↔ a ∈ noneα: Type u_1β: Type ?u.3576a, val✝: αsomea ∈ toList (some val✝) ↔ a ∈ some val✝ α: Type u_1β: Type ?u.3576a: αo: Option αa ∈ toList o ↔ a ∈ o<;>α: Type u_1β: Type ?u.3576a: αnonea ∈ toList none ↔ a ∈ noneα: Type u_1β: Type ?u.3576a, val✝: αsomea ∈ toList (some val✝) ↔ a ∈ some val✝ α: Type u_1β: Type ?u.3576a: αo: Option αa ∈ toList o ↔ a ∈ osimp [toList: {α : Type ?u.3819} → Option α → List αtoList, eq_comm: ∀ {α : Sort ?u.3821} {a b : α}, a = b ↔ b = aeq_comm]Goals accomplished! 🐙
#align option.mem_to_list Option.mem_toList: ∀ {α : Type u_1} {a : α} {o : Option α}, a ∈ toList o ↔ a ∈ oOption.mem_toList

instance liftOrGet_isCommutative: ∀ (f : α → α → α) [inst : IsCommutative α f], IsCommutative (Option α) (liftOrGet f)liftOrGet_isCommutative (f: α → α → αf : α: Type ?u.3969α → α: Type ?u.3969α → α: Type ?u.3969α) [IsCommutative: (α : Type ?u.3981) → (α → α → α) → PropIsCommutative α: Type ?u.3969α f: α → α → αf] :
IsCommutative: (α : Type ?u.3986) → (α → α → α) → PropIsCommutative (Option: Type ?u.3987 → Type ?u.3987Option α: Type ?u.3969α) (liftOrGet: {α : Type ?u.3988} → (α → α → α) → Option α → Option α → Option αliftOrGet f: α → α → αf) :=
⟨fun a: ?m.4023a b: ?m.4026b ↦ byGoals accomplished! 🐙 α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fa, b: Option αliftOrGet f a b = liftOrGet f b acases a: Option αaα: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fb: Option αnoneliftOrGet f none b = liftOrGet f b noneα: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fb: Option αval✝: αsomeliftOrGet f (some val✝) b = liftOrGet f b (some val✝) α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fa, b: Option αliftOrGet f a b = liftOrGet f b a<;>α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fb: Option αnoneliftOrGet f none b = liftOrGet f b noneα: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fb: Option αval✝: αsomeliftOrGet f (some val✝) b = liftOrGet f b (some val✝) α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fa, b: Option αliftOrGet f a b = liftOrGet f b acases b: Option αbα: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fval✝: αsome.noneliftOrGet f (some val✝) none = liftOrGet f none (some val✝)α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fval✝¹, val✝: αsome.someliftOrGet f (some val✝¹) (some val✝) = liftOrGet f (some val✝) (some val✝¹) α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fa, b: Option αliftOrGet f a b = liftOrGet f b a<;>α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fnone.noneliftOrGet f none none = liftOrGet f none noneα: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fval✝: αnone.someliftOrGet f none (some val✝) = liftOrGet f (some val✝) noneα: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fval✝: αsome.noneliftOrGet f (some val✝) none = liftOrGet f none (some val✝)α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fval✝¹, val✝: αsome.someliftOrGet f (some val✝¹) (some val✝) = liftOrGet f (some val✝) (some val✝¹) α: Type ?u.3969β: Type ?u.3972f: α → α → αinst✝: IsCommutative α fa, b: Option αliftOrGet f a b = liftOrGet f b asimp [liftOrGet: {α : Type ?u.4393} → (α → α → α) → Option α → Option α → Option αliftOrGet, IsCommutative.comm: ∀ {α : Type ?u.4395} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b aIsCommutative.comm]Goals accomplished! 🐙⟩

instance liftOrGet_isAssociative: ∀ (f : α → α → α) [inst : IsAssociative α f], IsAssociative (Option α) (liftOrGet f)liftOrGet_isAssociative (f: α → α → αf : α: Type ?u.4687α → α: Type ?u.4687α → α: Type ?u.4687α) [IsAssociative: (α : Type ?u.4699) → (α → α → α) → PropIsAssociative α: Type ?u.4687α f: α → α → αf] :
IsAssociative: (α : Type ?u.4704) → (α → α → α) → PropIsAssociative (Option: Type ?u.4705 → Type ?u.4705Option α: Type ?u.4687α) (liftOrGet: {α : Type ?u.4706} → (α → α → α) → Option α → Option α → Option αliftOrGet f: α → α → αf) :=
⟨fun a: ?m.4741a b: ?m.4744b c: ?m.4747c ↦ byGoals accomplished! 🐙 α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fa, b, c: Option αliftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)cases a: Option αaα: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fb, c: Option αnoneliftOrGet f (liftOrGet f none b) c = liftOrGet f none (liftOrGet f b c)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fb, c: Option αval✝: αsomeliftOrGet f (liftOrGet f (some val✝) b) c = liftOrGet f (some val✝) (liftOrGet f b c) α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fa, b, c: Option αliftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)<;>α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fb, c: Option αnoneliftOrGet f (liftOrGet f none b) c = liftOrGet f none (liftOrGet f b c)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fb, c: Option αval✝: αsomeliftOrGet f (liftOrGet f (some val✝) b) c = liftOrGet f (some val✝) (liftOrGet f b c) α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fa, b, c: Option αliftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)cases b: Option αbα: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fc: Option αnone.noneliftOrGet f (liftOrGet f none none) c = liftOrGet f none (liftOrGet f none c)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fc: Option αval✝: αnone.someliftOrGet f (liftOrGet f none (some val✝)) c = liftOrGet f none (liftOrGet f (some val✝) c) α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fa, b, c: Option αliftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)<;>α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fc: Option αnone.noneliftOrGet f (liftOrGet f none none) c = liftOrGet f none (liftOrGet f none c)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fc: Option αval✝: αnone.someliftOrGet f (liftOrGet f none (some val✝)) c = liftOrGet f none (liftOrGet f (some val✝) c)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fc: Option αval✝: αsome.noneliftOrGet f (liftOrGet f (some val✝) none) c = liftOrGet f (some val✝) (liftOrGet f none c)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fc: Option αval✝¹, val✝: αsome.someliftOrGet f (liftOrGet f (some val✝¹) (some val✝)) c = liftOrGet f (some val✝¹) (liftOrGet f (some val✝) c) α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fa, b, c: Option αliftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)cases c: Option αcα: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝: αsome.none.noneliftOrGet f (liftOrGet f (some val✝) none) none = liftOrGet f (some val✝) (liftOrGet f none none)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝¹, val✝: αsome.none.someliftOrGet f (liftOrGet f (some val✝¹) none) (some val✝) = liftOrGet f (some val✝¹) (liftOrGet f none (some val✝)) α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fa, b, c: Option αliftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)<;>α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fnone.none.noneliftOrGet f (liftOrGet f none none) none = liftOrGet f none (liftOrGet f none none)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝: αnone.none.someliftOrGet f (liftOrGet f none none) (some val✝) = liftOrGet f none (liftOrGet f none (some val✝))α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝: αnone.some.noneliftOrGet f (liftOrGet f none (some val✝)) none = liftOrGet f none (liftOrGet f (some val✝) none)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝¹, val✝: αnone.some.someliftOrGet f (liftOrGet f none (some val✝¹)) (some val✝) = liftOrGet f none (liftOrGet f (some val✝¹) (some val✝))α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝: αsome.none.noneliftOrGet f (liftOrGet f (some val✝) none) none = liftOrGet f (some val✝) (liftOrGet f none none)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝¹, val✝: αsome.none.someliftOrGet f (liftOrGet f (some val✝¹) none) (some val✝) = liftOrGet f (some val✝¹) (liftOrGet f none (some val✝))α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝¹, val✝: αsome.some.noneliftOrGet f (liftOrGet f (some val✝¹) (some val✝)) none = liftOrGet f (some val✝¹) (liftOrGet f (some val✝) none)α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fval✝², val✝¹, val✝: αsome.some.someliftOrGet f (liftOrGet f (some val✝²) (some val✝¹)) (some val✝) =   liftOrGet f (some val✝²) (liftOrGet f (some val✝¹) (some val✝)) α: Type ?u.4687β: Type ?u.4690f: α → α → αinst✝: IsAssociative α fa, b, c: Option αliftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)simp [liftOrGet: {α : Type ?u.7575} → (α → α → α) → Option α → Option α → Option αliftOrGet, IsAssociative.assoc: ∀ {α : Type ?u.8987} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)IsAssociative.assoc]Goals accomplished! 🐙⟩

instance liftOrGet_isIdempotent: ∀ (f : α → α → α) [inst : IsIdempotent α f], IsIdempotent (Option α) (liftOrGet f)liftOrGet_isIdempotent (f: α → α → αf : α: Type ?u.11257α → α: Type ?u.11257α → α: Type ?u.11257α) [IsIdempotent: (α : Type ?u.11269) → (α → α → α) → PropIsIdempotent α: Type ?u.11257α f: α → α → αf] :
IsIdempotent: (α : Type ?u.11274) → (α → α → α) → PropIsIdempotent (Option: Type ?u.11275 → Type ?u.11275Option α: Type ?u.11257α) (liftOrGet: {α : Type ?u.11276} → (α → α → α) → Option α → Option α → Option αliftOrGet f: α → α → αf) :=
⟨fun a: ?m.11311a ↦ byGoals accomplished! 🐙 α: Type ?u.11257β: Type ?u.11260f: α → α → αinst✝: IsIdempotent α fa: Option αliftOrGet f a a = acases a: Option αaα: Type ?u.11257β: Type ?u.11260f: α → α → αinst✝: IsIdempotent α fnoneliftOrGet f none none = noneα: Type ?u.11257β: Type ?u.11260f: α → α → αinst✝: IsIdempotent α fval✝: αsomeliftOrGet f (some val✝) (some val✝) = some val✝ α: Type ?u.11257β: Type ?u.11260f: α → α → αinst✝: IsIdempotent α fa: Option αliftOrGet f a a = a<;>α: Type ?u.11257β: Type ?u.11260f: α → α → αinst✝: IsIdempotent α fnoneliftOrGet f none none = noneα: Type ?u.11257β: Type ?u.11260f: α → α → αinst✝: IsIdempotent α fval✝: αsomeliftOrGet f (some val✝) (some val✝) = some val✝ α: Type ?u.11257β: Type ?u.11260f: α → α → αinst✝: IsIdempotent α fa: Option αliftOrGet f a a = asimp [liftOrGet: {α : Type ?u.11456} → (α → α → α) → Option α → Option α → Option αliftOrGet, IsIdempotent.idempotent: ∀ {α : Type ?u.11458} {op : α → α → α} [self : IsIdempotent α op] (a : α), op a a = aIsIdempotent.idempotent]Goals accomplished! 🐙⟩

instance liftOrGet_isLeftId: ∀ {α : Type u_1} (f : α → α → α), IsLeftId (Option α) (liftOrGet f) noneliftOrGet_isLeftId (f: α → α → αf : α: Type ?u.11597α → α: Type ?u.11597α → α: Type ?u.11597α) : IsLeftId: (α : Type ?u.11609) → (α → α → α) → outParam α → PropIsLeftId (Option: Type ?u.11610 → Type ?u.11610Option α: Type ?u.11597α) (liftOrGet: {α : Type ?u.11611} → (α → α → α) → Option α → Option α → Option αliftOrGet f: α → α → αf) none: {α : Type ?u.11630} → Option αnone :=
⟨fun a: ?m.11650a ↦ byGoals accomplished! 🐙 α: Type ?u.11597β: Type ?u.11600f: α → α → αa: Option αliftOrGet f none a = acases a: Option αaα: Type ?u.11597β: Type ?u.11600f: α → α → αnoneliftOrGet f none none = noneα: Type ?u.11597β: Type ?u.11600f: α → α → αval✝: αsomeliftOrGet f none (some val✝) = some val✝ α: Type ?u.11597β: Type ?u.11600f: α → α → αa: Option αliftOrGet f none a = a<;>α: Type ?u.11597β: Type ?u.11600f: α → α → αnoneliftOrGet f none none = noneα: Type ?u.11597β: Type ?u.11600f: α → α → αval✝: αsomeliftOrGet f none (some val✝) = some val✝ α: Type ?u.11597β: Type ?u.11600f: α → α → αa: Option αliftOrGet f none a = asimp [liftOrGet: {α : Type ?u.11748} → (α → α → α) → Option α → Option α → Option αliftOrGet]Goals accomplished! 🐙⟩

instance liftOrGet_isRightId: ∀ (f : α → α → α), IsRightId (Option α) (liftOrGet f) noneliftOrGet_isRightId (f: α → α → αf : α: Type ?u.11807α → α: Type ?u.11807α → α: Type ?u.11807α) : IsRightId: (α : Type ?u.11819) → (α → α → α) → outParam α → PropIsRightId (Option: Type ?u.11820 → Type ?u.11820Option α: Type ?u.11807α) (liftOrGet: {α : Type ?u.11821} → (α → α → α) → Option α → Option α → Option αliftOrGet f: α → α → αf) none: {α : Type ?u.11840} → Option αnone :=
⟨fun a: ?m.11860a ↦ byGoals accomplished! 🐙 α: Type ?u.11807β: Type ?u.11810f: α → α → αa: Option αliftOrGet f a none = acases a: Option αaα: Type ?u.11807β: Type ?u.11810f: α → α → αnoneliftOrGet f none none = noneα: Type ?u.11807β: Type ?u.11810f: α → α → αval✝: αsomeliftOrGet f (some val✝) none = some val✝ α: Type ?u.11807β: Type ?u.11810f: α → α → αa: Option αliftOrGet f a none = a<;>α: Type ?u.11807β: Type ?u.11810f: α → α → αnoneliftOrGet f none none = noneα: Type ?u.11807β: Type ?u.11810f: α → α → αval✝: αsomeliftOrGet f (some val✝) none = some val✝ α: Type ?u.11807β: Type ?u.11810f: α → α → αa: Option αliftOrGet f a none = asimp [liftOrGet: {α : Type ?u.11958} → (α → α → α) → Option α → Option α → Option αliftOrGet]Goals accomplished! 🐙⟩

#align option.lift_or_get_comm Option.liftOrGet_isCommutative: ∀ {α : Type u_1} (f : α → α → α) [inst : IsCommutative α f], IsCommutative (Option α) (liftOrGet f)Option.liftOrGet_isCommutative
#align option.lift_or_get_assoc Option.liftOrGet_isAssociative: ∀ {α : Type u_1} (f : α → α → α) [inst : IsAssociative α f], IsAssociative (Option α) (liftOrGet f)Option.liftOrGet_isAssociative
#align option.lift_or_get_idem Option.liftOrGet_isIdempotent: ∀ {α : Type u_1} (f : α → α → α) [inst : IsIdempotent α f], IsIdempotent (Option α) (liftOrGet f)Option.liftOrGet_isIdempotent
#align option.lift_or_get_is_left_id Option.liftOrGet_isLeftId: ∀ {α : Type u_1} (f : α → α → α), IsLeftId (Option α) (liftOrGet f) noneOption.liftOrGet_isLeftId
#align option.lift_or_get_is_right_id Option.liftOrGet_isRightId: ∀ {α : Type u_1} (f : α → α → α), IsRightId (Option α) (liftOrGet f) noneOption.liftOrGet_isRightId
```