Dual to `option.mem_unique`?

Stream: Is there code for X?

[Stuart Presnell]

Do we already have something like this, a kind of dual to docs#option.mem_unique? I tried library_search and it couldn't find anything.

example (o1 o2 : option α) (a : α) (h1 : a ∈ o1) (h2 : a ∈ o2) : o1 = o2 :=
by { rw option.mem_def at *,  exact eq.trans h1 h2.symm }

If not, is it worth adding to data/option/basic? Under what name?

[Johan Commelin]

I would call it docs#option.eq_of_mem_of_mem

[Johan Commelin]

Which doesn't exist yet...

[Stuart Presnell]

#11098

[Mario Carneiro]

it can be written more simply as h1.trans h2.symm

[Mario Carneiro]

I think this theorem is more useful in the one sided form,

example {α} {o : option α} {a : α} (h : a ∈ o) : o = some a := h

[Stuart Presnell]

Ah, h1.trans h2.symm is what I was looking for! I didn't realise I could treat an expression of the form a ∈ o1 like an equality without rewriting it first.

[Stuart Presnell]

In that case I guess eq_of_mem_of_mem (or the one-sided version) is too trivial to be worth naming?

[Yury G. Kudryashov]

I don't mind having option.mem.bi_unique

[Yury G. Kudryashov]

(and option.mem.right_unique)

[Eric Wieser]

I like eq_of_mem_of_mem better as a name.

[Yury G. Kudryashov]

I meant docs#relator.bi_unique