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