Lean 4: attribute [-instance] is never exported, even in the declaring file; use scoped instance

Tested on Lean v4.35.0 and v4.36.0-rc2, core only. Setup: class Pick where val : Nat, instance (priority := low) pickLow : Pick := ⟨1⟩, instance pickHigh : Pick := ⟨2⟩; #eval Pick.val shows which one is chosen. - In an importing file, attribute [-instance] pickHigh gives 1 until the end of the enclosing section (then 2 again). With attribute [-instance] pickHigh in, it covers just the next declaration. At file level, it holds to the end of that file only. A module importing that file sees 2 again. - The surprising case: putting attribute [-instance] pickHigh right after the declaration, in the declaring file, also stays local. That file sees 1, every importer sees 2. You cannot ship a declaration that is 'not an instance any more' this way. - Erasing something that isn't an instance is an error: 'Nat.add does not have [instance] attribute'. - If importers should opt in, declare it scoped: namespace P / scoped instance pickHigh : Pick := ⟨2⟩ / end P. It is inactive outside the namespace, even later in the same file (1). Importers get 1 by default, and 2 under open scoped P (until the section ends) or open P in. For a one-off use, letI : Pick := P.pickHigh inside a def also gives 2.