unfold notations used in set theory

Stream: maths

[tica]

Hello,

On this video at 8:45, a function is shown that allows to unfold the notations for the notations used in set theory.
Do you know what this function is?

Thanks

[Kevin Buzzard]

You mean #whnf? I usually just take the easier option of simply unfolding everything. First do set_option pp.notation false before your declaration and then unfold has_mem.mem set.mem ..., just keep unfolding until you find yourself in a situation where you like what you see.

[tica]

Kevin Buzzard said:

You mean #whnf? I usually just take the easier option of simply unfolding everything. First do set_option pp.notation false before your declaration and then unfold has_mem.mem set.mem ..., just keep unfolding until you find yourself in a situation where you like what you see.

Yes, that's it!
That's what I'm doing now but the function seems to do exactly what I want and in a simpler way...

[Kevin Buzzard]

You only need to unfold each function once to find out its secrets, then you can learn the answer and never do it again. You don't have to do the unfolding because most tactics work up to definitional equality.

[tica]

Ok ok, I'll continue like this.
thanks