chore: add missing lemma for List.range 1 (#8537)

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' -/
 

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)

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

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? -/