Universe level names are dropped in generated `_proof` subterms

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Some automatically generated lemmas do not preserve the universe level names of the end user.

Context

This is mildly annoying when trying to trace through auxiliary definitions.

Steps to Reproduce

Run:

def foo.{my_univ} : {x : ULift.{my_univ} Nat // x = x} := ⟨sorry, sorry⟩

#check foo._proof_1

Expected behavior: foo._proof_1.{my_univ} : sorry = sorry

Actual behavior: foo._proof_1.{u_1} : sorry = sorry

Versions

Lean 4.19.0-rc2

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Run the minimal Lean reproduction with foo and #check foo._proof_1, using the reported Lean 4.19.0-rc2 context or a current nightly. Trace how the generated _proof subterm is assigned universe names; done means foo._proof_1 preserves my_univ instead of exposing u_1.