rcases i with ⟨i,hi⟩
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Fin (length (ofFn f))
⊢ get (ofFn f) i = f (Fin.cast (_ : length (ofFn f) = n) i)
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (ofFn f)
⊢ get (ofFn f) { val := i, isLt := hi } = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })