case none
α : Type u_1
y : α
hx : none ≠ none
⊢ some (getD none y) = none

case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some (getD (some val✝) y) = some val✝
α : Type u_1
x : Option α
hx : x ≠ none
y : α
⊢ some (getD x y) = x
cases x
case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some (getD (some val✝) y) = some val✝
case none
α : Type u_1
y : α
hx : none ≠ none
⊢ some (getD none y) = none

case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some (getD (some val✝) y) = some val✝
{contradiction}
no goals
case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some (getD (some val✝) y) = some val✝
rw [getD_some]