Lean4中数组初始化表达式化简问题及相关报错咨询

我尝试证明如下命题：

example (n:Nat): #[n][0] = n := 
by
  sorry

虽然列表的等价命题很容易证明，但我了解到Lean4中数组化简存在难点。不过我仍希望完成该证明，因此尝试了多种方法，例如：

example (n:Nat)(arr: Array Nat)(p:arr=#[n]): #[n][0] = n := 
by
  rw [<-p]

从逻辑上看这是可行的，但却出现报错：

tactic 'rewrite' failed, motive is not type correct

这是我从未见过的错误！于是我尝试了更繁琐的写法：

example (n:Nat)(arr: Array Nat)(p:arr.data = [n])(i:Fin arr.size): arr[i] = n := 
by
  have p: arr.data.length = 1 := by simp [*];
  have q: i.val = 0 := (by linarith [i.isLt]);
  unfold Array.get

现在又出现报错：failed to unfold 'Array.get'，我无法理解为何展开操作会失败？

综上，我得出应避免使用数组的结论，想请教各位的看法？

内容的提问来源于stack exchange，提问作者redjamjar