Init.Data.Option.Lemmas

theorem mem_iff {a : α} {b : Option α} : a ∈ ba ∈ b ↔ b = some a := .rfl

theorem mem_some {a b : α} : a ∈ some ba ∈ some b ↔ b = a := by simp

theorem mem_some_self (a : α) : a ∈ some a := mem_some.2 rfl

theorem some_ne_none (x : α) : somesome x ≠ none := nofun

protected theorem «forall» {p : Option α → Prop} : (∀ x, p x) ↔ p none ∧ ∀ x, p (some x) :=
  ⟨fun h => ⟨h _, fun _ => h _⟩, fun h x => Option.casesOn x h.1 h.2⟩

protected theorem «exists» {p : Option α → Prop} :
    (∃ x, p x) ↔ p none ∨ ∃ x, p (some x) :=
  ⟨fun | ⟨none, hx⟩ => .inl hx | ⟨some x, hx⟩ => .inr ⟨x, hx⟩,
   fun | .inl h => ⟨_, h⟩ | .inr ⟨_, hx⟩ => ⟨_, hx⟩⟩

theorem get_mem : ∀ {o : Option α} (h : isSome o), o.get h ∈ o
  | some _, _ => rfl

theorem get_of_mem : ∀ {o : Option α} (h : isSome o), a ∈ o → o.get h = a
  | _, _, rfl => rfl

@[simp] theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun

theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x := by
  cases x; {contradiction}; rw [getD_some]

theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b ↔ (o = some b ∨ o = none ∧ a = b) := by
  cases o <;> simp

@[simp] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl

@[simp] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl

theorem get_eq_get! [Inhabited α] : (o : Option α) → {h : o.isSome} → o.get h = o.get!
  | some _, _ => rfl

theorem get_eq_getD {fallback : α} : (o : Option α) → {h : o.isSome} → o.get h = o.getD fallback
  | some _, _ => rfl

theorem some_get! [Inhabited α] : (o : Option α) → o.isSome → some (o.get!) = o
  | some _, _ => rfl

theorem get!_eq_getD [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl

@[deprecated get!_eq_getD (since := "2024-11-18")] abbrev get!_eq_getD_default := @get!_eq_getD

theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
  some.inj <| ha ▸ hb

@[ext] theorem ext : ∀ {o₁ o₂ : Option α}, (∀ a, a ∈ o₁a ∈ o₁ ↔ a ∈ o₂) → o₁ = o₂
  | none, none, _ => rfl
  | some _, _, H => ((H _).1 rfl).symm
  | _, some _, H => (H _).2 rfl

theorem isSome_iff_exists : isSomeisSome x ↔ ∃ a, x = some a := by cases x <;> simp [isSome]

theorem isSome_eq_isSome : (isSome x = isSome y) ↔ (x = none ↔ y = none) := by
  cases x <;> cases y <;> simp

@[simp] theorem not_isSome : isSomeisSome a = false ↔ a.isNone = true := by
  cases a <;> simp

theorem isSome_iff_ne_none : o.isSome ↔ o ≠ none := by
  cases o <;> simp

theorem not_isSome_iff_eq_none : ¬o.isSome¬o.isSome ↔ o = none := by
  cases o <;> simp

theorem ne_none_iff_isSome : o ≠ noneo ≠ none ↔ o.isSome := by cases o <;> simp

theorem ne_none_iff_exists : o ≠ noneo ≠ none ↔ ∃ x, some x = o := by cases o <;> simp

theorem ne_none_iff_exists' : o ≠ noneo ≠ none ↔ ∃ x, o = some x :=
  ne_none_iff_exists.trans <| exists_congr fun _ => eq_comm

theorem bex_ne_none {p : Option α → Prop} : (∃ x, ∃ (_ : x ≠ none), p x) ↔ ∃ x, p (some x) :=
  ⟨fun ⟨x, hx, hp⟩ => ⟨x.get <| ne_none_iff_isSome.1 hx, by rwa [some_get]⟩,
    fun ⟨x, hx⟩ => ⟨some x, some_ne_none x, hx⟩⟩

theorem ball_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x) ↔ ∀ x, p (some x) :=
  ⟨fun h x => h (some x) (some_ne_none x),
    fun h x hx => by
      have := h <| x.get <| ne_none_iff_isSome.1 hx
      simp [some_get] at this ⊢
      exact this⟩

