feat: unfold-boundaries in `to_dual`

[JovanGerb]

This PR introduces a new feature to to_dual that allows us to have definitions whose dual is not definitionally equal to the dual of the value. This is crucial for many definitions that are dual to something morally but not definitionally. For example, DecidableLE, Set.Ioo, Set.Ico, CovBy , Monotone.

TODO:

• [ ] Better tracing to see what this is doing?
• [x] Improve the UI of applying the to_dual_insert_cast and to_dual_insert_cast_fun attributes.
• [ ] Add tests
• [ ] Better documentation

---

[github-actions[bot]]

PR summary 3bd92fff08

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Tactic	1
Mathlib.Tactic.Translate.UnfoldBoundary (new file)	29

---

Declarations diff

+ Cov.Ico + Cov.Ioc + DecidableLE1 + DecidableLE2 + DecidableLE3 + DecidableLE4 + UnfoldBoundaries + UnfoldBoundaryExt.toUnfoldBoundaries + instance _root_.WithTop.decidableLE [LE α] [DecidableLE α] : DecidableLE (WithTop α) + instance _root_.WithTop.decidableLT [LT α] [DecidableLT α] : DecidableLT (WithTop α) + lt_sum_eq_of_le + mem_Ico + mkAppWithCast + mkCast + run + unfoldBoundaries? - Ici - Ici_def - Ioi - Ioi_def - LinearOrder.toDecidableLE' - LinearOrder.toDecidableLT' - WCovBy.of_le_of_le' - decidableEqofDecidableGE - decidableEqofDecidableLE' - decidableGTOfDecidableGE - exists_eq_l - l_bot - l_eq - l_eq_bot - l_u_bot - l_u_l_eq_l - l_u_l_eq_l' - l_u_le - l_u_le_trans - l_unique - le_u - mem_Ici - mem_Ioi - monotone_l

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.

---

No changes to technical debt.

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

[fpvandoorn]

This makes sense. I believe when you implemented correctness-checking for to_additive existing I commented something like this: sometimes it's useful to translate X to Y even when the translated value of X doesn't match the value of Y.

[mathlib4-merge-conflict-bot]

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

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for d7e591587c6856a583d42c8f2c9ae68e30c42af2 against cea71b808632582fadd1a3e9f81509173bf87ca0 are in! @JovanGerb

Small changes (2✅, 6🟥)

• ✅ build/module/Mathlib.Algebra.GeomSum//instructions: -127.8M (-2.5%)
• 🟥 build/module/Mathlib.Analysis.NormedSpace.Connected//instructions: +469.2M (+7.1%)
• ✅ build/module/Mathlib.CategoryTheory.MorphismProperty.RetractArgument//instructions: -433.6M (-5.3%)
• 🟥 build/module/Mathlib.FieldTheory.Galois.GaloisClosure//instructions: +441.7M (+1.7%)
• 🟥 build/module/Mathlib.NumberTheory.Cyclotomic.PID//instructions: +84.1M (+0.9%)
• 🟥 build/module/Mathlib.Order.WithBot//instructions: +3.6G (+5.5%)
• 🟥 build/module/Mathlib.Tactic.DefEqTransformations//instructions: +367.7M (+3.4%)
• 🟥 build/module/Mathlib.Tactic.Translate.ToDual//instructions: +3.3G (+50.3%)

[mathlib4-merge-conflict-bot]

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