conv =>
  lhs; unfold Array.ofFn; unfold Array.ofFn.go
  rw [dif_pos n.zero_lt_succ]
  rw [Array.ofFn_go_succ', Array.ofFn_go_eq]
  rw [Array.append_data']
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
⊢ (ofFn f).data = f { val := 0, isLt := (_ : 0 < Nat.succ n) } :: (ofFn (f ∘ Fin.succ)).data
no goals