From bf4ba1583dfe2ad9ef39540835c02b9f37686293 Mon Sep 17 00:00:00 2001
From: casavaca <96765450+casavaca@users.noreply.github.com>
Date: Fri, 18 Mar 2022 10:53:43 -0700
Subject: [PATCH] feat: add simp theorem for List, `(as.map f).length =
 as.length`

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

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 4000e4cfe4..d8dfa8fe54 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -499,6 +499,10 @@ def dropLast {α} : List α → List α
   | nil => simp
   | cons a as ih => simp [ih, Nat.succ_add]
 
+@[simp] theorem length_map (as : List α) (f : α → β) : (as.map f).length = as.length := by
+  induction as with
+  | nil => simp [List.map]
+  | cons a as ih => simp [List.map, ih]
 
 @[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by
   induction as with