`simp` cannot unfold field definition marked as `private`

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

When assigning the fields of a structure, the private modifier can be used. It creates unexposed helper declarations. In some situations, it is not possible to unfold them, making them effectively opaque.

Steps to Reproduce

1. Check out the Lake project in this branch: https://github.com/datokrat/lean-bug-reproductions/tree/bugs1
2. Open Reproductions/UnfoldingPrivate.lean and observe that the _private_ constant cannot be unfolded.

Here's the code:

module

public noncomputable instance instBEq {α : Type u} [LE α] [DecidableLE α] :
    BEq α where
  beq _ _ := private true

-- UPDATE: Ignore this first example. This is expected to fail because
-- True.intro is of type `True`, while we expect a value of type `true = true`.
/--
error: Type mismatch
  True.intro
has type
  True
but is expected to have type
  instBEq._private_1 = true
-/
#guard_msgs in
private theorem eq_of_beq [LE α] [DecidableLE α] (a b : α) : a == b := by
  simp only [BEq.beq]
  exact True.intro

/--
error: trying to realize `_private.Lean.Environment.0.Lean.Environment.RealizeConstKey` value but `enableRealizationsForConst` must be called for 'instBEq._private_1' first
---
error: unsolved goals
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
a b : α
⊢ instBEq._private_1 = true
-/
#guard_msgs in
private theorem eq_of_beq' [LE α] [DecidableLE α] (a b : α) : a == b := by
  simp only [BEq.beq, instBEq._private_1]

Expected behavior:

The helper declaration should be reducible or even semireducible in public contexts. (It is!) (d)simp should be able to unfold the helper declaration.

Alternatively, private should only be allowed for propositions and forbidden for other expected types.

Actual behavior:

Cannot unfold at all, there seems to be no way to finish my proof.
Cannot prove the theorem using only simp.

Versions

Lean 4.23.0-nightly-2025-08-11
Target: arm64-apple-darwin23.6.0 macOS

Impact

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

Run the minimal reproduction in Reproductions/UnfoldingPrivate.lean against the stated Lean nightly, then inspect how simp handles instBEq._private_1 after BEq.beq is unfolded. Done means the final #guard_msgs case proves the equality using simp without enabling realizations or leaving an unsolved goal.