I want to do the proof of n + 0 = n in Lean 4 using mathlib 4, my attempt:

-- Prove that n + 0 = n
theorem n_plus_zero : ∀ n : ℕ, n + 0 = n := by
  intro n
  -- use Nat.add to rewrite n + 0 to n
  rw [Nat.add]

but I get it fails to progress with error:

basic_nats_using_mathlib_nats.lean:14:13
Tactic state
1 goal
n : ℕ
⊢ n + 0 = n
Expected type
n : ℕ
⊢ ℕ → ℕ → ℕ
Messages (1)
basic_nats_using_mathlib_nats.lean:14:6
failed to rewrite using equation theorems for 'Nat.add'
All Messages (8)

but the definition of Nat.add from mathlib 4 looks right to me, so I'm not sure why it's failing:

set_option bootstrap.genMatcherCode false in
/--
Addition of natural numbers.

This definition is overridden in both the kernel and the compiler to efficiently
evaluate using the "bignum" representation (see `Nat`). The definition provided
here is the logical model (and it is soundness-critical that they coincide).
-/
@[extern "lean_nat_add"]
protected def Nat.add : (@& Nat) → (@& Nat) → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

but the rewrite tactic did work when I manually did the proof with my definition of add (using add left, which seemed to be the opposite side of what mathlib 4 has). How do I fix my proof using the definition of addition in mathlib 4. Note, I know it works with the Nat.add_zero theorem:

Nat.add_zero (n : ℕ) : n + 0 = n
import Init.Core

which is not what I am puzzled/trying to learn about.

Thanks!