chore(Algebra/Group/Pointwise/Set/SelfInv): put into lemmas into Set namespace

[justus-springer]

Move all lemmas about self inverse sets into the Set namespace. This was suggested by @eric-wieser in #42611. Dot-notation is still accessible using the DNRO feature.

to_additive needs a hint in order to translate into the correct namespace. I also fixed the to_additive of IsSelfInv.prod (this used to be translated to IsSelfInv.sum instead of IsSelfNeg.prod.

---

[github-actions]

PR summary fb393d8712

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

• +46 new declarations
• −46 removed declarations

-IsSelfInv.compl
-IsSelfInv.diff
-IsSelfInv.empty
-IsSelfInv.iInter
-IsSelfInv.iUnion
-IsSelfInv.inter
-IsSelfInv.inv_mem
-IsSelfInv.inv_subset
-IsSelfInv.of_compl
-IsSelfInv.of_inv_subset
-IsSelfInv.of_subset_inv
-IsSelfInv.prod
-IsSelfInv.sInter
-IsSelfInv.sUnion
-IsSelfInv.subset_inv
-IsSelfInv.union
-IsSelfInv.univ
-IsSelfNeg.compl
-IsSelfNeg.diff
-IsSelfNeg.empty
-IsSelfNeg.iInter
-IsSelfNeg.iUnion
-IsSelfNeg.inter
-IsSelfNeg.neg_mem
-IsSelfNeg.neg_subset
-IsSelfNeg.of_compl
-IsSelfNeg.of_neg_subset
-IsSelfNeg.of_subset_neg
-IsSelfNeg.sInter
-IsSelfNeg.sUnion
-IsSelfNeg.subset_neg
-IsSelfNeg.sum
-IsSelfNeg.union
-IsSelfNeg.univ
+Set.IsSelfInv.compl
+Set.IsSelfInv.diff
+Set.IsSelfInv.empty
+Set.IsSelfInv.iInter
+Set.IsSelfInv.iUnion
+Set.IsSelfInv.inter
+Set.IsSelfInv.inv_mem
+Set.IsSelfInv.inv_subset
+Set.IsSelfInv.of_compl
+Set.IsSelfInv.of_inv_subset
+Set.IsSelfInv.of_subset_inv
+Set.IsSelfInv.prod
+Set.IsSelfInv.sInter
+Set.IsSelfInv.sUnion
+Set.IsSelfInv.subset_inv
+Set.IsSelfInv.union
+Set.IsSelfInv.univ
+Set.IsSelfNeg.compl
+Set.IsSelfNeg.diff
+Set.IsSelfNeg.empty
+Set.IsSelfNeg.iInter
+Set.IsSelfNeg.iUnion
+Set.IsSelfNeg.inter
+Set.IsSelfNeg.neg_mem
+Set.IsSelfNeg.neg_subset
+Set.IsSelfNeg.of_compl
+Set.IsSelfNeg.of_neg_subset
+Set.IsSelfNeg.of_subset_neg
+Set.IsSelfNeg.prod
+Set.IsSelfNeg.sInter
+Set.IsSelfNeg.sUnion
+Set.IsSelfNeg.subset_neg
+Set.IsSelfNeg.union
+Set.IsSelfNeg.univ
+Set.isSelfInv_compl_iff
+Set.isSelfInv_iff_forall_inv_mem
+Set.isSelfInv_iff_forall_inv_mem_iff
+Set.isSelfInv_iff_inv_subset
+Set.isSelfInv_iff_subset_inv
+Set.isSelfInv_singleton_iff
+Set.isSelfNeg_compl_iff
+Set.isSelfNeg_iff_forall_neg_mem
+Set.isSelfNeg_iff_forall_neg_mem_iff
+Set.isSelfNeg_iff_neg_subset
+Set.isSelfNeg_iff_subset_neg
+Set.isSelfNeg_singleton_iff
-isSelfInv_compl_iff
-isSelfInv_iff_forall_inv_mem
-isSelfInv_iff_forall_inv_mem_iff
-isSelfInv_iff_inv_subset
-isSelfInv_iff_subset_inv
-isSelfInv_singleton_iff
-isSelfNeg_compl_iff
-isSelfNeg_iff_forall_neg_mem
-isSelfNeg_iff_forall_neg_mem_iff
-isSelfNeg_iff_neg_subset
-isSelfNeg_iff_subset_neg
-isSelfNeg_singleton_iff

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit fb393d8712
Reference commit 3a33b9d429

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

[tb65536]

Can you add deprecations?

[eric-wieser]

My original proposal would have been to call this one IsSelfInv.empty_set or IsSelfInv.setEmpty or similar, and only move the un-namespaced ones in the global namespace into Set.

Your approach looks reasonable too, though I'm not sure if it's one we use elsewhere. Perhaps this is worth a quick poll on zulip?

[justus-springer]

I think we have precedence for the bare names, e.g. MeasurableSet.empty, MeasurableSet.inter and so on. The difference here is that IsSelfInv is a predicate that also makes sense for other things rather than sets. But I would still prefer having the dot notation line up with the names of the set operations directly, e.g. write hs.inter ht (and not hs.inter_set ht) when hs : IsSelfInv s and ht : IsSelfInv t. So imo this is exactly the intended use case of the DNRO feature.

[justus-springer]

In this case I would rather not add deprecations. Having both Set.IsSelfInv.inter and a deprecated IsSelfInv.inter means that if a downstream file has h : IsSelfInv s, then h.inter resolves to the deprecated IsSelfInv.inter, even when the Set namespace is open. So this emits warnings and thus makes dot notation not usable while the deprecations are there. IsSelfInv only landed in mathlib two weeks ago, and there are currently no uses of it (my #43774 will add the first and can wait for this PR).