From 39258ab12210ed4abde4871bd31ffc81a6720a29 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 6 Nov 2024 16:10:56 +1100
Subject: [PATCH] lemma

---
 src/Lean/SimpLC/Whitelists/List.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Lean/SimpLC/Whitelists/List.lean b/src/Lean/SimpLC/Whitelists/List.lean
index 907bde4b324e..b110c7f5309c 100644
--- 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.