From dd1a4188a0cb6995d2519765fc20f461a0f546ff Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Fri, 14 Feb 2025 12:59:44 +0100
Subject: [PATCH] feat: `Fin.toNat` (#7079)

This PR introduces `Fin.toNat` as an alias for `Fin.val`. We add this
function for discoverability and consistency reasons. The normal form
for proofs remains `Fin.val`, and there is a `simp` lemma rewriting
`Fin.toNat` to `Fin.val`.
---
 src/Init/Data/Fin/Basic.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 48a5d12c7a..f9a7d7cd30 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -51,6 +51,14 @@ Returns `a` modulo `n + 1` as a `Fin n.succ`.
 protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) :=
   ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
 
+-- We provide this because other similar types have a `toNat` function, but `simp` rewrites
+-- `i.toNat` to `i.val`.
+@[inline, inherit_doc val]
+protected def toNat (i : Fin n) : Nat :=
+  i.val
+
+@[simp] theorem toNat_eq_val {i : Fin n} : i.toNat = i.val := rfl
+
 private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
   | 0,   h => Nat.mod_lt _ h
   | _+1, h =>