cases x <;> simp [isSome]
α : Sort ?u.13403
p q : α → Prop
α✝ : Type u_1
x : Option α✝
⊢ isSome x = true ↔ ∃ a, x = some a
case some
α : Sort ?u.13403
p q : α → Prop
α✝ : Type u_1
val✝ : α✝
⊢ ∃ a, val✝ = a