[Merged by Bors] - refactor(data/list/tfae): tfae.out

[digama0]

This version of tfae.out has slightly better automatic reduction behavior: if h : [a, b, c].tfae then the original of h.out 1 2 proves [a, b, c].nth_le 1 _ <-> [a, b, c].nth_le 2 _ while the new version of h.out 1 2 proves b <-> c. These are the same, of course, and you can mostly use them interchangeably, but the second one is a bit nicer to look at (and possibly works better with e.g. subsequent rewrites).

[cipher1024]

Is there any reason to keep the old version?

[digama0]

Not really, except for possible compatibility concerns.

[cipher1024]

There was a request recently for a version of tfae where propositions are named instead of numbered. I think we might want to be careful to not have too many different ways of using this tactic. And in the case of the named proposition feature, I think a case could be made to keep only that version.

[digama0]

This PR has nothing to do with the tfae tactic, it's just a theorem that lets you use the result of a tfae once it's been proved.

[jcommelin]

Not really, except for possible compatibility concerns.

Why don't we try to make this new version out (and remove the existing one) and see what CI thinks of that?

[semorrison]

LGTM.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests