apply results in hidden let values

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

The post state of the apply tactic results in the value of local declarations being hidden. From my reading of the pp code at https://github.com/leanprover/lean4/blob/48365b6052da47426e440f21b7703d5f7646c7c8/src/Lean/Meta/PPGoal.lean#L91 it seems this happens when a non-synthetic opaque metavariable is created, but I don't see exactly where here.

example : False := by
  let a := 1
  trace_state
  /- 
  a : Nat := 1
  ⊢ False -/
  apply id
  trace_state
  /-case a
  a : Nat := ⋯
  ⊢ False -/

I expect both to produce the same state.

Versions

live latest 4.23-rc1

Impact

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

Reproduce the example in the issue against the Lean nightly release and compare the two trace_state outputs before and after apply id. Start with the referenced src/Lean/Meta/PPGoal.lean code and trace how hidden local values are selected; done means the post-apply state preserves the visible value of a as in the initial state.