[Merged by Bors] - chore(Data/Fin/Tuple/Basic): Fill in the API hole (partly)

[YaelDillies]

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.

---

• depends on: [Merged by Bors] - doc(Data/Fin/Tuple/Basic): Compare start/end/middle addition of an entry in module doc #13567

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - doc(Data/Fin/Tuple/Basic): Compare start/end/middle addition of an entry in module doc #13567
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary cd19a39d7f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ insertNth_removeNth
+ insertNth_self_removeNth
+ removeNth
+ removeNth_insertNth
+ removeNth_last
+ removeNth_update
+ removeNth_zero
- extractNth_insertNth
- insertNth_extractNth

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[eric-wieser]

bors merge

Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style