feat(Logic/Relation): some EqvGen API

[chenson2018]

This is adapted from #40606 and existing lemmas in CSLib. I move two theorems (Equivalence.eqvGen_iff and Equivalence.eqvGen_eq) earlier for a better proof of EqvGen.lift' that matches what is done for other closures.

Co-authored-by: Dagur Asgeirsson dagurtomas@gmail.com

---

[github-actions]

PR summary 4072bec448

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ _root_.Equivalence.eqvGen_eq
+ _root_.Equivalence.eqvGen_iff
+ _root_.Relation.eqvGen_idem
+ _root_.Relation.reflTransGen_eq_eqvGen
+ _root_.Relation.reflTransGen_le_eqvGen
+ _root_.Relation.transGen_le_eqvGen
+ lift
+ lift'
+ reflGen_le_eqvGen
+ symmGen_le_eqvGen
++++ to_eqvGen
- Equivalence.eqvGen_eq
- Equivalence.eqvGen_iff

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

• +12 new declarations
• −0 removed declarations

+Relation.EqvGen.lift
+Relation.EqvGen.lift'
+Relation.ReflGen.to_eqvGen
+Relation.ReflTransGen.to_eqvGen
+Relation.SymmGen.to_eqvGen
+Relation.TransGen.to_eqvGen
+Relation.eqvGen_idem
+Relation.reflGen_le_eqvGen
+Relation.reflTransGen_eq_eqvGen
+Relation.reflTransGen_le_eqvGen
+Relation.symmGen_le_eqvGen
+Relation.transGen_le_eqvGen

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 4072bec448
Reference commit f3853dcbb5

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

[chenson2018]

Please see #40606 (comment) for previous discussion on this theorem.

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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