diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index a6dd924f16..f6d2ab1eef 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -179,6 +179,8 @@ protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
 
 /- Inequalities -/
 
+attribute [simp] Nat.le_refl
+
 theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m :=
   succ_le_succ