chore: use private proof elaborator to remove set_option backward.privateInPublic

[thorimur]

This PR applies the private proof elaborator in #42563 to get rid of some unnecessary backward.privateInPublic.

In addition to manual fixes, this PR runs skimmer to apply the suggestions of temporary Claude-coded linters in #42756, which are not intended to make it into mathlib (at least, not without a human rewrite). These linters (1) find places private can be used (2) find places where set_option backward.privateInPublic can now be removed. They produce a couple of false positives, hence the need for human attention I've given to the output.

They also identified a couple of cases where backward.privateInPublic was acting only as an elaboration-time affordance, and no private-in-public declarations were actually being used in a public position in the final declaration (but the private proof elaborator did not immediately apply). This PR therefore also performs some manual fixes to allow us to remove those set_options.

Dot notation

There is an unfortunate interaction with dot notation affecting certain Classical.choose (and similar) locations, where noncomputable data is constructed from a proof which can be private. Namely, the expected type is not available, causing private (and by exact, if you were to write that instead) to fail. However, deliberately insisting on no expected type via (t :) works: e.g. (private <term> :).some. There unfortunately isn't much to do on the elaborator side in private that would fix this, I don't think. But it might make sense to make this more readable somehow (though I'm not sure how).

variable issues

variables are currently elaborated for each declaration in the ambient scope, regardless of the private/public annotations on the declaration(s) they're being elaborated for. This means a variable in a public section that references a private declaration will silently cause a sorry, and demand backward.privateInPublic to elaborate successfully. Related lean core issues: leanprover/lean4#14708, leanprover/lean4#14718.

Restructuring public section so that it does not include variable is one way to fix this, and we do this for a couple of files (Mathlib.NumberTheory.NumberField.House; Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity; Mathlib.Topology.MetricSpace.GromovHausdorffRealized; Mathlib.CategoryTheory.Galois.Decomposition). In these cases, almost every declaration is private. We leave the private annotations on for readability (lest they accidentally become public if someone adds a public section later).

macros using private definitions

In Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean, we define a macro that refers to two private special-purpose theorems. I make these public but internal (e.g. m_pos -> _m_pos), as is standard best practices for tactic writing.

I suspect that the private definitions used by Aesop in Matroid.Basic should be treated similarly, but I'm not familiar enough with the area.

Misc.

Sometimes we construct both data and proofs with the same by block (e.g., apply a data-creating definition then discharge its proof obligations with the rest of the block). This prevents lean from auto-abstracting the proof during elaboration. A couple manual fixes therefore involve putting the proof segments of the tactic block into their own by blocks.

Sometimes, the private field annotation for structure instances is enough (e.g. fieldFoo := private ...), which is handled specially by lean and is not an instance of the new private proof elaborator.

In a handful of cases, we can make partial progress towards removing backward.privateInPublic by wrapping something with private but still need it for some other reason. In these cases we add set_option linter.privateProof.warnIfUnnecessary false to silence the warning from the private elaborator telling us that backward.privateInPublic is currently true.

This PR is fully human-reviewed, and all of this text is human-written.

---

• depends on: feat: private elaborator for proofs #42563

[github-actions]

PR summary e5aa71063d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8511 files with changed transitive imports taking up over 371900 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

+ F
+ FEq
+ _eps_pos
+ _m_pos
+ aPriv
+ aPrivBothErrors
+ aPrivSilenced
+ bPriv
+ bPrivSilenced
+ f
+ f'
+ fImplicit
+ fImplicit'
+ fLocal
+ fLocalSilenced
+ fNestedBy
+ fProofsInPublic
+ foo
+ fooPub
+ fooThm
+ fα
+ fα'
+ fα''
+ fαPub'
+ fαPub''
+ gImplicit
+ implicitThm
+ sup_aux
+ truncatedSup
+ usePriv
- 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 e5aa710).

• +2 new declarations
• −0 removed declarations

+Mathlib.Tactic.PrivateProof.linter.privateProof.warnIfUnnecessary
+Mathlib.Tactic.PrivateProof.privateElab

---

Increase in strong tech debt: (relative, absolute) = (0.35, 0.35)

Current number	Change	Type (strong)
backward.privateInPublic	367	-124
backward.privateInPublic.warn	152	-47
backward.proofsInPublic	1	1

No changes to weak technical debt.

Current commit e5aa71063d
Reference commit 9f7aa3a132

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).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.