simpNF linter complains about a `rfl` lemma

Stream: mathlib4

[Michael Stoll]

In

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Prime

namespace Nat

/-- `primesBelow n` is the set of primes less than `n` as a finset. -/
abbrev primesBelow (n : ℕ) : Finset ℕ := (Finset.range n).filter (fun p ↦ p.Prime)

@[simp]
lemma primesBelow_zero : primesBelow 0 = ∅ := rfl

end Nat

#lint

I get

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check Nat.primesBelow_zero /- simp can prove this:
  by simp only [@Finset.filter_congr_decidable,
 Finset.range_zero,
 @Finset.not_mem_empty,
 @IsEmpty.forall_iff,
 @forall_const,
 @Finset.filter_true_of_mem]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
 -/

I guess I should remove the simp attribute.
But it still strikes me as strange that the linter insists on a more complicated proof. Is this expected behavior?

[Michael Stoll]

Replacing abbrev by def also seems to help.

[Kevin Buzzard]

I guess the point is that because you made it an abbrev Lean can see things like (Finset.range 0).filter which it already knows how to simplify, so it's arguing that you don't need to tell it again.