Mem notation

Stream: mathlib4

[Kevin Buzzard]

Help! In mathlib4#8 I port the core Lean 3 file init.data.set, which contains some very basic set stuff (even more basic than mathlib's data.set.basic). I also add a Mem notation class.

I then wanted to get Data.List.Basic using my new Mem notation, so I added import Mathlib.Mem (the notation class) and tried to change infix:50 " ∈ " => mem to instance : Mem α (List α) := ⟨List.mem⟩ but then all the proofs break, because simp doesn't know to unfold something. I suspect there is an easy way to fix this but I couldn't figure it out.