Theorem: List.back?_toArray (Algorithm/Data/Classes/ToList.lean)

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

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