Theorem: Option.toList_eq_iff (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
o : Option α
a : α
⊢ o.toList = [a] ↔ o = some a
Tactic:
rcases o <;> simp
State after:
no goals