From 47814f9da13149baabb601de9e7c8c1cfa5dfd6c Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 10 Feb 2025 21:30:41 +1100
Subject: [PATCH] chore: add @[simp] to List.flatten_toArray (#7014)

---
 src/Init/Data/Array/Lemmas.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index caf0243a5f48..3e98cf9f34ab 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1878,7 +1878,8 @@ theorem append_eq_map_iff {f : α → β} :
   rw [← flatten_map_toArray]
   simp
 
-theorem flatten_toArray (l : List (Array α)) :
+-- We set this to lower priority so that `flatten_toArray_map` is applied first when relevant.
+@[simp 500] theorem flatten_toArray (l : List (Array α)) :
     l.toArray.flatten = (l.map Array.toList).flatten.toArray := by
   apply ext'
   simp
@@ -2140,7 +2141,8 @@ theorem flatMap_eq_foldl (f : α → Array β) (l : Array α) :
   | nil => simp
   | cons a l ih =>
     intro l'
-    simp [ih ((l' ++ (f a).toList)), toArray_append]
+    rw [List.foldl_cons, ih]
+    simp [toArray_append]
 
 /-! ### mkArray -/