chore: remove redundant backward.privateInPublic exceptions

[felixpernegger]

Remove all set_option backward.privateInPublic false which are not needed, excluding MathlibTest

---

• depends on: [Merged by Bors] - chore: remove (all) redundant backward.privateInPublic.warn exceptions #41382

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary ebd0686e1e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

- isoOfComponents_hom_hom_app
- isoOfComponents_inv_hom_app

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

• +0 new declarations
• −2 removed declarations

-CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_app
-CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_app

---

Decrease in strong tech debt: (relative, absolute) = (57.00, 0.08)

Current number	Change	Type (strong)
683	-57	backward.privateInPublic

No changes to weak technical debt.

Current commit ebd0686e1e
Reference commit 62aaa5c959

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

[felixpernegger]

All added lines come from this file, because we replace the global setting, so this really doesnt increase tech debt.

[grunweg]

splice-bot

[grunweg]

Makes sense, I'll happily merge a separate PR making this change. Hopefully, splice-bot will create such a PR for me.

[mathlib-splicebot]

Split PR created

Split off the changes to Mathlib/CategoryTheory/ComposableArrows/Basic.lean in #41407.

[felixpernegger]

There lemmas called some error (not sure why), but since they are outdated anyways, i just removed them

[felixpernegger]

!bench

[leanprover-radar]

Benchmark results for f4e5f0c against e2361c1 are in. No significant results found. @felixpernegger

• ✅ build//instructions: -31.9G (-0.02%)

No significant changes detected.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore: remove (all) redundant backward.privateInPublic.warn exceptions #41382
  By Dependent Issues (🤖). Happy coding!