feat: port Data.Fin.Tuple.Basic (#1516)

Co-authored-by: qawbecrdtey <40463813+qawbecrdtey@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Author: 4 people

Mathlib.lean

@@ -227,6 +227,7 @@ import Mathlib.Data.Erased
 import Mathlib.Data.Fin.Basic
 import Mathlib.Data.Fin.Fin2
 import Mathlib.Data.Fin.SuccPred
+import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Data.Finite.Defs
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Card

Mathlib/Data/Fin/Basic.lean

@@ -501,7 +501,7 @@ theorem revOrderIso_symm_apply (i : Fin n) : revOrderIso.symm i = OrderDual.toDu
 
 /-- The greatest value of `Fin (n+1)` -/
 def last (n : ℕ) : Fin (n + 1) :=
-  ⟨_, n.lt_succ_self⟩
+  ⟨n, n.lt_succ_self⟩
 #align fin.last Fin.last
 
 @[simp, norm_cast]