case none
α : Type u_1
β : Type ?u.19607
γ : Type ?u.19610
δ : Type ?u.19613
o' : Option α
⊢ (HOrElse.hOrElse none fun x => o') = none ↔ none = none ∧ o' = none

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