From 6d0b415edde8841b1ad7a15a809e46770521b3f9 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 28 Dec 2020 00:38:46 +0000
Subject: [PATCH] feat(data/list/basic): nth_zero (#5513)

---
 src/data/list/basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index ae3e027e1ec89..74ca3e48209ad 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -1017,6 +1017,8 @@ theorem mem_iff_nth_le {a} {l : list α} : a ∈ l ↔ ∃ n h, nth_le l n h = a
 theorem mem_iff_nth {a} {l : list α} : a ∈ l ↔ ∃ n, nth l n = some a :=
 mem_iff_nth_le.trans $ exists_congr $ λ n, nth_eq_some.symm
 
+lemma nth_zero (l : list α) : l.nth 0 = l.head' := by cases l; refl
+
 lemma nth_injective {α : Type u} {xs : list α} {i j : ℕ}
   (h₀ : i < xs.length)
   (h₁ : nodup xs)