From 0fd434d42520befb2c74fc6e342d5c170c755da4 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 13 Dec 2023 21:58:40 +1100
Subject: [PATCH] feat: List.reverse_eq_nil_iff (#441)

---
 Std/Data/List/Lemmas.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 54044dd03b..1a5aa9a726 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -1055,6 +1055,9 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
 
 @[simp] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by simp [reverse]
 
+@[simp] theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] ↔ xs = [] := by
+  induction xs <;> simp
+
 /-! ### insert -/
 
 section insert