rcases i with ⟨i, hi⟩
k : Nat
α : Type u_1
f : Fin k → α
i : Fin (ofFn f).length
⊢ (ofFn f).get i = f (Fin.cast ⋯ i)
case mk
k : Nat
α : Type u_1
f : Fin k → α
i : Nat
hi : i < (ofFn f).length
⊢ (ofFn f).get ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)