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

import Lean

namespace A

structure A (α : Type u) where
  a : α
deriving Lean.ToExpr

#check A.instToExprA.toExpr -- should this be called `A.instToExprAOfToLevel.toExpr`?
#check A.instToExprAOfToLevel

end A

The Batteries documentation string linter assumes that auxiliary declarations for a derived instance live in the namespace of the instance. I think this is a reasonable assumption, but it's violated by the Lean.ToExpr deriving handler, as the example shows.

Context

This issue was exposed by #10643, after which the issue above leads to a linter false positive in mathlib.

Steps to Reproduce

1. Copy the above code into live.lean-lang.org

Expected behavior: Auxiliary declarations for the instance live in the namespace whose name is the instance name.

Actual behavior: Auxiliary declarations live in a different namespace.

Versions

Lean 4.25.0-nightly-2025-10-05

Impact

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