rw [get_def]
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ get (ofFn f) ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ get (toList (ofFn f)) (Fin.cast ⋯ ⟨i, hi⟩) = f (Fin.cast ⋯ ⟨i, hi⟩)