Theorem: Option.isSome_iff_exists (Runtime/Utilities/Std.lean)

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

State before:
case some
α : Sort ?u.13403
p q : α → Prop
α✝ : Type u_1
val✝ : α✝
⊢ ∃ a, val✝ = a
Tactic:
exists ‹_›
State after:
no goals