feat: missing grind annotations

This PR marks `List.drop_length` and `List.take_length` with `[grind =]`.

src/Init/Data/List/TakeDrop.lean

@@ -68,9 +68,9 @@ theorem take_of_length_le {l : List α} (h : l.length ≤ i) : take i l = l := b
 theorem lt_length_of_take_ne_self {l : List α} {i} (h : l.take i ≠ l) : i < l.length :=
   gt_of_not_le (mt take_of_length_le h)
 
-@[simp] theorem drop_length {l : List α} : l.drop l.length = [] := drop_of_length_le (Nat.le_refl _)
+@[simp, grind =] theorem drop_length {l : List α} : l.drop l.length = [] := drop_of_length_le (Nat.le_refl _)
 
-@[simp] theorem take_length {l : List α} : l.take l.length = l := take_of_length_le (Nat.le_refl _)
+@[simp, grind =] theorem take_length {l : List α} : l.take l.length = l := take_of_length_le (Nat.le_refl _)
 
 @[simp]
 theorem getElem_cons_drop : ∀ {l : List α} {i : Nat} (h : i < l.length),

tests/lean/run/grind_list_drop_take.lean

@@ -0,0 +1,6 @@
+example : (List.range' 1 n).drop (List.range' 1 n).length = [] := by grind -- solves
+example : [].sum = 0 := by grind -- solves
+example : ((List.range' 1 n).drop (List.range' 1 n).length).sum = 0 := by grind -- solves
+example : ((List.range' 1 n).take (List.range' 1 n).length).sum = (List.range' 1 n).sum := by grind -- solves
+example (as bs : List Nat) : ((as ++ bs).take (as ++ bs).length).sum = (as ++ bs).sum := by grind -- solves
+example (as bs : List Nat) : ((as ++ bs).take (as ++ bs).length).sum = bs.sum + as.sum := by grind -- solves