option lemma

Stream: general

[Patrick Massot]

Is it possible that

@[simp] lemma option.mem_some_iff {α : Type*} {a b : α} : a ∈ some b ↔ b = a :=
by { rw [option.mem_iff], exact option.some_inj }

is missing? @Mario Carneiro ?

[Patrick Massot]

Is there a reason not to do that?

[Yaël Dillies]

I have this lemma on a branch! Definitely useful.

[Patrick Massot]

There is something weird going on. If I try to put this in its natural place then simp does it already

[Adam Topaz]

docs#option.mem_def

[Patrick Massot]

This is not exactly the same

[Adam Topaz]

I know, but that's the lemma that is used by simp, at least on my machine.

[Patrick Massot]

I added the missing lemma without the simp attribute, so it can't hurt.