α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ get? (ofFn f) i = ofFnNthVal f i
rw [get?_eq_get h, get_ofFn]
no goals
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i
. simp at h; simp [ofFnNthVal, h]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h✝ : i < length (ofFn f)
h : i < n
⊢ some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i
simp at h
no goals
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h✝ : i < length (ofFn f)
h : i < n
⊢ some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i
simp [ofFnNthVal, h]
no goals
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : ¬i < length (ofFn f)
⊢ get? (ofFn f) i = ofFnNthVal f i
rw [ofFnNthVal, dif_neg] <;>
simpa using h