fix: simp only [· ∈ ·]

This PR fixes `simp only [· ∈ ·]` after #5020.

Fixes #5905

src/Lean/Elab/BuiltinNotation.lean

@@ -322,7 +322,7 @@ def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
   let stx ← liftMacroM <| expandMacros stx
   match stx with
   | `(fun $binders* => $f $args*) =>
-    if binders == args then
+    if binders.raw.toList.isPerm args.raw.toList then
       try Term.resolveId? f catch _ => return none
     else
       return none
@@ -332,7 +332,7 @@ def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
   | `(fun $binders* => rightact% $f $a $b)
   | `(fun $binders* => binrel% $f $a $b)
   | `(fun $binders* => binrel_no_prop% $f $a $b) =>
-    if binders == #[a, b] then
+    if binders == #[a, b] || binders == #[b, a] then
       try Term.resolveId? f catch _ => return none
     else
       return none

tests/lean/cdotAtSimpArg.lean

@@ -1,25 +0,0 @@
-/-! Test `·` being able to refer to constants in `simp` -/
-
-example : ¬ true = false := by
-  simp [(¬ ·)]
-
-/-! Test `binop%` -/
-
-example (h : y = 0) : x + y = x := by
-  simp [(.+.)] -- Expands `HAdd.hAdd
-  trace_state
-  simp [Add.add]
-  simp [h, Nat.add]
-  done
-
-example (h : y = 0) : x + y = x := by
-  simp [.+.]
-  trace_state
-  simp [Add.add]
-  simp [h, Nat.add]
-  done
-
-/-! Test `binop%` variant `rightact%` as well -/
-
-example (x y : Nat) : x ^ y = y ^ x := by
-  simp only [.^.]

tests/lean/cdotAtSimpArg.lean.expected.out

@@ -1,9 +0,0 @@
-y x : Nat
-h : y = 0
-⊢ Add.add x y = x
-y x : Nat
-h : y = 0
-⊢ Add.add x y = x
-cdotAtSimpArg.lean:24:39-25:17: error: unsolved goals
-x y : Nat
-⊢ Pow.pow x y = Pow.pow y x

tests/lean/run/cdotAtSimpArg.lean

@@ -0,0 +1,66 @@
+/-! Test `·` being able to refer to constants in `simp` -/
+
+example : ¬ true = false := by
+  simp [(¬ ·)]
+
+/-! Test `binop%` -/
+
+/--
+info: y x : Nat
+h : y = 0
+⊢ Add.add x y = x
+-/
+#guard_msgs in
+example (h : y = 0) : x + y = x := by
+  simp [(.+.)] -- Expands `HAdd.hAdd
+  trace_state
+  simp [Add.add]
+  simp [h, Nat.add]
+  done
+
+/--
+info: y x : Nat
+h : y = 0
+⊢ Add.add x y = x
+-/
+#guard_msgs in
+example (h : y = 0) : x + y = x := by
+  simp [.+.]
+  trace_state
+  simp [Add.add]
+  simp [h, Nat.add]
+  done
+
+/-! Test `binop%` variant `rightact%` as well -/
+
+/--
+error: unsolved goals
+x y : Nat
+⊢ Pow.pow x y = Pow.pow y x
+-/
+#guard_msgs in
+example (x y : Nat) : x ^ y = y ^ x := by
+  simp only [.^.]
+
+
+def f (n m : Nat) : Nat := n + m
+macro "ff" t1:term:arg t2:term:arg : term => `(f $t2 $t1)
+
+/--
+error: unsolved goals
+x y : Nat
+⊢ [x + y, y + x].sum > 0
+-/
+#guard_msgs in
+example (x y : Nat) : [f x y, ff x y].sum > 0  := by
+  simp only [ff · ·] -- NB: ff is syntax, this unfolds also f
+
+
+/--
+error: unsolved goals
+x y : Nat
+⊢ List.Mem x [x]
+-/
+#guard_msgs in
+example (x y : Nat) : x ∈ [x] := by
+  simp only [· ∈ ·] -- syntax has arguments swapped, see #5905