feat(Aesop): Make some SetLike rules unsafe, add new SetLike rules

[artie2000]

• Make the following substructure membership Aesop rules unsafe:
  • mul_mem, add_mem, inv_mem, neg_mem, div_mem, sub_mem, pow_mem, nsmul_mem, zpow_mem, zsmul_mem, star_mem, SubfieldClass.nnqsmul_mem, SubfieldClass.qsmul_mem, skewAdjoint.smul_mem, ConvexCone.smul_mem, Algebra.elemental.self_mem, NonUnitalAlgebra.elemental.self_mem, NonUnitalStarSubalgebra.elemental.self_mem, NonUnitalStarSubalgebra.elemental.star_self_mem, StarSubalgebra.elemental.self_mem
• Add new Aesop rules <SubStructure>.closure_mem_of_mem
• Replace simps auto-generated lemmas around StarSubalgebra.adjoin with an Aesop-registered API
• Add new low-priority Aesop rule mem_of_star_mem

The rules above, which all have nontrivial hypotheses, have been made unsafe as they are not provability-preserving in the presence of more complicated membership rules. This is relevant to material I intend to PR soon. Since these rules are provability-preserving much of the time, and have simple membership hypotheses that can be abandoned quickly, I have given them a "success probability" of 90%. This success probability is the same as that assigned by Aesop to safe rule invocations that create new metavariables.

The new closure_mem_of_mem rules provide significant performance improvements in MathlibTest/set_like since they cause costly use of SetLike.mem_of_subset to be avoided in many cases.

The simps auto-generated lemmas I have removed produced messy output that harmed the performance of simp and Aesop without being particularly usable. The new, clean API brings StarSubalgebra.adjoin and friends in line with other closure operators such as Submonoid.closure.

mem_of_star_mem is set to the same low priority as SetLike.mem_of_subset since both rules have the potential to cause loops.

Moves (incidental):
NonUnitalSubalgebra.starClosure_toNonunitalSubalgebra -> NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra

---

[github-actions]

PR summary 9c216e1351

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ le_starClosure_toNonUnitalSubalgebra
+ le_starClosure_toSubalgebra
+ mem_of_star_mem
+ mem_span_of_mem
+ starClosure_toNonUnitalSubalgebra
+ star_le_starClosure_toNonUnitalSubalgebra
+ star_le_starClosure_toSubalgebra
++ mem_adjoin_of_star_mem
++ mem_starClosure_of_mem
++ mem_starClosure_of_star_mem
++ star_subset_starClosure
++ subset_starClosure
++++ mem_adjoin_of_mem
+++++++++ mem_closure_of_mem
- starClosure_toNonunitalSubalgebra

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

[artie2000]

!bench

[leanprover-bot]

Here are the benchmark results for commit bd8fd54.
There were no significant changes against commit 9b434d1.

[artie2000]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7cfb59a.
The entire run failed.
Found no significant differences.

[artie2000]

!bench

[leanprover-bot]

Here are the benchmark results for commit a6698ad.
There were no significant changes against commit 9b434d1.

[artie2000]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9c216e1.
There were no significant changes against commit 9b434d1.

[madvorak]

I am sorry, I am not competent to review this.