Refactoring `AlgEquiv` (#29354)

Stream: mathlib4

[Monica Omar]

I'm trying to revive my refactoring PR #29354 (refactoring AlgEquiv to also work for non-unital - see previous thread #mathlib4 > refactor `StarAlgEquiv` to extend `StarRingEquiv`), but I came across an error that's beyond me and I can't be bothered anymore (I've tried everything, but I can't figure it out).
It's the last error left, it's in the RingTheory/Etale/QuasiFinite file. I would really appreciate it if someone can help me figure out a fix for this :pray:
(@Andrew Yang, because you authored the file, so you might be the best for the job)

[Andrew Yang]

You need to add

  let : SMul (integralClosure R S) (Localization.Away s₂.1) := Algebra.toSMul

after the let : Algebra line because there's a diamond.

[Monica Omar]

Thank youuu!

[Jireh Loreaux]

Why is there a diamond? Is it pre-existing?

[Andrew Yang]

Yes it is pre-existing. If S is a subalgebra of R, then S has two algebra instances on R[1/M]: One through S being a subalgebra and another through R[1/M] being a localization.

[Jireh Loreaux]

I see, gross.

[Monica Omar]

benchmark results are still bad: instructions are up +850G (+0.49%)
https://github.com/leanprover-community/mathlib4/pull/29354#issuecomment-3946596500

[Monica Omar]

I'm thinking of a different refactor now for this (#29354) which could be better performance wise (but with a con):
So the current refactor changes the type classes from Algebra to Mul SMul and Add, but it could be better to instead have NonUnitalSemiring and Module (or even NonUnitalNonAssocSemiring and DistribMulAction like what docs#NonUnitalAlgHom uses).
The con is that StarAlgEquiv won't be able to extend AlgEquiv.

I don't want to waste time and do it without asking if people think this is a good idea or not. So what do we all think?

[Jireh Loreaux]

StarAlgEquiv could also be made to match.

[Monica Omar]

Changing to NonUnitalNonAssocSemiring and DistribMulAction gives so many unwanted problems. For some reason, type ascriptions are needed almost everywhere.
So I strengthened the hypotheses to NonUnitalNonAssocSemiring and Module, which solved those issues. The performance is so much worse than before though.
I'll try adding SMulCommClass and IsScalarTower so that it's literally just an algebra without a unit. Maybe that would perform better :fingers_crossed: