Exists in hypothesis

Stream: new members

[Trevor Fancher]

If I have the hypothesis h : b ∈ {x : α | P x} and also b : α, then how do I get a new hypothesis of type P b?

[Sebastien Gouezel]

This is just h.

[Sebastien Gouezel]

(If you want to see it, you may dsimp at h)

[Trevor Fancher]

Perfect. Thats exactly what I wanted. I didn't realize I could simp at h or dsimp at h. Thank you.

[Eric Wieser]

docs#set.mem_set_of_eq is the lemma that rewrites your goal to P x

[Trevor Fancher]

Right. I did figure that out because somehow I knew about simp and set_option trace.simplify.rewrite true but not that I could do simp at h.

[Kyle Miller]

Another way you can find the name of that lemma is to use squeeze_simp or simp?

[Eric Wieser]

Also a reminder that ∈ is not "exists" as the thread title suggests, but "mem". Exists is ∃