feat: add lemma Fin.list_reverse (#819)

Batteries/Data/Fin/Lemmas.lean

@@ -36,6 +36,22 @@ protected theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x =
 theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
   apply List.ext_get; simp; intro i; cases i <;> simp
 
+theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
+  rw [list_succ]
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [list_succ, List.map_cons castSucc, ih]
+    simp [Function.comp_def, succ_castSucc]
+
+theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    conv => lhs; rw [list_succ_last]
+    conv => rhs; rw [list_succ]
+    simp [List.reverse_map, ih, Function.comp_def, rev_succ]
+
 /-! ### foldl -/
 
 theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : m < n) :