diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean
index 5056e9f54e..8840cd937d 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -63,8 +63,8 @@ s.size == 0
 
 partial def toListAux (ds : FloatArray) : Nat → List Float → List Float
 | i, r =>
-  if i < ds.size then
-    toListAux (i+1) (ds.get! i :: r)
+  if h : i < ds.size then
+    toListAux (i+1) (ds.get ⟨i, h⟩ :: r)
   else
     r.reverse