add Mem notation for lists (#12)

* add Mem notation for lists

* delete comment

Mathlib/Data/List/Basic.lean

@@ -1,6 +1,6 @@
 import Mathlib.Logic.Basic
 import Mathlib.Data.Nat.Basic
-
+import Mathlib.Mem
 namespace List
 
 /-- The same as append, but with simpler defeq. (The one in the standard library is more efficient,
@@ -48,31 +48,43 @@ def mem (a : α) : List α → Prop
 | [] => False
 | (b :: l) => a = b ∨ mem a l
 
-infix:50 " ∈ " => mem
+instance : Mem α (List α) := ⟨mem⟩
+
+@[simp] lemma mem_nil (a : α) : a ∈ [] ↔ False := Iff.rfl
+
+@[simp] lemma mem_cons {a b : α} {l : List α} :
+  a ∈ (b :: l) ↔ a = b ∨ a ∈ l := Iff.rfl
 
 theorem mem_append {a} : ∀ {l₁ l₂ : List α}, a ∈ l₁ ++ l₂ ↔ a ∈ l₁ ∨ a ∈ l₂
-| [], _ => by simp [mem]
-| b :: l₁, l₂ => by simp only [List.cons_append, mem, or_assoc, mem_append]; exact Iff.rfl
+| [], _ => by simp
+| b :: l₁, l₂ => by simp [or_assoc, mem_append];
 
-theorem mem_map {f : α → β} {b} : ∀ {l}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ b = f a
-| [] => by simp [mem]; intro ⟨_, e⟩; exact e
+@[simp] theorem map_nil {f : α → β} : map f [] = [] := rfl
+@[simp] theorem map_cons {f : α → β} : map f (b :: l) = f b :: l.map f := rfl
+
+theorem mem_map {f : α → β} {b} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ b = f a
+| [] => by simp; intro ⟨_, e⟩; exact e
 | b :: l => by
-  simp only [join, mem, mem_map]
+  rw [map_cons, mem_cons, mem_map];
   exact ⟨fun | Or.inl h => ⟨_, Or.inl rfl, h⟩
              | Or.inr ⟨l, h₁, h₂⟩ => ⟨l, Or.inr h₁, h₂⟩,
          fun | ⟨_, Or.inl rfl, h⟩ => Or.inl h
              | ⟨l, Or.inr h₁, h₂⟩ => Or.inr ⟨l, h₁, h₂⟩⟩
 
+@[simp] theorem join_nil : join ([] : List (List α)) = [] := rfl
+
+@[simp] theorem join_cons : join (a :: l : List (List α)) = a ++ join l := rfl
+
 theorem mem_join {a} : ∀ {L : List (List α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l
-| [] => by simp [mem]; intro ⟨_, e⟩; exact e
+| [] => by simp; intro ⟨_, e⟩; exact e
 | b :: l => by
-  simp only [join, mem, mem_append, mem_join]
+  simp only [join, mem_append, mem_join]
   exact ⟨fun | Or.inl h => ⟨_, Or.inl rfl, h⟩
              | Or.inr ⟨l, h₁, h₂⟩ => ⟨l, Or.inr h₁, h₂⟩,
          fun | ⟨_, Or.inl rfl, h⟩ => Or.inl h
              | ⟨l, Or.inr h₁, h₂⟩ => Or.inr ⟨l, h₁, h₂⟩⟩
 
-theorem mem_bind {f : α → List β} {b} {l} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
+theorem mem_bind {f : α → List β} {b} {l : List α} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
   simp [List.bind, mem_map, mem_join]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