List.toArray_data

theorem List.toArray_data : ∀ {α : Type u_1} (as : List α), (List.toArray as).data = as

This theorem states that for any list `as` of type α, the data contained in the array resulting from converting the list `as` to an array using the `List.toArray` function is equal to the original list `as`. In other words, the `List.toArray` function preserves the data of the list during the conversion process from list to array.

More concisely: For any list `as` of type `α`, the `List.toArray` function returns an array with the same elements as list `as`.