Private proof materializes a public equation theorem

Prerequisites

• 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

A case where changing only the proof of a private theorem changes the exported .olean.

Context

Zulip thread

Steps to Reproduce

module
@[expose] public def f : Nat → Nat
    | n => n
-- version 1
private theorem privateProof : f 0 = 0 := by rfl
-- version 2
private theorem privateProof : f 0 = 0 := by simp [f]

Expected behavior: [Clear and concise description of what you expect to happen]

Two versions give the same .olean file.

Actual behavior: [Clear and concise description of what actually happens]

The generated .olean files are different.

Versions

Tested on Lean 4.35.0-nightly-2026-09-01 and Lean 4.33.1.

Additional Information

Impact

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

Start with the minimal Lean reproducer in the issue and compare the generated .olean files for the two private theorem proofs. Trace how the public equation theorem is materialized during compilation; done when changing only that private proof produces identical exported .olean files.