fix: reject attribute uses whose module is reachable only via IR#13613

Kha wants to merge 3 commits intoleanprover:masterleanprover/lean4:masterfrom

Kha:push-zpsqupyvkwxqKha/lean4:push-zpsqupyvkwxqCopy head branch name to clipboard