Theorem: Array.get?_toListRev (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
h : i < a.size
⊢ a.toListRev.get? i = a.get? (a.size - 1 - i)
Tactic:
rw [toListRev_eq, List.get?_reverse _ (by rwa [data_length]), get?_data]
State after:
no goals

State before:
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
h : i < a.size
⊢ i < a.data.length
Tactic:
rwa [data_length]
State after:
no goals