simpNF says lemma doesn't apply to own LHS

Stream: mathlib4

[Timo Carlin-Burns]

I've encountered an issue where simpNF claims that a lemma doesn't apply to its own left-hand side, but when tested, it clearly does. MWE:

import Mathlib

@[simp]
theorem foo {ι ι' : Sort*} (f : ι' → α) (e : ι → ι') (x : α) : (∃ y, f (e y) = x) ↔ ∃ y, f y = x :=
  sorry -- minimized; not true in general

#lint -- Left-hand side does not simplify, when using the simp lemma on itself

example  {ι ι' : Sort*} (f : ι' → α) (e : ι → ι') (x : α) : (∃ y, f (e y) = x) ↔ ∃ y, f y = x := by
  simp only [foo]

(Original error in context of PR)

[Eric Wieser]

Note that for this to be a fair test, you need to hide the RHS from simp

[Timo Carlin-Burns]

Still works

example  {ι ι' : Sort*} (f : ι' → α) (e : ι → ι') (x : α) : (∃ y, f (e y) = x) ↔ ∃ y, f y = x := by
  conv =>
    lhs
    simp only [foo]

[Timo Carlin-Burns]

I submitted std4#671. In the meantime, I can unblock my PR with nolint simpNF.