simp [List.instSeqList, *]
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi✝ : i < size (ofFn f)
this : ∀ (L : List τ), L = ofFn f → ∀ (hi' : i < L.length), get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
hi : i < n
⊢ i < (toList (ofFn f)).length
no goals