Update Lemmas.lean

leanprover · Nov 18, 2024 · 8943fce · 8943fce
1 parent 7a0b786
commit 8943fce
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
@@ -2395,7 +2395,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 
 @[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) :
     (replicate n a)[m] = a :=
-  eq_of_mem_replicate (get_mem _ _ _)
+  eq_of_mem_replicate (getElem_mem _)
 
 @[deprecated getElem_replicate (since := "2024-06-12")]
 theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by