Zulip Chat Archive

Stream: new members

Topic: Exists in hypothesis


Trevor Fancher (Sep 02 2021 at 17:30):

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 (Sep 02 2021 at 17:32):

This is just h.

Sebastien Gouezel (Sep 02 2021 at 17:32):

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

Trevor Fancher (Sep 02 2021 at 17:34):

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

Eric Wieser (Sep 02 2021 at 17:40):

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

Trevor Fancher (Sep 02 2021 at 17:48):

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 (Sep 02 2021 at 18:13):

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

Eric Wieser (Sep 02 2021 at 18:44):

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


Last updated: Dec 20 2023 at 11:08 UTC