refactor(data/list): rm redundant eq_nil_of_forall_not_mem

Author: spl

src/data/hash_map.lean

@@ -149,7 +149,7 @@ begin
 end
 
 theorem mk_as_list (n : ℕ+) : bucket_array.as_list (mk_array n.1 [] : bucket_array α β n) = [] :=
-list.eq_nil_of_forall_not_mem $ λ x m,
+list.eq_nil_iff_forall_not_mem.mpr $ λ x m,
 let ⟨i, h⟩ := (bucket_array.mem_as_list _).1 m in h
 
 theorem mk_valid (n : ℕ+) : @valid n (mk_array n.1 []) 0 :=

src/data/list/basic.lean

@@ -44,10 +44,6 @@ assume l₁ l₂, assume Pe, tail_eq_of_cons_eq Pe
 
 /- mem -/
 
-theorem eq_nil_of_forall_not_mem : ∀ {l : list α}, (∀ a, a ∉ l) → l = nil
-| []        := assume h, rfl
-| (b :: l') := assume h, absurd (mem_cons_self b l') (h b)
-
 theorem mem_singleton_self (a : α) : a ∈ [a] := mem_cons_self _ _
 
 theorem eq_of_mem_singleton {a b : α} : a ∈ [b] → a = b :=

src/data/multiset.lean

@@ -165,7 +165,7 @@ e.symm ▸ ⟨(l₁++l₂ : list α), quot.sound perm_middle⟩
 @[simp] theorem not_mem_zero (a : α) : a ∉ (0 : multiset α) := id
 
 theorem eq_zero_of_forall_not_mem {s : multiset α} : (∀x, x ∉ s) → s = 0 :=
-quot.induction_on s $ λ l H, by rw eq_nil_of_forall_not_mem H; refl
+quot.induction_on s $ λ l H, by rw eq_nil_iff_forall_not_mem.mpr H; refl
 
 theorem exists_mem_of_ne_zero {s : multiset α} : s ≠ 0 → ∃ a : α, a ∈ s :=
 quot.induction_on s $ assume l hl,