chore: prefer · == a over a == · (#430)

Std/Data/Array/Merge.lean

@@ -110,7 +110,7 @@ where
   go (xs ys : Array α) :=
     let xsSize := xs.size
     ys.foldl (init := xs) fun xs y =>
-      if xs.any (y == ·) (stop := xsSize) then xs else xs.push y
+      if xs.any (· == y) (stop := xsSize) then xs else xs.push y
 
 /--
 Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with

Std/Data/List/Basic.lean

@@ -361,7 +361,7 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
   | a :: l, n => bif p a then n else go l (n + 1)
 
 /-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
-def indexOf [BEq α] (a : α) : List α → Nat := findIdx (a == ·)
+def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
 
 /-- Removes the `n`th element of `l`, or the original list if `n` is out of bounds. -/
 @[simp] def removeNth : List α → Nat → List α
@@ -746,7 +746,7 @@ def findIdx? (p : α → Bool) : List α → (start : Nat := 0) → Option Nat
 | a :: l, i => if p a then some i else findIdx? p l (i + 1)
 
 /-- Return the index of the first occurrence of `a` in the list. -/
-@[inline] def indexOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (a == ·)
+@[inline] def indexOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
 
 /--
 `lookmap` is a combination of `lookup` and `filterMap`.

Std/Data/List/Count.lean

@@ -189,18 +189,20 @@ theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if a =
   split
   exacts [‹a = b› ▸ count_replicate_self .., count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›]
 
-theorem filter_beq' (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a := by
+theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a := by
   simp only [count, countP_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
   exact ⟨trivial, fun _ h => h.2⟩
 
-theorem filter_eq' (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
-  filter_beq' l a
+theorem filter_eq (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
+  filter_beq l a
 
-theorem filter_eq (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
-  simpa only [eq_comm] using filter_eq' l a
+@[deprecated filter_eq]
+theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
+  simpa only [eq_comm] using filter_eq l a
 
-theorem filter_beq (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a :=
-  filter_eq l a
+@[deprecated filter_beq]
+theorem filter_beq' (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a := by
+  simpa only [eq_comm (b := a)] using filter_eq l a
 
 theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l := by
   refine ⟨fun h => ?_, fun h => ?_⟩