diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 6d7681f056..649fe3eb23 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -457,7 +457,7 @@ inductive PNonScalar : Type u where
   /-- You should not use this function -/
   | mk (v : Nat) : PNonScalar
 
-@[simp] theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl
+@[simp] protected theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl
 
 theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α := rfl