mathlib documentation

core.init.data.option.instances

theorem option.eq_of_eq_some {α : Type u} {x y : option α} :
(∀ (z : α), x = some z y = some z)x = y

theorem option.eq_some_of_is_some {α : Type u} {o : option α} (h : (o.is_some)) :

theorem option.eq_none_of_is_none {α : Type u} {o : option α} :
(o.is_none) → o = none