refactor(Algebra): replace RingEquivClass.toRingEquiv by structure-specific coercions

[YaelDillies]

Remove the coercion from E to RingEquiv assuming RingEquivClass E and given by RingEquivClass.toRingEquiv. For each concrete type, reimplement this coercion through the relevant structure projection.

---

[github-actions]

PR summary b43655dfe2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coe_extendScalarsOfSurjective
+ instance : CoeOut (A ≃⋆+* B) (A ≃+* B) where coe := toRingEquiv
+ instance : CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂) where coe := AlgEquiv.toRingEquiv
+ instance : CoeOut (α ≃+*o β) (α ≃+* β) where coe := toRingEquiv
+ instance : CoeTC (RingInvo R) (R ≃+* Rᵐᵒᵖ) where coe := toRingEquiv
- hasCoeToRingEquiv
- instance [Mul α] [Add α] [Mul β] [Add β] [EquivLike F α β] [RingEquivClass F α β] :

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.

---

No changes to technical debt.

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]

Overall I agree that the generic hom coercions didn't turn out to be particularly useful, so I would be in favour of the PR.

Could you also check that the documentation on how to set up FunLikes is appropriately updated?

[YaelDillies]

I am not touching this PR for a while by lack of time. Feel free to take over if you feel like it!

[leanprover-community-bot-assistant]

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

[urkud]

Please add some explanations to the commit message.

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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

[Vierkantor]

What is the status of this PR? Because this is work that we want to get into Mathlib at some point, but I've been holding off on reviewing because of the empty PR description and WIP tag.

[YaelDillies]

The status is that it needs a lot more work before it's reviewable. I'm expecting the final diff to be around +-3k lines.

@j-loreaux suggested preliminary steps to this PR but I am not sure that one can actually take those steps before the whole PR.

Concretely, he suggests to first remove uses of hom classes in definitions, and then remove the generic coercions. The issue I see is that this will change the syntactic form of a lot of lemmas, and simp won't yet have been upgraded to handle that. My suggestion instead is to do the refactor one type of morphisms at a time, starting from the leaves of the morphism hierarchy and working towards the roots.

[mathlib4-merge-conflict-bot]

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.

[mathlib-merge-conflicts]

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