From c7819bd6ebc27ba9c5fdb66d8b954ff703d9a42d Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 25 Sep 2024 11:15:24 +1000
Subject: [PATCH] chore: missing List.set_replicate_self (#5460)

---
 src/Init/Data/List/Lemmas.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index e6beec0b2a..d150390705 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2392,6 +2392,12 @@ theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
 theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.length b :=
   map_const l b
 
+@[simp] theorem set_replicate_self : (replicate n a).set i a = replicate n a := by
+  apply ext_getElem
+  · simp
+  · intro i h₁ h₂
+    simp [getElem_set]
+
 @[simp] theorem append_replicate_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   rw [eq_replicate_iff]
   constructor