feat(Logic): declare optional simprocs for commuting equality and iff

[Vierkantor]

This PR introduces two simprocs eqComm and iffComm that can use @[simp] lemmas on symmetrical forms of an expression: if we have a simp lemma saying f a = b ↔ a = g b and the goal contains b = f a, then we would end up with g b = a. I developed these in #36534. Enabling them globally proved to be quite slow (+0,44% overall build time, which corresponds to +5% simping time), so this PR only declares them (and enables them locally, using e.g. simp [eqComm], when we see that it pays off in the proof).

---

[github-actions]

PR summary 91b2017b29

Import changes exceeding 2%

%	File
+3.61%	Mathlib.Algebra.GroupWithZero.Defs
+5.17%	Mathlib.Logic.Basic
+3.66%	Mathlib.Logic.Function.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Basic	58	61	+3 (+5.17%)
Mathlib.Logic.Function.Basic	82	85	+3 (+3.66%)
Mathlib.Algebra.GroupWithZero.Defs	83	86	+3 (+3.61%)
Mathlib.Data.Set.Prod	209	212	+3 (+1.44%)
Mathlib.Algebra.Group.Pi.Lemmas	232	235	+3 (+1.29%)
Mathlib.Data.Matrix.Diagonal	408	409	+1 (+0.25%)
Mathlib.Data.Fin.Tuple.Sort	566	567	+1 (+0.18%)
Mathlib.SetTheory.Cardinal.Order	620	621	+1 (+0.16%)
Mathlib.CategoryTheory.Preadditive.Biproducts	688	689	+1 (+0.15%)
Mathlib.Algebra.Order.Antidiag.Finsupp	697	698	+1 (+0.14%)
Mathlib.Data.ENNReal.Operations	720	721	+1 (+0.14%)
Mathlib.Data.EReal.Operations	722	723	+1 (+0.14%)
Mathlib.SetTheory.Cardinal.Aleph	732	733	+1 (+0.14%)
Mathlib.SetTheory.Ordinal.Notation	800	801	+1 (+0.12%)
Mathlib.Algebra.Exact	963	964	+1 (+0.10%)
Mathlib.GroupTheory.Perm.Cycle.Basic	992	993	+1 (+0.10%)
Mathlib.Algebra.Polynomial.Monic	1059	1060	+1 (+0.09%)
Mathlib.Algebra.MvPolynomial.Nilpotent	1373	1374	+1 (+0.07%)
Mathlib.Analysis.Normed.Module.Multilinear.Basic	1656	1657	+1 (+0.06%)
Mathlib.FieldTheory.Finite.Basic	1701	1702	+1 (+0.06%)
Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas	1708	1709	+1 (+0.06%)
Mathlib.FieldTheory.Finite.Polynomial	1720	1721	+1 (+0.06%)
Mathlib.Analysis.SpecialFunctions.Complex.Arg	1754	1755	+1 (+0.06%)
Mathlib.Analysis.SpecialFunctions.Pow.Real	1769	1770	+1 (+0.06%)
Mathlib.FieldTheory.SeparablyGenerated	1814	1815	+1 (+0.06%)
Mathlib.Analysis.Complex.Arg	1829	1830	+1 (+0.05%)
Mathlib.Tactic.NormNum.Irrational	1886	1887	+1 (+0.05%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi	1917	1918	+1 (+0.05%)
Mathlib.LinearAlgebra.Matrix.Permutation	2153	2154	+1 (+0.05%)
Mathlib.LinearAlgebra.Matrix.Stochastic	2154	2155	+1 (+0.05%)

Import changes for all files

Files	Import difference
There are 7516 files with changed transitive imports taking up over 330104 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ eq_comm_eq
+ iff_comm_eq

You can run this locally as follows

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

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

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

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.01)

Current number	Change	Type
450	-1	porting notes
82	-1	flexible linter exceptions

Current commit 884f5d61fb
Reference commit 91b2017b29

You can run this locally as

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

[Vierkantor]

Not sure if we want to keep this un-@[simp]ed, since we'd now need simp [eqComm].