diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 8a6e6f40eba7..f82839229390 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -481,7 +481,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
   Id.run <| as.allM p start stop
 
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
-  as.any fun b => a == b
+  as.any (· == a)
 
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 2393175685c7..2c10d674065c 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -369,7 +369,7 @@ def replace [BEq α] : List α → α → α → List α
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
-  | b::bs => match a == b with
+  | b::bs => match b == a with
     | true  => true
     | false => elem a bs
 
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 94bc391e93ba..c6e6a4b37382 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -501,8 +501,7 @@ theorem replace_cons [BEq α] {a : α} :
 
 @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
 theorem elem_cons [BEq α] {a : α} :
-    (a::as).elem b = match b == a with | true => true | false => as.elem b :=
-  rfl
+    (a::as).elem b = match a == b with | true => true | false => as.elem b := rfl
 @[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by
   simp [elem_cons]
 
@@ -1338,12 +1337,12 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
 @[simp] theorem contains_nil [BEq α] : ([] : List α).contains a = false := rfl
 
 @[simp] theorem contains_cons [BEq α] :
-    (a :: as : List α).contains x = (x == a || as.contains x) := by
+    (a :: as : List α).contains x = (a == x || as.contains x) := by
   simp only [contains, elem]
   split <;> simp_all
 
-theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
-  induction l with simp | cons b l => cases a == b <;> simp [*]
+theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (· == a) := by
+  induction l with simp | cons b l => cases b == a <;> simp [*]
 
 theorem not_all_eq_any_not (l : List α) (p : α → Bool) : (!l.all p) = l.any fun a => !p a := by
   induction l with simp | cons _ _ ih => rw [ih]
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index b68b2f6c91ef..fd2d08aa2e91 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -914,6 +914,9 @@ is `Bool` valued instead of `Prop` valued, and it also does not have any
 axioms like being reflexive or agreeing with `=`. It is mainly intended for
 programming applications. See `LawfulBEq` for a version that requires that
 `==` and `=` coincide.
+
+Typically we prefer to put the "more variable" term on the left,
+and the "more constant" term on the right.
 -/
 class BEq (α : Type u) where
   /-- Boolean equality, notated as `a == b`. -/
diff --git a/tests/lean/run/wfOverapplicationIssue.lean b/tests/lean/run/wfOverapplicationIssue.lean
index 55dda3ae009c..cacefc89be04 100644
--- a/tests/lean/run/wfOverapplicationIssue.lean
+++ b/tests/lean/run/wfOverapplicationIssue.lean
@@ -1,6 +1,6 @@
 theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by
   simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
-  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
+  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (b = a)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
     unfold anyM.loop
     intro h
     split at h