.

src/Init/Data/Array/Lemmas.lean

@@ -90,14 +90,17 @@ open Array
 @[simp] theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
   rw [foldlM_eq_foldlM_toList]
+  rw [toList_toArray]
 
 @[simp] theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
   rw [foldr_eq_foldr_toList]
+  rw [toList_toArray]
 
 @[simp] theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
   rw [foldl_eq_foldl_toList]
+  rw [toList_toArray]
 
 end List