Theorem: Array.getLast?_toList (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.getLast? = a.back?
Tactic:
rw [back?, get?_eq_data_get?, List.getLast?_eq_get?]
State after:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.get? (a.toList.length - 1) = a.data.get? (a.size - 1)

State before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.get? (a.toList.length - 1) = a.data.get? (a.size - 1)
Tactic:
simp
State after:
no goals