chore: adaptation notes for the backward.privateInPublic uses blocked on lean4#14708

[kim-em]

This PR adds an #adaptation_note at each variable declaration with an autoParam binder whose users need backward.privateInPublic. These uses (about 80 of the remaining option lines, in 14 files) are not removable on the Mathlib side: the autoParam helper declaration generated for a variable is always private, and any declaration using that variable in a public section silently elaborates to sorry without the option. This is leanprover/lean4#14708. The note says which set_options can go once that is fixed, and stops anyone from spending time on them before then. Each affected file was checked by removing its true-only option lines and observing the sorry warnings and the follow-on autoParam … is not a constant errors.

It also deletes the one option line in CategoryTheory/SmallObject/Iteration/ExtendToSucc that turned out to be unnecessary.

🤖 Prepared with Claude Code

[github-actions]

PR summary 929e884d7a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

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

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

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

Current number	Change	Type (strong)
backward.privateInPublic	520	29
adaptation notes	424	29

No changes to weak technical debt.

Current commit 929e884d7a
Reference commit 857cdd0aca

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