From f93c3a73709b3d550b09b0740716c0cbe7df085d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 7 Jun 2024 20:56:24 +0100
Subject: [PATCH] feat: missing modifyNth simp lemmas (#830)

---
 Batteries/Data/List/Lemmas.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 6109b4c9be..cd010a8150 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -274,6 +274,14 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
 
 /-! ### modifyNth -/
 
+@[simp] theorem modifyNth_nil (f : α → α) (n) : [].modifyNth f n = [] := by cases n <;> rfl
+
+@[simp] theorem modifyNth_zero_cons (f : α → α) (a : α) (l : List α) :
+    (a :: l).modifyNth f 0 = f a :: l := rfl
+
+@[simp] theorem modifyNth_succ_cons (f : α → α) (a : α) (l : List α) (n) :
+    (a :: l).modifyNth f (n + 1) = a :: l.modifyNth f n := by rfl
+
 theorem modifyNthTail_id : ∀ n (l : List α), l.modifyNthTail id n = l
   | 0, _ => rfl
   | _+1, [] => rfl