simp[hi, List.ofFnNthVal, List.get?_len_le (le_of_not_lt $ h ▸ hi)]
case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
no goals