From f629be745b8a9060f35db950db23371514b75d43 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Mar 2022 17:18:11 -0800
Subject: [PATCH] chore: add `Nat.le_refl` as `simp` theorem

---
 src/Init/Data/Nat/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

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