cases k with
| zero => dsimp [ofFn.go]
| succ k =>
  dsimp [ofFn.go]
  rw [get_ofFn_go]
  congr 2
  simp_arith
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j k i : Nat
h : i + 1 + j = k✝
hk : k < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
no goals