From cdcb5780b9d5b824a5e6f55789f4b9e65f3aa630 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 12 Jan 2025 20:57:26 +1100
Subject: [PATCH] fix

---
 src/Init/Data/Array/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index bfe25ca41efb..3eee4ef43784 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1508,7 +1508,7 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
 
 /-! ### singleton -/
 
-@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
+@[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
 
 /-! ### append -/