simp[length_ofFn_go] at hk
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < (ofFn.go f i j h).length
⊢ j + k < k✝
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < i
⊢ j + k < k✝