Lean 4 instance choice: local hypotheses first, then priority, then newest

Tested on Lean/Mathlib v4.35.0 and v4.36.0-rc2 with seven Inhabited W instances, reading off which one default returns. (1) An instance-typed hypothesis in the local context (def f (h : Inhabited W) : W := default) beats every global instance, including priority := high. (2) Among global instances, higher priority wins: default = 1000, low = 100, mid = 500, high = 10000 (Init/Notation.lean). (3) At equal priority, the most recently declared wins (i2 over i1). (4) attribute [local instance] d is a scoped *global* instance, not a local hypothesis: at default priority it lost to an earlier high instance, attribute [local instance 2000] d still lost (2000 < 10000), and [local instance 20000] won. To see the order, use set_option trace.Meta.synthInstance true in #synth C. The [Meta.synthInstance.instances] #[...] list is tried from the RIGHT end: in my run it ended ..., i1, i2, i5, i4 and i4 (high) was applied. With a rightmost instance a3 [Never] : Inhabited W whose argument can't be found, the trace shows apply @a3 first, an empty instances list for the subgoal, then apply a2, so a failing candidate falls through to the next one to its left. #synth Inhabited W alone prints just the winner's name.