Handler for `deriving Inhabited` on private structure introduces public auxiliary definition

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

In a module, deriving Inhabited for a private structure produces a private instance, but the auxiliary definition holding the default value is not private. This is a regression in v4.31.0, likely introduced by the new handler for deriving Inhabited in #9815.

This bug causes problems downstream. For example, the linter in Batteries would complain that the (public) auxiliary definition doesn't have a doc string.

Context

I raised this on Zulip: #general > Missing doc string for `deriving Inhabited`.

Steps to Reproduce

Build the following file:

module

private structure A where
deriving Inhabited

/--
info: @[instance_reducible] private def instInhabitedA : Inhabited A :=
{ default := instInhabitedA.default }
-/
#guard_msgs in
#print instInhabitedA

/--
info: private def instInhabitedA.default : A :=
{ }
-/
#guard_msgs in
#print instInhabitedA.default

Expected behavior: Build succeeds with no messages.

Actual behavior: Build fails with error message:

❌️ Docstring on `#guard_msgs` does not match generated message:

- info: private def instInhabitedA.default : A :=
+ info: def instInhabitedA.default : A :=
  { }

Versions

Lean 4.33.0-nightly-2026-07-09
Target: x86_64-unknown-linux-gnu

Additional Information

None.

Impact

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

Start by building the minimal module reproducer and compare the guarded output for the private structure's derived Inhabited instance and its default value. Then inspect the new deriving Inhabited handler introduced by #9815; done means the auxiliary default definition is private and the #guard_msgs checks succeed without messages.