From 7f77bfef4c2d19c8a20ef387b2209158e003b4cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Mon, 10 Nov 2025 23:16:08 -0500
Subject: [PATCH] feat: add `List.mem_finRange` (#9515)

This PR adds a missing lemma for the `List` API.

<!-- CURSOR_SUMMARY -->
---

> [!NOTE]
> Add `[simp]` lemma `List.mem_finRange` proving any `x : Fin n` is in
`finRange n`.
>
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
631f7ca852b1b2de5c7b1e3c7602c268ff47360e. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->

---------

Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
---
 src/Init/Data/List/FinRange.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean
index 7edc80f755..aa86031d2c 100644
--- a/src/Init/Data/List/FinRange.lean
+++ b/src/Init/Data/List/FinRange.lean
@@ -60,6 +60,10 @@ theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev :
     congr 2; funext
     simp [Fin.rev_succ]
 
+@[simp, grind ←]
+theorem mem_finRange {n} (x : Fin n) : x ∈ finRange n := by
+  simp [finRange]
+
 end List
 
 namespace Fin