fun_cases: fails when definition in a different module

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

It is not possible to unfold a well-founded recursive function from a different module. And using fun_cases fails with "Cannot derive functional cases principle (please report this issue)".

Context

I was trying to refactor my single file proof into modules (splitting definitions and theorems) and hit this error.

Steps to Reproduce

Content of Bug.lean:

module

public import Bug.Code
import Bug.Proof

Content of Bug/Code.lean:

module

@[expose]
public def List.chunks {T : Type} (xs : List T) (n : Nat) : List (List T) :=
  if 0 < n ∧ 0 < xs.length then xs.take n :: (xs.drop n).chunks n else []
termination_by xs.length

Content of Bug/Proof.lean:

module

import Bug.Code

theorem List.chunks_nil {T : Type} (n : Nat) : (@nil T).chunks n = [] := by
  fun_cases chunks
  /- unfold chunks -/
  sorry

Output of lean --version:

Lean (version 4.34.0-nightly-2026-07-26, x86_64-unknown-linux-gnu, commit b4fb9a75e9e1cfc8d936ee6a574a8b537662698b, Release)

Output of lake build:

✖ [3/5] Building Bug.Proof
trace: .> LEAN_PATH=/tmp/bug/.lake/build/lib/lean $HOME/.elan/toolchains/leanprover--lean4-nightly---nightly-2026-07-26/bin/lean /tmp/bug/Bug/Proof.lean -o /tmp/bug/.lake/build/lib/lean/Bug/Proof.olean -i /tmp/bug/.lake/build/lib/lean/Bug/Proof.ilean -c /tmp/bug/.lake/build/ir/Bug/Proof.c --setup /tmp/bug/.lake/build/ir/Bug/Proof.setup.json --json
error: Bug/Proof.lean:6:12: Failed to realize constant List.chunks.fun_cases_unfolding:
  Cannot derive functional cases principle (please report this issue)
    `List.chunks` has neither an unfold theorem nor a value
error: Bug/Proof.lean:6:12: No functional cases theorem for `chunks`, or function is mutually recursive
error: Lean exited with code 1
Some required targets logged failures:
- Bug.Proof
error: build failed

Expected behavior: The build should not fail. Also when using unfold chunks instead of fun_cases chunks, it should unfold the definition instead of unfolding to chunks._unary.

Actual behavior: The build fails as described above. And using unfold chunks does not unfold the definition.

Note that if the definition and theorem are in the same module, then both issues disappear. So this is related to the module system, contrary to those 2 related bugs:

• #10838
• #8213

Versions

Output of #version:

Lean 4: Lean 4.34.0-nightly-2026-07-26
Target: x86_64-unknown-linux-gnu Linux

Additional Information

None.

Impact

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