feat (GroupTheory/Congruence): add simp lemmas for comap equivalences

[hannahfechtner]

add a few lemmas, mostly about when the underlying types are equal, so too must be the quotient

[github-actions[bot]]

PR summary b0c18d3439

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ comapQuotientEquivOfSurj + comapQuotientEquivOfSurj_mk + comapQuotientEquivOfSurj_symm_mk + comapQuotientEquivOfSurj_symm_mk' + comap_conGen_equiv + comap_conGen_of_bijective + congr_mk + le_comap_conGen

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.

[tb65536]

Something's a bit messed up with this PR (the diff is 90k lines). Maybe merge master? Or if that doesn't work, ask on Zulip.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[Vierkantor]

bors r-

[mathlib-bors[bot]]

Canceled.

[Vierkantor]

Discussed with @jcommelin and approved so:

bors d+

[mathlib-bors[bot]]

:v: hannahfechtner can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[hannahfechtner]

bors r+

[Vierkantor]

Oh, it looks like my change wasn't yet applied. So we need to wait before merging until it is done. Is it okay if I push to your branch?

bors r-

[mathlib-bors[bot]]

Canceled.

[hannahfechtner]

@Vierkantor of course! thank you

[Vierkantor]

Pushed and built so Let's Get This Merged!

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style