lemma

leanprover · Nov 6, 2024 · 39258ab · 39258ab
1 parent 66ac702
commit 39258ab
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/Lean/SimpLC/Whitelists/List.lean b/src/Lean/SimpLC/Whitelists/List.lean
@@ -91,6 +91,12 @@ simp_lc ignore List.foldl_subtype
 simp_lc ignore List.foldr_subtype
 simp_lc ignore List.mapFinIdx_eq_mapIdx
 
+-- TODO move to library.
+@[simp] theorem List.modifyHead_dropLast {l : List α} : l.dropLast.modifyHead f = (l.modifyHead f).dropLast:= by
+  rcases l with _|⟨a, l⟩
+  · simp
+  · rcases l with _|⟨b, l⟩ <;> simp
+
 /-
 The actual checks happen in `tests/lean/run/simplc.lean`.
 This commented out command remains here for convenience while debugging.