Theorem: ToList.RandomAccess.get_toArray (Algorithm/Data/Classes/ToList.lean)

State before:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : RandomAccess C α
c : C
i : Fin (toArray c).size
⊢ (toArray c).get i = get c (Fin.cast ⋯ i)
Tactic:
rw [get_eq_get_toArray]
State after:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : RandomAccess C α
c : C
i : Fin (toArray c).size
⊢ (toArray c).get i = (toArray c).get (Fin.cast ⋯ (Fin.cast ⋯ i))

State before:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : RandomAccess C α
c : C
i : Fin (toArray c).size
⊢ (toArray c).get i = (toArray c).get (Fin.cast ⋯ (Fin.cast ⋯ i))
Tactic:
rfl
State after:
no goals