case none
α : Type u_1
β : Type ?u.19034
γ : Type ?u.19037
δ : Type ?u.19040
o' : Option α
x : α
⊢ (HOrElse.hOrElse none fun x => o') = some x ↔ none = some x ∨ none = none ∧ o' = some x

case some
α : Type u_1
β : Type ?u.19034
γ : Type ?u.19037
δ : Type ?u.19040
o' : Option α
x val✝ : α
⊢ (HOrElse.hOrElse (some val✝) fun x => o') = some x ↔ some val✝ = some x ∨ some val✝ = none ∧ o' = some x
α : Type u_1
β : Type ?u.19034
γ : Type ?u.19037
δ : Type ?u.19040
o o' : Option α
x : α
⊢ (HOrElse.hOrElse o fun x => o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
cases o
no goals
case none
α : Type u_1
β : Type ?u.19034
γ : Type ?u.19037
δ : Type ?u.19040
o' : Option α
x : α
⊢ (HOrElse.hOrElse none fun x => o') = some x ↔ none = some x ∨ none = none ∧ o' = some x
simp only [true_and, false_or, eq_self_iff_true, none_orElse]
no goals
case some
α : Type u_1
β : Type ?u.19034
γ : Type ?u.19037
δ : Type ?u.19040
o' : Option α
x val✝ : α
⊢ (HOrElse.hOrElse (some val✝) fun x => o') = some x ↔ some val✝ = some x ∨ some val✝ = none ∧ o' = some x
simp only [some_orElse, or_false, false_and]