From 9032ddd7734733c911e04e38347fdee36505f827 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Sep 2021 13:45:13 -0700
Subject: [PATCH] chore: add simp lemma for converting `Nat.add` back into `+`
 notation

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

diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index ccd4399537..dd9205c92a 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -44,6 +44,9 @@ namespace Nat
 @[simp] theorem zero_eq : Nat.zero = 0 :=
   rfl
 
+@[simp] theorem add_eq : Nat.add x y = x + y :=
+  rfl
+
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n
   | 0   => rfl
   | n+1 => congrArg succ (Nat.zero_add n)