SimpNF issues in PNat.find

Stream: mathlib4

[Arien Malec]

In mathlib4#1220, I'm getting SimpNF issues for one_le_find which is currently:

@[simp]
theorem one_le_find : 1 < PNat.find h ↔ ¬p 1 :=
  not_iff_not.mp <| by simp

where the linter tells me

simp can prove this:
  by simp only [PNat.lt_find_iff, PNat.le_one_iff, forall_eq]
One of the lemmas above could be a duplicate.

And of course, one_le_find is the specific lower bound on lt_find_iff.

I've tried moving it up, proving it from first principles, etc., but the linter refuses to be happy.

I don't think deleting it to make the linter happy is right -- should I nolint this (and how?)

[Ruben Van de Velde]

Why not just remove the simp attribute?

[Arien Malec]

Got it - the linter is complaining that anything one_le_find can prove in a simp so can lt_find_iff... so we don't need the simp

[Arien Malec]

Obvious in retrospect.

[Kevin Buzzard]

Asking is a good way to learn!