Extracting props from a set definition

Stream: new members

[VayusElytra]

Hi, I have the following context for a proof:

image.png

How can I extract the properties that hold for x from the hypothesis hmem?

[Kyle Miller]

If you do dsimp at hmem it will likely reduce it to something you'll know how to work with.

[VayusElytra]

It definitely did, thank you very much!

[Kyle Miller]

(If you are comfortable with definitional equality, hmem is the property that holds for x. You can do cases hmem for example since it's an Exists)

[VayusElytra]

Oh interesting, so you're saying hmem is definitionally equivalent to the stuff inside the parentheses? That's curious to me, since I am used to thinking of \in as a function into Prop.

[Kyle Miller]

Yeah, exactly. If you do dsimp? you can see which theorem is used to do the transformation. It's worth doing go-to-definition and inspect it. (By the way, dsimp guarantees that it transforms expressions into definitionally equal expressions.)