diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 0bd6d8572b..24433d1668 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -2096,7 +2096,7 @@ where
   | 0,   acc => acc
   | n+1, acc => loop n (n::acc)
 
-@[simp] theorem range_zero : range 0 = [] := rfl
+@[simp, grind =] theorem range_zero : range 0 = [] := rfl
 
 /-! ### range' -/
 
diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean
index ef07468b8e..abbf01cb17 100644
--- a/src/Init/Data/List/Range.lean
+++ b/src/Init/Data/List/Range.lean
@@ -142,6 +142,8 @@ theorem range'_eq_cons_iff : range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = r
 
 /-! ### range -/
 
+@[simp, grind =] theorem range_one : range 1 = [0] := rfl
+
 theorem range_loop_range' : ∀ s n, range.loop s (range' s n) = range' 0 (n + s)
   | 0, _ => rfl
   | s + 1, n => by rw [← Nat.add_assoc, Nat.add_right_comm n s 1]; exact range_loop_range' s (n + 1)
diff --git a/tests/lean/run/grind_list2.lean b/tests/lean/run/grind_list2.lean
index f98f7666b1..e5538c2c1b 100644
--- a/tests/lean/run/grind_list2.lean
+++ b/tests/lean/run/grind_list2.lean
@@ -1288,3 +1288,5 @@ end Hidden
 
 example {xs : List α} {i : Nat} (h : i < xs.length) : xs.take i ++ xs[i] :: xs.drop (i + 1) = xs := by
   apply List.ext_getElem <;> grind (splits := 10)
+
+example : (List.range 1).sum = 0 := by grind
diff --git a/tests/lean/run/list_simp.lean b/tests/lean/run/list_simp.lean
index 29f0caf3f6..6556d918e7 100644
--- a/tests/lean/run/list_simp.lean
+++ b/tests/lean/run/list_simp.lean
@@ -454,6 +454,8 @@ end Pairwise
 
 /-! ## Ranges and enumeration -/
 
+example : (List.range 1).sum = 0 := by simp
+
 /-! ### enumFrom -/
 
 /-! ### min? -/