formPerm_apply_get defined in terms of formPerm_apply_nthLe

Stream: mathlib4

[Kim Morrison]

Currently formPerm_apply_nthLe is proved using formPerm_apply_nthLe (and formPerm_apply_lt), which both use the deprecated List.nthLe.

Would someone mind cleaning this up? This one specifically is getting in my way, and I'll need to sort it out by tomorrow. More generally, we still have a lot of theorems mentioning nthLe which I hope we can start getting rid of!

[Richard Osborn]

I'm assuming you mean formPerm_apply_get needs to be rewritten? I can look at this tonight if no one else has claimed it by then.

[Michael Rothgang]

Doesn't #13446 handle this? It has a merge conflict, but is just waiting for review!

[Michael Rothgang]

(Perhaps the author, a new contributor, doesn't know that a merge conflict makes their PR drop off #queue. I certainly needed a while to realise this.)