Commit 2024-07-11 20:47 0679e1b6

View on Github →

chore(Data/Fin/Tuple/Basic): Fill in the API hole (partly) (#13568) As explained by the module doc, we are missing the Fin.succAbove equivalent of Fin.tail/Fin.init. In fact, it already exists as the second projection of extractNth, so this PR deletes extractNth and defines its second projection as a new function removeNth.

Estimated changes

Modified Mathlib/Data/Fin/Tuple/Basic.lean

modified theorem Fin.eq_insertNth_iff

deleted theorem Fin.extractNth_insertNth

modified theorem Fin.insertNth_eq_iff

deleted theorem Fin.insertNth_extractNth

added theorem Fin.insertNth_removeNth

added theorem Fin.insertNth_self_removeNth

added def Fin.removeNth

added theorem Fin.removeNth_insertNth

added theorem Fin.removeNth_last

added theorem Fin.removeNth_update

added theorem Fin.removeNth_zero

Modified Mathlib/Logic/Equiv/Fin.lean