From c57ab80c8dd20b345b29c81c446c78a6b3677d20 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 26 Sep 2024 00:34:21 +0200 Subject: [PATCH] refactor: avoid relying on rfl's behavior on ground terms (#832) --- Batteries/Data/Fin/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index bc1eb0d2c9..5ddde152de 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/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]