Fin.castSuccEmb and Fin.castLE

Stream: maths

[Antoine Chambert-Loir]

I just observed that the embedding of Fin n into Fin n.succprovided by docs#Fin.castSuccEmb is defined using Fin.castLE and not Fin.castSucc.
In particular, docs#Fin.castSuccEmb_apply seems slightly inconsistent in rewriting Fin.castSuccEmb n = Fin.castLE … n.
It gave me (minor) annoyances when I had to compute basic things (eg in #23962).

Would it be worth to restate it more consistently?

[Yury G. Kudryashov]

Note that we have docs#Fin.coe_castSuccEmb

[Yury G. Kudryashov]

I'm trying to fix it as a part of #23420

[Yury G. Kudryashov]

But it seems that I've just deleted the _apply lemma without deprecating it.

[Yury G. Kudryashov]

I'll push an update tomorrow.

[Yury G. Kudryashov]

UPD: cherry-picked to a separate PR #23967