diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean
index 24eaf5b01c..cd7afb4a17 100644
--- a/Std/Data/List/Basic.lean
+++ b/Std/Data/List/Basic.lean
@@ -415,8 +415,8 @@ def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
   exact (go #[] _).symm
 
 /-- Inserts an element into a list without duplication. -/
-@[inline] protected def insert [DecidableEq α] (a : α) (l : List α) : List α :=
-  if a ∈ l then l else a :: l
+@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
+  if l.elem a then l else a :: l
 
 /--
 Constructs the union of two lists, by inserting the elements of `l₁` in reverse order to `l₂`.
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 739edbaf51..8e1b5b5523 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -1069,10 +1069,10 @@ section insert
 variable [DecidableEq α]
 
 @[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by
-  simp only [List.insert, if_pos h]
+  simp only [List.insert, elem_iff, if_pos h]
 
 @[simp] theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l := by
-  simp only [List.insert, if_neg h]
+  simp only [List.insert,  elem_iff, if_neg h]
 
 @[simp] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
   if h : b ∈ l then