Data.List.Count (mathlib4#1410)

Stream: mathlib4

[Johan Commelin]

See https://github.com/leanprover-community/mathlib4/pull/1410#discussion_r1065461618

@[simp]
theorem count_nil (a : α) : count a [] = 0 := rfl
#align list.count_nil List.count_nil

Linter claims that simp can prove this. But it's a good dsimp-lemma. Also, simp can only prove it using https://github.com/leanprover-community/mathlib4/pull/1410/files#diff-cdbce63b7556c5dc37babb0180e51282c7467545742bb9be6bc251f1db148b97R256 below.
Should we bump priority here?

[Mario Carneiro]

sgtm

[Johan Commelin]

Hmm, it seems that the linter doesn't care about priorities

[Mario Carneiro]

nolint is also an option

[Johan Commelin]

ooh, adding a priority on the other lemma works

[Yaël Dillies]

Beware of #18087

[Mario Carneiro]

what does that mean? I'm starting to think you enjoy surfing the rising tide of mathlib

[Yaël Dillies]

If it gets merged before mathlib4#1410, then the latter should be updated.

[Eric Wieser]

I don't think that has to be true

[Eric Wieser]

Wall time synchronization is irrelevant, all that matters is that the sha in the PR reflects the thing it was ported from

[Eric Wieser]

If anything it's probably easier not to modify in-flight porting PRs to reflect mathlib3 changes unless the mathlib3 change is intended to fix a porting issue