dsimp [ofFn.go]
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f (n + 1) j h).length = n + 1
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f n (j + 1) ⋯).length + 1 = n + 1