Theorems in Mathlib are identical to theorems in Init

Stream: new members

[Laurance Lau]

I found some theorems in Mathlib.Data.Fin.Basic that seem to be (almost) identical to some theorems in Init.Data.Fin.Lemmas.

• Fin.eq_zero & Fin.fin_one_eq_zero
• Fin.size_positive' (URL breaks formatting) & Fin.pos'
• Fin.le_iff_val_le_val & Fin.le_def

There are also some pairs of theorems that say the same thing, differing only in the direction of the iff or whether the parameters are explicit.
I do not know if there is actually a purpose for having these duplicate theorems, whether cleaning up duplicate theorems is an important or safe task, and what the right way to go about doing it is, but I thought I would bring it up in case it needs to be done.

[Rado Kirov]

I am curious about this too. While working on MIL I accidentally forgot a ' and mixed up Nat.dvd_sub' vs Nat.dvd_sub only to learn that they are the same, except one of them has less hypotheses.

[Ruben Van de Velde]

For dvd_sub, the answer is that the lean core one should be replaced by the mathlib one, but contributing to core was/is a pain

[Ruben Van de Velde]

Core has lt_iff_val... so should probably also have le_iff..