@[simp] theorem pure_def : pure = @some α := rfl

@[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl

@[simp] theorem bind_some (x : Option α) : x.bind some = x := by cases x <;> rfl

@[simp] theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
  cases x <;> rfl

theorem bind_eq_some : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by
  cases x <;> simp

@[simp] theorem bind_eq_none {o : Option α} {f : α → Option β} :
    o.bind f = none ↔ ∀ a, o = some a → f a = none := by cases o <;> simp

theorem bind_eq_none' {o : Option α} {f : α → Option β} :
    o.bind f = none ↔ ∀ b a, a ∈ o → b ∉ f a := by
  simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]

theorem mem_bind_iff {o : Option α} {f : α → Option β} :
    b ∈ o.bind fb ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
  cases o <;> simp

theorem bind_comm {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 := by
  cases a <;> cases b <;> rfl

theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) :
    (x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl

theorem bind_congr {α β} {o : Option α} {f g : α → Option β} :
    (h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by
  cases o <;> simp

theorem join_eq_some : x.join = some a ↔ x = some (some a) := by
  simp [bind_eq_some]

theorem join_ne_none : x.join ≠ nonex.join ≠ none ↔ ∃ z, x = some (some z) := by
  simp only [ne_none_iff_exists', join_eq_some, iff_self]

theorem join_ne_none' : ¬x.join = none¬x.join = none ↔ ∃ z, x = some (some z) :=
  join_ne_none

theorem join_eq_none : o.join = none ↔ o = none ∨ o = some none :=
  match o with | none | some none | some (some _) => by simp

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

@[simp] theorem map_eq_map : Functor.map f = Option.map f := rfl

theorem map_none : f <$> none = none := rfl

theorem map_some : f <$> some a = some (f a) := rfl

@[simp] theorem map_eq_some' : x.map f = some b ↔ ∃ a, x = some a ∧ f a = b := by cases x <;> simp

theorem map_eq_some : f <$> xf <$> x = some b ↔ ∃ a, x = some a ∧ f a = b := map_eq_some'

@[simp] theorem map_eq_none' : x.map f = none ↔ x = none := by
  cases x <;> simp [map_none', map_some', eq_self_iff_true]

theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by
  cases x <;> simp

@[simp] theorem isSome_map' {x : Option α} : (x.map f).isSome = x.isSome := by
  cases x <;> simp

@[simp] theorem isNone_map' {x : Option α} : (x.map f).isNone = x.isNone := by
  cases x <;> simp

theorem map_eq_none : f <$> xf <$> x = none ↔ x = none := map_eq_none'

theorem map_eq_bind {x : Option α} : x.map f = x.bind (somesome ∘ f) := by
  cases x <;> simp [Option.bind]

theorem map_congr {x : Option α} (h : ∀ a, a ∈ x → f a = g a) : x.map f = x.map g := by
  cases x <;> simp only [map_none', map_some', h, mem_def]

@[simp] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
  funext; simp [map_id]

theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x

@[simp] theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id := by
  funext; simp [map_id']

theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
    (o.map f).get h = f (o.get (by simpa using h)) := by
  cases o with
  | none => simp at h
  | some a => simp

@[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
    (x.map g).map h = x.map (h ∘ g) := by
  cases x <;> simp only [map_none', map_some', ·∘·]

theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ g) = (x.map g).map h :=
  (map_map ..).symm

@[simp] theorem map_comp_map (f : α → β) (g : β → γ) :
    Option.mapOption.map g ∘ Option.map f = Option.map (g ∘ f) := by funext x; simp

theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some' ..

theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y → x = y) :
    o.map f = o'.map f ↔ o = o' := by
  cases o with
  | none => cases o' <;> simp
  | some a =>
    cases o' with
    | none => simp
    | some a' => simpa using ⟨fun h => w _ _ h, fun h => congrArg f h⟩

@[simp] theorem map_if {f : α → β} [Decidable c] :
     (if c then some a else none).map f = if c then some (f a) else none := by
  split <;> rfl

@[simp] theorem map_dif {f : α → β} [Decidable c] {a : c → α} :
     (if h : c then some (a h) else none).map f = if h : c then some (f (a h)) else none := by
  split <;> rfl

@[simp] theorem filter_none (p : α → Bool) : none.filter p = none := rfl

theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl

theorem isSome_of_isSome_filter (p : α → Bool) (o : Option α) (h : (o.filter p).isSome) :
    o.isSome := by
  cases o <;> simp at h ⊢

@[deprecated isSome_of_isSome_filter (since := "2025-03-18")]
abbrev isSome_filter_of_isSome := @isSome_of_isSome_filter

@[simp] theorem filter_eq_none {p : α → Bool} :
    o.filter p = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
  cases o <;> simp [filter_some]

@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} :
    o.filter p = some a ↔ a ∈ o ∧ p a := by
  cases o with
  | none => simp
  | some a =>
    simp [filter_some]
    split <;> rename_i h
    · simp only [some.injEq, iff_self_and]
      rintro rfl
      exact h
    · simp only [reduceCtorEq, false_iff, not_and, Bool.not_eq_true]
      rintro rfl
      simpa using h

theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
    a ∈ o.filter pa ∈ o.filter p ↔ a ∈ o ∧ p a := by
  simp

@[simp] theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
    Option.all q (guard p a) = (!p a!p a || q a) := by
  simp only [guard]
  split <;> simp_all

@[simp] theorem any_guard (p : α → Prop) [DecidablePred p] (a : α) :
    Option.any q (guard p a) = (p a && q a) := by
  simp only [guard]
  split <;> simp_all

theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
    x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp

theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
    (x.map f).bind g = x.bind (g ∘ f) := by cases x <;> simp

@[simp] theorem map_bind {f : α → Option β} {g : β → γ} {x : Option α} :
    (x.bind f).map g = x.bind (Option.mapOption.map g ∘ f) := by cases x <;> simp

theorem join_map_eq_map_join {f : α → β} {x : Option (Option α)} :
    (x.map (Option.map f)).join = x.join.map f := by cases x <;> simp

theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join).join := by
  cases x <;> simp

theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a ∈ x.join) : somesome a ∈ x :=
  h.symm ▸ join_eq_some.1 h

