jump to definition in dupNamespace linter warnings

Stream: mathlib4

[Kevin Buzzard]

I'm fixing up linter errors in a file and noticed an inconsistency. For the docBlame linter it's complaining about a declaraction and prints #check @foo /- definition missing documentation string -/ and if I ctrl-click on @foo I jump to definition so it's easy to fix.

But the next error is from the dupNamespace linter and it says #check @RestrictedProduct.foo /- The namespace RestrictedProduct is duplicated in the name -/. This time I can't figure out how to jump to the declaration, I have to copy, search, paste.

And then the next error is the unusedArguments linter and jumping to definition is working again.

Is there something funny about the dupNamespace linter or is it another issue?

MWE:

import Mathlib

theorem Foo.Foo.bar : 2+2=4 := by
  simp
#lint