simp sometimes gives an obscure error for nonexistent lemma

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

simp [prod.mk.inj_iff77] gives an obscure error:

invalid simplification lemma 'prod.mk.inj_iff77' (use command 'set_option trace.simp_lemmas true' for more details)
state:
⊢ true

The recommended option has no effect.

For some reason, some other names give a better error, for example, simp [potato] results in unknown identifier 'potato'.

Steps to Reproduce

set_option trace.simp_lemmas true
example : true :=
begin
  simp only [prod.mk.inj_iff77]
end

Expected behavior: Error: unknown identifier 'prod.mk.inj_iff77'

Actual behavior: Error: invalid simplification lemma 'prod.mk.inj_iff77' (use command 'set_option trace.simp_lemmas true' for more details)

Reproduces how often: Always, but unclear under what circumstances (see above).

Versions

Lean (version 3.9.0, commit cb9f9f838475, Release)
Also observed with
Lean (version 3.11.0, commit fb3f3e88be8a, Release)

Start with the provided simp only [prod.mk.inj_iff77] reproduction and compare it with simp [potato]. Trace the simplifier's handling of unresolved names, including whether set_option trace.simp_lemmas true is honored. Done means the nonexistent lemma reports unknown identifier, with the trace option behaving as documented.