Broken length_replicate proof (chapter 8)

In the "Induction and Recursion" chapter, the last proof in "Local recursive declaration" doesn't work:

theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
  exact aux n []
where
  aux (n : Nat) (as : List α)
      : (replicate.loop a n as).length = n + as.length := by
    match n with
    | 0   => simp [replicate.loop]
    | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add]

I was able to fix it by invoking add_succ and such_add from rw:

theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
  exact aux n []
where
  aux (n : Nat) (as : List α)
      : (replicate.loop a n as).length = n + as.length := by
    match n with
    | 0   => simp [replicate.loop]
    | n+1 => simp [replicate.loop, aux n]; rw [Nat.add_succ, Nat.succ_add]

leanprover / theorem_proving_in_lean4

Broken length_replicate proof (chapter 8) #138