Fin in std4

Stream: mathlib4

[Ruben Van de Velde]

The mess with "moving" Fin lemmas to std4 is only getting worse. First it took over the names of a whole bunch of bundled definitions for unbundled versions of the same, and now definitions that existed in mathlib like succAbove have just disappeared with no apparent replacement, and Fin.val_zero no longer works. Can we just revert everything to a working state rather than blocking std4 updates?

[Eric Wieser]

#5847 is some of the context here I assume?

[Mario Carneiro]

Ruben Van de Velde said:

The mess with "moving" Fin lemmas to std4 is only getting worse. First it took over the names of a whole bunch of bundled definitions for unbundled versions of the same, and now definitions that existed in mathlib like succAbove have just disappeared with no apparent replacement, and Fin.val_zero no longer works. Can we just revert everything to a working state rather than blocking std4 updates?

Definitions that "disappeared with no apparent replacement" were not ported. Don't delete them from mathlib

[Mario Carneiro]

As for val_zero, we want both versions, and I suggest renaming the mathlib theorem to val_zero'