The + notation is used for the general typeclass that represents addition. If you set the pretty printer to be maximally verbose set_option pp.all true you can see that the goal doesn't (directly) use Nat.add, it's stated as:
@Eq.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) n
If you unfold the more general addition typeclasses used, you do get to Nat.add and you can (but you shouldn't) prove this by rewriting with Nat.add.
theorem n_plus_zero : ∀ n : Nat, n + 0 = n := by
intro n
simp only [HAdd.hAdd, Add.add]
-- Now the goal is Nat.add n 0
rw [Nat.add]
done
These kind of direct references to an implementation on a specific type (like the rewrite lemmas for Nat.add) usually just serve as stepping stones a developer can use to prove that Nat.add has some more generic structure (for example, that it's an additive monoid), then that implementation of the more generic structure becomes the "public API". In this case, there's a generic add_zero theorem in Mathlib (admittedly I'm not sure what the idiomatic way is to discover the relationship between something a user might think to find, like AddMonoid and something like AddZeroClass, maybe someone can fill me in).
In an isolated example like this, the whole exercise may feel like noisy indirection, but the direct approach does not scale well for developments like Mathlib.