From 3ef63b219cc1eb4818c314a15b2a93340ab003e4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 23 Sep 2024 15:04:39 +1000
Subject: [PATCH] fix test

---
 tests/lean/run/2670.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/2670.lean b/tests/lean/run/2670.lean
index 64443b27b569..7120e52b5ee4 100644
--- a/tests/lean/run/2670.lean
+++ b/tests/lean/run/2670.lean
@@ -12,12 +12,12 @@ def enumFromTR' (n : Nat) (l : List α) : List (Nat × α) :=
 
 open List in
 theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by
-  funext α n l; simp [enumFromTR', -Array.size_toArray]
+  funext α n l; simp only [enumFromTR']
   let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
     | [], n => rfl
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_data]
+  rw [Array.foldr_eq_foldr_toList]
   simp [go] -- Should close the goal