defeq abuse in `WithAbs`/`WithVal`

Stream: mathlib4

[Salvatore Mercuri]

In some recent PRs I noticed some defeq abuse (of my own making) in the type synonyms WithAbs and WithVal. Specifically, instances of the form Algebra (WithVal v) S were inferred through defeq, so I propose a fix in #34049 to compose with the canonical isomorphism between WithVal and the original type as Algebra.compHom S (WithVal.equiv v).toRingHom. In a review @Christian Merten suggested we might use a 1-field structure as the definition instead to avoid this happening in the first place and I then saw that precisely that had occurred for WithLp (see Zulip thread).

Is the general consensus that type synonyms should now be 1-field structures as is done in docs#WithLp ? Or is it case-by-case?

[Violeta Hernández]

I think there's some consensus that we want to do this, but it would be too difficult in some situations such as with docs#OrderDual, where we abuse the def-eq all over the place.

[Wrenna Robson]

I think we should do it with OrderDual as well, I'd happily do the work, I am just waiting to be encouraged to do it.

[Violeta Hernández]

I think we should wait for most of the library to be tagged with to_dual, which should get rid of most of the def-eq abuse.

[Kim Morrison]

Wrenna Robson said:

I think we should do it with OrderDual as well, I'd happily do the work, I am just waiting to be encouraged to do it.

Don't forget my enthusiasm for getting WithTop and WithBot sorted asap! :-)