From 8ba10521e6f3997e9912be0d4f99748cf59bf0d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Aug 2021 12:58:02 -0700
Subject: [PATCH] feat: add theorem for tutorial

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

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index a09b1dbdab..dbcfb4c3d9 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -45,6 +45,9 @@ theorem reverseAux_reverseAux (as bs cs : List α) : reverseAux (reverseAux as b
   | nil => rfl
   | cons a as ih => simp [reverseAux, ih (a::bs), ih [a]]
 
+@[simp] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
+  simp [reverse]; rw [reverseAux_reverseAux_nil]; rfl
+
 protected def append : List α → List α → List α
   | [],    bs => bs
   | a::as, bs => a :: List.append as bs