[Merged by Bors] - chore: remove backward.privateInPublic from lakefile

[jcommelin]

This PR removes the global backward.privateInPublic true setting from the lakefile.
It adds the setting locally to many declarations. This is technical debt that will need to be cleaned later.

A few modules seem to be particularly problematic. In those the backward compatibility setting is enabled at the file level, instead of at the declaration level.

Part of the diff has been created with the help of Claude. But it struggled to do things correctly at scale and speed.

To help review, I'm giving some hints below on how to digest the diff. These might be useful in the future, so I suggest including them in the commit message.

Review hints

Deletions

This PR contains 14 deletions. They are contained in the following files:

$ git diff master --numstat | awk '$2 > 0 && $3 ~ /\.lean$/ {print $3}' | xargs git diff master --stat --
 Mathlib/Algebra/Lie/TraceForm.lean                | 4 ++--
 Mathlib/Analysis/SpecialFunctions/Exp.lean        | 4 +---
 Mathlib/LinearAlgebra/LinearIndependent/Defs.lean | 2 +-
 Mathlib/Topology/DiscreteSubset.lean              | 4 +++-
 Mathlib/Topology/Homeomorph/Defs.lean             | 2 +-
 lakefile.lean                                     | 6 ------
 6 files changed, 8 insertions(+), 14 deletions(-)

The lakefile.lean deletions remove the backward.privateInPublic* options.

The other files had to be slightly refactored. Mostly convert proofs broke in unexpected ways. I think the new proofs are better anyways.

You can inspect the diff of these files with

$ git diff master --numstat | awk '$2 > 0 && $3 ~ /\.lean$/ {print $3}' | xargs git diff master --

Additions (decl-local set_options)

The bulk of this PR consists of adding

set_option backward.privateInPublic true in
set_option backward.privateInPublic.warn false in

before declarations. There are 1538 of such additions.

$ git diff master -- '*.lean' | grep "^+set_option backward.privateInPublic.*in$" | wc -l
1538

Additions (various)

For formatting reasons, we also add some empty lines.

$ git diff master -- '*.lean' | grep "^+$" | wc -l
14

There are also 8 additions coming from the refactors mentioned under "Deletions" above.

I've also added two comments on decls that I think we're intended to be private but were not.

$ git diff master | grep "^+--" | wc -l
2

These are added in the files

• Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean
• Mathlib/ModelTheory/PartialEquiv.lean
  Inspect their diff with

git diff master -- Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean Mathlib/ModelTheory/PartialEquiv.lean | grep -C5 "^+--"

which returns

 @[simps!]
@@ -200,6 +203,9 @@ private def unitIso : 𝟭 (Comon (C ⥤ D)) ≅ functor ⋙ inverse :=
     { hom := .mk' { app := fun _ => 𝟙 _ }
       inv := .mk' { app := fun _ => 𝟙 _ } })

+-- probably this was originally also intended to be a private def
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
 /-- The counit for the equivalence `Mon (C ⥤ D) ≌ C ⥤ Mon D`.
 -/
 @[simps!]
--
+++ b/Mathlib/ModelTheory/PartialEquiv.lean
@@ -138,6 +138,7 @@ theorem le_iff {f g : M ≃ₚ[L] N} : f ≤ g ↔
     rw [le_def]
     exact ⟨dom_le_dom, by ext; change subtype _ (g.toEquiv _) = _; rw [← h_eq]; rfl⟩

+-- probably the initial design intended this to be private, just like `le_refl` and `le_antisymm`?
 theorem le_trans (f g h : M ≃ₚ[L] N) : f ≤ g → g ≤ h → f ≤ h := by
   rintro ⟨le_fg, eq_fg⟩ ⟨le_gh, eq_gh⟩
   refine ⟨le_fg.trans le_gh, ?_⟩
@@ -145,8 +146,10 @@ theorem le_trans (f g h : M ≃ₚ[L] N) : f ≤ g → g ≤ h → f ≤ h := by
   ext

This accounts for 1562 of the 1581 additions.

Additions (non decl-locl set_options)

The remaining 19 lines come from set_options without in.

$ git diff master -- '*.lean' | grep "^+set_option backward.privateInPublic" | grep -v "in$" | wc -l
19

These appear in the following files:

$ git diff master --name-only -- '*.lean' | while read file; do
  if git diff master "$file" | grep "^+set_option backward.privateInPublic" | grep -v " in$" > /dev/null; then
    echo "$file"
  fi
done
Mathlib/CategoryTheory/ComposableArrows/Basic.lean
Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
Mathlib/Combinatorics/Matroid/Basic.lean
Mathlib/GroupTheory/OreLocalization/Basic.lean
Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
Mathlib/NumberTheory/NumberField/House.lean
Mathlib/RingTheory/OreLocalization/Basic.lean
Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
Mathlib/Tactic/Linter/MinImports.lean
Mathlib/Tactic/TFAE.lean
Mathlib/Tactic/ToExpr.lean
Mathlib/Util/CompileInductive.lean

It is not entirely clear to me why these files need the more global setting. But it seems to be related to auto-generated decls that end up being private, but that are needed in other modules.

---

[github-actions]

PR summary 99bc1514ad

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ordConnected_preimage_mk'
+ toNatTrans_congr

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (99.65, 2.05)

Current number	Change	Type
1554	1507	backwards compatibility flags
1507	1507	privateInPublic flags
52	4	adaptation notes

Current commit da7e40fc04
Reference commit 99bc1514ad

You can run this locally as

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

[eric-wieser]

Should this (and many others) be in the proof instead of for the whole command?

[jcommelin]

I personally think this is local enough, for the purposes of localizing the technical debt.

[eric-wieser]

I think like classical, debt in the types of the statement is much more worrying than debt in the proofs.

[jcommelin]

At the moment we have debt in the entire library. That's even more worrying.

[grunweg]

Can you add comments about the non-local set_options, such as

-- TODO: investigate why local set_option's do not suffice here (and fix this)

[grunweg]

In fact, it seems that GroupTheory/OreLocalization/Basic.lean does not need the file-level change. (Locally, the file builds fine.) edit: but dependent files need it; this is more involved. Let's move that to a separate PR.

The same is true for CategoryTheory/ComposableArrows/Basic.lean.

[jcommelin]

No, they are needed because they need to expose something that is use in other downstream files.

[jcommelin]

I think the -- TODO is implicit. All these set_options are tech debt.

[grunweg]

The interesting parts of the diff look good to me.

[grunweg]

I scrolled through a bit of the mechanical diff. I trust you that it's entirely mechanical; let's land this now and refine later. Thanks for doing this!
bors d+

[mathlib-bors]

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jcommelin]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Post-Build Step
• Build
• Lint style