Lean 4 set notation

Stream: general

[Kevin Buzzard]

In Lean 3 we have to write sets in this slightly funny (to me) way (AFAIK):

def commutator : subgroup α :=
subgroup.normal_closure {x | ∃ p q, p * q * p⁻¹ * q⁻¹ = x}

(link to mathlib source for MWE). This is quite a neat trick: the fact that all the variables have type alpha is inferred. But I want more. In Lean 4, can we have

{p * q * p⁻¹ * q⁻¹} : set X

? In Lean 3??

I didn't even know there was any other Lean 3 notation for sets at all in fact, until someone on the chat (let me know who) pointed out the existence of [set.sep](https://github.com/leanprover-community/lean/blob/05d7184a6642e240e7bc659420267595893ad7bd/library/init/data/set.lean#L34), a notation typeclass making the notation { a ∈ c | p a } work.