@[simp] theorem some_orElse (a : α) (x : Option α) : (some a <|> x) = some a := rfl

@[simp] theorem none_orElse (x : Option α) : (none <|> x) = x := rfl

@[simp] theorem orElse_none (x : Option α) : (x <|> none) = x := by cases x <;> rfl

theorem map_orElse {x y : Option α} : (x <|> y).map f = (x.map f <|> y.map f) := by
  cases x <;> simp

@[simp] theorem guard_eq_some [DecidablePred p] : guardguard p a = some b ↔ a = b ∧ p a :=
  if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]

@[simp] theorem isSome_guard [DecidablePred p] : (Option.guard p a).isSome ↔ p a :=
  if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]

@[deprecated isSome_guard (since := "2025-03-18")]
abbrev guard_isSome := @isSome_guard

@[simp] theorem guard_eq_none [DecidablePred p] : Option.guardOption.guard p a = none ↔ ¬ p a :=
  if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]

@[simp] theorem guard_pos [DecidablePred p] (h : p a) : Option.guard p a = some a := by
  simp [Option.guard, h]

@[congr] theorem guard_congr {f g : α → Prop} [DecidablePred f] [DecidablePred g]
    (h : ∀ a, f a ↔ g a):
    guard f = guard g := by
  funext a
  simp [guard, h]

@[simp] theorem guard_false {α} :
    guard (fun (_ : α) => False) = fun _ => none := by
  funext a
  simp [guard]

@[simp] theorem guard_true {α} :
    guard (fun (_ : α) => True) = some := by
  funext a
  simp [guard]

theorem guard_comp {p : α → Prop} [DecidablePred p] {f : β → α} :
    guardguard p ∘ f = Option.mapOption.map f ∘ guard (p ∘ f) := by
  ext1 b
  simp [guard]

theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
    ∀ o₁ o₂, liftOrGetliftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
  | none, none => .inl rfl
  | some _, none => .inl rfl
  | none, some _ => .inr rfl
  | some a, some b => by have := h a b; simp [liftOrGet] at this ⊢; exact this

@[simp] theorem liftOrGet_none_left {f} {b : Option α} : liftOrGet f none b = b := by
  cases b <;> rfl

@[simp] theorem liftOrGet_none_right {f} {a : Option α} : liftOrGet f a none = a := by
  cases a <;> rfl

@[simp] theorem liftOrGet_some_some {f} {a b : α} :
  liftOrGet f (some a) (some b) = f a b := rfl

@[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl

@[simp] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl

@[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
  (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl

/--
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`.
-/
noncomputable def choice (α : Type _) : Option α :=
  if h : Nonempty α then some (Classical.choice h) else none

theorem choice_eq {α : Type _} [Subsingleton α] (a : α) : choice α = some a := by
  simp [choice]
  rw [dif_pos (⟨a⟩ : Nonempty α)]
  simp; apply Subsingleton.elim

theorem isSome_choice_iff_nonempty {α : Type _} : (choice α).isSome ↔ Nonempty α :=
  ⟨fun h => ⟨(choice α).get h⟩, fun h => by simp only [choice, dif_pos h, isSome_some]⟩

@[deprecated isSome_choice_iff_nonempty (since := "2025-03-18")]
abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty

@[simp] theorem toList_some (a : α) : (a : Option α).toList = [a] := rfl

@[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl

@[simp] theorem some_or : (some a).or o = some a := rfl

@[simp] theorem none_or : none.or o = o := rfl

theorem or_eq_right_of_none {o o' : Option α} (h : o = none) : o.or o' = o' := by
  cases h; simp

@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl

/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
@[simp] theorem or_some' {o : Option α} : o.or (some a) = o.getD a := by
  cases o <;> rfl

theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
  cases o <;> rfl

@[simp] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
  cases o <;> rfl

@[simp] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
  cases o <;> rfl

@[simp] theorem or_eq_none : oror o o' = none ↔ o = none ∧ o' = none := by
  cases o <;> simp

@[simp] theorem or_eq_some : oror o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a) := by
  cases o <;> simp

theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
  cases o₁ <;> cases o₂ <;> rfl

instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩

@[simp]
theorem or_none : or o none = o := by
  cases o <;> rfl

theorem or_eq_left_of_none {o o' : Option α} (h : o' = none) : o.or o' = o := by
  cases h; simp

instance : Std.LawfulIdentity (or (α := α)) none where
  left_id := @none_or _
  right_id := @or_none _

@[simp]
theorem or_self : or o o = o := by
  cases o <;> rfl

instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩

theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
  cases o <;> rfl

theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o') := by
  cases o <;> rfl

theorem map_or' : (or o o').map f = (o.map f).or (o'.map f) := by
  cases o <;> rfl

theorem or_of_isSome {o o' : Option α} (h : o.isSome) : o.or o' = o := by
  match o, h with
  | some _, _ => simp

theorem or_of_isNone {o o' : Option α} (h : o.isNone) : o.or o' = o' := by
  match o, h with
  | none, _ => simp

@[simp] theorem none_beq_none : ((none : Option α) == none) = true := rfl

@[simp] theorem none_beq_some (a : α) : ((none : Option α) == some a) = false := rfl

@[simp] theorem some_beq_none (a : α) : ((some a : Option α) == none) = false := rfl

@[simp] theorem some_beq_some {a b : α} : (some a == some b) = (a == b) := rfl

@[simp] theorem reflBEq_iff : ReflBEqReflBEq (Option α) ↔ ReflBEq α := by
  constructor
  · intro h
    constructor
    intro a
    suffices (some a == some a) = true by
      simpa only [some_beq_some]
    simp
  · intro h
    constructor
    · rintro (_ | a) <;> simp

@[simp] theorem lawfulBEq_iff : LawfulBEqLawfulBEq (Option α) ↔ LawfulBEq α := by
  constructor
  · intro h
    constructor
    · intro a b h
      apply Option.some.inj
      apply eq_of_beq
      simpa
    · intro a
      suffices (some a == some a) = true by
        simpa only [some_beq_some]
      simp
  · intro h
    constructor
    · intro a b h
      simpa using h
    · intro a
      simp

@[simp] theorem dite_none_left_eq_some {p : Prop} [Decidable p] {b : ¬p → Option β} :
    (if h : p then none else b h) = some a ↔ ∃ h, b h = some a := by
  split <;> simp_all

@[simp] theorem dite_none_right_eq_some {p : Prop} [Decidable p] {b : p → Option α} :
    (if h : p then b h else none) = some a ↔ ∃ h, b h = some a := by
  split <;> simp_all

@[simp] theorem some_eq_dite_none_left {p : Prop} [Decidable p] {b : ¬p → Option β} :
    somesome a = (if h : p then none else b h) ↔ ∃ h, some a = b h := by
  split <;> simp_all

@[simp] theorem some_eq_dite_none_right {p : Prop} [Decidable p] {b : p → Option α} :
    somesome a = (if h : p then b h else none) ↔ ∃ h, some a = b h := by
  split <;> simp_all

@[simp] theorem ite_none_left_eq_some {p : Prop} [Decidable p] {b : Option β} :
    (if p then none else b) = some a ↔ ¬ p ∧ b = some a := by
  split <;> simp_all

@[simp] theorem ite_none_right_eq_some {p : Prop} [Decidable p] {b : Option α} :
    (if p then b else none) = some a ↔ p ∧ b = some a := by
  split <;> simp_all

@[simp] theorem some_eq_ite_none_left {p : Prop} [Decidable p] {b : Option β} :
    somesome a = (if p then none else b) ↔ ¬ p ∧ some a = b := by
  split <;> simp_all

@[simp] theorem some_eq_ite_none_right {p : Prop} [Decidable p] {b : Option α} :
    somesome a = (if p then b else none) ↔ p ∧ some a = b := by
  split <;> simp_all

theorem mem_dite_none_left {x : α} [Decidable p] {l : ¬ p → Option α} :
    (x ∈ if h : p then none else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
  simp

theorem mem_dite_none_right {x : α} [Decidable p] {l : p → Option α} :
    (x ∈ if h : p then l h else none) ↔ ∃ h : p, x ∈ l h := by
  simp

theorem mem_ite_none_left {x : α} [Decidable p] {l : Option α} :
    (x ∈ if p then none else l) ↔ ¬ p ∧ x ∈ l := by
  simp

theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
    (x ∈ if p then l else none) ↔ p ∧ x ∈ l := by
  simp

@[simp] theorem isSome_dite {p : Prop} [Decidable p] {b : p → β} :
    (if h : p then some (b h) else none).isSome = true ↔ p := by
  split <;> simpa

@[simp] theorem isSome_ite {p : Prop} [Decidable p] :
    (if p then some b else none).isSome = true ↔ p := by
  split <;> simpa

@[simp] theorem isSome_dite' {p : Prop} [Decidable p] {b : ¬ p → β} :
    (if h : p then none else some (b h)).isSome = true ↔ ¬ p := by
  split <;> simpa

@[simp] theorem isSome_ite' {p : Prop} [Decidable p] :
    (if p then none else some b).isSome = true ↔ ¬ p := by
  split <;> simpa

@[simp] theorem get_dite {p : Prop} [Decidable p] (b : p → β) (w) :
    (if h : p then some (b h) else none).get w = b (by simpa using w) := by
  split
  · simp
  · exfalso
    simp at w
    contradiction

@[simp] theorem get_ite {p : Prop} [Decidable p] (h) :
    (if p then some b else none).get h = b := by
  simpa using get_dite (p := p) (fun _ => b) (by simpa using h)

@[simp] theorem get_dite' {p : Prop} [Decidable p] (b : ¬ p → β) (w) :
    (if h : p then none else some (b h)).get w = b (by simpa using w) := by
  split
  · exfalso
    simp at w
    contradiction
  · simp

@[simp] theorem get_ite' {p : Prop} [Decidable p] (h) :
    (if p then none else some b).get h = b := by
  simpa using get_dite' (p := p) (fun _ => b) (by simpa using h)

@[simp] theorem pbind_none : pbind none f = none := rfl

@[simp] theorem pbind_some : pbind (some a) f = f a (mem_some_self a) := rfl

@[simp] theorem map_pbind {o : Option α} {f : (a : α) → a ∈ o → Option β} {g : β → γ} :
    (o.pbind f).map g = o.pbind (fun a h => (f a h).map g) := by
  cases o <;> simp

@[congr] theorem pbind_congr {o o' : Option α} (ho : o = o')
    {f : (a : α) → a ∈ o → Option β} {g : (a : α) → a ∈ o' → Option β}
    (hf : ∀ a h, f a (ho ▸ h) = g a h) : o.pbind f = o'.pbind g := by
  subst ho
  exact (funext fun a => funext fun h => hf a h) ▸ Eq.refl (o.pbind f)

theorem pbind_eq_none_iff {o : Option α} {f : (a : α) → a ∈ o → Option β} :
    o.pbind f = none ↔ o = none ∨ ∃ a h, f a h = none := by
  cases o with
  | none => simp
  | some a =>
    simp only [pbind_some, reduceCtorEq, mem_def, some.injEq, false_or]
    constructor
    · intro h
      exact ⟨a, rfl, h⟩
    · rintro ⟨a, rfl, h⟩
      exact h

theorem pbind_isSome {o : Option α} {f : (a : α) → a ∈ o → Option β} :
    (o.pbind f).isSome = ∃ a h, (f a h).isSome := by
  cases o with
  | none => simp
  | some a =>
    simp only [pbind_some, mem_def, some.injEq, eq_iff_iff]
    constructor
    · intro h
      exact ⟨a, rfl, h⟩
    · rintro ⟨a, rfl, h⟩
      exact h

theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → a ∈ o → Option β} {b : β} :
    o.pbind f = some b ↔ ∃ a h, f a h = some b := by
  cases o with
  | none => simp
  | some a =>
    simp only [pbind_some, mem_def, some.injEq]
    constructor
    · intro h
      exact ⟨a, rfl, h⟩
    · rintro ⟨a, rfl, h⟩
      exact h

@[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
    pmap f none h = none := rfl

@[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h}:
    pmap f (some a) h = f a (h a (mem_some_self a)) := rfl

@[simp] theorem pmap_eq_none_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
    pmappmap f o h = none ↔ o = none := by
  cases o <;> simp

@[simp] theorem pmap_isSome {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
    (pmap f o h).isSome = o.isSome := by
  cases o <;> simp

@[simp] theorem pmap_eq_some_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
    pmappmap f o h = some b ↔ ∃ (a : α) (h : p a), o = some a ∧ b = f a h := by
  cases o with
  | none => simp
  | some a =>
    simp only [pmap, eq_comm, some.injEq, exists_and_left, exists_eq_left']
    constructor
    · exact fun w => ⟨h a rfl, w⟩
    · rintro ⟨h, rfl⟩
      rfl

@[simp]
theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
    @pmap _ _ p (fun a _ => f a) o H = Option.map f o := by
  cases o <;> simp

theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) :
    Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H := by
  cases o <;> simp

theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) :
    pmap g (o.map f) H =
      pmap (fun a h => g (f a) h) o (fun a m => H (f a) (mem_map_of_mem f m)) := by
  cases o <;> simp

@[simp] theorem pelim_none : pelim none b f = b := rfl

@[simp] theorem pelim_some : pelim (some a) b f = f a rfl := rfl

@[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
  cases o <;> simp

@[simp] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
    (H : ∀ (a : α), a ∈ o → p a) (g : γ) (g' : β → γ) :
    (o.pmap f H).elim g g' =
       o.pelim g (fun a h => g' (f a (H a h))) := by
  cases o <;> simp

@[simp] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]

@[simp] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]

@[simp] theorem some_lt_some [LT α] {a b : α} : somesome a < some b ↔ a < b := by simp [LT.lt, Option.lt]

@[simp] theorem none_le [LE α] {a : Option α} : none ≤ a := by cases a <;> simp [LE.le, Option.le]

@[simp] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le]

@[simp] theorem some_le_some [LE α] {a b : α} : somesome a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le]

theorem min_eq_left [LE α] [Min α] (min_eq_left : ∀ x y : α, x ≤ y → min x y = x)
    {a b : Option α} (h : a ≤ b) : min a b = a := by
  cases a <;> cases b <;> simp_all

theorem min_eq_right [LE α] [Min α] (min_eq_right : ∀ x y : α, y ≤ x → min x y = y)
    {a b : Option α} (h : b ≤ a) : min a b = b := by
  cases a <;> cases b <;> simp_all

theorem min_eq_left_of_lt [LT α] [Min α] (min_eq_left : ∀ x y : α, x < y → min x y = x)
    {a b : Option α} (h : a < b) : min a b = a := by
  cases a <;> cases b <;> simp_all

theorem min_eq_right_of_lt [LT α] [Min α] (min_eq_right : ∀ x y : α, y < x → min x y = y)
    {a b : Option α} (h : b < a) : min a b = b := by
  cases a <;> cases b <;> simp_all

theorem min_eq_or [LE α] [Min α] (min_eq_or : ∀ x y : α, minmin x y = x ∨ min x y = y)
    {a b : Option α} : minmin a b = a ∨ min a b = b := by
  cases a <;> cases b <;> simp_all

theorem min_le_left [LE α] [Min α] (min_le_left : ∀ x y : α, min x y ≤ x)
    {a b : Option α} : min a b ≤ a := by
  cases a <;> cases b <;> simp_all

theorem min_le_right [LE α] [Min α] (min_le_right : ∀ x y : α, min x y ≤ y)
    {a b : Option α} : min a b ≤ b := by
  cases a <;> cases b <;> simp_all

theorem le_min [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 := by
  cases a <;> cases b <;> cases c <;> simp_all

theorem max_eq_left [LE α] [Max α] (max_eq_left : ∀ x y : α, x ≤ y → max x y = y)
    {a b : Option α} (h : a ≤ b) : max a b = b := by
  cases a <;> cases b <;> simp_all

theorem max_eq_right [LE α] [Max α] (max_eq_right : ∀ x y : α, y ≤ x → max x y = x)
    {a b : Option α} (h : b ≤ a) : max a b = a := by
  cases a <;> cases b <;> simp_all

theorem max_eq_left_of_lt [LT α] [Max α] (max_eq_left : ∀ x y : α, x < y → max x y = y)
    {a b : Option α} (h : a < b) : max a b = b := by
  cases a <;> cases b <;> simp_all

theorem max_eq_right_of_lt [LT α] [Max α] (max_eq_right : ∀ x y : α, y < x → max x y = x)
    {a b : Option α} (h : b < a) : max a b = a := by
  cases a <;> cases b <;> simp_all

theorem max_eq_or [LE α] [Max α] (max_eq_or : ∀ x y : α, maxmax x y = x ∨ max x y = y)
    {a b : Option α} : maxmax a b = a ∨ max a b = b := by
  cases a <;> cases b <;> simp_all

theorem left_le_max [LE α] [Max α] (le_refl : ∀ x : α, x ≤ x) (left_le_max : ∀ x y : α, x ≤ max x y)
    {a b : Option α} : a ≤ max a b := by
  cases a <;> cases b <;> simp_all

theorem right_le_max [LE α] [Max α] (le_refl : ∀ x : α, x ≤ x) (right_le_max : ∀ x y : α, y ≤ max x y)
    {a b : Option α} : b ≤ max a b := by
  cases a <;> cases b <;> simp_all

theorem max_le [LE α] [Max α] (max_le : ∀ x y z : α, maxmax x y ≤ z ↔ x ≤ z ∧ y ≤ z)
    {a b c : Option α} : maxmax a b ≤ c ↔ a ≤ c ∧ b ≤ c := by
  cases a <;> cases b <;> cases c <;> simp_all