Local notations conflict downstream

[hrmacbeth]

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.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Marking a notation as local does not seem to truly work, in that the name it is given is preserved and can later come into conflict with other uses of that name.

Steps to Reproduce

1. Make two files whose content is

local infix:50 " ≺ " => LE.le

2. Import both these files into a third file

Expected behavior: [What you expect to happen]

Should not give error.

Actual behavior: [What actually happens]

Error

import Mathlib.Order.test2 failed, environment already contains '«term_≺_»' from Mathlib.Order.test1

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

Nightly 2022-12-23

Additional Information

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Local.20notation.20conflict

Some affected mathlib4 PRs:
leanprover-community/mathlib4#1205
leanprover-community/mathlib4#1254