fix: prepend underscore on autogenerated 'proof_{n}' constant names

[dwrensha]

Mathlib's library_search is frequently picking up constants named proof_1, preventing it from finding more appropriate lemmas. I opened a PR there to work around the problem (https://github.com/leanprover-community/mathlib4/pull/2349), but it risks wrongly ignoring user-written lemmas whose names happen to start with the prefix proof_. It would be much cleaner if core Lean 4 gave us a way to know exactly which constants to ignore.

This PR proposes to achieve that by prepending an underscore to the generated proof_{n} constants, allowing them to be detected by the existing Lean.Name.isInternal function.