From 1e40151e2c123e80bca74607f3fc5c179e351689 Mon Sep 17 00:00:00 2001
From: JovanGerb <56355248+JovanGerb@users.noreply.github.com>
Date: Mon, 24 Mar 2025 09:50:16 +0000
Subject: [PATCH] =?UTF-8?q?chore:=20swap=20`=E2=89=A0`=20in=20`count=5Fcon?=
 =?UTF-8?q?s=5Fof=5Fne`=20(#7650)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes the argument order in the inequality in `count_cons_of_ne`
so that it is consistent and follows the convention of "the more
variable argument goes on the left".

This also allows for golfing the proof.

[#lean4 > argument order
in&#96;count_cons_of_ne&#96;](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/argument.20order.20in.60count_cons_of_ne.60)
---
 src/Init/Data/List/Count.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean
index a460e86b77..15e2c8a811 100644
--- a/src/Init/Data/List/Count.lean
+++ b/src/Init/Data/List/Count.lean
@@ -257,9 +257,8 @@ variable [LawfulBEq α]
 @[simp] theorem count_cons_self (a : α) (l : List α) : count a (a :: l) = count a l + 1 := by
   simp [count_cons]
 
-@[simp] theorem count_cons_of_ne (h : a ≠ b) (l : List α) : count a (b :: l) = count a l := by
-  simp only [count_cons, cond_eq_if, beq_iff_eq]
-  split <;> simp_all
+@[simp] theorem count_cons_of_ne (h : b ≠ a) (l : List α) : count a (b :: l) = count a l := by
+  simp [count_cons, h]
 
 theorem count_singleton_self (a : α) : count a [a] = 1 := by simp