max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: swap ≠ in count_cons_of_ne (#7650)

Browse source 
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`count_cons_of_ne`](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/argument.20order.20in.60count_cons_of_ne.60)
This commit is contained in:
JovanGerb 2025-03-24 09:50:16 +00:00 • committed by GitHub
parent 608a5899dc
commit 1e40151e2c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Data/List/Count.lean
View file

@ -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