Coercion for `WithBot` and `WithTop`

Stream: mathlib4

[Brendan Seamas Murphy]

Hi @Jon Eugster , do you remember why the coercion for WithBot was changed to coe from coeTC during the port? I was wondering why the coercion types are different for WithTop and WithBot and from the git blame I figure it was an oversight

[Kevin Buzzard]

The whole coercion machinery changed quite a bit from lean 3 to lean 4 and there was no obvious bijection between the way to do things in lean 3 and in Lean 4 (did coeTC even exist in lean 3?)

[Brendan Seamas Murphy]

(deleted)

[Brendan Seamas Murphy]

Sorry, misread

[Brendan Seamas Murphy]

I don't really understand the hierarchy, although I haven't had cause to. This inconsistency just stood out to me

[Brendan Seamas Murphy]

It seems like WithTop and WithBot should have entirely synced APIs (even have everything done through an automatic dualization like to_additive, but that seems like a big project to implement)

[Jon Eugster]

I don't think that's a deliberate difference, and as Kevin said, I think it wasn't always obvious what to do with coersions in the port, especially if there were weird errors afterwards.

You should see if you can create a PR that aligns WithBot and WithTop