RBTree (Red-Black Tree)
RBTree is a set implemented as a red-black tree. In metaprogramming, Lean provides several "aliases" (pre-defined versions) of RBTree so you don't have to provide the comparison function manually, like NameSet is an alias for RBTree Name Name.quickCmp.
def s1 : NameSet := {}
def s2 := s1.insert `x
def s3 := s2.insert `y
#eval s3.contains `x
#eval s3.toList