chore: list hints in order of priority#37580

ldct wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

ldct:ldct-sort-hint-priorityldct/mathlib4:ldct-sort-hint-priorityCopy head branch name to clipboard