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