refactor: avoid relying on rfl's behavior on ground terms (#832)

Batteries/Data/Fin/Lemmas.lean

@@ -40,14 +40,14 @@ theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
 theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
   rw [list_succ]
   induction n with
-  | zero => rfl
+  | zero => simp [last]
   | 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
+  | zero => simp [last]
   | succ n ih =>
     conv => lhs; rw [list_succ_last]
     conv => rhs; rw [list_succ]