chore: remove backward.privateInPublic by wrapping proofs with private_decl%

[kim-em]

This PR removes 171 uses of backward.privateInPublic across 37 files. Wherever a public declaration used a private lemma in a proof position, the proof is wrapped with core's private_decl% elaborator, or with the field := private proof structure-instance syntax where the proof fills a structure field. Both elaborate the proof in a private context and hide it behind an auxiliary declaration, which is harmless by proof irrelevance. No declaration changes visibility and no statement changes, except that in Combinatorics/SetFamily/AhlswedeZhang the Finset → Set coercion in lowerClosure s is now written explicitly, since private_decl% elaborates eagerly and otherwise sees the coercion's pending metavariable.

This follows the plan of #42755 by @thorimur and takes its non-elaborator changes verbatim: moving variable commands out of public section in four files where almost every declaration is private (Galois/Decomposition, ChevalleyComplexity, GromovHausdorffRealized, NumberField/House; see leanprover/lean4#14708 and leanprover/lean4#14718), making the two lemmas used by the sz_positivity macro public under internal names, and separating data from proof in binomExpansion and archimedeanClassOrderIso. The difference is that this PR uses the elaborator that already exists in core rather than the private term elaborator proposed in #42563, so that it can land now. Once #42563 is in, every private_decl% (…) here can be replaced mechanically by private …. The 13 files that only need the field syntax are in #44023 and are not touched here.

🤖 Prepared with Claude Code

[github-actions]

PR summary ad86c4cc21

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ _eps_pos
+ _m_pos
- eps_pos
- m_pos

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit ad86c4c).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

Decrease in strong tech debt: (relative, absolute) = (51.48, 0.56)

Current number	Change	Type (strong)
backward.privateInPublic	408	-122
backward.privateInPublic.warn	170	-45
adaptation notes	397	2

No changes to weak technical debt.

Current commit ad86c4cc21
Reference commit 0a6c8e0355

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

All uses of private_decl% add extra brackets. Can we instead override the syntax to work without extra brackets (in the way the by exact doesn't need extra brackets)?

[kim-em]

All uses of private_decl% add extra brackets. Can we instead override the syntax to work without extra brackets (in the way the by exact doesn't need extra brackets)?

Could we do this separately, please? I would prefer to not have any metaprogramming in this PR.

If someone wants to adjust the syntax, either by overriding in mathlib4, or adjusting in lean4 (I would merge!) then it's a simple matter to strip the then-unnecessary parentheses.