From 4d66e7bdc07584b7d7515aeaa5a88b352b78fed6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 28 Jan 2025 11:25:58 +1100 Subject: [PATCH] feat: add List.modifyHead_dropLast (#6803) This PR adds the simp lemma `List.modifyHead_dropLast`. This is one of many small PRs that will improve simp lemma confluence. --- src/Init/Data/List/Nat/Modify.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean index aac841c02a..84dd888a55 100644 --- a/src/Init/Data/List/Nat/Modify.lean +++ b/src/Init/Data/List/Nat/Modify.lean @@ -76,6 +76,12 @@ theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} : @[simp] theorem modifyHead_id : modifyHead (id : α → α) = id := by funext l; cases l <;> simp +@[simp] theorem modifyHead_dropLast {l : List α} {f : α → α} : + l.dropLast.modifyHead f = (l.modifyHead f).dropLast := by + rcases l with _|⟨a, l⟩ + · simp + · rcases l with _|⟨b, l⟩ <;> simp + /-! ### modifyTailIdx -/ @[simp] theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l