resolve is_some elegantly

Stream: new members

[Henning Dieterichs]

I have an hypothesis h: ↥(f.is_some). How do I get x: (...) and h: f = some x from it with a single tactic? It works with cases and eliminating the none case, but that is quite involved. I tried rewriting or somehow applying option.get, but that didn't work out. I'm sure that there is a short way!

[Shing Tak Lam]

import data.option.basic

example {α : Type} (f : option α) (h : f.is_some) : true :=
begin
  set x := option.get h,                      -- x : α
  have hx : f = some x := option.get_mem h,   -- hx : f = some x
end

[Henning Dieterichs]

thanks, that makes sense! I don't understand the theorem get_mem though... What does \in mean here?

[Shing Tak Lam]

example {α : Type}  (a : α) (f : option α) : a ∈ f ↔ f = some a := iff.rfl

so a ∈ f is defined to be f = some a

[Henning Dieterichs]

I see. Thanks!