From ae86c18ac19cee9bdf4e63cde2c11694e3217b70 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 6 Nov 2025 00:00:04 +0100
Subject: [PATCH] chore: `backward.privateInPublic` should not break
 irrelevance of proofs for rebuilds (#11097)

---
 src/Lean/Elab/MutualDef.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index bc9e40c38d..279d8bb948 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1322,6 +1322,9 @@ where
           if !(← isProp header.type) then
             return false
         return true))) do
+    -- Never export private decls from theorem bodies to make sure they stay irrelevant for rebuilds
+    withOptions (fun opts =>
+      if headers.any (·.kind.isTheorem) then ResolveName.backward.privateInPublic.set opts false else opts) do
     let headers := headers.map fun header =>
       { header with modifiers.attrs := header.modifiers.attrs.filter (!·.name ∈ [`expose, `no_expose]) }
     let values ← try